proposition: Lemma mutate_free_u_sound : forall f g u l1 s2 t2, unit_theory g = U u -> (acu (Term f l1) t2 /\ acu (Term u nil) s2) \/ (acu (Term f l1) s2 /\ acu (Term u nil) t2) -> acu (Term f l1) (Term g (s2 :: t2 :: nil)).
proof: Proof. unfold acu, th_eq; intros f g u l1 s2 t2 UTg [ [H u_eq_s2] | [ H u_eq_t2] ]. apply trans_clos_is_trans with t2; trivial. apply trans_clos_is_trans with (Term g ((Term u nil) :: t2 :: nil)). apply rwr_incl with (sym_refl unit_one_step_at_top). clear 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 left_unit; right; trivial. apply general_context; simpl. apply rwr_list_cons; trivial. apply trans_clos_is_trans with s2; trivial. apply trans_clos_is_trans with (Term g (s2 :: (Term u nil) :: nil)). apply rwr_incl with (sym_refl unit_one_step_at_top). clear t2 u_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; right; 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)