proposition: Lemma Psi_rwr : forall t s, Psi s t -> trans_clos (P_step R (inner R)) s t.
proof: Proof. assert (red_dec :=compute_red_is_correct rule_list Rreg' R Req). assert (nf_dec := dec_nf _ _ red_dec). intros t; pattern t; apply term_rec3; clear t. intros v s P; assert False; [idtac | contradiction]. apply (Psi_not_nf (Var v) s); trivial. apply nf_var. intros f l IH s P; destruct (psi_char (Term f l)) as [[H1 H2] | P']. assert False; [idtac | contradiction]. apply (Psi_not_nf (Term f l) s); trivial. rewrite (Psi_unique _ _ _ P P'). inversion P'; clear P'; subst. apply t_step; apply P_at_top; trivial. rewrite H; rewrite psi_not_inner. apply P_general_context. destruct H3 as [s' [t [st_in_ll not_nf_t]]]. rewrite psi_not_inner in H. injection H; clear H; intro H. rewrite rwr_list_expand. destruct (In_split _ _ st_in_ll) as [ll1 [ll2 H']]; subst. exists t; exists s'; simpl. exists (map (@snd term term) ll1). exists (map (@snd term term) ll2). exists (map (@fst term term) ll1). exists (map (@fst term term) ll2). split. rewrite map_app; trivial. split. rewrite <- H; rewrite map_app; trivial. assert (H' : forall kk, (forall u v, In (u,v) kk -> refl_trans_clos (P_step R (inner R)) u v) -> refl_trans_clos (one_step_list (P_step R (inner R))) (map (@fst _ _) kk) (map (@snd _ _) kk)). intros kk; induction kk as [ | [u1 v1] kk]; intros H'. left; trivial. simpl; rewrite refl_trans_clos_one_step_list_head_tail; split. apply H'; left; apply eq_refl. apply IHkk; intros; apply H'; right; assumption. split. apply H'; intros u v uv_in_ll1; destruct (H2 u v) as [H2' | [H2' _]]. apply in_or_app; left; trivial. right; apply IH; trivial; rewrite in_map_iff; exists (u,v); split; trivial; apply in_or_app; left; trivial. subst; left. split. apply IH. rewrite in_map_iff; exists (s',t); split; trivial. destruct (H2 s' t) as [H2' | [_ H2']]; trivial. absurd (nf (one_step R) t); trivial. apply H'; intros u v uv_in_ll2; destruct (H2 u v) as [H2' | [H2' _]]. apply in_or_app; do 2 right; trivial. right; apply IH; trivial; rewrite in_map_iff; exists (u,v); split; trivial; apply in_or_app; do 2 right; trivial. subst; left. unfold inner; intro H'; apply not_nf_t; apply H'; simpl; rewrite in_map_iff; exists (s',t); split; trivial. destruct H3 as [s' [t [st_in_ll not_nf_t]]]. unfold inner; intro H'; apply not_nf_t; apply H'; simpl; 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)