Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ιιο be given.
Assume H0: ∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3.
Assume H1: 4402e.. x1 x2.
Assume H2: cf2df.. x1 x2.
Let x3 of type ι be given.
Assume H3: x3x1.
Assume H4: x0setminus x1 (Sing x3).
Let x4 of type ι be given.
Assume H5: x4x0.
Let x5 of type ι be given.
Assume H6: x5x0.
Let x6 of type ι be given.
Assume H7: x6x0.
Let x7 of type ι be given.
Assume H8: x7x0.
Let x8 of type ι be given.
Assume H9: x8x0.
Let x9 of type ι be given.
Assume H10: x9x0.
Let x10 of type ι be given.
Assume H11: x10x0.
Let x11 of type ι be given.
Assume H12: x11x0.
Let x12 of type ι be given.
Assume H13: x12x0.
Apply setminusE with x1, Sing x3, x4, ...∀ x13 : ο . ..................(............x2 ... ...x2 x9 x3not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)x13)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3x2 x11 x3not (x2 x12 x3)x13)(not (x2 x4 x3)not (x2 x5 x3)x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3x2 x11 x3not (x2 x12 x3)x13)(not (x2 x4 x3)x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3x2 x11 x3not (x2 x12 x3)x13)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)x2 x10 x3x2 x11 x3not (x2 x12 x3)x13)(not (x2 x4 x3)not (x2 x5 x3)x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3x2 x10 x3x2 x11 x3not (x2 x12 x3)x13)x13 leaving 2 subgoals.
...
...