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.
Let x13 of type ι be given.
Assume H14: x13x0.
Let x14 of type ι be given.
Assume H15: x14x0.
Apply setminusE with x1, Sing x3, x4, f7297.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14∀ x15 : ο . (not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)not (x2 x13 x3)x2 x14 x3x15)(not (x2 x4 x3)x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)not (x2 x13 x3)x2 x14 x3x15)(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)not (x2 x13 x3)x2 x14 x3x15)x15 leaving 2 subgoals.
Apply H4 with x4.
The subproof is completed by applying H5.
Assume H16: x4x1.
Assume H17: nIn x4 (Sing x3).
Apply setminusE with x1, Sing x3, x5, ...∀ x15 : ο . ......(............not (x2 x8 ...)not (x2 x9 x3)x2 x10 x3x2 x11 x3not (x2 x12 x3)not (x2 x13 x3)x2 x14 x3x15)x15 leaving 2 subgoals.
...
...