proposition: Lemma wf_inner_no_wf : forall R : relation term, (forall (t : term) (x : variable), ~ R t (Var x)) -> (forall s t : term, R s t -> forall x : variable, In x (var_list s) -> In x (var_list t)) -> forall rule_list : list (term * term), (forall l r : term, R r l <-> In (l, r) rule_list) -> well_founded (P_step R (inner R)) -> non_overlapping R -> well_founded (one_step R).
proof: Proof. intros R Rvar Rreg rule_list Req wf_inner NO. apply wf_inner_wf with rule_list; trivial. intros t s s' It H H'; inversion H as [r l sigma]; inversion H' as [d g tau]; subst. assert (H6 := NO l r g d sigma tau H0 H3). destruct l as [v | f l]. absurd (R r (Var v)); trivial. destruct (H6 f l (@nil nat) (eq_refl _) (sym_eq H5)) as [ _ [H7 H8]]; clear H6; subst. apply sym_eq; rewrite <- subst_eq_vars. intros v v_in_d; rewrite <- subst_eq_vars in H5. apply H5; apply Rreg with d; trivial. intros l r sigma H0; left; intros p g d tau H3 Sub Igtau. assert (H6 := NO l r g d sigma tau H0 H3). assert (H7 := subterm_in_instantiated_term _ _ _ Sub). case_eq (subterm_at_pos l p). intros u' Sub'; rewrite Sub' in H7. destruct u' as [v | f' l']. right; exists p; exists (@nil nat); exists v; split; trivial; rewrite <- app_nil_end; trivial. destruct (H6 f' l' p Sub' (sym_eq H7)) as [p_eq_nil _]; left; trivial. intros Sub'; rewrite Sub' in H7. destruct H7 as [v [q [q' [H7 [v_in_l [Sub'' Sub3]]]]]]. right; exists q; exists q'; exists v; split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)