proposition: Lemma mutate_ru_ru_sound : forall f g uf ug s1 t1 s2 t2, unit_theory f = RU uf -> unit_theory g = RU ug -> (acu (Term g (s2 :: t2 :: nil)) s1 /\ acu (Term uf nil) t1) \/ (acu (Term f (s1 :: t1 :: nil)) s2 /\ acu (Term ug nil) t2) -> acu (Term f (s1 :: t1 :: nil)) (Term g (s2 :: t2 :: nil)).
proof: Proof. unfold acu, th_eq; intros f g uf ug s1 t1 s2 t2 UTf UTg [ [H uf_eq_t1 ] | [H ug_eq_t2]]. apply trans_clos_is_trans with s1; trivial. apply trans_clos_is_trans with (Term f (s1 :: (Term uf nil) :: nil)). apply general_context; simpl. apply rwr_list_tail; apply rwr_list_cons; apply th_sym; trivial. apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 uf_eq_t1 H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; right; trivial. apply R_in_rwr_R; left; apply right_unit; left; trivial. apply th_sym; trivial. apply trans_clos_is_trans with s2; trivial. apply trans_clos_is_trans with (Term g (s2 :: (Term ug nil) :: nil)). apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 ug_eq_t2 H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; right; trivial. apply th_sym; unfold th_eq; apply R_in_rwr_R; 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)