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