proposition: Lemma def_dec_rules : 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 rule_list; generalize R; clear R; induction rule_list as [ | [l r] rule_list]; intros R Equiv f. right; intro Df; inversion Df as [f' k u H]; subst. rewrite Equiv in H; contradiction. set (R' := fun r l => In (l,r) rule_list). assert (Equiv' : forall l r : term, R' r l <-> In (l, r) rule_list). intros l1 r1; unfold R'; split; trivial. destruct (IHrule_list R' Equiv' f) as [Df | Cf]. left; inversion Df as [f' k u H]; subst. apply (Def R f k u). rewrite Equiv; right; trivial. destruct l as [v | f' k']. right; intro Df; inversion Df as [f' k u H]; subst. apply Cf. rewrite Equiv in H. destruct H as [H | H]. discriminate. rewrite <- Equiv' in H. apply (Def R' f k u); trivial. generalize (F.Symb.eq_bool_ok f f'); case (F.Symb.eq_bool f f'); [intros f_eq_f' | intros f_diff_f']. left; apply (Def R f k' r); subst; rewrite Equiv; left; trivial. right; intro Df; inversion Df as [f'' k u H]; subst. rewrite Equiv in H; destruct H as [H | H]. apply f_diff_f'; injection H; intros; subst; trivial. apply Cf. rewrite <- Equiv' in H. apply (Def R' f k u); trivial. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)