proposition: Lemma mutate_ru : forall f u, arity f = Free 2 -> unit_theory f = RU u -> forall s1 t1 s2 t2, well_formed s1 -> well_formed t1 -> well_formed s2 -> well_formed t2 -> acu (Term f (s1 :: t1 :: nil)) (Term f (s2 :: t2 :: nil)) -> (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).
proof: Proof. unfold acu; intros f u Af UT s1 t1 s2 t2 Ws1 Wt1 Ws2 Wt2 H; generalize (acu_is_ac_on_unit_nf (Term f (s1 :: t1 :: nil)) (Term f (s2 :: t2 :: nil))); intros [_ H']; generalize (H' H); clear H'; intro H'; generalize (ac_size_eq H') (ac_cf_eq H'); clear H H'; intros S H. simpl in H; rewrite UT in H. revert H; generalize (T.eq_bool_ok (unit_nf t1) (Term u nil)); case (T.eq_bool (unit_nf t1) (Term u nil)); [intro t1_eq_u | intro t1_diff_u]. intro H; right; left; split. generalize (acu_is_ac_on_unit_nf t1 (Term u nil)); intros [ H' _]; apply H'; rewrite <- t1_eq_u; rewrite unit_nf_is_idempotent; unfold ac; apply th_refl. generalize (acu_is_ac_on_unit_nf s1 (Term f (s2 :: t2 :: nil))); intros [ H' _]; apply H'; apply cf_eq_ac. apply well_formed_unit_nf; trivial. apply well_formed_unit_nf; unfold well_formed; simpl; rewrite Af; rewrite Ws2; rewrite Wt2; trivial. rewrite H; simpl; rewrite UT; trivial. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil)); [intro t2_eq_u | intro t2_diff_u]. intro H; right; right; split. generalize (acu_is_ac_on_unit_nf (Term u nil) t2); intros [ H' _]; apply H'; rewrite <- t2_eq_u; rewrite unit_nf_is_idempotent; unfold ac; apply th_refl. generalize (acu_is_ac_on_unit_nf (Term f (s1 :: t1 :: nil)) s2); intros [ H' _]; apply H'; apply cf_eq_ac. apply well_formed_unit_nf; unfold well_formed; simpl; rewrite Af; rewrite Ws1; rewrite Wt1; trivial. apply well_formed_unit_nf; trivial. rewrite <- H; simpl; rewrite UT; rewrite Af; generalize (T.eq_bool_ok (unit_nf t1) (Term u nil)); case (T.eq_bool (unit_nf t1) (Term u nil)); [intro t1_eq_u | intros _]. absurd (unit_nf t1 = Term u nil); trivial. simpl; rewrite Af; trivial. left; split; [ generalize (acu_is_ac_on_unit_nf s1 s2); intros [ H' _] | generalize (acu_is_ac_on_unit_nf t1 t2); intros [ H' _]]; apply H'; (apply cf_eq_ac; [ apply well_formed_unit_nf; trivial | apply well_formed_unit_nf; trivial | injection H; rewrite Af; clear H; intro H; injection H; trivial]). Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)