proposition: Lemma filtering : forall R shift f l l1, c_in_context R shift f l1 l -> one_step_list (C_step R) (actives f shift l1) (actives f shift l).
proof: Proof. intros R shift f l; revert f shift. induction l as [ | t l]; simpl; intros f shift l1. intros [n [H _]]; inversion H. intros [n [K H]]; inversion K; clear K; subst; simpl. generalize (mem_bool_ok _ _ beq_nat_ok shift (mu f)); case (mem_bool Nat.eqb shift (mu f)). intro shift_in_mu_f; left; assumption. intro shift_not_in_mu; apply False_rect; rewrite Nat.add_comm in H; apply shift_not_in_mu; apply in_impl_mem; trivial. generalize (mem_bool_ok _ _ beq_nat_ok shift (mu f)); case (mem_bool Nat.eqb shift (mu f)). intros _; right; apply IHl. exists i; split; trivial. revert H; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. intros _; apply IHl. exists i; split; trivial. revert H; 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)