proposition: Lemma one_step_nf_inner_step_nf : forall (R : relation term), (forall t v, R t (Var v) -> False) -> forall t, nf (one_step R) t <-> nf (P_step R (inner R)) t.
proof: Proof. intros R Rvar t; split. intros H s H'; apply (H s); apply (P_step_one_step R (inner R)); trivial. pattern t; apply term_rec3; clear t. intros v _ s H'; inversion H' as [t1 t2 H'' | f' l1 l2 H'']; clear H'; subst. inversion H''; clear H''; subst. destruct t2 as [v2 | f2 l2]. apply (Rvar t1 v2); trivial. discriminate. intros f l IH H s H'. apply (H s); apply P_at_top. intros t t_in_l; apply IH; trivial. apply nf_P_step_subterm with (Term f l); trivial. inversion H' as [t1 t2 H'' | f' l1 l2 H'']; clear H'; subst; trivial. assert (H' : forall t, In t l -> nf (one_step R) t). intros t t_in_l; apply IH; trivial. apply nf_P_step_subterm with (Term f l); trivial. assert False. generalize l1 H'' H'; clear IH H l1 H'' H'; induction l as [ | t l]; intros l1 H'' H'; inversion H'' as [t1 t2' l' H3 | t' l1' l2' H3]; clear H''; subst. apply (H' t (or_introl _ (eq_refl _)) t1); trivial. apply (IHl l1'); trivial. intros s s_in_l; apply H'; right; trivial. contradiction. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)