fact: Definition decomposition_step (pb : unification_problem) : exc unification_problem := match pb.(unsolved_part) with | nil => @Not_appliable _ pb | (s,t) :: l => if T.eq_bool s t then Normal _ (mk_pb pb.(solved_part) l) else match s, t with | Var x, Var y => let x_maps_to_y := (x, t) :: nil in let solved_part' := map_subst (fun _ v_sigma => apply_subst ((x,t) :: nil) v_sigma) pb.(solved_part) in let l' := map (fun uv => match uv with | (u, v) => (apply_subst ((x,t) :: nil) u, apply_subst ((x,t) :: nil) v) end) l in match find X.eq_bool x solved_part' with | Some x_val => Normal _ (mk_pb ((x, t) :: solved_part') ((t, x_val) :: l')) | None => Normal _ (mk_pb ((x, t) :: solved_part') l') end | Var x, (Term _ _ as u) => match find X.eq_bool x pb.(solved_part) with | None => Normal _ (mk_pb ((x,u) :: pb.(solved_part)) l) | Some x_val => if lt_ge_dec (T.size u) (T.size x_val) then Normal _ (mk_pb ((x,u) :: pb.(solved_part)) ((x_val,u) :: l)) else Normal _ (mk_pb pb.(solved_part) ((x_val,u) :: l)) end | (Term _ _ as u), Var x => match find X.eq_bool x pb.(solved_part) with | None => Normal _ (mk_pb ((x,u) :: pb.(solved_part)) l) | Some x_val => if lt_ge_dec (T.size u) (T.size x_val) then Normal _ (mk_pb ((x,u) :: pb.(solved_part)) ((x_val,u) :: l)) else Normal _ (mk_pb pb.(solved_part) ((x_val,u) :: l)) end | Term f l1, Term g l2 => if F.Symb.eq_bool f g then match Nat.eqb (length l1) (length l2) with | true => Normal _ (mk_pb pb.(solved_part) (combine _ l l1 l2)) | false => @No_solution _ end else @No_solution _ end end.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)