proposition: Lemma actives_ok : forall f n l s, In s (actives f n l) <-> shifted_active_in_list n f l s.
proof: Proof. intros f n l; revert n; induction l as [ | t l]; intros n s; simpl; split. contradiction. intros [[ | i] [_ H]]; discriminate. generalize (mem_bool_ok _ _ beq_nat_ok n (mu f)). case (mem_bool Nat.eqb n (mu f)). intro n_in_mu_f. simpl; intros [s_eq_t | s_in_actives]. subst s; exists 0; split; trivial. rewrite Nat.add_comm; apply mem_impl_in with (@eq _); trivial. rewrite IHl in s_in_actives; destruct s_in_actives as [i [H1 H2]]. exists (S i); split; trivial. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; assumption. intro n_not_in_mu_f. rewrite IHl; intros [i [H1 H2]]. exists (S i); split; trivial. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; assumption. generalize (mem_bool_ok _ _ beq_nat_ok n (mu f)). case (mem_bool Nat.eqb n (mu f)). intro n_in_mu_f. intros [[ | i] [H1 H2]]. simpl in H2; injection H2; clear H2; intro; subst s; left; apply eq_refl. right; rewrite IHl. exists i; split; trivial. revert H1; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. intro n_not_in_mu_f. intros [[ | i] [H1 H2]]. rewrite Nat.add_comm in H1; apply False_rect; apply n_not_in_mu_f; apply in_impl_mem; trivial. rewrite IHl; exists i; split; trivial. revert H1; 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)