proposition: Lemma psi_not_inner : forall f l, ~(inner R (Term f l)) -> psi (Term f l) = Term f (map psi l).
proof: Proof. intros f l not_nf_fl. assert (red_dec :=compute_red_is_correct rule_list Rreg' R Req). assert (nf_dec := dec_nf _ _ red_dec). destruct (psi_char (Term f l)) as [[H1 H2] | P]. absurd (inner R (Term f l)); trivial. intros s s_in_l; simpl in s_in_l. apply nf_one_step_subterm with (Term f l); trivial. apply Psi_unique with (Term f l); trivial. apply Psi_in_context_bis; trivial. inversion P; subst. absurd (inner R (Term f l)); trivial. destruct H3 as [s [t [st_in_llst not_nf_t]]]. exists t; split; trivial. rewrite in_map_iff; exists (s,t); split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)