Search for blocks/addresses/...

Proofgold Proof

pf
Claim L0: ...
...
Claim L1: ...
...
Claim L2: ...
...
Claim L3: ...
...
Claim L4: ...
...
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.
Let x8 of type ι → ι → ι be given.
Let x9 of type ι → ι be given.
Let x10 of type ι → ι → ι be given.
Let x11 of type ι → ι → ο be given.
Let x12 of type ι → ι → ο be given.
Let x13 of type ι be given.
Assume H5: ∀ x14 x15 x16 . x12 x16 x13 ⟶ x12 x14 x13 ⟶ x12 x15 x13 ⟶ x11 x16 x14 ⟶ x11 x14 x15 ⟶ (x11 x16 x15 ⟶ False) ⟶ False.
Assume H6: ∀ x14 x15 x16 . x12 x16 x13 ⟶ x12 x14 x13 ⟶ x12 x15 x13 ⟶ x16 = x0 x14 x15 ⟶ (x11 x15 x16 ⟶ False) ⟶ False.
Assume H7: ∀ x14 x15 x16 . x12 x16 x13 ⟶ x12 x14 x13 ⟶ x12 x15 x13 ⟶ x11 x16 x14 ⟶ (x0 x15 (x10 x14 x16) = x10 (x0 x15 x14) x16 ⟶ False) ⟶ False.
Assume H8: (x1 = x2 ⟶ False) ⟶ False.
Assume H9: ∀ x14 . (x12 (x9 x14) x14 ⟶ False) ⟶ False.
Assume H10: ∀ x14 x15 . x12 x15 x13 ⟶ x12 x14 x13 ⟶ (x12 (x0 x15 x14) x13 ⟶ False) ⟶ False.
Assume H11: ∀ x14 x15 . x12 x15 x13 ⟶ x12 x14 x13 ⟶ (x12 (x10 x15 x14) x13 ⟶ False) ⟶ False.
Assume H12: (x12 x1 x3 ⟶ False) ⟶ False.
Assume H13: ∀ x14 x15 . x12 x15 x13 ⟶ x12 x14 x13 ⟶ (x11 x14 x15 ⟶ False) ⟶ (x8 x15 x14 = x7 x1 (x10 x14 x15) ⟶ False) ⟶ False.
Assume H14: ∀ x14 x15 . x12 x15 x13 ⟶ x12 x14 x13 ⟶ x11 x14 x15 ⟶ (x8 x15 x14 = x10 x15 x14 ⟶ False) ⟶ False.
Assume H15: ∀ x14 x15 . x12 x15 x13 ⟶ x12 x14 x13 ⟶ (x11 x15 x14 ⟶ False) ⟶ (x11 x14 x15 ⟶ False) ⟶ False.
Assume H16: ∀ x14 x15 . x12 x15 x13 ⟶ x12 x14 x13 ⟶ (x0 x15 x14 = x0 x14 x15 ⟶ False) ⟶ False.
Assume H17: x0 x4 (x10 x6 x5) = x8 (x0 x4 x6) x5 ⟶ False.
Assume H18: (x11 x5 x6 ⟶ False) ⟶ False.
Assume H19: (x12 x4 x13 ⟶ False) ⟶ False.
Assume H20: (x12 x6 x13 ⟶ False) ⟶ False.
Assume H21: (x12 x5 x13 ⟶ False) ⟶ False.
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
Claim L31: ...
...
Claim L32: ...
...
Claim L33: ...
...
Claim L34: ...
...
Claim L35: ...
...
Claim L36: ...
...
Claim L37: ...
...
Claim L38: ...
...
Claim L39: ...
...
Claim L40: ...
...
Claim L41: ...
...
Claim L42: ...
...
Claim L43: ...
...
Claim L44: ...
...
Claim L45: ...
...
Claim L46: ...
...
Claim L47: ...
...
Claim L48: ...
...
Claim L49: ...
...
Claim L50: ...
...
Claim L51: ...
...
Claim L52: ...
...
Claim L53: ...
...
Claim L54: ...
...
Claim L55: ...
...
Claim L56: ...
...
Claim L57: ...
...
Claim L58: ...
...
Claim L59: ...
...
Claim L60: ...
...
Claim L61: ...
...
Claim L62: ...
...
Claim L63: ...
...
Claim L64: ...
...
Claim L65: ...
...
Claim L66: ...
...
Claim L67: ...
...
Claim L68: ...
...
Claim L69: ...
...
Claim L70: ...
...
Claim L71: ...
...
Claim L72: ...
...
Claim L73: ...
...
Claim L74: x12 (x0 x4 x6) x13 ⟶ False
Assume H74: x12 (x0 x4 x6) x13.
Apply L73 leaving 2 subgoals.
The subproof is completed by applying H74.
Assume H75: ....
...
Apply L47.
Assume H75: x12 (x0 x4 x6) x13.
Apply L74.
The subproof is completed by applying H75.
■