proposition: Lemma R2_case : forall (s t : term), Interp_dom R1 R2 s -> one_step R2 t s -> exists s', exists t', Interp s s' /\ Interp t t' /\ rwr (Pi pi V0 V1) t' s'.
proof: Proof. intro s; pattern s; apply term_rec2; clear s. intro n; induction n as [ | n]; intros s Size_s t Is t_R_s. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size s); trivial; apply size_ge_one. induction t_R_s as [t' s' t'_R_s' | f' lt ls lt_R_ls]; subst. inversion t'_R_s' as [t3 s3 sigma t3_R_s3]; subst. assert (It : Interp_dom R1 R2 (apply_subst sigma t3)). refine (interp_dom_R2 R1 R2 _ _ _ _ _ _ Is _); trivial. apply at_top; trivial. destruct (interp_defined _ Is) as [s' Hs']. destruct (interp_defined _ It) as [t' Ht']. exists s'; exists t'; split; trivial. split; trivial. destruct s3 as [v | f ls]. absurd (R2 t3 (Var v)); trivial; apply R2_var. simpl in Is; refine (recover_red f _ _ _ _ _ Is Hs' Ht' _); trivial. apply (Def _ _ _ _ t3_R_s3). apply one_step_incl with R2. intros; right; trivial. apply at_top; trivial. destruct (def_dec f') as [Df' | Cf']. destruct (interp_defined _ Is) as [s' Hs']. assert (It : Interp_dom R1 R2 (Term f' lt)). refine (interp_dom_R2 R1 R2 _ _ _ _ _ _ Is _); trivial. apply one_step_incl with R2; trivial. apply in_context; trivial. destruct (interp_defined _ It) as [t' Ht']. exists s'; exists t'; split; trivial. split; trivial. simpl in Is; refine (recover_red f' _ _ _ _ _ Is Hs' Ht' _); trivial. apply one_step_incl with R2. intros; right; trivial. apply in_context; trivial. assert (It : Interp_dom R1 R2 (Term f' lt)). refine (interp_dom_R2 R1 R2 _ _ _ _ _ _ Is _); trivial. apply one_step_incl with R2; trivial. apply in_context; trivial. destruct (interp_defined _ Is) as [s' Hs']. destruct (interp_defined _ It) as [t' Ht']. exists s'; exists t'; split; trivial. split; trivial. inversion Hs' as [ | f l' l'' ll Cf Hl Hl' Hll | f l' l'' ll Df Hl Hl' Hll]. inversion Ht' as [ | g k' k'' kk Cg Hk Hk' Hkk | g k' k'' kk Dg Hk Hk' Hkk]. assert (Size_ls : forall s, In s ls -> size s <= n). intros s s_in_ls; apply le_S_n; apply Nat.le_trans with (size (Term f' ls)); trivial. apply size_direct_subterm; trivial. assert (Hls : forall s, In s ls -> Interp_dom R1 R2 s). intros; apply interp_well_defined_1 with f' ls; trivial. assert (Hlt : forall t, In t lt -> Interp_dom R1 R2 t). intros; apply interp_well_defined_1 with f' lt; trivial. apply general_context. subst f g l'' l' s' k'' k' t'. generalize ll Hl Hll kk Hk Hkk ; clear Size_s Is Hs' It Ht' ll Hl Hll kk Hk Hkk. induction lt_R_ls as [t s l t_R2_s | s lt ls lt_R2_ls]; subst; intros ll Hl Hll kk Hk Hkk. destruct ll as [ | [s' s''] ll]. discriminate. simpl in Hl; injection Hl; clear Hl; intros; subst. destruct kk as [ | [t' t''] kk]. discriminate. simpl in Hk; injection Hk; clear Hk; intros; subst. simpl; replace (map (fun st : term * term => snd st) kk) with (map (fun st : term * term => snd st) ll). assert (t''_R_s'' : rwr (Pi pi V0 V1) t'' s''). assert (Size_s' : size s' <= n). apply Size_ls; left; trivial. assert (Is' : Interp_dom R1 R2 s'). apply Hls; left; trivial. destruct (IHn s' Size_s' t') as [u [v [Hu [Hv H1]]]]; trivial. rewrite (interp_unicity s' Is' s'' u); trivial. assert (It' : Interp_dom R1 R2 t'). apply Hlt; left; trivial. rewrite (interp_unicity t' It' t'' v); trivial. apply Hkk; left; trivial. apply Hll; left; trivial. revert t''_R_s''; clear; intro H; induction H as [t1 t2 H | t1 t2 t3 H1 H2]. do 2 left; assumption. right with (t2 :: map (fun st : term * term => snd st) ll); trivial. left; assumption. assert (Hkl : forall u u' u'', In (u,u') ll -> In (u,u'') kk -> u' = u''). intros u u' u'' uu'_in_ll uu''_in_kk; refine (interp_unicity u _ u' u'' _ _). apply Hlt; trivial. right; rewrite in_map_iff; exists (u,u'); split; trivial. apply Hll; right; trivial. apply Hkk; right; trivial. generalize ll kk H Hkl; clear H Hkl; intro l1; induction l1 as [ | [u u'] l1]; intros [ | [v v'] l2] H Hkl. trivial. discriminate. discriminate. simpl in H; injection H; clear H; intros H u_eq_v; subst v. simpl; rewrite (IHl1 l2); trivial. rewrite (Hkl u u' v'); trivial; left; trivial. intros w w' w'' H1 H2; apply (Hkl w); right; trivial. destruct ll as [ | [s' s''] ll]. discriminate. simpl in Hl; injection Hl; clear Hl; intros; subst. destruct kk as [ | [t' t''] kk]. discriminate. simpl in Hk; injection Hk; clear Hk; intros; subst. simpl; assert (t''_eq_s'' : t'' = s''). refine (interp_unicity t' _ t'' s'' _ _). apply Hlt; left; trivial. apply Hkk; left; trivial. apply Hll; left; trivial. subst t''. assert (H : rwr_list (one_step (Pi pi V0 V1)) (map (fun st : term * term => snd st) kk) (map (fun st : term * term => snd st) ll)). apply IHlt_R2_ls; trivial. intros; apply Size_ls; right; trivial. intros; apply Hls; right; trivial. intros; apply Hlt; right; trivial. intros; apply Hll; right; trivial. intros; apply Hkk; right; trivial. revert H; clear; intro H; induction H as [l1 l2 H | l1 l2 l3 H1 H2]. left; right; assumption. right with (s'' :: l2); trivial. right; assumption. absurd (defined R2 f'); trivial. subst. simpl in Is; refine (recover_red f' _ _ _ _ _ Is Hs' Ht' _); trivial. apply one_step_incl with R2. intros; right; trivial. apply in_context; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)