Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ⟶ x1 x3 x2.
Assume H1: atleastp u8 x0.
Assume H2: 4402e.. x0 x1.
Assume H3: 35fb6.. x0 x1.
Let x2 of type ο be given.
Assume H4: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ cbd9e.. x1 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ x2.
Assume H5: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ e643b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ x2.
Assume H6: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ ∀ x10 . x10 ∈ x0 ⟶ 89dbd.. x1 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ x2.
Claim L7: ...
...
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
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: ...
...
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: ...
...
Apply unknownprop_d130c2da353f8a96ebfd044dc62865ee3ee198eb4370e3aa9882d0f235dc1fef with x0, x1, x2 leaving 183 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying L8.
Let x3 of type ι be given.
Assume H67: x3 ∈ x0.
Let x4 of type ι be given.
Assume H68: x4 ∈ x0.
Let x5 of type ι be given.
Assume H69: x5 ∈ x0.
Let x6 of type ι be given.
Assume H70: x6 ∈ x0.
Let x7 of type ι be given.
Assume H71: x7 ∈ x0.
Let x8 of type ι be given.
Assume H72: x8 ∈ x0.
Let x9 of type ι be given.
Assume H73: x9 ∈ x0.
Let x10 of type ι be given.
Assume H74: x10 ∈ x0.
Assume H75: 372ed.. x1 x3 x4 x5 x6 x7 x8 x9 x10.
Apply H75 with x2.
Assume H76: 7f677.. x1 x3 x4 x5 x6 x7 x8 x9.
Apply FalseE with ... ⟶ (... ⟶ ∀ x11 : ο . x11) ⟶ (x5 = x10 ⟶ ∀ x11 : ο . x11) ⟶ (x6 = x10 ⟶ ∀ x11 : ο . x11) ⟶ (x7 = x10 ⟶ ∀ x11 : ο . x11) ⟶ (x8 = x10 ⟶ ∀ x11 : ο . x11) ⟶ (x9 = x10 ⟶ ∀ x11 : ο . x11) ⟶ x1 x3 x10 ⟶ not (x1 x4 x10) ⟶ not (x1 x5 x10) ⟶ not (x1 x6 x10) ⟶ not (x1 x7 x10) ⟶ not (x1 x8 x10) ⟶ not (x1 x9 x10) ⟶ x2.
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
...
■