proposition: Lemma possible_antisym_topo_sort : forall R, eq_dec A -> rel_dec R -> irreflexive (clos_trans R) -> antisym_topo_sortable R.
proof: Proof. do 4 intro. assert (forall l, rel_dec (LETS R l)). intro. apply LETS_dec; hyp. pose (eq_dec_midex X). pose (rel_dec_midex X0). exists (fun l x y => if (X1 l x y) then true else false). simpl. split. do 5 intro. case (X1 (x :: y :: nil) x y). case (X1 (y :: x :: nil) x y). do 2 intro. absurd (LETS R (x :: y :: nil) x y /\ LETS R (y :: x :: nil) x y). apply LETS_antisym; hyp. tauto. do 3 intro. destruct H3. inversion H4. do 2 intro. destruct H3. inversion H3. split. do 3 intro. destruct (X1 l x y). apply (LETS_restricted R l x y). hyp. inversion H0. split. do 3 intro. destruct (X1 l x y). trivial. absurd (LETS R l x y). hyp. apply LETS_restriction_clos_trans. eapply incl_tc. refl. hyp. split. do 5 intro. destruct (X1 l x y). destruct (X1 l y z). pose (LETS_transitive R l x y z l0 l1). destruct (X1 l x z). trivial. contr. inversion H1. inversion H0. split. do 2 intro. destruct (X1 l x x). absurd (LETS R l x x). destruct (LETS_irrefl R l). hyp. apply H1. apply irreflexive_incl with (clos_trans R). apply tc_incl. apply incl_restriction. hyp. hyp. inversion H0. do 4 intro. unfold trichotomy. destruct (X1 l x y). tauto. destruct (X1 l y x). tauto. destruct (LETS_total l e r x y); tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)