Skip to content

Instantly share code, notes, and snippets.

@Gbury

Gbury/script.v

Created August 19, 2018 23:22
Show Gist options
  • Save Gbury/6d42a203e44d73be8cacc4f15e489593 to your computer and use it in GitHub Desktop.
Save Gbury/6d42a203e44d73be8cacc4f15e489593 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
script.v
(**
Proof automatically generated by Archsat
Input file: eq_diamond6.smt2
**)
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 11, character 0-18 *)
Parameter U : Type.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 12, character 0-21 *)
Parameter x0 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 13, character 0-21 *)
Parameter y0 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 14, character 0-21 *)
Parameter z0 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 15, character 0-21 *)
Parameter x1 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 16, character 0-21 *)
Parameter y1 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 17, character 0-21 *)
Parameter z1 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 18, character 0-21 *)
Parameter x2 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 19, character 0-21 *)
Parameter y2 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 20, character 0-21 *)
Parameter z2 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 21, character 0-21 *)
Parameter x3 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 22, character 0-21 *)
Parameter y3 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 23, character 0-21 *)
Parameter z3 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 24, character 0-21 *)
Parameter x4 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 25, character 0-21 *)
Parameter y4 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 26, character 0-21 *)
Parameter z4 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 27, character 0-21 *)
Parameter x5 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 28, character 0-21 *)
Parameter y5 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 29, character 0-21 *)
Parameter z5 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 30, character 0-315 *)
Axiom hyp_1 : ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
/\ (~ (x0 = x5))).
(* Implicitly declared *)
Theorem implicit_goal : False.
Proof.
(* Prelude: Alias *)
pose ( and_elim :=
(fun (A B P: Prop) (o: (A /\ B)) (f: (A -> B -> P)) => (and_ind f o)) ).
(* Prelude: Alias *)
pose ( or_elim :=
(fun (A B P: Prop) (o: (A \/ B)) (f: (A -> P)) (g: (B -> P)) =>
(or_ind f g o)) ).
(* PROOF START *)
assert (L0: (~ ~ (z4 = x5) -> ~ ~ (x4 = z4) -> ~ ~ (y1 = x2)
-> ~ ~ (x1 = y1) -> ~ (x5 = x1) -> ~ ~ (x2 = x3)
-> ~ ~ (x3 = x4) -> False)).
{ intro E0.
intro E1.
intro E2.
intro E3.
intro E4.
intro E5.
intro E6.
apply E6.
intro E7.
apply E5.
intro E8.
apply E3.
intro E9.
apply E2.
intro E10.
apply E1.
intro E11.
apply E0.
intro E12.
apply (not_eq_sym E4).
exact (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans E8 E7))
(eq_trans E11 E12)). }
assert (L1: (~ (x0 = x5) -> ~ ~ (y0 = x1) -> ~ ~ (x0 = y0)
-> ~ ~ (x5 = x1) -> False)).
{ intro E0.
intro E1.
intro E2.
intro E3.
apply E3.
intro E4.
apply E2.
intro E5.
apply E1.
intro E6.
apply (not_eq_sym E0).
exact (eq_trans (eq_trans E4 (eq_sym E6)) (eq_sym E5)). }
assert (L2: (~ ~ ((((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
/\ (~ (x0 = x5))) -> ~ ~ (x0 = x5) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
(~ (x0 = x5)) False Ax2).
intro A0.
intro A1.
apply (and_elim ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
(((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))) False A0).
intro A2.
intro A3.
apply (and_elim (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
(((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))) False A2).
intro A4.
intro A5.
apply (and_elim ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
(((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))) False A4).
intro A6.
intro A7.
apply (and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6).
intro A8.
intro A9.
exact (Ax1 A1). }
assert (C0: ~ ~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
/\ (~ (x0 = x5)))).
{ intro Ax0.
exact (Ax0 hyp_1). }
(* Resolution L2/C0 -> R0 *)
pose proof ((fun (l0: ~ ~ (x0 = x5)) => (L2 C0 l0))) as R0.
(* Resolution L1/R0 -> R1 *)
pose proof (
(fun (l0: ~ ~ (y0 = x1)) (l1: ~ ~ (x0 = y0)) (l2: ~ ~ (x5 = x1)) =>
(L1 (fun (r0: (x0 = x5)) => (R0 (fun (r1: ~ (x0 = x5)) => (r1 r0))))
l0 l1 l2))
) as R1.
assert (L3: (~ ~ ((x0 = y0) /\ (y0 = x1)) -> ~ (y0 = x1) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x0 = y0) (y0 = x1) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution R1/L3 -> R2 *)
pose proof (
(fun (l0: ~ ~ ((x0 = y0) /\ (y0 = x1))) (l1: ~ ~ (x0 = y0)) (l2:
~ ~ (x5 = x1)) => (R1 (fun (r0: ~ (y0 = x1)) => (L3 l0 r0)) l1 l2))
) as R2.
assert (L4: (~ ~ ((x0 = y0) /\ (y0 = x1)) -> ~ (x0 = y0) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x0 = y0) (y0 = x1) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R2/L4 -> R3 *)
pose proof (
(fun (l0: ~ ~ ((x0 = y0) /\ (y0 = x1))) (l1: ~ ~ (x5 = x1)) =>
(R2 l0 (fun (r0: ~ (x0 = y0)) => (L4 l0 r0)) l1))
) as R3.
assert (L5: (~ ~ (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
-> ~ ((x0 = y0) /\ (y0 = x1)) -> ~ ((x0 = z0) /\ (z0 = x1)) ->
False)).
{ intro Ax0.
intro Ax1.
intro Ax2.
apply Ax0.
intro Ax3.
apply (or_elim ((x0 = y0) /\ (y0 = x1)) ((x0 = z0) /\ (z0 = x1)) False
Ax3).
- intro O0.
exact (Ax1 O0).
- intro O0.
exact (Ax2 O0). }
assert (L6: (~ ~ ((((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
/\ (~ (x0 = x5)))
-> ~ (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) ->
False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
(~ (x0 = x5)) False Ax2).
intro A0.
intro A1.
apply (and_elim ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
(((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))) False A0).
intro A2.
intro A3.
apply (and_elim (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
(((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))) False A2).
intro A4.
intro A5.
apply (and_elim ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
(((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))) False A4).
intro A6.
intro A7.
apply (and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6).
intro A8.
intro A9.
exact (Ax1 A8). }
(* Resolution L6/C0 -> R4 *)
pose proof (
(fun (l0: ~ (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))) =>
(L6 C0 l0))
) as R4.
(* Resolution L5/R4 -> R5 *)
pose proof (
(fun (l0: ~ ((x0 = y0) /\ (y0 = x1))) (l1: ~ ((x0 = z0) /\ (z0 = x1))) =>
(L5 R4 l0 l1))
) as R5.
(* Resolution R3/R5 -> R6 *)
pose proof (
(fun (l0: ~ ((x0 = z0) /\ (z0 = x1))) (l1: ~ ~ (x5 = x1)) =>
(R3 (fun (r0: ~ ((x0 = y0) /\ (y0 = x1))) => (R5 r0 l0)) l1))
) as R6.
assert (L7: (~ (x0 = x5) -> ~ ~ (z0 = x1) -> ~ ~ (x0 = z0)
-> ~ ~ (x5 = x1) -> False)).
{ intro E0.
intro E1.
intro E2.
intro E3.
apply E3.
intro E4.
apply E2.
intro E5.
apply E1.
intro E6.
apply (not_eq_sym E0).
exact (eq_trans (eq_trans E4 (eq_sym E6)) (eq_sym E5)). }
(* Resolution L7/R0 -> R7 *)
pose proof (
(fun (l0: ~ ~ (z0 = x1)) (l1: ~ ~ (x0 = z0)) (l2: ~ ~ (x5 = x1)) =>
(L7 (fun (r0: (x0 = x5)) => (R0 (fun (r1: ~ (x0 = x5)) => (r1 r0))))
l0 l1 l2))
) as R7.
assert (L8: (~ ~ ((x0 = z0) /\ (z0 = x1)) -> ~ (z0 = x1) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x0 = z0) (z0 = x1) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution R7/L8 -> R8 *)
pose proof (
(fun (l0: ~ ~ ((x0 = z0) /\ (z0 = x1))) (l1: ~ ~ (x0 = z0)) (l2:
~ ~ (x5 = x1)) => (R7 (fun (r0: ~ (z0 = x1)) => (L8 l0 r0)) l1 l2))
) as R8.
assert (L9: (~ ~ ((x0 = z0) /\ (z0 = x1)) -> ~ (x0 = z0) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x0 = z0) (z0 = x1) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R8/L9 -> R9 *)
pose proof (
(fun (l0: ~ ~ ((x0 = z0) /\ (z0 = x1))) (l1: ~ ~ (x5 = x1)) =>
(R8 l0 (fun (r0: ~ (x0 = z0)) => (L9 l0 r0)) l1))
) as R9.
(* Resolution R6/R9 -> R10 *)
pose proof (
(fun (l0: ~ ~ (x5 = x1)) =>
(R6 (fun (r0: ((x0 = z0) /\ (z0 = x1))) =>
(R9 (fun (r1: ~ ((x0 = z0) /\ (z0 = x1))) => (r1 r0)) l0))
l0))
) as R10.
(* Resolution L0/R10 -> R11 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) (l2: ~ ~ (y1 = x2)) (l3:
~ ~ (x1 = y1)) (l4: ~ ~ (x2 = x3)) (l5: ~ ~ (x3 = x4)) =>
(L0 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: ~ (x5 = x1)) => (r1 r0)))) l4
l5))
) as R11.
assert (L10: (~ ~ (z2 = x3) -> ~ ~ (x2 = z2) -> ~ (x2 = x3) -> False)).
{ intro E0.
intro E1.
intro E2.
apply E1.
intro E3.
apply E0.
intro E4.
apply E2.
exact (eq_trans E3 E4). }
assert (L11: (~ ~ ((x2 = z2) /\ (z2 = x3)) -> ~ (z2 = x3) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x2 = z2) (z2 = x3) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution L10/L11 -> R12 *)
pose proof (
(fun (l0: ~ ~ ((x2 = z2) /\ (z2 = x3))) (l1: ~ ~ (x2 = z2)) (l2:
~ (x2 = x3)) => (L10 (fun (r0: ~ (z2 = x3)) => (L11 l0 r0)) l1 l2))
) as R12.
assert (L12: (~ ~ ((x2 = z2) /\ (z2 = x3)) -> ~ (x2 = z2) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x2 = z2) (z2 = x3) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R12/L12 -> R13 *)
pose proof (
(fun (l0: ~ ~ ((x2 = z2) /\ (z2 = x3))) (l1: ~ (x2 = x3)) =>
(R12 l0 (fun (r0: ~ (x2 = z2)) => (L12 l0 r0)) l1))
) as R13.
assert (L13: (~ ~ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3)))
-> ~ ((x2 = y2) /\ (y2 = x3))
-> ~ ((x2 = z2) /\ (z2 = x3)) -> False)).
{ intro Ax0.
intro Ax1.
intro Ax2.
apply Ax0.
intro Ax3.
apply (or_elim ((x2 = y2) /\ (y2 = x3)) ((x2 = z2) /\ (z2 = x3)) False
Ax3).
- intro O0.
exact (Ax1 O0).
- intro O0.
exact (Ax2 O0). }
assert (L14: (~ ~ ((((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5)))) /\ (~ (x0 = x5)))
-> ~ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))) ->
False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
(~ (x0 = x5)) False Ax2).
intro A0.
intro A1.
apply (and_elim ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
(((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))) False A0).
intro A2.
intro A3.
apply (and_elim (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
(((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))) False A2).
intro A4.
intro A5.
apply (and_elim ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
(((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))) False A4).
intro A6.
intro A7.
apply (and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6).
intro A8.
intro A9.
exact (Ax1 A7). }
(* Resolution L14/C0 -> R14 *)
pose proof (
(fun (l0: ~ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3)))) =>
(L14 C0 l0))
) as R14.
(* Resolution L13/R14 -> R15 *)
pose proof (
(fun (l0: ~ ((x2 = y2) /\ (y2 = x3))) (l1: ~ ((x2 = z2) /\ (z2 = x3))) =>
(L13 R14 l0 l1))
) as R15.
(* Resolution R13/R15 -> R16 *)
pose proof (
(fun (l0: ~ ((x2 = y2) /\ (y2 = x3))) (l1: ~ (x2 = x3)) =>
(R13 (fun (r0: ~ ((x2 = z2) /\ (z2 = x3))) => (R15 l0 r0)) l1))
) as R16.
assert (L15: (~ ~ (y2 = x3) -> ~ ~ (x2 = y2) -> ~ (x2 = x3) -> False)).
{ intro E0.
intro E1.
intro E2.
apply E1.
intro E3.
apply E0.
intro E4.
apply E2.
exact (eq_trans E3 E4). }
assert (L16: (~ ~ ((x2 = y2) /\ (y2 = x3)) -> ~ (y2 = x3) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x2 = y2) (y2 = x3) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution L15/L16 -> R17 *)
pose proof (
(fun (l0: ~ ~ ((x2 = y2) /\ (y2 = x3))) (l1: ~ ~ (x2 = y2)) (l2:
~ (x2 = x3)) => (L15 (fun (r0: ~ (y2 = x3)) => (L16 l0 r0)) l1 l2))
) as R17.
assert (L17: (~ ~ ((x2 = y2) /\ (y2 = x3)) -> ~ (x2 = y2) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x2 = y2) (y2 = x3) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R17/L17 -> R18 *)
pose proof (
(fun (l0: ~ ~ ((x2 = y2) /\ (y2 = x3))) (l1: ~ (x2 = x3)) =>
(R17 l0 (fun (r0: ~ (x2 = y2)) => (L17 l0 r0)) l1))
) as R18.
(* Resolution R16/R18 -> R19 *)
pose proof (
(fun (l0: ~ (x2 = x3)) =>
(R16 (fun (r0: ((x2 = y2) /\ (y2 = x3))) =>
(R18 (fun (r1: ~ ((x2 = y2) /\ (y2 = x3))) => (r1 r0)) l0))
l0))
) as R19.
(* Resolution R11/R19 -> R20 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) (l2: ~ ~ (y1 = x2)) (l3:
~ ~ (x1 = y1)) (l4: ~ ~ (x3 = x4)) => (R11 l0 l1 l2 l3 R19 l4))
) as R20.
assert (L18: (~ ~ (z3 = x4) -> ~ ~ (x3 = z3) -> ~ (x3 = x4) -> False)).
{ intro E0.
intro E1.
intro E2.
apply E1.
intro E3.
apply E0.
intro E4.
apply (not_eq_sym E2).
exact (eq_trans (eq_sym E4) (eq_sym E3)). }
assert (L19: (~ ~ ((x3 = z3) /\ (z3 = x4)) -> ~ (z3 = x4) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x3 = z3) (z3 = x4) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution L18/L19 -> R21 *)
pose proof (
(fun (l0: ~ ~ ((x3 = z3) /\ (z3 = x4))) (l1: ~ ~ (x3 = z3)) (l2:
~ (x3 = x4)) => (L18 (fun (r0: ~ (z3 = x4)) => (L19 l0 r0)) l1 l2))
) as R21.
assert (L20: (~ ~ ((x3 = z3) /\ (z3 = x4)) -> ~ (x3 = z3) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x3 = z3) (z3 = x4) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R21/L20 -> R22 *)
pose proof (
(fun (l0: ~ ~ ((x3 = z3) /\ (z3 = x4))) (l1: ~ (x3 = x4)) =>
(R21 l0 (fun (r0: ~ (x3 = z3)) => (L20 l0 r0)) l1))
) as R22.
assert (L21: (~ ~ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4)))
-> ~ ((x3 = y3) /\ (y3 = x4))
-> ~ ((x3 = z3) /\ (z3 = x4)) -> False)).
{ intro Ax0.
intro Ax1.
intro Ax2.
apply Ax0.
intro Ax3.
apply (or_elim ((x3 = y3) /\ (y3 = x4)) ((x3 = z3) /\ (z3 = x4)) False
Ax3).
- intro O0.
exact (Ax1 O0).
- intro O0.
exact (Ax2 O0). }
assert (L22: (~ ~ ((((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5)))) /\ (~ (x0 = x5)))
-> ~ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))) ->
False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
(~ (x0 = x5)) False Ax2).
intro A0.
intro A1.
apply (and_elim ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
(((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))) False A0).
intro A2.
intro A3.
apply (and_elim (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
(((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))) False A2).
intro A4.
intro A5.
apply (and_elim ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
(((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))) False A4).
intro A6.
intro A7.
apply (and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6).
intro A8.
intro A9.
exact (Ax1 A5). }
(* Resolution L22/C0 -> R23 *)
pose proof (
(fun (l0: ~ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4)))) =>
(L22 C0 l0))
) as R23.
(* Resolution L21/R23 -> R24 *)
pose proof (
(fun (l0: ~ ((x3 = y3) /\ (y3 = x4))) (l1: ~ ((x3 = z3) /\ (z3 = x4))) =>
(L21 R23 l0 l1))
) as R24.
(* Resolution R22/R24 -> R25 *)
pose proof (
(fun (l0: ~ ((x3 = y3) /\ (y3 = x4))) (l1: ~ (x3 = x4)) =>
(R22 (fun (r0: ~ ((x3 = z3) /\ (z3 = x4))) => (R24 l0 r0)) l1))
) as R25.
assert (L23: (~ ~ (y3 = x4) -> ~ ~ (x3 = y3) -> ~ (x3 = x4) -> False)).
{ intro E0.
intro E1.
intro E2.
apply E1.
intro E3.
apply E0.
intro E4.
apply E2.
exact (eq_trans E3 E4). }
assert (L24: (~ ~ ((x3 = y3) /\ (y3 = x4)) -> ~ (y3 = x4) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x3 = y3) (y3 = x4) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution L23/L24 -> R26 *)
pose proof (
(fun (l0: ~ ~ ((x3 = y3) /\ (y3 = x4))) (l1: ~ ~ (x3 = y3)) (l2:
~ (x3 = x4)) => (L23 (fun (r0: ~ (y3 = x4)) => (L24 l0 r0)) l1 l2))
) as R26.
assert (L25: (~ ~ ((x3 = y3) /\ (y3 = x4)) -> ~ (x3 = y3) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x3 = y3) (y3 = x4) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R26/L25 -> R27 *)
pose proof (
(fun (l0: ~ ~ ((x3 = y3) /\ (y3 = x4))) (l1: ~ (x3 = x4)) =>
(R26 l0 (fun (r0: ~ (x3 = y3)) => (L25 l0 r0)) l1))
) as R27.
(* Resolution R25/R27 -> R28 *)
pose proof (
(fun (l0: ~ (x3 = x4)) =>
(R25 (fun (r0: ((x3 = y3) /\ (y3 = x4))) =>
(R27 (fun (r1: ~ ((x3 = y3) /\ (y3 = x4))) => (r1 r0)) l0))
l0))
) as R28.
(* Resolution R20/R28 -> R29 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) (l2: ~ ~ (y1 = x2)) (l3:
~ ~ (x1 = y1)) => (R20 l0 l1 l2 l3 R28))
) as R29.
assert (L26: (~ ~ ((x1 = y1) /\ (y1 = x2)) -> ~ (x1 = y1) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x1 = y1) (y1 = x2) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
assert (L27: (~ ~ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2)))
-> ~ ((x1 = y1) /\ (y1 = x2))
-> ~ ((x1 = z1) /\ (z1 = x2)) -> False)).
{ intro Ax0.
intro Ax1.
intro Ax2.
apply Ax0.
intro Ax3.
apply (or_elim ((x1 = y1) /\ (y1 = x2)) ((x1 = z1) /\ (z1 = x2)) False
Ax3).
- intro O0.
exact (Ax1 O0).
- intro O0.
exact (Ax2 O0). }
assert (L28: (~ ~ ((((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5)))) /\ (~ (x0 = x5)))
-> ~ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) ->
False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
(~ (x0 = x5)) False Ax2).
intro A0.
intro A1.
apply (and_elim ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
(((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))) False A0).
intro A2.
intro A3.
apply (and_elim (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
(((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))) False A2).
intro A4.
intro A5.
apply (and_elim ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
(((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))) False A4).
intro A6.
intro A7.
apply (and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6).
intro A8.
intro A9.
exact (Ax1 A9). }
(* Resolution L28/C0 -> R30 *)
pose proof (
(fun (l0: ~ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2)))) =>
(L28 C0 l0))
) as R30.
(* Resolution L27/R30 -> R31 *)
pose proof (
(fun (l0: ~ ((x1 = y1) /\ (y1 = x2))) (l1: ~ ((x1 = z1) /\ (z1 = x2))) =>
(L27 R30 l0 l1))
) as R31.
assert (L29: (~ ~ (z4 = x5) -> ~ ~ (x4 = z4) -> ~ ~ (z1 = x2)
-> ~ ~ (x1 = z1) -> ~ (x5 = x1) -> ~ ~ (x2 = x3)
-> ~ ~ (x3 = x4) -> False)).
{ intro E0.
intro E1.
intro E2.
intro E3.
intro E4.
intro E5.
intro E6.
apply E6.
intro E7.
apply E5.
intro E8.
apply E3.
intro E9.
apply E2.
intro E10.
apply E1.
intro E11.
apply E0.
intro E12.
apply (not_eq_sym E4).
exact (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans E8 E7))
(eq_trans E11 E12)). }
(* Resolution L29/R10 -> R32 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) (l2: ~ ~ (z1 = x2)) (l3:
~ ~ (x1 = z1)) (l4: ~ ~ (x2 = x3)) (l5: ~ ~ (x3 = x4)) =>
(L29 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: ~ (x5 = x1)) => (r1 r0)))) l4
l5))
) as R32.
(* Resolution R32/R19 -> R33 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) (l2: ~ ~ (z1 = x2)) (l3:
~ ~ (x1 = z1)) (l4: ~ ~ (x3 = x4)) => (R32 l0 l1 l2 l3 R19 l4))
) as R33.
(* Resolution R33/R28 -> R34 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) (l2: ~ ~ (z1 = x2)) (l3:
~ ~ (x1 = z1)) => (R33 l0 l1 l2 l3 R28))
) as R34.
assert (L30: (~ ~ ((x1 = z1) /\ (z1 = x2)) -> ~ (z1 = x2) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x1 = z1) (z1 = x2) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution R34/L30 -> R35 *)
pose proof (
(fun (l0: ~ ~ ((x1 = z1) /\ (z1 = x2))) (l1: ~ ~ (z4 = x5)) (l2:
~ ~ (x4 = z4)) (l3: ~ ~ (x1 = z1)) =>
(R34 l1 l2 (fun (r0: ~ (z1 = x2)) => (L30 l0 r0)) l3))
) as R35.
assert (L31: (~ ~ ((x1 = z1) /\ (z1 = x2)) -> ~ (x1 = z1) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x1 = z1) (z1 = x2) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R35/L31 -> R36 *)
pose proof (
(fun (l0: ~ ~ ((x1 = z1) /\ (z1 = x2))) (l1: ~ ~ (z4 = x5)) (l2:
~ ~ (x4 = z4)) =>
(R35 l0 l1 l2 (fun (r0: ~ (x1 = z1)) => (L31 l0 r0))))
) as R36.
assert (L32: (~ ~ ((x4 = z4) /\ (z4 = x5)) -> ~ (x4 = z4) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x4 = z4) (z4 = x5) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
assert (L33: (~ ~ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5)))
-> ~ ((x4 = y4) /\ (y4 = x5))
-> ~ ((x4 = z4) /\ (z4 = x5)) -> False)).
{ intro Ax0.
intro Ax1.
intro Ax2.
apply Ax0.
intro Ax3.
apply (or_elim ((x4 = y4) /\ (y4 = x5)) ((x4 = z4) /\ (z4 = x5)) False
Ax3).
- intro O0.
exact (Ax1 O0).
- intro O0.
exact (Ax2 O0). }
assert (L34: (~ ~ ((((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5)))) /\ (~ (x0 = x5)))
-> ~ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))) ->
False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (((((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
(~ (x0 = x5)) False Ax2).
intro A0.
intro A1.
apply (and_elim ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
(((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))) False A0).
intro A2.
intro A3.
apply (and_elim (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
(((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))) False A2).
intro A4.
intro A5.
apply (and_elim ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
(((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))) False A4).
intro A6.
intro A7.
apply (and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6).
intro A8.
intro A9.
exact (Ax1 A3). }
(* Resolution L34/C0 -> R37 *)
pose proof (
(fun (l0: ~ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5)))) =>
(L34 C0 l0))
) as R37.
(* Resolution L33/R37 -> R38 *)
pose proof (
(fun (l0: ~ ((x4 = y4) /\ (y4 = x5))) (l1: ~ ((x4 = z4) /\ (z4 = x5))) =>
(L33 R37 l0 l1))
) as R38.
assert (L35: (~ ~ (y4 = x5) -> ~ ~ (x4 = y4) -> ~ ~ (y1 = x2)
-> ~ ~ (x1 = y1) -> ~ (x5 = x1) -> ~ ~ (x2 = x3)
-> ~ ~ (x3 = x4) -> False)).
{ intro E0.
intro E1.
intro E2.
intro E3.
intro E4.
intro E5.
intro E6.
apply E6.
intro E7.
apply E5.
intro E8.
apply E3.
intro E9.
apply E2.
intro E10.
apply E1.
intro E11.
apply E0.
intro E12.
apply (not_eq_sym E4).
exact (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans E8 E7))
(eq_trans E11 E12)). }
(* Resolution L35/R10 -> R39 *)
pose proof (
(fun (l0: ~ ~ (y4 = x5)) (l1: ~ ~ (x4 = y4)) (l2: ~ ~ (y1 = x2)) (l3:
~ ~ (x1 = y1)) (l4: ~ ~ (x2 = x3)) (l5: ~ ~ (x3 = x4)) =>
(L35 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: ~ (x5 = x1)) => (r1 r0)))) l4
l5))
) as R39.
(* Resolution R39/R19 -> R40 *)
pose proof (
(fun (l0: ~ ~ (y4 = x5)) (l1: ~ ~ (x4 = y4)) (l2: ~ ~ (y1 = x2)) (l3:
~ ~ (x1 = y1)) (l4: ~ ~ (x3 = x4)) => (R39 l0 l1 l2 l3 R19 l4))
) as R40.
(* Resolution R40/R28 -> R41 *)
pose proof (
(fun (l0: ~ ~ (y4 = x5)) (l1: ~ ~ (x4 = y4)) (l2: ~ ~ (y1 = x2)) (l3:
~ ~ (x1 = y1)) => (R40 l0 l1 l2 l3 R28))
) as R41.
assert (L36: (~ ~ ((x1 = y1) /\ (y1 = x2)) -> ~ (y1 = x2) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x1 = y1) (y1 = x2) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution R41/L36 -> R42 *)
pose proof (
(fun (l0: ~ ~ ((x1 = y1) /\ (y1 = x2))) (l1: ~ ~ (y4 = x5)) (l2:
~ ~ (x4 = y4)) (l3: ~ ~ (x1 = y1)) =>
(R41 l1 l2 (fun (r0: ~ (y1 = x2)) => (L36 l0 r0)) l3))
) as R42.
(* Resolution R42/L26 -> R43 *)
pose proof (
(fun (l0: ~ ~ ((x1 = y1) /\ (y1 = x2))) (l1: ~ ~ (y4 = x5)) (l2:
~ ~ (x4 = y4)) =>
(R42 l0 l1 l2 (fun (r0: ~ (x1 = y1)) => (L26 l0 r0))))
) as R43.
(* Resolution R43/R31 -> R44 *)
pose proof (
(fun (l0: ~ ((x1 = z1) /\ (z1 = x2))) (l1: ~ ~ (y4 = x5)) (l2:
~ ~ (x4 = y4)) =>
(R43 (fun (r0: ~ ((x1 = y1) /\ (y1 = x2))) => (R31 r0 l0)) l1 l2))
) as R44.
assert (L37: (~ ~ (y4 = x5) -> ~ ~ (x4 = y4) -> ~ ~ (z1 = x2)
-> ~ ~ (x1 = z1) -> ~ (x5 = x1) -> ~ ~ (x2 = x3)
-> ~ ~ (x3 = x4) -> False)).
{ intro E0.
intro E1.
intro E2.
intro E3.
intro E4.
intro E5.
intro E6.
apply E6.
intro E7.
apply E5.
intro E8.
apply E3.
intro E9.
apply E2.
intro E10.
apply E1.
intro E11.
apply E0.
intro E12.
apply (not_eq_sym E4).
exact (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans E8 E7))
(eq_trans E11 E12)). }
(* Resolution L37/R10 -> R45 *)
pose proof (
(fun (l0: ~ ~ (y4 = x5)) (l1: ~ ~ (x4 = y4)) (l2: ~ ~ (z1 = x2)) (l3:
~ ~ (x1 = z1)) (l4: ~ ~ (x2 = x3)) (l5: ~ ~ (x3 = x4)) =>
(L37 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: ~ (x5 = x1)) => (r1 r0)))) l4
l5))
) as R45.
(* Resolution R45/R19 -> R46 *)
pose proof (
(fun (l0: ~ ~ (y4 = x5)) (l1: ~ ~ (x4 = y4)) (l2: ~ ~ (z1 = x2)) (l3:
~ ~ (x1 = z1)) (l4: ~ ~ (x3 = x4)) => (R45 l0 l1 l2 l3 R19 l4))
) as R46.
(* Resolution R46/R28 -> R47 *)
pose proof (
(fun (l0: ~ ~ (y4 = x5)) (l1: ~ ~ (x4 = y4)) (l2: ~ ~ (z1 = x2)) (l3:
~ ~ (x1 = z1)) => (R46 l0 l1 l2 l3 R28))
) as R47.
(* Resolution R47/L30 -> R48 *)
pose proof (
(fun (l0: ~ ~ ((x1 = z1) /\ (z1 = x2))) (l1: ~ ~ (y4 = x5)) (l2:
~ ~ (x4 = y4)) (l3: ~ ~ (x1 = z1)) =>
(R47 l1 l2 (fun (r0: ~ (z1 = x2)) => (L30 l0 r0)) l3))
) as R48.
(* Resolution R48/L31 -> R49 *)
pose proof (
(fun (l0: ~ ~ ((x1 = z1) /\ (z1 = x2))) (l1: ~ ~ (y4 = x5)) (l2:
~ ~ (x4 = y4)) =>
(R48 l0 l1 l2 (fun (r0: ~ (x1 = z1)) => (L31 l0 r0))))
) as R49.
(* Resolution R44/R49 -> R50 *)
pose proof (
(fun (l0: ~ ~ (y4 = x5)) (l1: ~ ~ (x4 = y4)) =>
(R44 (fun (r0: ((x1 = z1) /\ (z1 = x2))) =>
(R49 (fun (r1: ~ ((x1 = z1) /\ (z1 = x2))) => (r1 r0)) l0
l1)) l0 l1))
) as R50.
assert (L38: (~ ~ ((x4 = y4) /\ (y4 = x5)) -> ~ (y4 = x5) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x4 = y4) (y4 = x5) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution R50/L38 -> R51 *)
pose proof (
(fun (l0: ~ ~ ((x4 = y4) /\ (y4 = x5))) (l1: ~ ~ (x4 = y4)) =>
(R50 (fun (r0: ~ (y4 = x5)) => (L38 l0 r0)) l1))
) as R51.
assert (L39: (~ ~ ((x4 = y4) /\ (y4 = x5)) -> ~ (x4 = y4) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x4 = y4) (y4 = x5) False Ax2).
intro A0.
intro A1.
exact (Ax1 A0). }
(* Resolution R51/L39 -> R52 *)
pose proof (
(fun (l0: ~ ~ ((x4 = y4) /\ (y4 = x5))) =>
(R51 l0 (fun (r0: ~ (x4 = y4)) => (L39 l0 r0))))
) as R52.
(* Resolution R38/R52 -> R53 *)
pose proof (
(fun (l0: ~ ((x4 = z4) /\ (z4 = x5))) =>
(R38 (fun (r0: ((x4 = y4) /\ (y4 = x5))) =>
(R52 (fun (r1: ~ ((x4 = y4) /\ (y4 = x5))) => (r1 r0)))) l0))
) as R53.
(* Resolution L32/R53 -> R54 *)
pose proof ((fun (l0: ~ (x4 = z4)) => (L32 R53 l0))) as R54.
(* Resolution R36/R54 -> R55 *)
pose proof (
(fun (l0: ~ ~ ((x1 = z1) /\ (z1 = x2))) (l1: ~ ~ (z4 = x5)) =>
(R36 l0 l1 R54))
) as R55.
assert (L40: (~ ~ ((x4 = z4) /\ (z4 = x5)) -> ~ (z4 = x5) -> False)).
{ intro Ax0.
intro Ax1.
apply Ax0.
intro Ax2.
apply (and_elim (x4 = z4) (z4 = x5) False Ax2).
intro A0.
intro A1.
exact (Ax1 A1). }
(* Resolution L40/R53 -> R56 *)
pose proof ((fun (l0: ~ (z4 = x5)) => (L40 R53 l0))) as R56.
(* Resolution R55/R56 -> R57 *)
pose proof (
(fun (l0: ~ ~ ((x1 = z1) /\ (z1 = x2))) => (R55 l0 R56))
) as R57.
(* Resolution R31/R57 -> R58 *)
pose proof (
(fun (l0: ~ ((x1 = y1) /\ (y1 = x2))) =>
(R31 l0
(fun (r0: ((x1 = z1) /\ (z1 = x2))) =>
(R57 (fun (r1: ~ ((x1 = z1) /\ (z1 = x2))) => (r1 r0))))))
) as R58.
(* Resolution L26/R58 -> R59 *)
pose proof ((fun (l0: ~ (x1 = y1)) => (L26 R58 l0))) as R59.
(* Resolution R29/R59 -> R60 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) (l2: ~ ~ (y1 = x2)) =>
(R29 l0 l1 l2 R59))
) as R60.
(* Resolution L36/R58 -> R61 *)
pose proof ((fun (l0: ~ (y1 = x2)) => (L36 R58 l0))) as R61.
(* Resolution R60/R61 -> R62 *)
pose proof (
(fun (l0: ~ ~ (z4 = x5)) (l1: ~ ~ (x4 = z4)) => (R60 l0 l1 R61))
) as R62.
(* Resolution R62/R56 -> R63 *)
pose proof ((fun (l0: ~ ~ (x4 = z4)) => (R62 R56 l0))) as R63.
(* Resolution R63/R54 -> R64 *)
pose proof ((R63 R54)) as R64.
exact R64.
(* PROOF END *)
Qed.
Raw
term.v
(**
Proof automatically generated by Archsat
Input file: eq_diamond6.smt2
**)
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 11, character 0-18 *)
Parameter U : Type.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 12, character 0-21 *)
Parameter x0 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 13, character 0-21 *)
Parameter y0 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 14, character 0-21 *)
Parameter z0 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 15, character 0-21 *)
Parameter x1 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 16, character 0-21 *)
Parameter y1 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 17, character 0-21 *)
Parameter z1 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 18, character 0-21 *)
Parameter x2 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 19, character 0-21 *)
Parameter y2 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 20, character 0-21 *)
Parameter z2 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 21, character 0-21 *)
Parameter x3 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 22, character 0-21 *)
Parameter y3 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 23, character 0-21 *)
Parameter z3 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 24, character 0-21 *)
Parameter x4 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 25, character 0-21 *)
Parameter y4 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 26, character 0-21 *)
Parameter z4 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 27, character 0-21 *)
Parameter x5 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 28, character 0-21 *)
Parameter y5 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 29, character 0-21 *)
Parameter z5 : U.
(* File '/home/guigui/build/bench/smtlib/QF_UF/eq_diamond/eq_diamond6.smt2', line 30, character 0-315 *)
Axiom hyp_1 : ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))
/\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))
/\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))
/\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))
/\ (~ (x0 = x5))).
(* Prelude: Alias *)
Definition and_elim :
(forall (A B P: Prop), ((A /\ B) -> (A -> B -> P) -> P)) :=
(fun (A B P: Prop) (o: (A /\ B)) (f: (A -> B -> P)) => (and_ind f o)).
(* Prelude: Alias *)
Definition or_elim :
(forall (A B P: Prop), ((A \/ B) -> (A -> P) -> (B -> P) -> P)) :=
(fun (A B P: Prop) (o: (A \/ B)) (f: (A -> P)) (g: (B -> P)) =>
(or_ind f g o)).
(* Implicitly declared *)
Definition implicit_goal : False :=
(* PROOF START *)
let L0 := (fun (E0: (~ (~ (z4 = x5)))) (E1: (~ (~ (x4 = z4)))) (E2: (~ (~
(y1 = x2)))) (E3: (~ (~ (x1 = y1)))) (E4: (~ (x5 = x1)))
(E5: (~ (~ (x2 = x3)))) (E6: (~ (~ (x3 = x4)))) => (E6
(fun (E7: (x3 = x4)) => (E5 (fun (E8: (x2 = x3)) => (E3
(fun (E9: (x1 = y1)) => (E2 (fun (E10: (y1 = x2)) => (E1
(fun (E11: (x4 = z4)) => (E0 (fun (E12: (z4 = x5)) => (not_eq_sym
E4 (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans E8 E7))
(eq_trans E11 E12))))))))))))))))
in
let L1 := (fun (E0: (~ (x0 = x5))) (E1: (~ (~ (y0 = x1)))) (E2: (~ (~ (x0
= y0)))) (E3: (~ (~ (x5 = x1)))) => (E3
(fun (E4: (x5 = x1)) => (E2 (fun (E5: (x0 = y0)) => (E1
(fun (E6: (y0 = x1)) => (not_eq_sym E0 (eq_trans (eq_trans E4
(eq_sym E6)) (eq_sym E5))))))))))
in
let L2 := (fun (Ax0: (~ (~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0)
/\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) /\ (~ (x0 = x5)))))) (Ax1: (~ (~ (x0
= x5)))) => (Ax0
(fun (Ax2: ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) /\ (~ (x0 = x5)))) => (and_elim (((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5)))) (~ (x0 = x5)) False Ax2
(fun (A0: (((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5))))) (A1: (~ (x0 = x5))) => (and_elim ((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4)))) (((x4 = y4) /\ (y4 = x5)) \/ ((x4
= z4) /\ (z4 = x5))) False A0
(fun (A2: ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))))) (A3: (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) => (and_elim (((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))) False A2
(fun (A4: (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3))))) (A5: (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) => (and_elim ((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2)))) (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3))) False A4
(fun (A6: ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2)))))
(A7: (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3)))) =>
(and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6
(fun (A8: (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))))
(A9: (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2)))) =>
(Ax1 A1))))))))))))))
in
let C0 := (fun (Ax0: (~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) /\ (~ (x0 = x5))))) => (Ax0 hyp_1))
in
let R0 := (fun (l0: (~ (~ (x0 = x5)))) => (L2 C0 l0)) in
let R1 := (fun (l0: (~ (~ (y0 = x1)))) (l1: (~ (~ (x0 = y0)))) (l2: (~ (~
(x5 = x1)))) => (L1 (fun (r0: (x0 = x5)) => (R0
(fun (r1: (~ (x0 = x5))) => (r1 r0)))) l0 l1 l2))
in
let L3 := (fun (Ax0: (~ (~ ((x0 = y0) /\ (y0 = x1))))) (Ax1: (~ (y0 = x1))) =>
(Ax0 (fun (Ax2: ((x0 = y0) /\ (y0 = x1))) => (and_elim (x0 = y0)
(y0 = x1) False Ax2 (fun (A0: (x0 = y0)) (A1: (y0 = x1)) => (Ax1
A1))))))
in
let R2 := (fun (l0: (~ (~ ((x0 = y0) /\ (y0 = x1))))) (l1: (~ (~ (x0
= y0)))) (l2: (~ (~ (x5 = x1)))) => (R1
(fun (r0: (~ (y0 = x1))) => (L3 l0 r0)) l1 l2))
in
let L4 := (fun (Ax0: (~ (~ ((x0 = y0) /\ (y0 = x1))))) (Ax1: (~ (x0 = y0))) =>
(Ax0 (fun (Ax2: ((x0 = y0) /\ (y0 = x1))) => (and_elim (x0 = y0)
(y0 = x1) False Ax2 (fun (A0: (x0 = y0)) (A1: (y0 = x1)) => (Ax1
A0))))))
in
let R3 := (fun (l0: (~ (~ ((x0 = y0) /\ (y0 = x1))))) (l1: (~ (~ (x5
= x1)))) => (R2 l0 (fun (r0: (~ (x0 = y0))) => (L4 l0 r0))
l1))
in
let L5 := (fun (Ax0: (~ (~ (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1)))))) (Ax1: (~ ((x0 = y0) /\ (y0 = x1)))) (Ax2: (~ ((x0
= z0) /\ (z0 = x1)))) => (Ax0
(fun (Ax3: (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1)))) => (or_elim ((x0 = y0) /\ (y0 = x1)) ((x0 = z0)
/\ (z0 = x1)) False Ax3 (fun (O0: ((x0 = y0) /\ (y0 = x1))) =>
(Ax1 O0)) (fun (O0: ((x0 = z0) /\ (z0 = x1))) => (Ax2 O0))))))
in
let L6 := (fun (Ax0: (~ (~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0)
/\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) /\ (~ (x0 = x5)))))) (Ax1: (~ (((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))))) => (Ax0
(fun (Ax2: ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) /\ (~ (x0 = x5)))) => (and_elim (((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5)))) (~ (x0 = x5)) False Ax2
(fun (A0: (((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5))))) (A1: (~ (x0 = x5))) => (and_elim ((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4))
\/ ((x3 = z3) /\ (z3 = x4)))) (((x4 = y4) /\ (y4 = x5)) \/ ((x4
= z4) /\ (z4 = x5))) False A0
(fun (A2: ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))))) (A3: (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) => (and_elim (((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))) False A2
(fun (A4: (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3))))) (A5: (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) => (and_elim ((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2)))) (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3))) False A4
(fun (A6: ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
/\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2)))))
(A7: (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3)))) =>
(and_elim (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1)))
(((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))) False A6
(fun (A8: (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))))
(A9: (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2)))) =>
(Ax1 A8))))))))))))))
in
let R4 := (fun (l0: (~ (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))))) => (L6 C0 l0))
in
let R5 := (fun (l0: (~ ((x0 = y0) /\ (y0 = x1)))) (l1: (~ ((x0 = z0) /\ (z0
= x1)))) => (L5 R4 l0 l1))
in
let R6 := (fun (l0: (~ ((x0 = z0) /\ (z0 = x1)))) (l1: (~ (~ (x5 = x1)))) =>
(R3 (fun (r0: (~ ((x0 = y0) /\ (y0 = x1)))) => (R5 r0 l0)) l1))
in
let L7 := (fun (E0: (~ (x0 = x5))) (E1: (~ (~ (z0 = x1)))) (E2: (~ (~ (x0
= z0)))) (E3: (~ (~ (x5 = x1)))) => (E3
(fun (E4: (x5 = x1)) => (E2 (fun (E5: (x0 = z0)) => (E1
(fun (E6: (z0 = x1)) => (not_eq_sym E0 (eq_trans (eq_trans E4
(eq_sym E6)) (eq_sym E5))))))))))
in
let R7 := (fun (l0: (~ (~ (z0 = x1)))) (l1: (~ (~ (x0 = z0)))) (l2: (~ (~
(x5 = x1)))) => (L7 (fun (r0: (x0 = x5)) => (R0
(fun (r1: (~ (x0 = x5))) => (r1 r0)))) l0 l1 l2))
in
let L8 := (fun (Ax0: (~ (~ ((x0 = z0) /\ (z0 = x1))))) (Ax1: (~ (z0 = x1))) =>
(Ax0 (fun (Ax2: ((x0 = z0) /\ (z0 = x1))) => (and_elim (x0 = z0)
(z0 = x1) False Ax2 (fun (A0: (x0 = z0)) (A1: (z0 = x1)) => (Ax1
A1))))))
in
let R8 := (fun (l0: (~ (~ ((x0 = z0) /\ (z0 = x1))))) (l1: (~ (~ (x0
= z0)))) (l2: (~ (~ (x5 = x1)))) => (R7
(fun (r0: (~ (z0 = x1))) => (L8 l0 r0)) l1 l2))
in
let L9 := (fun (Ax0: (~ (~ ((x0 = z0) /\ (z0 = x1))))) (Ax1: (~ (x0 = z0))) =>
(Ax0 (fun (Ax2: ((x0 = z0) /\ (z0 = x1))) => (and_elim (x0 = z0)
(z0 = x1) False Ax2 (fun (A0: (x0 = z0)) (A1: (z0 = x1)) => (Ax1
A0))))))
in
let R9 := (fun (l0: (~ (~ ((x0 = z0) /\ (z0 = x1))))) (l1: (~ (~ (x5
= x1)))) => (R8 l0 (fun (r0: (~ (x0 = z0))) => (L9 l0 r0))
l1))
in
let R10 := (fun (l0: (~ (~ (x5 = x1)))) => (R6
(fun (r0: ((x0 = z0) /\ (z0 = x1))) => (R9
(fun (r1: (~ ((x0 = z0) /\ (z0 = x1)))) => (r1 r0)) l0)) l0))
in
let R11 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) (l2: (~ (~
(y1 = x2)))) (l3: (~ (~ (x1 = y1)))) (l4: (~ (~ (x2
= x3)))) (l5: (~ (~ (x3 = x4)))) => (L0 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: (~ (x5 = x1))) => (r1
r0)))) l4 l5))
in
let L10 := (fun (E0: (~ (~ (z2 = x3)))) (E1: (~ (~ (x2 = z2)))) (E2: (~ (x2
= x3))) => (E1 (fun (E3: (x2 = z2)) => (E0
(fun (E4: (z2 = x3)) => (E2 (eq_trans E3 E4)))))))
in
let L11 := (fun (Ax0: (~ (~ ((x2 = z2) /\ (z2 = x3))))) (Ax1: (~ (z2
= x3))) => (Ax0 (fun (Ax2: ((x2 = z2) /\ (z2 = x3))) =>
(and_elim (x2 = z2) (z2 = x3) False Ax2
(fun (A0: (x2 = z2)) (A1: (z2 = x3)) => (Ax1 A1))))))
in
let R12 := (fun (l0: (~ (~ ((x2 = z2) /\ (z2 = x3))))) (l1: (~ (~ (x2
= z2)))) (l2: (~ (x2 = x3))) => (L10
(fun (r0: (~ (z2 = x3))) => (L11 l0 r0)) l1 l2))
in
let L12 := (fun (Ax0: (~ (~ ((x2 = z2) /\ (z2 = x3))))) (Ax1: (~ (x2
= z2))) => (Ax0 (fun (Ax2: ((x2 = z2) /\ (z2 = x3))) =>
(and_elim (x2 = z2) (z2 = x3) False Ax2
(fun (A0: (x2 = z2)) (A1: (z2 = x3)) => (Ax1 A0))))))
in
let R13 := (fun (l0: (~ (~ ((x2 = z2) /\ (z2 = x3))))) (l1: (~ (x2 = x3))) =>
(R12 l0 (fun (r0: (~ (x2 = z2))) => (L12 l0 r0)) l1))
in
let L13 := (fun (Ax0: (~ (~ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))))) (Ax1: (~ ((x2 = y2) /\ (y2 = x3)))) (Ax2: (~
((x2 = z2) /\ (z2 = x3)))) => (Ax0
(fun (Ax3: (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) => (or_elim ((x2 = y2) /\ (y2 = x3)) ((x2 = z2)
/\ (z2 = x3)) False Ax3 (fun (O0: ((x2 = y2) /\ (y2 = x3))) =>
(Ax1 O0)) (fun (O0: ((x2 = z2) /\ (z2 = x3))) => (Ax2 O0))))))
in
let L14 := (fun (Ax0: (~ (~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0)
/\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) /\ (~ (x0 = x5)))))) (Ax1: (~ (((x2 = y2)
/\ (y2 = x3)) \/ ((x2 = z2) /\ (z2 = x3))))) => (Ax0
(fun (Ax2: ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) /\ (~ (x0 = x5)))) => (and_elim (((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4
= x5)) \/ ((x4 = z4) /\ (z4 = x5)))) (~ (x0 = x5)) False Ax2
(fun (A0: (((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5))))) (A1: (~ (x0 = x5))) => (and_elim ((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5))) False A0
(fun (A2: ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))))) (A3: (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) => (and_elim (((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) (((x3 = y3) /\ (y3 = x4)) \/ ((x3
= z3) /\ (z3 = x4))) False A2
(fun (A4: (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3))))) (A5: (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) => (and_elim ((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) (((x2 = y2) /\ (y2 = x3)) \/ ((x2
= z2) /\ (z2 = x3))) False A4
(fun (A6: ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2))))) (A7: (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) => (and_elim (((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2))) False A6
(fun (A8: (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1)))) (A9: (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) => (Ax1 A7))))))))))))))
in
let R14 := (fun (l0: (~ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3))))) => (L14 C0 l0))
in
let R15 := (fun (l0: (~ ((x2 = y2) /\ (y2 = x3)))) (l1: (~ ((x2 = z2)
/\ (z2 = x3)))) => (L13 R14 l0 l1))
in
let R16 := (fun (l0: (~ ((x2 = y2) /\ (y2 = x3)))) (l1: (~ (x2 = x3))) =>
(R13 (fun (r0: (~ ((x2 = z2) /\ (z2 = x3)))) => (R15 l0 r0))
l1))
in
let L15 := (fun (E0: (~ (~ (y2 = x3)))) (E1: (~ (~ (x2 = y2)))) (E2: (~ (x2
= x3))) => (E1 (fun (E3: (x2 = y2)) => (E0
(fun (E4: (y2 = x3)) => (E2 (eq_trans E3 E4)))))))
in
let L16 := (fun (Ax0: (~ (~ ((x2 = y2) /\ (y2 = x3))))) (Ax1: (~ (y2
= x3))) => (Ax0 (fun (Ax2: ((x2 = y2) /\ (y2 = x3))) =>
(and_elim (x2 = y2) (y2 = x3) False Ax2
(fun (A0: (x2 = y2)) (A1: (y2 = x3)) => (Ax1 A1))))))
in
let R17 := (fun (l0: (~ (~ ((x2 = y2) /\ (y2 = x3))))) (l1: (~ (~ (x2
= y2)))) (l2: (~ (x2 = x3))) => (L15
(fun (r0: (~ (y2 = x3))) => (L16 l0 r0)) l1 l2))
in
let L17 := (fun (Ax0: (~ (~ ((x2 = y2) /\ (y2 = x3))))) (Ax1: (~ (x2
= y2))) => (Ax0 (fun (Ax2: ((x2 = y2) /\ (y2 = x3))) =>
(and_elim (x2 = y2) (y2 = x3) False Ax2
(fun (A0: (x2 = y2)) (A1: (y2 = x3)) => (Ax1 A0))))))
in
let R18 := (fun (l0: (~ (~ ((x2 = y2) /\ (y2 = x3))))) (l1: (~ (x2 = x3))) =>
(R17 l0 (fun (r0: (~ (x2 = y2))) => (L17 l0 r0)) l1))
in
let R19 := (fun (l0: (~ (x2 = x3))) => (R16
(fun (r0: ((x2 = y2) /\ (y2 = x3))) => (R18
(fun (r1: (~ ((x2 = y2) /\ (y2 = x3)))) => (r1 r0)) l0)) l0))
in
let R20 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) (l2: (~ (~
(y1 = x2)))) (l3: (~ (~ (x1 = y1)))) (l4: (~ (~ (x3
= x4)))) => (R11 l0 l1 l2 l3 R19 l4))
in
let L18 := (fun (E0: (~ (~ (z3 = x4)))) (E1: (~ (~ (x3 = z3)))) (E2: (~ (x3
= x4))) => (E1 (fun (E3: (x3 = z3)) => (E0
(fun (E4: (z3 = x4)) => (not_eq_sym E2 (eq_trans (eq_sym E4)
(eq_sym E3))))))))
in
let L19 := (fun (Ax0: (~ (~ ((x3 = z3) /\ (z3 = x4))))) (Ax1: (~ (z3
= x4))) => (Ax0 (fun (Ax2: ((x3 = z3) /\ (z3 = x4))) =>
(and_elim (x3 = z3) (z3 = x4) False Ax2
(fun (A0: (x3 = z3)) (A1: (z3 = x4)) => (Ax1 A1))))))
in
let R21 := (fun (l0: (~ (~ ((x3 = z3) /\ (z3 = x4))))) (l1: (~ (~ (x3
= z3)))) (l2: (~ (x3 = x4))) => (L18
(fun (r0: (~ (z3 = x4))) => (L19 l0 r0)) l1 l2))
in
let L20 := (fun (Ax0: (~ (~ ((x3 = z3) /\ (z3 = x4))))) (Ax1: (~ (x3
= z3))) => (Ax0 (fun (Ax2: ((x3 = z3) /\ (z3 = x4))) =>
(and_elim (x3 = z3) (z3 = x4) False Ax2
(fun (A0: (x3 = z3)) (A1: (z3 = x4)) => (Ax1 A0))))))
in
let R22 := (fun (l0: (~ (~ ((x3 = z3) /\ (z3 = x4))))) (l1: (~ (x3 = x4))) =>
(R21 l0 (fun (r0: (~ (x3 = z3))) => (L20 l0 r0)) l1))
in
let L21 := (fun (Ax0: (~ (~ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))))) (Ax1: (~ ((x3 = y3) /\ (y3 = x4)))) (Ax2: (~
((x3 = z3) /\ (z3 = x4)))) => (Ax0
(fun (Ax3: (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) => (or_elim ((x3 = y3) /\ (y3 = x4)) ((x3 = z3)
/\ (z3 = x4)) False Ax3 (fun (O0: ((x3 = y3) /\ (y3 = x4))) =>
(Ax1 O0)) (fun (O0: ((x3 = z3) /\ (z3 = x4))) => (Ax2 O0))))))
in
let L22 := (fun (Ax0: (~ (~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0)
/\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) /\ (~ (x0 = x5)))))) (Ax1: (~ (((x3 = y3)
/\ (y3 = x4)) \/ ((x3 = z3) /\ (z3 = x4))))) => (Ax0
(fun (Ax2: ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) /\ (~ (x0 = x5)))) => (and_elim (((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4
= x5)) \/ ((x4 = z4) /\ (z4 = x5)))) (~ (x0 = x5)) False Ax2
(fun (A0: (((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5))))) (A1: (~ (x0 = x5))) => (and_elim ((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5))) False A0
(fun (A2: ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))))) (A3: (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) => (and_elim (((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) (((x3 = y3) /\ (y3 = x4)) \/ ((x3
= z3) /\ (z3 = x4))) False A2
(fun (A4: (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3))))) (A5: (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) => (and_elim ((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) (((x2 = y2) /\ (y2 = x3)) \/ ((x2
= z2) /\ (z2 = x3))) False A4
(fun (A6: ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2))))) (A7: (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) => (and_elim (((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2))) False A6
(fun (A8: (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1)))) (A9: (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) => (Ax1 A5))))))))))))))
in
let R23 := (fun (l0: (~ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))))) => (L22 C0 l0))
in
let R24 := (fun (l0: (~ ((x3 = y3) /\ (y3 = x4)))) (l1: (~ ((x3 = z3)
/\ (z3 = x4)))) => (L21 R23 l0 l1))
in
let R25 := (fun (l0: (~ ((x3 = y3) /\ (y3 = x4)))) (l1: (~ (x3 = x4))) =>
(R22 (fun (r0: (~ ((x3 = z3) /\ (z3 = x4)))) => (R24 l0 r0))
l1))
in
let L23 := (fun (E0: (~ (~ (y3 = x4)))) (E1: (~ (~ (x3 = y3)))) (E2: (~ (x3
= x4))) => (E1 (fun (E3: (x3 = y3)) => (E0
(fun (E4: (y3 = x4)) => (E2 (eq_trans E3 E4)))))))
in
let L24 := (fun (Ax0: (~ (~ ((x3 = y3) /\ (y3 = x4))))) (Ax1: (~ (y3
= x4))) => (Ax0 (fun (Ax2: ((x3 = y3) /\ (y3 = x4))) =>
(and_elim (x3 = y3) (y3 = x4) False Ax2
(fun (A0: (x3 = y3)) (A1: (y3 = x4)) => (Ax1 A1))))))
in
let R26 := (fun (l0: (~ (~ ((x3 = y3) /\ (y3 = x4))))) (l1: (~ (~ (x3
= y3)))) (l2: (~ (x3 = x4))) => (L23
(fun (r0: (~ (y3 = x4))) => (L24 l0 r0)) l1 l2))
in
let L25 := (fun (Ax0: (~ (~ ((x3 = y3) /\ (y3 = x4))))) (Ax1: (~ (x3
= y3))) => (Ax0 (fun (Ax2: ((x3 = y3) /\ (y3 = x4))) =>
(and_elim (x3 = y3) (y3 = x4) False Ax2
(fun (A0: (x3 = y3)) (A1: (y3 = x4)) => (Ax1 A0))))))
in
let R27 := (fun (l0: (~ (~ ((x3 = y3) /\ (y3 = x4))))) (l1: (~ (x3 = x4))) =>
(R26 l0 (fun (r0: (~ (x3 = y3))) => (L25 l0 r0)) l1))
in
let R28 := (fun (l0: (~ (x3 = x4))) => (R25
(fun (r0: ((x3 = y3) /\ (y3 = x4))) => (R27
(fun (r1: (~ ((x3 = y3) /\ (y3 = x4)))) => (r1 r0)) l0)) l0))
in
let R29 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) (l2: (~ (~
(y1 = x2)))) (l3: (~ (~ (x1 = y1)))) => (R20 l0 l1 l2 l3
R28))
in
let L26 := (fun (Ax0: (~ (~ ((x1 = y1) /\ (y1 = x2))))) (Ax1: (~ (x1
= y1))) => (Ax0 (fun (Ax2: ((x1 = y1) /\ (y1 = x2))) =>
(and_elim (x1 = y1) (y1 = x2) False Ax2
(fun (A0: (x1 = y1)) (A1: (y1 = x2)) => (Ax1 A0))))))
in
let L27 := (fun (Ax0: (~ (~ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))))) (Ax1: (~ ((x1 = y1) /\ (y1 = x2)))) (Ax2: (~
((x1 = z1) /\ (z1 = x2)))) => (Ax0
(fun (Ax3: (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) => (or_elim ((x1 = y1) /\ (y1 = x2)) ((x1 = z1)
/\ (z1 = x2)) False Ax3 (fun (O0: ((x1 = y1) /\ (y1 = x2))) =>
(Ax1 O0)) (fun (O0: ((x1 = z1) /\ (z1 = x2))) => (Ax2 O0))))))
in
let L28 := (fun (Ax0: (~ (~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0)
/\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) /\ (~ (x0 = x5)))))) (Ax1: (~ (((x1 = y1)
/\ (y1 = x2)) \/ ((x1 = z1) /\ (z1 = x2))))) => (Ax0
(fun (Ax2: ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) /\ (~ (x0 = x5)))) => (and_elim (((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4
= x5)) \/ ((x4 = z4) /\ (z4 = x5)))) (~ (x0 = x5)) False Ax2
(fun (A0: (((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5))))) (A1: (~ (x0 = x5))) => (and_elim ((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5))) False A0
(fun (A2: ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))))) (A3: (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) => (and_elim (((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) (((x3 = y3) /\ (y3 = x4)) \/ ((x3
= z3) /\ (z3 = x4))) False A2
(fun (A4: (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3))))) (A5: (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) => (and_elim ((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) (((x2 = y2) /\ (y2 = x3)) \/ ((x2
= z2) /\ (z2 = x3))) False A4
(fun (A6: ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2))))) (A7: (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) => (and_elim (((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2))) False A6
(fun (A8: (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1)))) (A9: (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) => (Ax1 A9))))))))))))))
in
let R30 := (fun (l0: (~ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2))))) => (L28 C0 l0))
in
let R31 := (fun (l0: (~ ((x1 = y1) /\ (y1 = x2)))) (l1: (~ ((x1 = z1)
/\ (z1 = x2)))) => (L27 R30 l0 l1))
in
let L29 := (fun (E0: (~ (~ (z4 = x5)))) (E1: (~ (~ (x4 = z4)))) (E2: (~ (~
(z1 = x2)))) (E3: (~ (~ (x1 = z1)))) (E4: (~ (x5 = x1)))
(E5: (~ (~ (x2 = x3)))) (E6: (~ (~ (x3 = x4)))) => (E6
(fun (E7: (x3 = x4)) => (E5 (fun (E8: (x2 = x3)) => (E3
(fun (E9: (x1 = z1)) => (E2 (fun (E10: (z1 = x2)) => (E1
(fun (E11: (x4 = z4)) => (E0 (fun (E12: (z4 = x5)) =>
(not_eq_sym E4 (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans
E8 E7)) (eq_trans E11 E12))))))))))))))))
in
let R32 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) (l2: (~ (~
(z1 = x2)))) (l3: (~ (~ (x1 = z1)))) (l4: (~ (~ (x2
= x3)))) (l5: (~ (~ (x3 = x4)))) => (L29 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: (~ (x5 = x1))) => (r1
r0)))) l4 l5))
in
let R33 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) (l2: (~ (~
(z1 = x2)))) (l3: (~ (~ (x1 = z1)))) (l4: (~ (~ (x3
= x4)))) => (R32 l0 l1 l2 l3 R19 l4))
in
let R34 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) (l2: (~ (~
(z1 = x2)))) (l3: (~ (~ (x1 = z1)))) => (R33 l0 l1 l2 l3
R28))
in
let L30 := (fun (Ax0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) (Ax1: (~ (z1
= x2))) => (Ax0 (fun (Ax2: ((x1 = z1) /\ (z1 = x2))) =>
(and_elim (x1 = z1) (z1 = x2) False Ax2
(fun (A0: (x1 = z1)) (A1: (z1 = x2)) => (Ax1 A1))))))
in
let R35 := (fun (l0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) (l1: (~ (~ (z4
= x5)))) (l2: (~ (~ (x4 = z4)))) (l3: (~ (~ (x1 = z1)))) =>
(R34 l1 l2 (fun (r0: (~ (z1 = x2))) => (L30 l0 r0)) l3))
in
let L31 := (fun (Ax0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) (Ax1: (~ (x1
= z1))) => (Ax0 (fun (Ax2: ((x1 = z1) /\ (z1 = x2))) =>
(and_elim (x1 = z1) (z1 = x2) False Ax2
(fun (A0: (x1 = z1)) (A1: (z1 = x2)) => (Ax1 A0))))))
in
let R36 := (fun (l0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) (l1: (~ (~ (z4
= x5)))) (l2: (~ (~ (x4 = z4)))) => (R35 l0 l1 l2
(fun (r0: (~ (x1 = z1))) => (L31 l0 r0))))
in
let L32 := (fun (Ax0: (~ (~ ((x4 = z4) /\ (z4 = x5))))) (Ax1: (~ (x4
= z4))) => (Ax0 (fun (Ax2: ((x4 = z4) /\ (z4 = x5))) =>
(and_elim (x4 = z4) (z4 = x5) False Ax2
(fun (A0: (x4 = z4)) (A1: (z4 = x5)) => (Ax1 A0))))))
in
let L33 := (fun (Ax0: (~ (~ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))))) (Ax1: (~ ((x4 = y4) /\ (y4 = x5)))) (Ax2: (~
((x4 = z4) /\ (z4 = x5)))) => (Ax0
(fun (Ax3: (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) => (or_elim ((x4 = y4) /\ (y4 = x5)) ((x4 = z4)
/\ (z4 = x5)) False Ax3 (fun (O0: ((x4 = y4) /\ (y4 = x5))) =>
(Ax1 O0)) (fun (O0: ((x4 = z4) /\ (z4 = x5))) => (Ax2 O0))))))
in
let L34 := (fun (Ax0: (~ (~ ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0)
/\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) /\ (~ (x0 = x5)))))) (Ax1: (~ (((x4 = y4)
/\ (y4 = x5)) \/ ((x4 = z4) /\ (z4 = x5))))) => (Ax0
(fun (Ax2: ((((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5)))) /\ (~ (x0 = x5)))) => (and_elim (((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) /\ (((x4 = y4) /\ (y4
= x5)) \/ ((x4 = z4) /\ (z4 = x5)))) (~ (x0 = x5)) False Ax2
(fun (A0: (((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4)))) /\ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5))))) (A1: (~ (x0 = x5))) => (and_elim ((((((x0 = y0)
/\ (y0 = x1)) \/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1
= x2)) \/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2
= x3)) \/ ((x2 = z2) /\ (z2 = x3)))) /\ (((x3 = y3) /\ (y3
= x4)) \/ ((x3 = z3) /\ (z3 = x4)))) (((x4 = y4) /\ (y4 = x5))
\/ ((x4 = z4) /\ (z4 = x5))) False A0
(fun (A2: ((((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3)))) /\ (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3) /\ (z3
= x4))))) (A3: (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4)
/\ (z4 = x5)))) => (and_elim (((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) /\ (((x2 = y2) /\ (y2 = x3))
\/ ((x2 = z2) /\ (z2 = x3)))) (((x3 = y3) /\ (y3 = x4)) \/ ((x3
= z3) /\ (z3 = x4))) False A2
(fun (A4: (((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2)))) /\ (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2) /\ (z2
= x3))))) (A5: (((x3 = y3) /\ (y3 = x4)) \/ ((x3 = z3)
/\ (z3 = x4)))) => (and_elim ((((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) /\ (((x1 = y1) /\ (y1 = x2))
\/ ((x1 = z1) /\ (z1 = x2)))) (((x2 = y2) /\ (y2 = x3)) \/ ((x2
= z2) /\ (z2 = x3))) False A4
(fun (A6: ((((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1))) /\ (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1) /\ (z1
= x2))))) (A7: (((x2 = y2) /\ (y2 = x3)) \/ ((x2 = z2)
/\ (z2 = x3)))) => (and_elim (((x0 = y0) /\ (y0 = x1))
\/ ((x0 = z0) /\ (z0 = x1))) (((x1 = y1) /\ (y1 = x2)) \/ ((x1
= z1) /\ (z1 = x2))) False A6
(fun (A8: (((x0 = y0) /\ (y0 = x1)) \/ ((x0 = z0) /\ (z0
= x1)))) (A9: (((x1 = y1) /\ (y1 = x2)) \/ ((x1 = z1)
/\ (z1 = x2)))) => (Ax1 A3))))))))))))))
in
let R37 := (fun (l0: (~ (((x4 = y4) /\ (y4 = x5)) \/ ((x4 = z4) /\ (z4
= x5))))) => (L34 C0 l0))
in
let R38 := (fun (l0: (~ ((x4 = y4) /\ (y4 = x5)))) (l1: (~ ((x4 = z4)
/\ (z4 = x5)))) => (L33 R37 l0 l1))
in
let L35 := (fun (E0: (~ (~ (y4 = x5)))) (E1: (~ (~ (x4 = y4)))) (E2: (~ (~
(y1 = x2)))) (E3: (~ (~ (x1 = y1)))) (E4: (~ (x5 = x1)))
(E5: (~ (~ (x2 = x3)))) (E6: (~ (~ (x3 = x4)))) => (E6
(fun (E7: (x3 = x4)) => (E5 (fun (E8: (x2 = x3)) => (E3
(fun (E9: (x1 = y1)) => (E2 (fun (E10: (y1 = x2)) => (E1
(fun (E11: (x4 = y4)) => (E0 (fun (E12: (y4 = x5)) =>
(not_eq_sym E4 (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans
E8 E7)) (eq_trans E11 E12))))))))))))))))
in
let R39 := (fun (l0: (~ (~ (y4 = x5)))) (l1: (~ (~ (x4 = y4)))) (l2: (~ (~
(y1 = x2)))) (l3: (~ (~ (x1 = y1)))) (l4: (~ (~ (x2
= x3)))) (l5: (~ (~ (x3 = x4)))) => (L35 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: (~ (x5 = x1))) => (r1
r0)))) l4 l5))
in
let R40 := (fun (l0: (~ (~ (y4 = x5)))) (l1: (~ (~ (x4 = y4)))) (l2: (~ (~
(y1 = x2)))) (l3: (~ (~ (x1 = y1)))) (l4: (~ (~ (x3
= x4)))) => (R39 l0 l1 l2 l3 R19 l4))
in
let R41 := (fun (l0: (~ (~ (y4 = x5)))) (l1: (~ (~ (x4 = y4)))) (l2: (~ (~
(y1 = x2)))) (l3: (~ (~ (x1 = y1)))) => (R40 l0 l1 l2 l3
R28))
in
let L36 := (fun (Ax0: (~ (~ ((x1 = y1) /\ (y1 = x2))))) (Ax1: (~ (y1
= x2))) => (Ax0 (fun (Ax2: ((x1 = y1) /\ (y1 = x2))) =>
(and_elim (x1 = y1) (y1 = x2) False Ax2
(fun (A0: (x1 = y1)) (A1: (y1 = x2)) => (Ax1 A1))))))
in
let R42 := (fun (l0: (~ (~ ((x1 = y1) /\ (y1 = x2))))) (l1: (~ (~ (y4
= x5)))) (l2: (~ (~ (x4 = y4)))) (l3: (~ (~ (x1 = y1)))) =>
(R41 l1 l2 (fun (r0: (~ (y1 = x2))) => (L36 l0 r0)) l3))
in
let R43 := (fun (l0: (~ (~ ((x1 = y1) /\ (y1 = x2))))) (l1: (~ (~ (y4
= x5)))) (l2: (~ (~ (x4 = y4)))) => (R42 l0 l1 l2
(fun (r0: (~ (x1 = y1))) => (L26 l0 r0))))
in
let R44 := (fun (l0: (~ ((x1 = z1) /\ (z1 = x2)))) (l1: (~ (~ (y4 = x5))))
(l2: (~ (~ (x4 = y4)))) => (R43
(fun (r0: (~ ((x1 = y1) /\ (y1 = x2)))) => (R31 r0 l0)) l1 l2))
in
let L37 := (fun (E0: (~ (~ (y4 = x5)))) (E1: (~ (~ (x4 = y4)))) (E2: (~ (~
(z1 = x2)))) (E3: (~ (~ (x1 = z1)))) (E4: (~ (x5 = x1)))
(E5: (~ (~ (x2 = x3)))) (E6: (~ (~ (x3 = x4)))) => (E6
(fun (E7: (x3 = x4)) => (E5 (fun (E8: (x2 = x3)) => (E3
(fun (E9: (x1 = z1)) => (E2 (fun (E10: (z1 = x2)) => (E1
(fun (E11: (x4 = y4)) => (E0 (fun (E12: (y4 = x5)) =>
(not_eq_sym E4 (eq_trans (eq_trans (eq_trans E9 E10) (eq_trans
E8 E7)) (eq_trans E11 E12))))))))))))))))
in
let R45 := (fun (l0: (~ (~ (y4 = x5)))) (l1: (~ (~ (x4 = y4)))) (l2: (~ (~
(z1 = x2)))) (l3: (~ (~ (x1 = z1)))) (l4: (~ (~ (x2
= x3)))) (l5: (~ (~ (x3 = x4)))) => (L37 l0 l1 l2 l3
(fun (r0: (x5 = x1)) => (R10 (fun (r1: (~ (x5 = x1))) => (r1
r0)))) l4 l5))
in
let R46 := (fun (l0: (~ (~ (y4 = x5)))) (l1: (~ (~ (x4 = y4)))) (l2: (~ (~
(z1 = x2)))) (l3: (~ (~ (x1 = z1)))) (l4: (~ (~ (x3
= x4)))) => (R45 l0 l1 l2 l3 R19 l4))
in
let R47 := (fun (l0: (~ (~ (y4 = x5)))) (l1: (~ (~ (x4 = y4)))) (l2: (~ (~
(z1 = x2)))) (l3: (~ (~ (x1 = z1)))) => (R46 l0 l1 l2 l3
R28))
in
let R48 := (fun (l0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) (l1: (~ (~ (y4
= x5)))) (l2: (~ (~ (x4 = y4)))) (l3: (~ (~ (x1 = z1)))) =>
(R47 l1 l2 (fun (r0: (~ (z1 = x2))) => (L30 l0 r0)) l3))
in
let R49 := (fun (l0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) (l1: (~ (~ (y4
= x5)))) (l2: (~ (~ (x4 = y4)))) => (R48 l0 l1 l2
(fun (r0: (~ (x1 = z1))) => (L31 l0 r0))))
in
let R50 := (fun (l0: (~ (~ (y4 = x5)))) (l1: (~ (~ (x4 = y4)))) => (R44
(fun (r0: ((x1 = z1) /\ (z1 = x2))) => (R49
(fun (r1: (~ ((x1 = z1) /\ (z1 = x2)))) => (r1 r0)) l0 l1)) l0
l1))
in
let L38 := (fun (Ax0: (~ (~ ((x4 = y4) /\ (y4 = x5))))) (Ax1: (~ (y4
= x5))) => (Ax0 (fun (Ax2: ((x4 = y4) /\ (y4 = x5))) =>
(and_elim (x4 = y4) (y4 = x5) False Ax2
(fun (A0: (x4 = y4)) (A1: (y4 = x5)) => (Ax1 A1))))))
in
let R51 := (fun (l0: (~ (~ ((x4 = y4) /\ (y4 = x5))))) (l1: (~ (~ (x4
= y4)))) => (R50 (fun (r0: (~ (y4 = x5))) => (L38 l0 r0))
l1))
in
let L39 := (fun (Ax0: (~ (~ ((x4 = y4) /\ (y4 = x5))))) (Ax1: (~ (x4
= y4))) => (Ax0 (fun (Ax2: ((x4 = y4) /\ (y4 = x5))) =>
(and_elim (x4 = y4) (y4 = x5) False Ax2
(fun (A0: (x4 = y4)) (A1: (y4 = x5)) => (Ax1 A0))))))
in
let R52 := (fun (l0: (~ (~ ((x4 = y4) /\ (y4 = x5))))) => (R51 l0
(fun (r0: (~ (x4 = y4))) => (L39 l0 r0))))
in
let R53 := (fun (l0: (~ ((x4 = z4) /\ (z4 = x5)))) => (R38
(fun (r0: ((x4 = y4) /\ (y4 = x5))) => (R52
(fun (r1: (~ ((x4 = y4) /\ (y4 = x5)))) => (r1 r0)))) l0))
in
let R54 := (fun (l0: (~ (x4 = z4))) => (L32 R53 l0)) in
let R55 := (fun (l0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) (l1: (~ (~ (z4
= x5)))) => (R36 l0 l1 R54))
in
let L40 := (fun (Ax0: (~ (~ ((x4 = z4) /\ (z4 = x5))))) (Ax1: (~ (z4
= x5))) => (Ax0 (fun (Ax2: ((x4 = z4) /\ (z4 = x5))) =>
(and_elim (x4 = z4) (z4 = x5) False Ax2
(fun (A0: (x4 = z4)) (A1: (z4 = x5)) => (Ax1 A1))))))
in
let R56 := (fun (l0: (~ (z4 = x5))) => (L40 R53 l0)) in
let R57 := (fun (l0: (~ (~ ((x1 = z1) /\ (z1 = x2))))) => (R55 l0 R56)) in
let R58 := (fun (l0: (~ ((x1 = y1) /\ (y1 = x2)))) => (R31 l0
(fun (r0: ((x1 = z1) /\ (z1 = x2))) => (R57
(fun (r1: (~ ((x1 = z1) /\ (z1 = x2)))) => (r1 r0))))))
in
let R59 := (fun (l0: (~ (x1 = y1))) => (L26 R58 l0)) in
let R60 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) (l2: (~ (~
(y1 = x2)))) => (R29 l0 l1 l2 R59))
in
let R61 := (fun (l0: (~ (y1 = x2))) => (L36 R58 l0)) in
let R62 := (fun (l0: (~ (~ (z4 = x5)))) (l1: (~ (~ (x4 = z4)))) => (R60 l0
l1 R61))
in
let R63 := (fun (l0: (~ (~ (x4 = z4)))) => (R62 R56 l0)) in
let R64 := (R63 R54) in
R64
(* PROOF END *).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment