proposition: Lemma acc_decomposed_term : (forall s, well_formed s -> Acc (one_step R) s) -> forall s, well_formed s -> forall l, Acc (one_step_list (one_step R)) l -> forall sigma, l = map (fun x => apply_subst sigma (Var x)) (var_list s) -> (forall x u, In (x,u) sigma -> Acc (one_step R) u) -> (forall x u, In (x,u) sigma -> match u with | Var _ => True | Term f l => (match F.arity f with Free n => n | _ => 2 end) <> length l end) -> (forall x u v, In (x,u) sigma -> In (x,v) sigma -> u = v) -> (forall x y u, In (x,u) sigma -> In (y,u) sigma -> x = y) -> (forall x, In x (var_list s) -> In x (map (@fst _ _) sigma)) -> Acc (one_step R) (apply_subst sigma s).
proof: Proof. intros WfwfR s Ws. assert (Acc_s := Acc_Rwf WfwfR s Ws). induction Acc_s as [s Acc_s IHs]. clear Acc_s; intros l Acc_l; revert s Ws IHs. induction Acc_l as [l Acc_l' IHl]. assert (Acc_l : Acc (one_step_list (one_step R)) l). apply Acc_intro; apply Acc_l'. clear Acc_l'. intros s Ws IHs sigma H0 Acc_sigma H1 H2 H3 H4; apply Acc_intro. intros u H. destruct (rewrite_decomposed_term (apply_subst sigma s) s sigma (eq_refl _) Ws H1 H2 H3 H4 u H) as [[t [J1 J2]] | J2]; clear H. rewrite J2; apply (IHs t) with (map (fun x => apply_subst sigma (Var x)) (var_list t)); trivial. apply one_step_Rwf; trivial. apply well_formed_rwr with R s; trivial. apply t_step; trivial. rewrite <- acc_one_step_list. intros v v_in_sig; rewrite in_map_iff in v_in_sig. destruct v_in_sig as [x [v_in_sig x_in_t]]. rewrite <- acc_one_step_list in Acc_l. apply Acc_l; rewrite H0; rewrite in_map_iff; exists x; split; trivial. apply R_reg_one_step with t; trivial. intros x x_in_t; apply H4; apply R_reg_one_step with t; trivial. destruct J2 as [p [x [u' [Sub [H H']]]]]. assert (H5 : exists y, exists s', exists sigma', s' = replace_at_pos s (Var y) p /\ (sigma' = sigma \/ (~In y (var_list s)) /\ sigma' = (y,u') :: sigma) /\ well_formed s' /\ u = apply_subst sigma' s' /\ Acc (one_step_list (one_step R)) (map (fun x => apply_subst sigma' (Var x)) (var_list s')) /\ (forall (x : T1.variable) (u : T1.term), In (x, u) sigma' -> Acc (one_step R) u) /\ (forall (x : T1.variable) (u : T1.term), In (x, u) sigma' -> match u with | T1.Var _ => True | T1.Term f l => match T1.F.arity f with | AC => 2 | C => 2 | Free n => n end <> length l end) /\ (forall (x : T1.variable) (u v : T1.term), In (x, u) sigma' -> In (x, v) sigma' -> u = v) /\ (forall (x y : T1.variable) (u : T1.term), In (x, u) sigma' -> In (y, u) sigma' -> x = y) /\ (forall x : T1.variable, In x (T1.var_list s') -> In x (map (@fst _ _) sigma')) /\ (In (y,u') sigma')). generalize (mem_bool_ok _ _ T.eq_bool_ok u' (map (@snd _ _) sigma)); case (mem_bool T.eq_bool u' (map (@snd _ _) sigma)); [intro u'_in_sigma | intro u'_not_in_sigma]. assert (u'_in_sigma' : In u' (map (@snd _ _) sigma)). apply mem_impl_in with (@eq _); trivial. rewrite in_map_iff in u'_in_sigma'; destruct u'_in_sigma' as [[y u''] [u'_eq_u'' u'_in_sigma']]; simpl in u'_eq_u''; subst u''. exists y; exists (replace_at_pos s (Var y) p); exists sigma. split. reflexivity. split. left; reflexivity. split. apply well_formed_replace_at_pos; simpl; [trivial | reflexivity]. split. rewrite subst_replace_at_pos. rewrite H'; apply (f_equal (fun u => replace_at_pos (apply_subst sigma s) u p)). simpl; case_eq (find X.eq_bool y sigma); [intros y_val y_sigma | intro y_sigma]. apply H2 with y; trivial. destruct (find_mem _ _ X.eq_bool_ok _ _ y_sigma) as [y' [sig1 [sig2 [y_eq_y' K]]]]; subst y'. rewrite K; apply in_or_app; right; left; reflexivity. apply False_rect; apply (find_not_found X.eq_bool y y u' sigma y_sigma (eq_var_bool_refl y) u'_in_sigma'). rewrite is_a_pos_exists_subterm; exists (Var x); assumption. split. rewrite <- acc_one_step_list. intros v v_in_sig; rewrite in_map_iff in v_in_sig. destruct v_in_sig as [z [v_in_sig z_in_t]]. rewrite <- acc_one_step_list in Acc_l. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intro z_diff_y]. subst z. rewrite <- v_in_sig; simpl. case_eq (find X.eq_bool y sigma); [intros y_val y_sigma | intro y_sigma]. replace y_val with u'. apply Acc_sigma with y; trivial. apply (H2 y); trivial. destruct (find_mem _ _ X.eq_bool_ok _ _ y_sigma) as [y' [sig1 [sig2 [y'_eq_y K]]]]; subst y'. rewrite K; apply in_or_app; right; left; reflexivity. apply False_rect; apply (find_not_found X.eq_bool y y u' sigma y_sigma (eq_var_bool_refl y) u'_in_sigma'). destruct (var_in_replace_at_pos _ _ _ _ z_in_t) as [z_in_s | z_in_y]. apply Acc_sigma with z. rewrite <- v_in_sig; simpl. case_eq (find X.eq_bool z sigma); [intros z_val z_sigma | intro z_sigma]. destruct (find_mem _ _ X.eq_bool_ok _ _ z_sigma) as [z' [sig1 [sig2 [z_eq_z' K]]]]; subst z. rewrite K; apply in_or_app; right; left; reflexivity. assert (z_in_sig := H4 _ z_in_s). rewrite in_map_iff in z_in_sig; destruct z_in_sig as [[z' z_val] [z_eq_z' z_in_sig]]. simpl in z_eq_z'; subst z'. apply False_rect; apply (find_not_found X.eq_bool z z z_val sigma z_sigma (eq_var_bool_refl z) z_in_sig). destruct z_in_y as [z_eq_y | z_in_nil]. absurd (z=y); trivial; apply sym_eq; trivial. contradiction. split. assumption. split. assumption. split. assumption. split. assumption. split. intros z z_in_t; destruct (var_in_replace_at_pos _ _ _ _ z_in_t) as [z_in_s | z_in_y]. apply H4; trivial. destruct z_in_y as [z_eq_y | z_in_nil]. subst z; rewrite in_map_iff; exists (y,u'); split; trivial. contradiction. trivial. set (m := (S (maxl _ (map (fun xt => (inject_inv (fst xt), snd xt)) sigma)))). exists (inject m). exists (replace_at_pos s (Var (inject m)) p). exists ((inject m, u') :: sigma); split. reflexivity. split. right; split. intro m_in_s; assert (m_in_sig := H4 _ m_in_s); absurd (m < m). apply Nat.lt_irrefl. rewrite in_map_iff in m_in_sig; destruct m_in_sig as [[z' t] [z_eq_z' z_in_sig]]; simpl in z_eq_z'; subst z'. unfold m at 2; apply le_n_S. apply maxl_is_max with t. rewrite in_map_iff; exists (inject m,t); split; simpl; trivial. rewrite Hinject2; trivial. reflexivity. split. apply well_formed_replace_at_pos; simpl; [trivial | reflexivity]. split. rewrite subst_replace_at_pos. rewrite H'; simpl. rewrite eq_var_bool_refl. apply (f_equal (fun s => replace_at_pos s u' p)). rewrite <- subst_eq_vars; intros z z_in_s; simpl. generalize (X.eq_bool_ok z (inject m)); case (X.eq_bool z (inject m)); [intro z_eq_m | intros _; reflexivity]. absurd (m < m). apply Nat.lt_irrefl. apply Nat.le_lt_trans with (inject_inv z). subst z; rewrite Hinject2; apply le_n. assert (z_in_sig := H4 _ z_in_s). rewrite in_map_iff in z_in_sig; destruct z_in_sig as [[z' t] [z_eq_z' z_in_sig]]; simpl in z_eq_z'; subst z'. subst m; apply le_n_S. apply maxl_is_max with t. rewrite in_map_iff; exists (z,t); split; trivial. rewrite is_a_pos_exists_subterm; exists (Var x); assumption. split. rewrite <- acc_one_step_list. intros t t_in_sigma'; rewrite in_map_iff in t_in_sigma'. destruct t_in_sigma' as [z [K1 K2]]. destruct (var_in_replace_at_pos _ _ _ _ K2) as [z_in_s | z_in_m]. rewrite <- acc_one_step_list in Acc_l. apply Acc_l; rewrite H0; rewrite in_map_iff; exists z; split; trivial. revert K1; simpl. generalize (X.eq_bool_ok z (inject m)); case (X.eq_bool z (inject m)); [intro z_eq_m | intros _; trivial]. absurd (m < m). apply Nat.lt_irrefl. apply Nat.le_lt_trans with (inject_inv z). subst z; rewrite Hinject2; apply le_n. assert (z_in_sig := H4 _ z_in_s). rewrite in_map_iff in z_in_sig; destruct z_in_sig as [[z' t'] [z_eq_z' z_in_sig]]; simpl in z_eq_z'; subst z'. subst m; apply le_n_S. apply maxl_is_max with t'. rewrite in_map_iff; exists (z,t'); split; trivial. destruct z_in_m as [z_eq_m | z_in_nil]; [subst z | contradiction]. revert K1; simpl. rewrite eq_var_bool_refl. intro; subst t. apply Acc_inv with (apply_subst sigma (Var x)). simpl. case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma]. apply Acc_sigma with x. destruct (find_mem _ _ X.eq_bool_ok _ _ x_sigma) as [x' [sig1 [sig2 [x_eq_x' H'']]]]; subst x'. rewrite H''; apply in_or_app; right; left; reflexivity. apply WfwfR; simpl; trivial. reflexivity. assumption. split. intros y uu [yuu_eq_xu | yuu_in_sigma]. injection yuu_eq_xu; intros; subst uu. apply Acc_inv with (apply_subst sigma (Var x)). simpl. case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma]. apply Acc_sigma with x. destruct (find_mem _ _ X.eq_bool_ok _ _ x_sigma) as [x' [sig1 [sig2 [x_eq_x' H'']]]]; subst x'. rewrite H''; apply in_or_app; right; left; reflexivity. apply WfwfR; simpl; trivial. reflexivity. assumption. apply Acc_sigma with y; assumption. split. intros y uu [yuu_eq_xu | yuu_in_sigma]. injection yuu_eq_xu; intros; subst y uu. destruct u' as [ | f k]; trivial. inversion H as [t1' t2' H'' | f' l1 l2' H'']; clear H; subst. inversion H'' as [r l tau H''']; clear H''; subst. destruct l as [y | g l]. apply False_rect; apply (R_var _ _ H'''). apply False_rect. revert H0; case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma]; [idtac | intro; discriminate]. assert (x_in_sig : In (x,x_val) sigma). destruct (find_mem _ _ X.eq_bool_ok _ _ x_sigma) as [x' [sig1 [sig2 [x_eq_x' K]]]]; subst x'. rewrite K; apply in_or_app; right; left; reflexivity. intro e; generalize (H1 _ _ x_in_sig); rewrite <- e; simpl. rewrite map_length; intro L; apply L. destruct (well_formed_unfold (proj2 (WR _ _ H'''))) as [_ L']; apply sym_eq; destruct (F.arity g); assumption. generalize (H1 x (Term f l2')). replace (length k) with (length l2'). intro K; apply K. rewrite H7; revert H7. case_eq (find X.eq_bool x sigma); [intros x_val x_sigma | intro x_sigma]; [idtac | intro; discriminate]. intros _; destruct (find_mem _ _ X.eq_bool_ok _ _ x_sigma) as [x' [sig1 [sig2 [x_eq_x' K']]]]; subst x'. rewrite K'; apply in_or_app; right; left; reflexivity. revert H''; clear; intro H''; induction H''. reflexivity. simpl; rewrite IHH''; trivial. apply (H1 y); trivial. split. simpl; intros y uu vv [yuu_eq_xu | yuu_in_sigma] [yvv_eq_xu | yvv_in_sigma]. injection yuu_eq_xu; intros; subst y uu. injection yvv_eq_xu; intros; subst vv; trivial. injection yuu_eq_xu; intros _ y_eq_m. absurd (m < m). apply Nat.lt_irrefl. apply Nat.le_lt_trans with (inject_inv y). subst y; rewrite Hinject2; apply le_n. subst m; apply le_n_S. apply maxl_is_max with vv. rewrite in_map_iff; exists (y, vv); split; trivial. injection yvv_eq_xu; intros _ y_eq_m. absurd (m < m). apply Nat.lt_irrefl. apply Nat.le_lt_trans with (inject_inv y). subst y; rewrite Hinject2; apply le_n. subst m; apply le_n_S. apply maxl_is_max with uu. rewrite in_map_iff; exists (y, uu); split; trivial. apply (H2 y); assumption. split. simpl; intros y z uu [yuu_eq_xu | yuu_in_sigma] [zuu_eq_xu | zuu_in_sigma]. injection yuu_eq_xu; intros; subst y uu. injection zuu_eq_xu; intros; subst; trivial. injection yuu_eq_xu; intros uu_eq_u' y_eq_m. apply False_rect; apply u'_not_in_sigma; subst u'; apply in_impl_mem. reflexivity. rewrite in_map_iff; exists (z,uu); split; trivial. injection zuu_eq_xu; intros uu_eq_u' z_eq_m. apply False_rect; apply u'_not_in_sigma; subst u'; apply in_impl_mem. reflexivity. rewrite in_map_iff; exists (y,uu); split; trivial. apply (H3 y z uu); assumption. split. intros z z_in_s'; destruct (var_in_replace_at_pos _ _ _ _ z_in_s') as [z_in_s | z_in_m]. right; apply H4; assumption. destruct z_in_m as [z_eq_m | z_in_nil]; [left; trivial | contradiction]. left; reflexivity. destruct H5 as [y [s' [sigma' [k0 [K0 [Ws' [K [Acc_sigma' [K1 [K2 [K3 [K4 [K5 K6]]]]]]]]]]]]]. rewrite K. apply IHl with (map (fun x => apply_subst sigma' (Var x)) (var_list s')); trivial. assert (y_sig : apply_subst sigma' (Var y) = u'). simpl; case_eq (find X.eq_bool y sigma'); [intros y_val y_sig | intro y_sig]. apply (K3 y); trivial. destruct (find_mem _ _ X.eq_bool_ok _ _ y_sig) as [y' [sig1 [sig3 [y_eq_y' J]]]]; subst y. rewrite J; apply in_or_app; right; left; reflexivity. apply False_rect; apply (find_not_found X.eq_bool y y u' sigma' y_sig (eq_var_bool_refl y) K6). assert (x_sig : forall x, x<> y -> apply_subst sigma' (Var x) = apply_subst sigma (Var x)). intros z z_diff_y; destruct K0 as [K0 | [y_not_in_s K0]]; subst sigma'. reflexivity. simpl. generalize (X.eq_bool_ok z y); case (X.eq_bool z y); [intro z_eq_y | intros _; reflexivity]. absurd (z=y); trivial. rewrite H0; rewrite k0. destruct K0 as [K0 | [y_not_in_s K0]]; subst sigma'. clear x_sig. revert H y_sig Sub. clear. revert sigma p x u' y; pattern s; apply term_rec3; clear s. intros v sigma p x u' y H y_sig Sub. destruct p as [ | ]; [injection Sub; clear Sub; intros; subst v | discriminate]. simpl replace_at_pos; simpl var_list; simpl; simpl in y_sig; rewrite y_sig. left; assumption. intros f l IHl sigma p x u' y H y_sig Sub. destruct p as [ | i p]. discriminate. simpl in Sub. revert Sub; generalize (nth_error_ok_in i l). destruct (nth_error l i) as [ti | ]; [idtac | intros; discriminate]. intro H'; destruct (H' _ (eq_refl _)) as [l1 [l2 [L H'']]]; clear H'. intro Sub. subst l. rewrite replace_at_pos_unfold. rewrite replace_at_pos_list_replace_at_pos_in_subterm; trivial. do 2 (rewrite var_list_unfold; rewrite var_list_list_app; rewrite map_app). simpl var_list_list; do 2 rewrite map_app. set (k1 := (map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list_list l1))) in *. set (k2 := (map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list_list l2))) in *. clearbody k1 k2. assert (Hi : one_step_list (one_step R) (map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list (replace_at_pos ti (Var y) p))) (map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list ti))). apply IHl with x u'; trivial. apply in_or_app; right; left; reflexivity. set (k := map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list ti)) in *. set (k' := map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list (replace_at_pos ti (Var y) p))) in *. clearbody k k'. induction k1 as [ | s1 k1]. induction Hi; [left | right]; assumption. right; assumption. revert H x_sig y_sig y_not_in_s Sub. clear. revert sigma p x u' y; pattern s; apply term_rec3; clear s. intros v sigma p x u' y H x_sig y_sig y_not_in_s Sub. destruct p as [ | ]; [injection Sub; clear Sub; intros; subst v | discriminate]. simpl replace_at_pos; simpl var_list; simpl; simpl in y_sig; rewrite y_sig. left; assumption. intros f l IHl sigma p x u' y H x_sig y_sig y_not_in_s Sub. destruct p as [ | i p]. discriminate. simpl in Sub. revert Sub; generalize (nth_error_ok_in i l). destruct (nth_error l i) as [ti | ]; [idtac | intros; discriminate]. intro H'; destruct (H' _ (eq_refl _)) as [l1 [l2 [L H'']]]; clear H'. intro Sub. subst l. rewrite replace_at_pos_unfold. rewrite replace_at_pos_list_replace_at_pos_in_subterm; trivial. do 2 (rewrite var_list_unfold; rewrite var_list_list_app; rewrite map_app). simpl var_list_list; do 2 rewrite map_app. set (k1 := (map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list_list l1))) in *. set (k1' := (map (fun x0 : variable => apply_subst ((y, u') :: sigma) (Var x0)) (var_list_list l1))) in *. assert (k1_eq_k1' : k1 = k1'). assert (y_not_in_l1 : ~In y (var_list_list l1)). intro y_in_l1; apply y_not_in_s. simpl; rewrite var_list_list_app; apply in_or_app; left; assumption. set (vl1 := (var_list_list l1)) in *. clearbody vl1. induction vl1 as [ | v1 vl1]; trivial. subst k1 k1'. simpl; simpl in IHvl1; rewrite <- IHvl1; clear IHvl1. assert (v1_sig := x_sig v1). simpl in v1_sig; rewrite v1_sig; clear v1_sig; trivial. intro v1_eq_y; apply y_not_in_l1; left; assumption. intro y_in_l1; apply y_not_in_l1; right; assumption. clearbody k1 k1'; subst k1. set (k2 := (map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list_list l2))) in *. set (k2' := (map (fun x0 : variable => apply_subst ((y, u') :: sigma) (Var x0)) (var_list_list l2))) in *. assert (k2_eq_k2' : k2 = k2'). assert (y_not_in_l2 : ~In y (var_list_list l2)). intro y_in_l2; apply y_not_in_s. simpl; rewrite var_list_list_app; apply in_or_app; right; apply in_or_app; right; assumption. set (vl2 := (var_list_list l2)) in *. clearbody vl2. induction vl2 as [ | v2 vl2]; trivial. subst k2 k2'. simpl; simpl in IHvl2; rewrite <- IHvl2; clear IHvl2. assert (v2_sig := x_sig v2). simpl in v2_sig; rewrite v2_sig; clear v2_sig; trivial. intro v2_eq_y; apply y_not_in_l2; left; assumption. intro y_in_l2; apply y_not_in_l2; right; assumption. clearbody k2 k2'; subst k2. assert (Hi : one_step_list (one_step R) (map (fun x0 : variable => apply_subst ((y,u') :: sigma) (Var x0)) (var_list (replace_at_pos ti (Var y) p))) (map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list ti))). apply IHl with x; trivial. apply in_or_app; right; left; reflexivity. intro y_in_ti; apply y_not_in_s; rewrite var_list_unfold; rewrite var_list_list_app; apply in_or_app; right; apply in_or_app; left; assumption. set (k := map (fun x0 : variable => apply_subst sigma (Var x0)) (var_list ti)) in *. set (k' := map (fun x0 : variable => apply_subst ((y,u') :: sigma) (Var x0)) (var_list (replace_at_pos ti (Var y) p))) in *. clearbody k k'. induction k1' as [ | s1 k1]. induction Hi; [left | right]; assumption. right; assumption. intros s'' s''_R_s' Ws'' l'' Acc_l'' sigma'' J0 Acc_sigma'' J1 J2 J3 J4. apply IHs with l''; trivial. inversion s''_R_s' as [t' t'' J]; subst t' t''. subst s'; apply Ren. replace (collapse_subst s) with (collapse_subst (replace_at_pos s (Var y) p)); trivial. revert Sub. clear; intro Sub. assert (col_map : forall t, collapse_subst t = match t with | Var _ => Var (inject 0) | Term f l => Term f (map collapse_subst l) end). clear. intro t; pattern t; apply term_rec3; clear t. intros v; unfold collapse_subst; simpl. rewrite eq_var_bool_refl; reflexivity. intros f l IHl; unfold collapse_subst. rewrite var_list_unfold. simpl; apply f_equal; clear f. apply map_eq. intros t t_in_l. rewrite <- subst_eq_vars; intros v v_in_t'. simpl; rewrite find_col. rewrite find_col; trivial. destruct (in_split _ _ t_in_l) as [l1 [l2 H]]; subst l; rewrite var_list_list_app; apply in_or_app; right. simpl; apply in_or_app; left; trivial. revert p Sub; pattern s; apply term_rec3; clear s. intros v p Sub; destruct p as [ | i p]; [idtac | discriminate]. injection Sub; clear Sub; intros; subst v. simpl; do 2 rewrite col_map; trivial. intros f l IH p Sub; destruct p as [ | i p]. discriminate. rewrite replace_at_pos_unfold. do 2 rewrite col_map. apply f_equal. simpl in Sub. revert Sub; case_eq (nth_error l i); [intros ti H Sub| intros; discriminate]. destruct (nth_error_ok_in _ _ H) as [l1 [l2 [L H']]]. subst l; rewrite replace_at_pos_list_replace_at_pos_in_subterm; trivial. do 2 rewrite map_app; simpl. apply f_equal. apply (f_equal (fun t => t :: map collapse_subst l2)). apply IH; trivial. apply in_or_app; right; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)