proposition: Lemma active_is_active : forall s t, active_subterm s t <-> (exists p, active_position t p = true /\ subterm_at_pos t p = Some s).
proof: Proof. intros s t; split. intro H; inversion H as [u | s' t' H']; clear H. subst; exists nil; simpl; split; apply eq_refl. subst s' t'; rewrite trans_clos_trans_clos_alt in H'; induction H' as [x y H | x y z H1 H2]. destruct y as [v | f l]. contradiction. destruct H as [i [K1 K2]]. exists (i :: nil); simpl; split. generalize (mem_bool_ok _ _ beq_nat_ok i (mu f)); case (mem_bool Nat.eqb i (mu f)). intros _; simpl; rewrite K2; apply eq_refl. intro i_not_in_mu_f; apply False_rect; apply i_not_in_mu_f. apply (in_impl_mem (@eq _) (fun a => eq_refl a) i (mu f) K1). rewrite K2; apply eq_refl. destruct z as [v | f l]. contradiction. destruct H as [i [K1 K2]]. destruct H2 as [p [K3 K4]]. exists (i :: p); simpl; split. generalize (mem_bool_ok _ _ beq_nat_ok i (mu f)); case (mem_bool Nat.eqb i (mu f)). intros _; simpl; rewrite K2; assumption. intro i_not_in_mu_f; apply False_rect; apply i_not_in_mu_f. apply (in_impl_mem (@eq _) (fun a => eq_refl a) i (mu f) K1). rewrite K2; assumption. intros [p [H1 H2]]. revert s t H1 H2; induction p as [ | i p]; intros s t H1 H2. simpl in H2; injection H2; clear H2; intros; subst; left. destruct t as [x | f l]. discriminate. simpl in H1; simpl in H2. revert H1 H2; generalize (nth_error_ok_in i l); case (nth_error l i). intros ti H; destruct (H _ (eq_refl _)) as [l1 [l2 [L H']]]; clear H. generalize (mem_bool_ok _ _ beq_nat_ok i (mu f)); case (mem_bool Nat.eqb i (mu f)). intro i_in_mu_f; simpl; intros H1 H2. apply refl_trans_clos_is_trans with ti. apply IHp; trivial. right; left; exists i; split. apply mem_impl_in with (@eq _); trivial. subst l i; rewrite nth_error_at_pos; apply eq_refl. intros; discriminate. intros; discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)