proposition: Lemma defined_subterms_is_complete: forall is_def lhs, forall r p f l acc, subterm_at_pos r p = Some (Term f l) -> is_def f = true -> (~exists i, exists p, subterm_at_pos lhs (i :: p) = Some (Term f l)) -> In (Term f l) (defined_subterms is_def lhs acc r).
proof: Proof. intros is_def lhs r. induction r using term_rec3. intros p f l acc H f_in_def Sub; destruct p; simpl in H; discriminate. intros [ | i p] g k acc H' g_in_def Sub. simpl in H'; injection H'; clear H'; intros; subst g k; simpl. apply fold_left_in_acc. intros; apply defined_subterms_accumulates; auto. rewrite g_in_def. generalize (eq_bool_ok lhs (Term f l)); case (eq_bool lhs (Term f l)); [intro lhs_eq_fl | intro lhs_diff_fl]. left; apply eq_refl. generalize (is_subterm_ok_true (Term f l) lhs). case (is_subterm (Term f l) lhs); [intro Sub' | intros _]. apply False_ind. apply Sub. destruct (Sub' (eq_refl _)) as [[ | i p] Sub'']. simpl in Sub''; absurd (lhs = Term f l); trivial; injection Sub''; intros; trivial. exists i; exists p; trivial. left; trivial. generalize (more_list.nth_error_ok_in i l). simpl in H'; destruct (nth_error l i) as [ti | ]. intro h; destruct (h _ (eq_refl _)) as [l1 [l2 [h1 h2]]]; clear h; subst. simpl; rewrite fold_left_app; simpl. apply fold_left_in_acc. intros; apply defined_subterms_accumulates; auto. apply H with p; auto with *. discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)