Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Let x1 of type ι → ι be given.
Assume H0: ∀ x2 . x2 ∈ u16 ⟶ x1 x2 ∈ u16.
Assume H1: ∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.
Assume H2: ∀ x2 . x2 ∈ u16 ⟶ ∀ x3 . x3 ∈ u16 ⟶ x0 (x1 x2) (x1 x3) ⟶ x0 x2 x3.
Assume H3: ∀ x2 . x2 ∈ u16 ⟶ x1 (x1 (x1 (x1 x2))) = x2.
Assume H4: x1 u12 = u13.
Assume H5: x1 u13 = u14.
Assume H6: x1 u14 = u15.
Assume H7: x1 u15 = u12.
Let x2 of type ι be given.
Assume H8: x2 ⊆ u16.
Assume H9: atleastp u6 x2.
Assume H10: ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ not (x0 x3 x4).
Assume H11: atleastp u2 (setminus x2 u12).
Let x3 of type ο be given.
Assume H12: ∀ x4 . x4 ⊆ u16 ⟶ atleastp u6 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u12 ∈ x4 ⟶ u13 ∈ x4 ⟶ x3.
Assume H13: ∀ x4 . x4 ⊆ u16 ⟶ atleastp u6 x4 ⟶ (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ not (x0 x5 x6)) ⟶ u12 ∈ x4 ⟶ u14 ∈ x4 ⟶ x3.
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Claim L20: ...
...
Claim L21: ...
...
Apply unknownprop_8d334858d1804afd99b1b9082715c7f916daee31e697b66b5c752e0c8756ebae with setminus x2 u12, x3 leaving 2 subgoals.
The subproof is completed by applying H11.
Apply L15 with x3.
Let x4 of type ι be given.
Assume H22: x4 ∈ setminus x2 u12.
Let x5 of type ι be given.
Assume H23: x5 ∈ setminus x2 u12.
Assume H24: x4 ∈ x5.
Apply setminusE with x2, u12, x4, x3 leaving 2 subgoals.
The subproof is completed by applying H22.
Assume H25: x4 ∈ x2.
Assume H26: nIn x4 u12.
Apply setminusE with x2, u12, x5, x3 leaving 2 subgoals.
The subproof is completed by applying H23.
Assume H27: x5 ∈ x2.
Assume H28: nIn x5 u12.
Apply L14 with x4, x3 leaving 6 subgoals.
Apply H8 with x4.
The subproof is completed by applying H25.
Assume H29: x4 ∈ u12.
Apply FalseE with x3.
Apply H26.
The subproof is completed by applying H29.
Assume H29: x4 = u12.
Apply L14 with x5, x3 leaving 6 subgoals.
Apply H8 with x5.
The subproof is completed by applying H27.
Assume H30: x5 ∈ u12.
Apply FalseE with x3.
Apply H28.
The subproof is completed by applying H30.
Assume H30: x5 = u12.
Apply FalseE with x3.
Apply In_irref with x4.
Apply H29 with λ x6 x7 . x4 ∈ x7.
Apply H30 with λ x6 x7 . x4 ∈ x6.
The subproof is completed by applying H24.
Assume H30: x5 = u13.
Apply H12 with x2 leaving 5 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Apply H29 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H25.
Apply H30 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H27.
Assume H30: x5 = u14.
Apply H13 with x2 leaving 5 subgoals.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
The subproof is completed by applying H10.
Apply H29 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H25.
Apply H30 with λ x6 x7 . x6 ∈ x2.
The subproof is completed by applying H27.
Assume H30: x5 = u15.
Apply H12 with {x1 x6|x6 ∈ x2} leaving 5 subgoals.
The subproof is completed by applying L16.
Apply atleastp_tra with u6, x2, {x1 x6|x6 ∈ x2} leaving 2 subgoals.
The subproof is completed by applying H9.
Apply equip_atleastp with x2, {...|x6 ∈ ...}.
...
...
...
...
...
...
...
■