proposition: Lemma mutate_ru_sound : forall f u, unit_theory f = RU u -> forall s1 t1 s2 t2, ((acu s1 s2 /\ acu t1 t2) \/ (acu t1 (Term u nil) /\ acu s1 (Term f (s2 :: t2 :: nil))) \/ (acu (Term u nil) t2 /\ acu (Term f (s1 :: t1:: nil)) s2)) -> acu (Term f (s1 :: t1 :: nil)) (Term f (s2 :: t2 :: nil)).
proof: Proof. unfold acu, th_eq; intros f u UT s1 t1 s2 t2 [[H1 H2] | [[t1_eq_u H] | [u_eq_t2 H]]]. apply general_context; simpl. apply rwr_list_split; trivial. apply rwr_list_cons; trivial. apply trans_clos_is_trans with (Term f (s1 :: (Term u nil) :: nil)). apply general_context; simpl. apply rwr_list_tail; apply rwr_list_cons; trivial. apply trans_clos_is_trans with s1; trivial; apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 t1_eq_u H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; right; trivial. unfold th_eq; apply R_in_rwr_R; left; apply right_unit; left; trivial. apply trans_clos_is_trans with (Term f (s2 :: (Term u nil) :: nil)). apply trans_clos_is_trans with s2; trivial; apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 u_eq_t2 H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; right; trivial. apply th_sym; unfold th_eq; apply R_in_rwr_R; unfold th_eq; left; apply right_unit; left; trivial. apply general_context; simpl. apply rwr_list_tail; 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)