proposition: Lemma Psi_def : forall t, ~nf (one_step R) t -> {t' : term | Psi t' t}.
proof: Proof. assert (red_dec :=compute_red_is_correct rule_list Rreg' R Req). assert (nf_dec := dec_nf _ _ red_dec). assert (inner_dec := nf_dec_inner_dec _ nf_dec). intros t; assert (Acc_t := wf_inner t); rewrite P_acc_with_subterm in Acc_t. induction Acc_t as [t Acc_t IH]. intro t_not_nf. destruct t as [v | f l]. absurd (nf (one_step R) (Var v)); trivial. apply nf_var. assert (red_dec_fl := red_dec (Term f l)). destruct (compute_red rule_list (Term f l)) as [ | r rl]. absurd (nf (one_step R) (Term f l)); trivial. intros s H; rewrite <- red_dec_fl in H; contradiction. destruct (inner_dec (Term f l)) as [inner_fl | not_inner_fl]. assert (H' : one_step R r (Term f l)). rewrite <- red_dec_fl; left; trivial. exists r; inversion H' as [t1 t2 H'' | g k1 k2 H'']; subst. apply Psi_at_top; trivial; apply Acc_intro; trivial. assert False; [idtac | contradiction]. unfold inner in inner_fl; simpl in inner_fl. generalize inner_fl; clear f Acc_t IH t_not_nf red_dec_fl H' inner_fl. induction H''; intros nf_l. apply (nf_l t2 (or_introl _ (eq_refl _)) t1 H). apply IHH''; intros; apply nf_l; right; trivial. assert (H : forall t, In t l -> ~ nf (one_step R) t -> { t' : term | Psi t' t} ). intros t t_in_l; apply IH; right; trivial. assert (H' : {ll : list (term * term) | map (@snd term term) ll = l /\ (forall s t, In (s,t) ll -> Psi s t \/ (s=t /\ nf (one_step R) t))}). clear f Acc_t IH t_not_nf red_dec_fl not_inner_fl r rl. induction l as [ | t l]. exists (@nil (term * term)); split; trivial. intros; contradiction. destruct IHl as [ll [H1 H2]]. intros; apply H; trivial; right; trivial. destruct (nf_dec t) as [nf_t | not_nf_t]. exists ((t,t) :: ll); simpl; split. subst l; trivial. intros u v [uv_eq_tt | uv_in_ll]. injection uv_eq_tt; intros; do 2 subst. right; split; trivial. apply H2; trivial. destruct (H t (or_introl _ (eq_refl _))) as [t' P]; trivial. exists ((t',t) :: ll); simpl; split. subst l; trivial. intros u v [uv_eq_tt' | uv_in_ll]. injection uv_eq_tt'; intros; subst. left; trivial. apply H2; trivial. destruct H' as [ll [H1 H2]]. exists (Term f (map (@fst term term) ll)). rewrite <- H1; apply Psi_in_context; trivial. assert (H3 : exists t, In t l /\ ~nf (one_step R) t). unfold inner in not_inner_fl; simpl in not_inner_fl. clear Acc_t IH t_not_nf red_dec_fl H H1 H2 r rl f. induction l as [ | s l]. assert False; [idtac | contradiction]. apply not_inner_fl; intros; contradiction. destruct (nf_dec s) as [nf_s | not_nf_s]. destruct IHl as [t [t_in_l H]]. intro; apply not_inner_fl. simpl; intros u [u_eq_s | u_in_l]. subst; trivial. apply H; trivial. exists t; split; trivial; right; trivial. exists s; split; trivial. left; trivial. destruct H3 as [t [t_in_l H4]]. destruct (H t t_in_l H4) as [t' H5]. exists t'; exists t; split; trivial. rewrite <- H1 in t_in_l. rewrite in_map_iff in t_in_l. destruct t_in_l as [[u' u] [H6 H7]]. simpl in H6; subst u. destruct (H2 _ _ H7) as [H8 | [H8 H9]]. replace t' with u'; trivial. refine (Psi_unique _ _ _ H8 H5). assert False; [idtac | contradiction]. apply Psi_not_nf with t t'; trivial. Defined.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)