proposition: Lemma active_dec : forall s t, {active_subterm s t}+{~ active_subterm s t}.
proof: Proof. intros s t; revert s; pattern t; apply term_rec3. intros v s; generalize (eq_bool_ok s (Var v)); case (eq_bool s (Var v)). intros s_eq_v; left; subst s; left. intros s_diff_v; right; intro A; apply s_diff_v. inversion A; subst; trivial. rewrite trans_clos_trans_clos_alt in H. inversion H; clear H; subst. inversion H0. inversion H1. intros f l IH s. generalize (eq_bool_ok s (Term f l)); case (eq_bool s (Term f l)). intro s_eq_fl; left; subst s; left. intros s_diff_fl. assert (H : {ti | In ti l /\ active_subterm s ti /\ active_direct_subterm ti (Term f l)}+ {forall ti, In ti l -> active_direct_subterm ti (Term f l) -> active_subterm s ti -> False}). clear s_diff_fl; simpl. unfold active_in_list; generalize 0. revert s; induction l as [ | t1 l]. intros s n; right; intros; contradiction. intros s n; simpl. generalize (mem_bool_ok _ _ beq_nat_ok n (mu f)); case (mem_bool Nat.eqb n (mu f)). intro n_in_mu_f; destruct (IH _ (or_introl _ (eq_refl _)) s) as [A1 | not_A1]. left; exists t1; split. left; apply eq_refl. split; trivial. exists 0; split. rewrite Nat.add_comm; apply mem_impl_in with (@eq _); trivial. apply eq_refl. destruct (IHl (tail_set _ IH) s (S n)) as [Ai | not_Al]. destruct Ai as [ti [ti_in_l [Ai Al]]]. left; exists ti; split; [idtac | split]. right; assumption. assumption. destruct Al as [i [H1 H2]]. exists (S i); split; trivial. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. right; intros ti [t1_eq_ti | ti_in_l] Al Ai. apply not_A1; subst ti; assumption. destruct Al as [[ | i] [H1 H2]]. injection H2; clear H2; intro; subst ti. apply not_A1; assumption. apply (not_Al ti ti_in_l); trivial. exists i; split; trivial. revert H1; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. intro not_mem_n_mu_f. destruct (IHl (tail_set _ IH) s (S n)) as [Ai | not_Al]. destruct Ai as [ti [ti_in_l [Ai Al]]]. left; exists ti; split; [idtac | split]. right; assumption. assumption. destruct Al as [i [H1 H2]]. exists (S i); split; trivial. rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. right; intros ti [t1_eq_ti | ti_in_l] Al Ai. destruct Al as [[ | i] [H1 H2]]. rewrite Nat.add_comm in H1; apply not_mem_n_mu_f; apply in_impl_mem; trivial. apply (not_Al ti); trivial. simpl in H2; destruct (nth_error_ok_in _ _ H2) as [l1 [l2 [L H]]]; subst l; apply in_or_app; right; left; apply eq_refl. exists i; split; trivial. revert H1; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. apply (not_Al ti); trivial. destruct Al as [[ | i] [H1 H2]]. apply False_rect; rewrite Nat.add_comm in H1; apply not_mem_n_mu_f; apply in_impl_mem; trivial. simpl in H2; exists i; split; trivial. revert H1; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. destruct H as [[ti [ti_in_l [Ai Al]]] | H]. left; apply refl_trans_clos_is_trans with ti; trivial. right; left; trivial. right; intro A; inversion A as [u | x y A']; clear A. subst; apply s_diff_fl; apply eq_refl. rewrite trans_clos_trans_clos_alt in A'; inversion A' as [x' y' A'' | x' y' z' A1 A2]; clear A'; subst. apply (H s); trivial. destruct A'' as [i [H1 H2]]. simpl in H2; destruct (nth_error_ok_in _ _ H2) as [l1 [l2 [L H3]]]; subst l; apply in_or_app; right; left; apply eq_refl. left. apply (H y'); trivial. destruct A2 as [i [H1 H2]]. simpl in H2; destruct (nth_error_ok_in _ _ H2) as [l1 [l2 [L H3]]]; subst l; apply in_or_app; right; left; apply eq_refl. rewrite <- trans_clos_trans_clos_alt in A1; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)