proposition: Lemma Gdec : forall R Rlist, (forall l r, R r l <-> In (l,r) Rlist) -> forall P Plist, (forall u v, P v u <-> In (u,v) Plist) -> let G := fun f => defined (fun r l => R r l /\ ~ UsableRules R P r l) f in forall f, {~G f} + {G f}.
proof: Proof. intros R Rlist Rlist_ok P Plist Plist_ok. assert (H : {rule_list : list (term * term) | (forall l r : term, R r l /\ ~ UsableRules R P r l <-> In (l, r) rule_list)}). destruct (usablerules_dec _ _ Rlist_ok _ _ Plist_ok) as [URlist URlist_ok]. exists (filter (fun st => if In_dec eq_term_dec2 st URlist then false else true) Rlist). intros l r; split. intros [H1 H2]; rewrite filter_In; split. rewrite <- Rlist_ok; assumption. destruct (In_dec eq_term_dec2 (l,r) URlist). apply False_rect; apply H2; rewrite URlist_ok; assumption. apply eq_refl. rewrite filter_In; intros [H1 H2]; split. rewrite Rlist_ok; assumption. destruct (In_dec eq_term_dec2 (l,r) URlist). discriminate. rewrite URlist_ok; assumption. destruct H as [rule_list H]. intros G f; destruct (defined_dec(fun r l : term => R r l /\ ~ UsableRules R P r l) _ H f) as [Df | nDf]. right; assumption. left; assumption. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)