proposition: Lemma decompose_term : forall t, {s : term & {sigma : substitution | t = apply_subst sigma s /\ well_formed s /\ (forall x u, In (x,u) sigma -> match u with | Var _ => True | Term f l => (match F.arity f with Free n => n | _ => 2 end) <> length l end) /\ (forall x u v, In (x,u) sigma -> In (x,v) sigma -> u = v) /\ (forall x y u, In (x,u) sigma -> In (y,u) sigma -> x = y) /\ (forall x, In x (var_list s) <-> In x (map (@fst _ _) sigma))}}.
proof: Proof. intro t; destruct (decompose_term_aux t nil) as [s [sigma [H0 [Ws [H1 [H2 [H3 H4]]]]]]]. intros; contradiction. intros; contradiction. intros; contradiction. exists s; exists (subst_rest (var_list s) sigma); repeat split; trivial. rewrite H0; rewrite <- app_nil_end. rewrite <- subst_eq_vars; intros v v_in_s. rewrite subst_rest_ok; trivial. intros x u xu_in_rest_sig; apply (H1 x u); rewrite <- app_nil_end; apply (subst_rest_subst _ _ _ _ xu_in_rest_sig). intros x u v xu_in_rest_sig xv_in_rest_sig; apply (H2 x u v); rewrite <- app_nil_end. apply (subst_rest_subst _ _ _ _ xu_in_rest_sig). apply (subst_rest_subst _ _ _ _ xv_in_rest_sig). intros x y u xu_in_rest_sig yu_in_rest_sig; apply (H3 x y u); rewrite <- app_nil_end. apply (subst_rest_subst _ _ _ _ xu_in_rest_sig). apply (subst_rest_subst _ _ _ _ yu_in_rest_sig). intros x_in_s; generalize (H4 _ x_in_s); rewrite <- app_nil_end. do 2 rewrite in_map_iff. intros [[x' u] [x_eq_x' x_in_sig]]; simpl in x_eq_x'; subst x'. exists (x,u); split; trivial. apply subst_rest_subst_rest; trivial. intro x_in_sig; rewrite in_map_iff in x_in_sig. destruct x_in_sig as [[x' u] [x_eq_x' x_in_sig]]; simpl in x_eq_x'; subst x'. apply subst_rest_rest with sigma u; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)