proposition: Lemma rwr_rule_not_H : forall l r, R r l -> (match l with Var _ => False | Term g _ => G g end) -> forall s t, Interp_dom s -> Interp_dom t -> one_step (fun r' l' => In (r',l') ((r,l) :: nil)) t s -> forall s' t', Interp s s' -> Interp t t' -> rwr (Pi pi V0 V1) t' s'.
proof: Proof. intros l r K K' s; pattern s; apply term_rec3; clear s. intros v t _ _ K''; inversion K''; clear K''; subst. inversion H; inversion H; subst. destruct H5 as [H5 | H5]; [injection H5; clear H5; intros; subst | contradiction]. destruct t3 as [x3 | ]; [contradiction | discriminate]. intros f k IH t Acc_s Acc_t K'' s' t' Is It. inversion K''; clear K''; intros; subst. inversion H; clear H; subst. destruct H2 as [H2 | H2]; [injection H2; clear H2; intros; subst | contradiction]. apply rwr_at_top_not_H with t2 t1 sigma; trivial. rewrite H0; assumption. rewrite H0; assumption. inversion Is; clear Is. inversion It; clear It. subst; apply general_context. destruct (one_step_in_list H1) as [u [u' [l1 [l2 [K1 [K2 K3]]]]]]. destruct (split_map_set _ _ _ _ K2) as [ll1 [[ | [u1 u2] ll2] [K4 [K5 K6]]]]; clear K2. discriminate. destruct (split_map_set _ _ _ _ K3) as [ll3 [[ | [u3 u4] ll4] [K7 [K8 K9]]]]; clear K3. discriminate. simpl in K6; injection K6; clear K6; intros K10 K11; subst. simpl in K9; injection K9; clear K9; intros K10 K11; subst. do 2 rewrite map_app; simpl. assert (ll1_eq_ll3 : ll1 = ll3). assert (Aux : forall t t' t'', In (t,t') ll1 -> In (t,t'') ll3 -> t' = t''). intros t t' t'' tt'_in_ll1 tt''_in_ll3; apply (interp_unicity t). apply interp_well_defined. destruct (In_split _ _ tt'_in_ll1) as [lll1 [lll2 H15]]. apply interp_dom_subterm with (Term f (map (fun st : term * term => fst st) (ll1 ++ (u, u2) :: ll2))) (length lll1 :: nil); trivial. subst ll1; simpl; rewrite <- ass_app; rewrite map_app. rewrite <- (length_map (fun st : term * term => fst st) lll1). simpl; rewrite nth_error_at_pos; apply eq_refl. apply H6; apply in_or_app; left; trivial. apply H13; apply in_or_app; left; trivial. revert K8 Aux; clear; revert ll3; induction ll1 as [ | [a1 a2] ll1]; intros [ | [b1 b2] ll3] K8 Aux. apply eq_refl. discriminate. discriminate. simpl in K8; injection K8; clear K8; intros; subst. rewrite (Aux a1 a2 b2 (or_introl _ (eq_refl _)) (or_introl _ (eq_refl _))); rewrite (IHll1 ll3); trivial. intros t t' t'' H1 H2; apply (Aux t); right; assumption. assert (ll2_eq_ll4 : ll2 = ll4). assert (Aux : forall t t' t'', In (t,t') ll2 -> In (t,t'') ll4 -> t' = t''). intros t t' t'' tt'_in_ll2 tt''_in_ll4; apply (interp_unicity t). apply interp_well_defined. destruct (In_split _ _ tt'_in_ll2) as [lll1 [lll2 H15]]. apply interp_dom_subterm with (Term f (map (fun st : term * term => fst st) (ll1 ++ (u, u2) :: ll2))) (length (ll1 ++ (u,u2) :: lll1) :: nil); trivial. subst ll2; simpl; rewrite app_comm_cons; rewrite ass_app; rewrite map_app. rewrite <- (length_map (fun st : term * term => fst st) (ll1 ++ (u,u2) :: lll1)). simpl; rewrite nth_error_at_pos; apply eq_refl. apply H6; apply in_or_app; do 2 right; trivial. apply H13; apply in_or_app; do 2 right; trivial. revert K10 Aux; clear; revert ll4; induction ll2 as [ | [a1 a2] ll2]; intros [ | [b1 b2] ll4] K10 Aux. apply eq_refl. discriminate. discriminate. simpl in K10; injection K10; clear K10; intros; subst. rewrite (Aux a1 a2 b2 (or_introl _ (eq_refl _)) (or_introl _ (eq_refl _))); rewrite (IHll2 ll4); trivial. intros t t' t'' H1 H2; apply (Aux t); right; assumption. subst ll3 ll4. unfold rwr_list; rewrite rwr_list_expand_strong; exists u2; exists u4; exists (map (fun st : term * term => snd st) ll1); exists (map (fun st : term * term => snd st) ll2); exists (map (fun st : term * term => snd st) ll2). split. apply eq_refl. split. apply eq_refl. split. apply IH with u u'. rewrite map_app; apply in_or_app; right; left; apply eq_refl. apply interp_dom_subterm with (Term f (map (fun st : term * term => fst st) (ll1 ++ (u, u2) :: ll2))) (length ll1 :: nil); trivial. rewrite map_app. rewrite <- (length_map (fun st : term * term => fst st) ll1). simpl; rewrite nth_error_at_pos; apply eq_refl. apply interp_dom_subterm with (Term f (map (fun st : term * term => fst st) (ll1 ++ (u', u4) :: ll2))) (length ll1 :: nil); trivial. rewrite map_app. rewrite <- (length_map (fun st : term * term => fst st) ll1). simpl; rewrite nth_error_at_pos; apply eq_refl. assumption. apply H6; apply in_or_app; right; left; apply eq_refl. apply H13; apply in_or_app; right; left; apply eq_refl. left. absurd (G f); assumption. subst f0 l0 s'. assert (fl1_in_kk : In (Term f l1) (map (fun st : term * term => fst st) kk)). rewrite <- H6, FB. apply one_step_incl with (fun r' l' : term => In (r', l') ((r, l) :: nil)). intros t1 t2 [t1t2_eq_rl | t1t2_in_nil]; [injection t1t2_eq_rl; intros; subst; assumption | contradiction]. apply in_context; assumption. apply project_comb; right; subst k'; rewrite in_map_iff in fl1_in_kk. destruct fl1_in_kk as [[fl1 t''] [fl1_eq_fl1 fl1_in_kk]]. simpl in fl1_eq_fl1; subst fl1. rewrite in_map_iff; exists (Term f l1, t''); split; trivial. simpl; apply (interp_unicity (Term f l1)); trivial. apply interp_well_defined; trivial. apply H9; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)