proposition: Lemma acc_nf_subst : forall R FB, (forall t s, In s (FB t) <-> one_step R s t) -> forall sigma, (forall x val, find eq_var_bool x sigma = Some val -> Acc (one_step R) val) -> {sigma' : substitution | (forall x val', In (x,val') sigma' <-> find eq_var_bool x sigma' = Some val') /\ (forall x val, find eq_var_bool x sigma = Some val -> exists val', (In (x,val') sigma' /\ nf (one_step R) val' /\ (val' = val \/ trans_clos (one_step R) val' val))) /\ (forall x val', In (x,val') sigma' -> nf (one_step R) val') /\ (forall x val', In (x,val') sigma' -> find eq_var_bool x sigma <> None)}.
proof: Proof. intros R FB red_dec sigma Acc_sigma. destruct (remove_garbage_subst sigma) as [tau [H1 [H H']]]. assert (H'' : {sigma' : substitution | (forall x val', In (x,val') sigma' <-> find eq_var_bool x sigma' = Some val') /\ (forall x val, find eq_var_bool x tau = Some val -> exists val', (In (x,val') sigma' /\ nf (one_step R) val' /\ (val' = val \/ trans_clos (one_step R) val' val))) /\ (forall x val', In (x,val') sigma' -> nf (one_step R) val') /\ (forall x val', In (x,val') sigma' -> find eq_var_bool x tau <> None)}). assert (Acc_tau : forall (x : variable) (val : term), In (x,val) tau -> Acc (one_step R) val). intros x val H''; apply (Acc_sigma x val); rewrite H1; apply H; trivial. clear sigma Acc_sigma H1; induction tau as [ | [x val] tau]. exists (nil : substitution); repeat split; simpl. contradiction. discriminate. intros; discriminate. contradiction. contradiction. destruct IHtau as [sigma' [H1 [H2 [H3 K3]]]]. intros y valy H4; destruct (In_split _ _ H4) as [tau1 [tau2 H5]]; subst tau. rewrite <- (H y valy). simpl; generalize (X.eq_bool_ok y x); case (eq_var_bool y x); [intro y_eq_x; absurd (y = x) | intro y_diff_x]; trivial. subst y; apply (H' x x val valy nil tau1 tau2); trivial. right; apply in_or_app; right; left; trivial. intros y z valy valz tau1 tau2 tau3 H1; apply (H' y z valy valz ((x,val) :: tau1) tau2 tau3); subst; trivial. intros y valy H''; apply Acc_tau with y; right; trivial. destruct (acc_nf FB red_dec (Acc_tau x val (or_introl _ (eq_refl _)))) as [val' [H4 H5]]. exists ((x,val') :: sigma'); split. intros y valy; split; intro H6. simpl in H6; destruct H6 as [H6 | H6]. injection H6; clear H6; intros; subst; simpl. generalize (X.eq_bool_ok y y); case (eq_var_bool y y); [intros _ | intro y_diff_y; absurd (y = y)]; trivial. assert (H7 := K3 _ _ H6). assert (H8 := find_mem _ _ X.eq_bool_ok y tau). destruct (find eq_var_bool y tau) as [valy' | ]; [idtac | absurd (@None term = None); trivial]. destruct (H8 _ (eq_refl _)) as [y' [tau1 [tau2 [H9 H10]]]]; subst y'; subst; clear H7 H8. generalize (H y valy') (X.eq_bool_ok y x); simpl; case (eq_var_bool y x); [intros _ y_eq_x | intros H7 y_diff_x]. subst y; absurd (x = x); trivial; apply (H' x x val valy' nil tau1 tau2); trivial. rewrite <- H1; trivial. destruct (find_mem _ _ X.eq_bool_ok _ _ H6) as [y' [l1 [l2 [H7 H8]]]]; subst y'; rewrite H8. apply in_or_app; right; left; trivial. repeat split. intros y valy; simpl. generalize (X.eq_bool_ok y x); case (eq_var_bool y x); [intros y_eq_x H6 | intros y_diff_x H6]. injection H6; clear H6; intros; subst y valy; exists val'; repeat split; trivial; left; trivial. destruct (H2 _ _ H6) as [valy' [K1 [K2 K4]]]. exists valy'; repeat split; trivial; right; trivial. simpl; intros y valy [H6 | H6]. injection H6; clear H6; intros; subst y valy; trivial. apply H3 with y; trivial. intros y valy; simpl. generalize (X.eq_bool_ok y x); case (eq_var_bool y x); [intros y_eq_x H6 | intros y_diff_x H6]. discriminate. apply K3 with valy; trivial. destruct H6 as [H6 | H6]; trivial. injection H6; intros; subst y; absurd (x = x); trivial. destruct H'' as [sigma' [H2 [H3 [H4 H5]]]]. exists sigma'; split; [idtac | repeat split]; trivial. intros x val H''; rewrite H1 in H''; apply H3; trivial. intros x val H''; rewrite H1; apply H5 with val; trivial. Defined.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)