proposition: Lemma mutate_ru_u : forall f g uf ug s1 t1 s2 t2, f <> g -> unit_theory f = RU uf -> unit_theory g = U ug -> acu (Term f (s1 :: t1 :: nil)) (Term g (s2 :: t2 :: nil)) -> (acu (Term g (s2 :: t2 :: nil)) s1 /\ acu (Term uf nil) t1) \/ (acu (Term f (s1 :: t1 :: nil)) t2 /\ acu (Term ug nil) s2) \/ (acu (Term f (s1 :: t1 :: nil)) s2 /\ acu (Term ug nil) t2).
proof: Proof. intros f g uf ug s1 t1 s2 t2 f_diff_g UTf UTg H; generalize (acu_is_ac_on_unit_nf (Term f (s1 :: t1 :: nil)) (Term g (s2 :: t2 :: nil))); intros [ _ H' ]; generalize (H' H); clear H' H; intro H; assert (G := H); simpl in H; rewrite UTf in H; revert H. generalize (T.eq_bool_ok (unit_nf t1) (Term uf nil)); case (T.eq_bool (unit_nf t1) (Term uf nil)); [intro t1_eq_uf | intro t1_diff_uf]. intro H; left; split. generalize (acu_is_ac_on_unit_nf (Term g (s2 :: t2 :: nil)) s1); intros [H' _]; generalize (H' (th_sym _ _ _ H)); trivial. rewrite <- t1_eq_uf. unfold acu, th_eq; apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 t1_eq_uf G H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; right; trivial. apply th_sym; apply unit_nf_is_sound. simpl in G; rewrite UTg in G; revert G; generalize (T.eq_bool_ok (unit_nf s2) (Term ug nil)); case (T.eq_bool (unit_nf s2) (Term ug nil)); [intro s2_eq_ug | intro s2_diff_ug]. intro G; right; left; split. generalize (acu_is_ac_on_unit_nf (Term f (s1 :: t1 :: nil)) t2); intros [H' _]; generalize (H' G); trivial. rewrite <- s2_eq_ug. unfold acu, th_eq; apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 t1_diff_uf G H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; right; trivial. apply th_sym; apply unit_nf_is_sound. generalize (T.eq_bool_ok (unit_nf t2) (Term ug nil)); case (T.eq_bool (unit_nf t2) (Term ug nil)); [intro t2_eq_ug | intro t2_diff_ug]. right; right; split. generalize (acu_is_ac_on_unit_nf (Term f (s1 :: t1 :: nil)) s2); intros [H' _]; generalize (H' G); trivial. rewrite <- t2_eq_ug. unfold acu, th_eq; apply rwr_incl with (sym_refl unit_one_step_at_top). clear t1 t2 t1_diff_uf t2_eq_ug G H; intros t1 t2 [H | [H | H]]; [left | right; left | right; right; trivial]; unfold union; right; trivial. apply th_sym; apply unit_nf_is_sound. intros G H; absurd (f=g); trivial. rewrite UTg in H; generalize (ac_top_eq H); generalize (T.eq_bool_ok (unit_nf s2) (Term ug nil)); case (T.eq_bool (unit_nf s2) (Term ug nil)); [intro s2_eq_ug | intros _]. absurd (unit_nf s2 = Term ug nil); trivial. generalize (T.eq_bool_ok (unit_nf t2) (Term ug nil)); case (T.eq_bool (unit_nf t2) (Term ug nil)); [intro t2_eq_ug | intros _]. absurd (unit_nf t2 = Term ug nil); trivial. trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)