proposition: Lemma Psi_sim_one_step : forall t s, one_step R s t -> rwr R (psi s) (psi t) \/ P_step R (inner R) s t \/ exists s', rwr R s s' /\ P_step R (inner R) s' t.
proof: Proof. assert (W : well_founded (union _ (P_step R (inner R)) direct_subterm)). intro t; rewrite <-P_acc_with_subterm; apply wf_inner. intro t; pattern t; refine (well_founded_ind W _ _ t); clear t. intros t IHt s H; inversion H as [t1 t2 H' | f' l1 l2 H']; clear H; subst. rename H' into H; inversion H as [r l sigma H']; clear H; subst. destruct (psi_char (apply_subst sigma l)) as [[_ H] | P]. absurd (one_step R (apply_subst sigma r) (apply_subst sigma l)). intro H''; apply (H _ H''). apply at_top; apply instance; trivial. inversion P as [u v H Acc_u H3 | f' ll H K H1 H2]; clear P; subst. assert (H7 : psi (apply_subst sigma l) = apply_subst sigma r). apply (UIR (apply_subst sigma l)); trivial. apply instance; trivial. rewrite H7. destruct (psi_char (apply_subst sigma r)) as [[H1 H2] | P]. right; left; apply P_at_top; trivial; apply instance; trivial. left; apply trans_incl with (P_step R (inner R)). intros s t H6; apply P_step_one_step with (inner R); trivial. apply Psi_rwr; trivial. set (tau := map (fun xval => (@fst variable term xval, psi (@snd variable term xval))) sigma). 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). destruct (AICR _ _ sigma H') as [H6 | H6]. assert (H3' : psi (apply_subst sigma l) = apply_subst tau l). assert (H4 : forall s p, subterm_at_pos l p = Some s -> psi (apply_subst sigma s) = apply_subst tau s). intro s; pattern s; apply term_rec3; clear s. intros v p Sub; simpl; subst tau. assert (H5 := @find_map _ X.eq_bool _ _ psi v sigma). destruct (find X.eq_bool v sigma) as [val | ]; rewrite H5; trivial. apply psi_nf; apply nf_var. intros f k IH p Sub. assert (H3' : forall s, In s k -> psi (apply_subst sigma s) = apply_subst tau s). intros s s_in_k; destruct (In_split _ _ s_in_k) as [k1 [k2 H4]]; subst k. apply (IH s s_in_k (p ++ (length k1 :: nil))). apply subterm_in_subterm with (Term f (k1 ++ s :: k2)); trivial. simpl; rewrite nth_error_at_pos; trivial. destruct (inner_dec (apply_subst sigma (Term f k))) as [inner_fk | not_inner_fk]. destruct (psi_char (apply_subst sigma (Term f k))) as [[H4 H5] | P]. rewrite H4; simpl; apply (f_equal (fun l => Term f l)); apply map_eq. intros s s_in_k; rewrite <- H3'; trivial. apply sym_eq; apply psi_nf. apply nf_one_step_subterm with (apply_subst sigma (Term f k)); trivial. simpl; rewrite in_map_iff; exists s; split; trivial. inversion P as [s t H'' _ | f'' ll' H'' K']; clear P; subst. inversion H'' as [d g phi H3 H4 H5]. destruct (H6 p g d phi H3) as [H7 | H7]. rewrite H5. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos l p sigma). rewrite Sub; simpl; trivial. rewrite H5; trivial. subst p; injection Sub; clear Sub; intro Sub; subst l. simpl; rewrite psi_not_inner. apply (f_equal (fun l => Term f l)). rewrite map_map; apply map_eq; trivial. intro H7; destruct K as [s [t [st_in_ll not_nf_t]]]; apply not_nf_t. apply H7; simpl in H2; rewrite <- H2; simpl; rewrite in_map_iff; exists (s,t); split; trivial. destruct H7 as [q [q' [v [H7 Sub']]]]; subst p. destruct (subterm_in_subterm2 _ _ _ Sub) as [u [Sub'' H7]]. rewrite Sub' in Sub''; injection Sub''; clear Sub''; intro; subst u. destruct q'; discriminate. destruct K' as [s' [t' [st_in_ll' not_nf_t']]]. absurd (nf (one_step R) t'); trivial. apply inner_fk; simpl; rewrite <- H4; rewrite in_map_iff; exists (s',t'); split; trivial. simpl; rewrite psi_not_inner; trivial. apply (f_equal (fun l => Term f l)); rewrite map_map; apply map_eq; trivial. apply (H4 l (@nil nat)); simpl; trivial. rewrite H1; rewrite H3'. assert (P := psi_subst sigma tau (eq_refl _) r). inversion P as [pr H4 H4' | pr pr' H4]. left; apply t_step; apply at_top; rewrite H4'; apply instance; trivial. left; apply trans_clos_is_trans with (apply_subst tau r). apply trans_incl with (P_step R (inner R)); trivial. intros s t H''; apply P_step_one_step with (inner R); trivial. apply t_step; apply at_top; apply instance; trivial. right; right; rewrite H2; destruct H6 as [s' [H6 H7]]; exists s'; split; trivial. destruct (one_step_in_list H') as [t [s [k1 [k2 [H1 [H2 H3]]]]]]. destruct (psi_char (Term f' l2)) as [[K1 K2] | P]. apply False_rect. apply (K2 (Term f' l1)); apply in_context; trivial. inversion P as [ss tt H K | g ll H4 K]; clear P. subst ss tt. apply False_rect. refine (K t _ s H1); simpl; subst l2; apply in_or_app; right; left; trivial. subst g. assert (H6 : map (fst (A:=term) (B:=term)) ll = map psi l2). rewrite <- H5; clear K H5 H. induction ll as [ | [u v] ll]; trivial. simpl; rewrite <- IHll. apply (f_equal (fun t => t :: map (fst (A:=term) (B:=term)) ll)). destruct (H4 _ _ (or_introl _ (eq_refl _))) as [H5 | [H5 H6]]. apply Psi_unique with v; trivial. apply psi_not_nf; intro H6; apply (Psi_not_nf v u); trivial. rewrite psi_nf; trivial. intros; apply H4; right; trivial. rewrite H6 in *; rewrite H5 in *. clear H4 H5 H6; rename H into H4. destruct (map_psi f' l1) as [H5 | [H5 H5']]. rewrite H5. assert (t_in_k : In t (k1 ++ t :: k2)). apply in_or_app; right; left; trivial. rewrite <- H2 in t_in_k. destruct (IHt t (or_intror _ t_in_k) _ H1) as [H6 | [H6 | [s' [H6 H7]]]]. left; subst l1 l2; do 2 rewrite map_app; simpl; apply context_in; trivial. right; left; subst l1 l2; apply P_step_context_in; trivial. do 2 right; subst l1 l2; exists (Term f' (k1 ++ s' :: k2)); split. apply context_in; trivial. apply P_step_context_in; trivial. assert (t_in_k : In t (k1 ++ t :: k2)). apply in_or_app; right; left; trivial. rewrite <- H2 in t_in_k. destruct (IHt t (or_intror _ t_in_k) _ H1) as [H6 | [H6 | [s' [H6 H7]]]]. left; apply trans_clos_is_trans with (Term f' (map psi l1)). apply t_step; apply P_step_one_step with (inner R); trivial. subst l2 l1; do 2 rewrite map_app; simpl; apply context_in; assumption. right; left; subst l1 l2; apply P_step_context_in; trivial. do 2 right; subst l1 l2; exists (Term f' (k1 ++ s' :: k2)); split. apply context_in; trivial. apply P_step_context_in; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)