proposition: Lemma LETS_antisym : forall R, antisym R (LETS R).
proof: Proof. unfold LETS. do 7 intro. simpl in *|- . destruct H2. assert (is_restricted (restriction R (x :: y :: nil)) (x::y::nil)). apply restricted_restriction. assert (is_restricted (try_add_arc (clos_trans (restriction R (x :: y :: nil))) y y) (x::y::nil)). apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans. hyp. assert (is_restricted (try_add_arc (clos_trans (try_add_arc (clos_trans (restriction R (x :: y :: nil))) y y)) y x) (x::y::nil)). apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans. hyp. assert (is_restricted (try_add_arc (clos_trans (try_add_arc (clos_trans (try_add_arc (clos_trans (restriction R (x :: y :: nil))) y y)) y x)) x y) (x::y::nil)). apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans. hyp. assert (is_restricted (try_add_arc (clos_trans (try_add_arc (clos_trans (try_add_arc (clos_trans (try_add_arc (clos_trans (restriction R (x :: y :: nil))) y y)) y x)) x y)) x x) (x::y::nil)). apply restricted_try_add_arc; simpl; try tauto. apply restricted_clos_trans. hyp. pose (clos_trans_restricted_pair H8 H2). inversion t; try tauto. clear H10 H11 z t0. pose (clos_trans_restricted_pair H7 H9). inversion t0. clear H11 H12 z t1. pose (clos_trans_restricted_pair H6 H10). inversion t1; try tauto. clear H12 H13 z t2. pose (clos_trans_restricted_pair H5 H11). inversion t2. clear H13 H14 z t3. assert (restriction R (x :: y :: nil) x y). apply clos_trans_restricted_pair; hyp. unfold restriction in H13. tauto. tauto. absurd (clos_trans (try_add_arc (clos_trans (try_add_arc (clos_trans (restriction R (x :: y :: nil))) y y)) y x) y x). hyp. constructor. constructor 2. intro. rewrite H14 in H10. tauto. intro. pose (clos_trans_restricted_pair H5 H14). inversion t1; try tauto. clear H16 H17 z t2. pose (clos_trans_restricted_pair H4 H15). unfold restriction in r. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)