proposition: Lemma acc_filtering : forall R shift f l, Acc (c_in_context R shift f) l <-> Acc (one_step_list (C_step R)) (actives f shift l).
proof: Proof. intros R shift f l; revert f shift. induction l as [ | t l]; simpl; split. intro Acc_nil; apply Acc_intro; intros y H; inversion H. intro Acc_nil; apply Acc_intro; intros y [n [H _]]; inversion H. intro Acc_l. apply Acc_intro. generalize (mem_bool_ok _ _ beq_nat_ok shift (mu f)); case (mem_bool Nat.eqb shift (mu f)). intro shift_in_mu_f. intros k H. inversion H; clear H; subst. rewrite <- acc_one_step_list. simpl; intros u [u_eq_t1 | u_in_actives]. subst; apply Acc_inv with t; trivial. apply (shifting_head _ _ _ _ Acc_l); trivial. exists l; apply eq_refl. revert u u_in_actives. rewrite acc_one_step_list. rewrite <- IHl. revert Acc_l; clear. apply shifting_context. rewrite <- acc_one_step_list. simpl; intros u [u_eq_t1 | u_in_actives]. subst u; apply (shifting_head _ _ _ _ Acc_l); trivial. exists l; apply eq_refl. revert u u_in_actives; rewrite acc_one_step_list. apply Acc_inv with (actives f (S shift) l); trivial. rewrite <- IHl. apply (shifting_context _ _ _ _ Acc_l). intros shift_not_in_mu_f. intros k H. apply Acc_inv with (actives f (S shift) l); trivial. rewrite <- IHl. apply (shifting_context _ _ _ _ Acc_l). generalize (mem_bool_ok _ _ beq_nat_ok shift (mu f)); case (mem_bool Nat.eqb shift (mu f)). intro shift_in_mu_f. rewrite <- acc_one_step_list. intros Acc_tl. assert (Acc_l := tail_prop _ Acc_tl). rewrite acc_one_step_list in Acc_l. rewrite <- IHl in Acc_l. assert (Acc_t := Acc_tl _ (or_introl _ (eq_refl _))). clear Acc_tl. clear IHl; revert l Acc_l. induction Acc_t as [t Acc_t IH]. intros l Acc_l. revert t Acc_t IH; induction Acc_l as [l Acc_l IHl]. intros t Acc_t IHt. apply Acc_intro; intros k H. destruct H as [n [H1 H2]]. inversion H1; clear H1; subst. apply IHt; trivial. apply Acc_intro; assumption. apply IHl; trivial. exists i; split; trivial. revert H2; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. intros shift_not_in_mu_f. rewrite <- IHl. clear IHl. intro Acc_l; induction Acc_l as [l Acc_l IH]. apply Acc_intro; intros k H. destruct H as [n [H1 H2]]. inversion H1; clear H1; subst. apply False_rect; apply shift_not_in_mu_f. apply in_impl_mem; trivial. rewrite Nat.add_comm in H2; assumption. apply IH; exists i; split; trivial. revert H2; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)