proposition: Lemma ddp_list_is_complete : forall R rule_list, (forall l r, R r l <-> In (l,r) rule_list) -> forall is_def, (forall f, is_def f = true <-> defined R f) -> forall x y, ddp R x y -> In (y,x) (ddp_list is_def rule_list).
proof: Proof. intros R Rlist Rlist_ok is_def is_def_ok x y [H Sub]. inversion H as [ll r p f l K Sub' Df]; clear H; subst. rewrite Rlist_ok in K. clear Rlist_ok; induction Rlist as [ | [l1 r1] Rlist]. contradiction. simpl in K; destruct K as [K | K]. injection K; clear K; intros; subst; unfold ddp_list; simpl. apply fold_left_in_acc. intros acc [a b] z z_in_acc _; apply in_or_app; right; assumption. apply in_or_app; left; unfold ddp_rule; rewrite in_map_iff. exists (Term f l); split. apply eq_refl. apply defined_subterms_is_complete with p; trivial. rewrite is_def_ok; assumption. intros [i [q Sub'']]; apply (Sub i q Sub''). unfold ddp_list; simpl. replace (ddp_rule is_def l1 r1 ++ nil) with (nil ++ (ddp_rule is_def l1 r1 ++ nil)); [ | apply eq_refl]. rewrite fold_left_in_acc_split. left; apply IHRlist; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)