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.
Assume H5: ∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ x7 x11 x10 ⟶ (x6 x11 (x5 x10 x11) = x10 ⟶ False) ⟶ False.
Assume H6: ∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ x7 x11 x10 ⟶ (x8 (x5 x10 x11) x9 ⟶ False) ⟶ False.
Assume H7: ∀ x10 x11 x12 . x8 x12 x9 ⟶ x8 x10 x9 ⟶ x8 x11 x9 ⟶ x12 = x6 x10 x11 ⟶ (x7 x11 x12 ⟶ False) ⟶ False.
Assume H8: ∀ x10 x11 x12 . x8 x12 x9 ⟶ x8 x10 x9 ⟶ x8 x11 x9 ⟶ (x0 x12 (x6 x10 x11) = x6 (x0 x12 x10) (x0 x12 x11) ⟶ False) ⟶ False.
Assume H9: ∀ x10 . (x8 (x4 x10) x10 ⟶ False) ⟶ False.
Assume H10: ∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x8 (x0 x11 x10) x9 ⟶ False) ⟶ False.
Assume H11: ∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x8 (x6 x11 x10) x9 ⟶ False) ⟶ False.
Assume H12: ∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x7 x11 x10 ⟶ False) ⟶ (x7 x10 x11 ⟶ False) ⟶ False.
Assume H13: ∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x0 x11 x10 = x0 x10 x11 ⟶ False) ⟶ False.
Assume H14: ∀ x10 x11 . x8 x11 x9 ⟶ x8 x10 x9 ⟶ (x6 x11 x10 = x6 x10 x11 ⟶ False) ⟶ False.
Assume H15: x7 (x0 x1 x3) (x0 x2 x3) ⟶ False.
Assume H16: (x7 x1 x2 ⟶ False) ⟶ False.
Assume H17: (x8 x3 x9 ⟶ False) ⟶ False.
Assume H18: (x8 x2 x9 ⟶ False) ⟶ False.
Assume H19: (x8 x1 x9 ⟶ False) ⟶ False.
Claim L20: ...
...
Claim L21: ...
...
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: ...
...
Claim L75: ...
...
Claim L76: ...
...
Claim L77: ...
...
Claim L78: ...
...
Claim L79: ...
...
Claim L80: ...
...
Claim L81: ...
...
Claim L82: ...
...
Claim L83: ...
...
Claim L84: ...
...
Claim L85: ...
...
Claim L86: ...
...
Claim L87: ...
...
Claim L88: ...
...
Claim L89: ...
...
Claim L90: ...
...
Claim L91: ...
...
Claim L92: ...
...
Claim L93: ...
...
Claim L94: ...
...
Claim L95: ...
...
Claim L96: ...
...
Claim L97: ...
...
Claim L98: ...
...
Claim L99: x6 (x0 x3 (x5 x2 x1)) ... = ... ⟶ False
...
Claim L100: x0 x2 x3 = x0 x2 x3 ⟶ False
Assume H100: x0 x2 x3 = x0 x2 x3.
Apply L90.
Assume H101: x6 (x0 x3 (x5 x2 x1)) (x0 x1 x3) = x0 x2 x3.
Apply L99.
Apply H101 with λ x10 x11 . x11 = x0 x2 x3.
The subproof is completed by applying H100.
Apply L100.
The subproof is completed by applying L0 with x0 x2 x3.
■