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.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Assume H0: ∀ x8 : ι → ο . x8 x2x8 x3x8 x4x8 x5x8 x6x8 x7∀ x9 . x0 x9x8 x9.
Assume H1: ∀ x8 . x0 x8not (x1 x8)∀ x9 : ι → ο . x9 x6x9 x7x9 x8.
Assume H2: x0 x2.
Assume H3: x0 x3.
Assume H4: x0 x4.
Assume H5: x0 x5.
Assume H6: x0 x6.
Assume H7: x0 x7.
Let x8 of type ιιιιο be given.
Assume H8: ∀ x9 . x0 x9∀ x10 . x0 x10not (x8 x9 x7 x10 x6).
Assume H9: ∀ x9 . x0 x9not (x8 x2 x9 x2 x9).
Assume H10: ∀ x9 . x0 x9not (x8 x3 x9 x2 x9).
Assume H11: ∀ x9 . x0 x9not (x8 x4 x9 x2 x9).
Assume H12: ∀ x9 . x0 x9not (x8 x5 x9 x2 x9).
Assume H13: ∀ x9 . x0 x9not (x8 x6 x9 x2 x9).
Assume H14: ∀ x9 . x0 x9not (x8 x7 x9 x2 x9).
Assume H15: ∀ x9 . x0 x9not (x8 x3 x9 x3 x9).
Assume H16: ∀ x9 . x0 x9not (x8 x4 x9 x3 x9).
Assume H17: ∀ x9 . x0 x9not (x8 x5 x9 x3 x9).
Assume H18: ∀ x9 . x0 x9not (x8 x6 x9 x3 x9).
Assume H19: ∀ x9 . x0 x9not (x8 x7 x9 x3 x9).
Assume H20: ∀ x9 . x0 x9not (x8 x4 x9 x4 x9).
Assume H21: ∀ x9 . x0 x9not (x8 x5 x9 x4 x9).
Assume H22: ∀ x9 . x0 x9not (x8 x6 x9 x4 x9).
Assume H23: ∀ x9 . x0 x9not (x8 x7 x9 x4 x9).
Assume H24: ∀ x9 . x0 x9not (x8 x5 x9 x5 x9).
Assume H25: ∀ x9 . x0 x9not (x8 x6 x9 x5 x9).
Assume H26: ∀ x9 . x0 x9not (x8 x7 x9 x5 x9).
Assume H27: ∀ x9 . x0 x9not (x8 x6 x9 x6 x9).
Assume H28: ∀ x9 . ...not (x8 x7 x9 x6 ...).
...