fact: Definition F_wf_solve (lpb : list well_formed_matching_problem) : (forall y, o_lpb y lpb -> list well_formed_matching_problem) -> list well_formed_matching_problem := match lpb return ((forall y : list well_formed_matching_problem, o_lpb y lpb -> list well_formed_matching_problem) -> list well_formed_matching_problem) with | nil => fun _ => nil | wpb :: tl_lpb => match wpb return ((forall y : list well_formed_matching_problem, o_lpb y (wpb :: tl_lpb) -> list well_formed_matching_problem) -> list well_formed_matching_problem) with | W pb w => match pb return (forall w1 : well_formed_pb pb, (forall y : list well_formed_matching_problem, o_lpb y (W pb w1 :: tl_lpb) -> list well_formed_matching_problem) -> list well_formed_matching_problem) with | mk_pb existential_vars unsolved_part solved_part partly_solved_part => fun w1 srec => match unsolved_part return (forall w2 : well_formed_pb (mk_pb existential_vars unsolved_part solved_part partly_solved_part), (forall y : list well_formed_matching_problem, o_lpb y (W (mk_pb existential_vars unsolved_part solved_part partly_solved_part) w2 :: tl_lpb) -> list well_formed_matching_problem) -> list well_formed_matching_problem) with | nil => fun w2 srec3 => W (mk_pb existential_vars nil solved_part partly_solved_part) w2 :: srec3 tl_lpb (F_wf_solve_dec1 (W (mk_pb existential_vars nil solved_part partly_solved_part) w2) tl_lpb) | p :: unsolved_part0 => fun w2 srec3 => srec3 (wf_solve (W (mk_pb existential_vars (p :: unsolved_part0) solved_part partly_solved_part) w2) ++ tl_lpb) (F_wf_solve_dec2 (W (mk_pb existential_vars (p :: unsolved_part0) solved_part partly_solved_part) w2) tl_lpb) end w1 srec end w end end.
imports: Coq(Arith List Wellfounded Wf_nat) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory ac matching dickson matching_well_formed matching_well_founded matching_sound matching_complete dickson)