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.
Assume H0: ∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4).
Assume H1: ∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x2 x3 x4).
Assume H2: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x1 x3 (x1 x4 x5) = x1 x4 (x1 x3 x5).
Assume H3: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x1 (x1 x3 x4) x5 = x1 x3 (x1 x4 x5).
Assume H4: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5).
Assume H5: ∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5).
Let x3 of type ι → ι be given.
Assume H6: ∀ x4 . x0 x4 ⟶ x3 x4 = x2 x4 x4.
Let x4 of type ι → ι be given.
Assume H7: ∀ x5 . x0 x5 ⟶ x0 (x4 x5).
Assume H8: ∀ x5 . x0 x5 ⟶ x4 (x4 x5) = x5.
Assume H9: ∀ x5 x6 . x0 x5 ⟶ x0 x6 ⟶ x1 (x4 x5) (x1 x5 x6) = x6.
Assume H10: ∀ x5 x6 . x0 x5 ⟶ x0 x6 ⟶ x1 x5 (x1 (x4 x5) x6) = x6.
Assume H11: ∀ x5 x6 . x0 x5 ⟶ x0 x6 ⟶ x2 (x4 x5) x6 = x4 (x2 x5 x6).
Assume H12: ∀ x5 x6 . x0 x5 ⟶ x0 x6 ⟶ x2 x5 (x4 x6) = x4 (x2 x5 x6).
Assume H13: ∀ x5 x6 . x0 x5 ⟶ x0 x6 ⟶ x2 x5 x6 = x2 x6 x5.
Assume H14: ∀ x5 x6 x7 x8 . x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x2 x5 x6) (x2 x7 x8) = x2 (x2 x5 x7) (x2 x6 x8).
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Claim L27: ...
...
Claim L28: ...
...
Claim L29: ...
...
Claim L30: ...
...
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.
Assume H31: x0 x5.
Assume H32: x0 x6.
Assume H33: x0 x7.
Assume H34: x0 x8.
Assume H35: x0 x9.
Assume H36: x0 x10.
Assume H37: x0 x11.
Assume H38: x0 x12.
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: ...
...
Claim L100: ...
...
Claim L101: ...
...
Claim L102: ...
...
Claim L103: ...
...
Claim L104: ...
...
Claim L105: ...
...
Claim L106: ...
...
Claim L107: ...
...
Claim L108: ...
...
Claim L109: ...
...
Claim L110: ...
...
Claim L111: ...
...
Claim L112: ...
...
Claim L113: ...
...
Claim L114: ...
...
Claim L115: ...
...
Claim L116: ...
...
Claim L117: ...
...
Claim L118: ...
...
Claim L119: ...
...
Claim L120: ...
...
Claim L121: ...
...
Claim L122: ...
...
Claim L123: ...
...
Claim L124: ...
...
Claim L125: ...
...
Claim L126: ...
...
Claim L127: ...
...
Claim L128: ...
...
Claim L129: ...
...
Claim L130: ...
...
Claim L131: ...
...
Claim L132: ...
...
Claim L133: ...
...
Claim L134: ...
...
Claim L135: ...
...
Claim L136: ...
...
Claim L137: ...
...
Claim L138: ...
...
Claim L139: ...
...
Claim L140: ...
...
Claim L141: ...
...
Claim L142: ...
...
Claim L143: ...
...
Claim L144: ...
...
Claim L145: ...
...
Claim L146: ...
...
Claim L147: ...
...
Claim L148: ...
...
Claim L149: ...
...
Claim L150: ...
...
Claim L151: ...
...
Claim L152: ...
...
Claim L153: ...
...
Claim L154: ...
...
Claim L155: ...
...
Claim L156: ...
...
Claim L157: ...
...
Claim L158: ...
...
Claim L159: ...
...
Claim L160: ...
...
Claim L161: ...
...
Claim L162: ...
...
Claim L163: ...
...
Claim L164: ...
...
Claim L165: ...
...
Claim L166: ...
...
Claim L167: ...
...
Claim L168: ...
...
Claim L169: ...
...
Claim L170: ...
...
Claim L171: ...
...
Claim L172: ...
...
Claim L173: ...
...
Claim L174: ...
...
Claim L175: ...
...
Claim L176: ...
...
Claim L177: ...
...
Claim L178: ...
...
Claim L179: ...
...
Apply L176 with λ x13 x14 . x2 (x1 (x3 x5) (x1 (x3 x6) (x1 (x3 x7) (x3 x8)))) (x1 (x3 ...) ...) = ....
...
■