proposition: Lemma rwr_not_H : forall l r, R r l -> forall s t, Interp_dom s -> Interp_dom t -> (match s with Var _ => False | Term g _ => G g end) -> 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 s; pattern s; apply term_rec3; clear s. intros; contradiction. intros f k IH t Acc_s Acc_t K' 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. destruct t2 as [x2 | f2 l2]; simpl in K'. apply (R_var _ _ K). injection H0; clear H0; intros; subst; assumption. rewrite H0; assumption. rewrite H0; assumption. inversion Is; clear Is. subst; 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; assumption. 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)