proposition: Lemma mutate_c_sound : forall f, arity f = C -> (unit_theory f = Nothing) -> forall s1 t1 s2 t2, (acu s1 s2 /\ acu t1 t2) \/ (acu s1 t2 /\ acu t1 s2) -> acu (Term f (s1 :: t1 :: nil)) (Term f (s2 :: t2 :: nil)).
proof: Proof. unfold acu, th_eq; intros f Af UT s1 t1 s2 t2 [[s1_eq_s2 t1_eq_t2] | [s1_eq_t2 t1_eq_s2]]. apply general_context; simpl. apply rwr_list_split; trivial. apply rwr_list_cons; trivial. apply trans_clos_is_trans with (Term f (t1 :: s1 :: nil)). apply rwr_incl with (sym_refl ac_one_step_at_top). clear t1 t2 s1_eq_t2 t1_eq_s2; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; left; trivial. apply comm; left; trivial. apply general_context; simpl. apply rwr_list_split; trivial. apply rwr_list_cons; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)