proposition: Lemma defined_dec : forall R rule_list, (forall l r, R r l <-> In (l,r) rule_list) -> forall f, {defined R f} + { ~ defined R f}.
proof: Proof. intros R Rlist Rlist_ok f. case_eq (list_exists (fun lr => match fst lr with Var _ => false | Term g _ => eq_symb_bool f g end) Rlist). intro Df; left; rewrite list_exists_is_sound in Df. destruct Df as [[l r] [H1 H2]]; destruct l as [ | g]. discriminate. generalize (F.Symb.eq_bool_ok f g); simpl in H2; rewrite H2; intro; subst g. constructor 1 with l r; rewrite Rlist_ok; assumption. intro nDf; right; intro Df. inversion Df as [f' l t H]; subst f'; rewrite Rlist_ok in H. assert (nDf' := list_exists_is_complete_false _ _ nDf _ H); simpl in nDf'; rewrite eq_symb_bool_refl in nDf'; discriminate. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)