Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ιιι be given.
Assume H0: ∀ x2 . In x2 x0∀ x3 . In x3 x0In (x1 x2 x3) x0.
Let x2 of type ιιιι be given.
Assume H1: ∀ x3 . In x3 x0∀ x4 . In x4 x0∀ x5 . In x5 x0In (x2 x3 x4 x5) x0.
Let x3 of type ι be given.
Assume H2: In x3 x0.
Let x4 of type ι be given.
Assume H3: In x4 x0.
Let x5 of type ιιι be given.
Assume H4: ∀ x6 . In x6 x0∀ x7 . In x7 x0In (x5 x6 x7) x0.
Let x6 of type ιιι be given.
Assume H5: ∀ x7 . In x7 x0∀ x8 . In x8 x0In (x6 x7 x8) x0.
Let x7 of type ι be given.
Assume H6: In x7 x0.
Let x8 of type ιιι be given.
Assume H7: ∀ x9 . In x9 x0∀ x10 . In x10 x0In (x8 x9 x10) x0.
Assume H8: ∀ x9 . In x9 x0(x8 x7 x9 = x9False)False.
Assume H9: ∀ x9 . In x9 x0∀ x10 . In x10 x0(x1 x9 (x8 x9 x10) = x10False)False.
Assume H10: ∀ x9 . In x9 x0∀ x10 . In x10 x0(x6 x9 x10 = x8 (x1 x9 x10) (x1 (x1 x9 x7) x7)False)False.
Assume H11: ∀ x9 . In x9 x0(x1 x9 x9 = x7False)False.
Assume H12: ∀ x9 . In x9 x0(x5 x7 x9 = x9False)False.
Assume H13: ∀ x9 . In x9 x0∀ x10 . In x10 x0(x2 x7 x9 x10 = x10False)False.
Assume H14: ∀ x9 . In x9 x0∀ x10 . In x10 x0(x2 x9 x7 x10 = x10False)False.
Assume H15: ∀ x9 . ...∀ x10 . ...∀ x11 . ...∀ x12 . In ... ...(x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 (x2 x9 x11 (x6 x10 x12))))))))))))))))))) = x12False)False.
...