proposition: Lemma defined_list_sound : forall R rule_list, (forall l r, R r l <-> In (l,r) rule_list) -> forall f, In f (defined_list rule_list nil) -> defined R f .
proof: Proof. assert (forall R rule_list, (forall l r, R r l <-> In (l,r) rule_list) -> forall f acc, In f (defined_list rule_list acc) -> (defined R f \/ In f acc)). intros R Rlist; revert R; induction Rlist as [ | [l1 r1] Rlist]; intros R Rlist_ok f acc Df. right; assumption. assert (Rlist_ok' : forall l r : term, In (l, r) Rlist <-> In (l, r) Rlist). do 2 intro; split; intro; assumption. simpl in Df; destruct l1 as [ | f1 l1]. destruct (IHRlist _ Rlist_ok' f acc Df) as [Df' | f_in_acc]. left; inversion Df' as [f' l t H]; subst; constructor 1 with l t; rewrite Rlist_ok; right; assumption. right; assumption. destruct (IHRlist _ Rlist_ok' f (f1 :: acc) Df) as [Df' | f_in_f1acc]. left; inversion Df' as [f' l t H]; subst; constructor 1 with l t; rewrite Rlist_ok; right; assumption. simpl in f_in_f1acc; destruct f_in_f1acc as [f_eq_f1 | f_in_acc]. left; constructor 1 with l1 r1; rewrite Rlist_ok; left; subst f1; apply eq_refl. right; assumption. intros R Rlist Rlist_ok f Df; destruct (H _ _ Rlist_ok f nil Df) as [Df' | f_in_nil]; [assumption | contradiction]. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)