proposition: Lemma Rquo_dec : forall x y, {Rquo x y} + {~Rquo x y}.
proof: Proof. intros; simpl in *. unfold Rquo. cut ({exists r, SCC'_tag r = Some x /\ (exists s, SCC'_tag s = Some y /\ R r s) /\ In r Dom} + {~exists r, SCC'_tag r = Some x /\ (exists s, SCC'_tag s = Some y /\ R r s) /\ In r Dom}). intro. destruct H. left; destruct e; exists x0; tauto. right. intuition. apply n. do 2 destruct H. exists x0; intuition. destruct H0; ded (restriction x0 x1). tauto. cut ({exists r, (fun t => SCC'_tag t = Some x /\ exists s, SCC'_tag s = Some y /\ R t s) r /\ In r Dom} + {~exists r, (fun t => SCC'_tag t = Some x /\ exists s, SCC'_tag s = Some y /\ R t s) r /\ In r Dom}). intro. destruct H. left; destruct e; auto. exists x0. intuition. right. intuition. apply n. destruct H. exists x0. intuition. apply exists_in_list_dec. intro r. destruct (eq_opt_dec eq_nat_dec (SCC'_tag r) (Some x)). 2: { right. tauto. } cut ({exists s, SCC'_tag s = Some y /\ R r s} + {~exists s, SCC'_tag s = Some y /\ R r s}). intros. destruct H. left. intuition. right; intuition. change ({exists s, (fun t => SCC'_tag t = Some y /\ R r t) s} + {~exists s, (fun t => SCC'_tag t = Some y /\ R r t) s}). assert ({exists s, (fun t => SCC'_tag t = Some y /\ R r t) s /\ In s Dom} + {~exists s, (fun t => SCC'_tag t = Some y /\ R r t) s /\In s Dom}). apply exists_in_list_dec. intro r0. destruct (eq_opt_dec eq_nat_dec (SCC'_tag r0) (Some y)); destruct (R_dec r r0). left; auto. right; tauto. right; tauto. right; tauto. destruct H. left; destruct e0; exists x0; tauto. right; intuition; apply n. destruct H. exists x0; intuition. ded (restriction r x0); tauto. Defined.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)