Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Assume H0: x0 0 u2.
Assume H1: x0 u4 u6.
Assume H2: x0 u1 u12.
Assume H3: x0 u5 u12.
Assume H4: x0 u8 u12.
Assume H5: x0 u9 u12.
Assume H6: x0 u3 u13.
Assume H7: x0 u7 u13.
Assume H8: x0 u10 u13.
Assume H9: x0 u2 u14.
Assume H10: x0 u6 u14.
Assume H11: x0 u11 u14.
Assume H12: x0 0 u15.
Assume H13: x0 u4 u15.
Assume H14: x0 u3 u4.
Assume H15: x0 0 u7.
Assume H16: x0 u10 u14.
Let x1 of type ι be given.
Assume H17: x1 ⊆ u16.
Assume H18: atleastp u6 x1.
Assume H19: u12 ∈ x1.
Assume H20: u14 ∈ x1.
Assume H21: ∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ not (x0 x2 x3).
Claim L22: ...
...
Claim L23: ...
...
Claim L24: ...
...
Claim L25: ...
...
Claim L26: ...
...
Apply xm with u13 ∈ x1, False leaving 2 subgoals.
Assume H27: u13 ∈ x1.
Apply unknownprop_0397a08554d02eca12a49d1b016d535c1fa787322f197d101b2112b6e0f961b4 with x0, x1 leaving 20 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 H3.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
The subproof is completed by applying H13.
The subproof is completed by applying H17.
The subproof is completed by applying H18.
The subproof is completed by applying H19.
The subproof is completed by applying H27.
The subproof is completed by applying H20.
The subproof is completed by applying H21.
Assume H27: nIn u13 x1.
Claim L28: ...
...
Apply unknownprop_95c6cbd2308b27a7edcd2a1d9389b377988e902d740d05dc7c88e6b8da945ab9 with binintersect x1 u12, False leaving 2 subgoals.
The subproof is completed by applying L28.
Let x2 of type ι be given.
Assume H29: x2 ∈ binintersect x1 u12.
Let x3 of type ι be given.
Assume H30: x3 ∈ binintersect x1 u12.
Let x4 of type ι be given.
Assume H31: x4 ∈ binintersect x1 u12.
Claim L32: x2 ∈ x1 ⟶ x3 ∈ x1 ⟶ x4 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x5 : ο . x5) ⟶ (x2 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ False
Apply L23 with x2, λ x5 . x5 ∈ x1 ⟶ x3 ∈ x1 ⟶ x4 ∈ x1 ⟶ (x5 = x3 ⟶ ∀ x6 : ο . x6) ⟶ (x5 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x3 = x4 ⟶ ∀ x6 : ο . x6) ⟶ False leaving 5 subgoals.
The subproof is completed by applying H29.
Apply L23 with x3, λ x5 . 0 ∈ x1 ⟶ x5 ∈ x1 ⟶ x4 ∈ x1 ⟶ (0 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (0 = x4 ⟶ ∀ x6 : ο . x6) ⟶ (x5 = x4 ⟶ ∀ x6 : ο . x6) ⟶ False leaving 5 subgoals.
The subproof is completed by applying H30.
Assume H32: 0 ∈ x1.
Assume H33: 0 ∈ x1.
Assume H34: x4 ∈ x1.
Assume H35: 0 = 0 ⟶ ∀ x5 : ο . x5.
Apply FalseE with (0 = x4 ⟶ ∀ x5 : ο . x5) ⟶ (0 = x4 ⟶ ∀ x5 : ο . x5) ⟶ False.
Apply H35.
Let x5 of type ι → ι → ο be given.
Assume H36: x5 0 0.
The subproof is completed by applying H36.
Apply L23 with x4, λ x5 . ... ⟶ ... ⟶ ... ⟶ (... ⟶ ∀ x6 : ο . x6) ⟶ (0 = x5 ⟶ ∀ x6 : ο . x6) ⟶ (u3 = x5 ⟶ ∀ x6 : ο . x6) ⟶ False leaving 5 subgoals.
...
...
...
...
...
...
...
...
...
...
Apply L32 leaving 3 subgoals.
Apply binintersectE1 with x1, u12, x2.
The subproof is completed by applying H29.
Apply binintersectE1 with x1, u12, x3.
The subproof is completed by applying H30.
Apply binintersectE1 with x1, u12, x4.
The subproof is completed by applying H31.
■