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: x0 x2.
Assume H2: x0 x3.
Assume H3: x0 x4.
Assume H4: x0 x5.
Assume H5: x0 x6.
Assume H6: x0 x7.
Assume H7: x1 x2.
Assume H8: x1 x3.
Assume H9: x1 x4.
Assume H10: x1 x5.
Let x8 of type ιι be given.
Let x9 of type ιι be given.
Let x10 of type ιι be given.
Assume H11: x8 x2 = x3.
Assume H12: x8 x3 = x2.
Assume H13: x8 x4 = x5.
Assume H14: x8 x5 = x4.
Assume H15: x9 x2 = x4.
Assume H16: x9 x3 = x5.
Assume H17: x9 x4 = x2.
Assume H18: x9 x5 = x3.
Assume H19: x10 x2 = x5.
Assume H20: x10 x3 = x4.
Assume H21: x10 x4 = x3.
Assume H22: x10 x5 = x2.
Let x11 of type ιιιιο be given.
Assume H23: ∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x12 x13).
Assume H24: ∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15x11 x14 x15 x12 x13.
Assume H25: ∀ x12 x13 . x0 x12x0 x13not (x11 x12 x13 x7 x7).
Assume H26: ∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x8 x13) x14 (x8 x15)).
Assume H27: ∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x9 x13) x14 (x9 x15)).
Assume H28: ∀ x12 x13 x14 x15 . x0 x12x1 x13x0 x14x1 x15not (x11 x12 x13 x14 x15)not (x11 x12 (x10 x13) x14 (x10 x15)).
Assume H29: ∀ x12 . x0 x12not (x11 x4 x6 x5 x12).
Assume H30: ∀ x12 . x0 x12not (x11 x4 x6 x7 x12).
Assume H31: ∀ x12 . x0 x12not (x11 x5 x6 x6 x12).
Assume H32: ∀ x12 . x0 x12not (x11 x5 x7 x6 x12).
Assume H33: ∀ x12 . x0 x12not (x11 x6 x6 x4 x12).
...