Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: ∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2.
Assume H1: ∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4).
Let x2 of type ι be given.
Assume H2: x2 ⊆ x0.
Assume H3: equip x2 u4.
Claim L4: ...
...
Let x3 of type ι → ι be given.
Let x4 of type ι → ι be given.
Assume H5: ∀ x5 . x5 ∈ u4 ⟶ x3 x5 ∈ x2.
Assume H6: ∀ x5 . x5 ∈ u4 ⟶ x4 x5 ∈ x2.
Assume H7: ∀ x5 . x5 ∈ u4 ⟶ x3 x5 = x4 x5 ⟶ ∀ x6 : ο . x6.
Assume H8: ∀ x5 . x5 ∈ u4 ⟶ x1 (x3 x5) (x4 x5).
Assume H9: ∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x3 x6 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.
Assume H10: ∀ x5 . x5 ∈ u4 ⟶ ∀ x6 . x6 ∈ u4 ⟶ x3 x5 = x4 x6 ⟶ x4 x5 = x3 x6 ⟶ x5 = x6.
Apply dneg with f1360.. x1 u3 x2.
Assume H11: not (f1360.. x1 u3 x2).
Claim L12: ...
...
Claim L13: ...
...
Claim L14: ...
...
Claim L15: ...
...
Apply L12 with 0, False leaving 3 subgoals.
The subproof is completed by applying In_0_4.
Let x5 of type ι be given.
Assume H16: x5 ∈ u4.
Assume H17: 0 = x5 ⟶ ∀ x6 : ο . x6.
Assume H18: x3 x5 = x4 0.
Assume H19: x4 x5 = x3 0 ⟶ ∀ x6 : ο . x6.
Apply L12 with x5, False leaving 3 subgoals.
The subproof is completed by applying H16.
Let x6 of type ι be given.
Assume H20: x6 ∈ u4.
Assume H21: x5 = x6 ⟶ ∀ x7 : ο . x7.
Assume H22: x3 x6 = x4 x5.
Assume H23: x4 x6 = x3 x5 ⟶ ∀ x7 : ο . x7.
Claim L24: ...
...
Apply L12 with x6, False leaving 3 subgoals.
The subproof is completed by applying H20.
Let x7 of type ι be given.
Assume H25: x7 ∈ u4.
Assume H26: x6 = x7 ⟶ ∀ x8 : ο . x8.
Assume H27: x3 x7 = x4 x6.
Assume H28: x4 x7 = x3 x6 ⟶ ∀ x8 : ο . x8.
Claim L29: ...
...
Apply H11.
Apply L13 with x3 0, x3 x5, x3 x6, x3 x7 leaving 14 subgoals.
Apply H5 with 0.
The subproof is completed by applying In_0_4.
Apply H5 with x5.
The subproof is completed by applying H16.
Apply H5 with x6.
The subproof is completed by applying H20.
Apply H5 with x7.
The subproof is completed by applying H25.
Apply H18 with λ x8 x9 . x3 0 = x9 ⟶ ∀ x10 : ο . x10.
Apply H7 with 0.
The subproof is completed by applying In_0_4.
Apply H22 with λ x8 x9 . x3 0 = x9 ⟶ ∀ x10 : ο . x10.
Apply neq_i_sym with x4 x5, x3 0.
The subproof is completed by applying H19.
Apply L29 with λ x8 x9 . x8 = x3 x7 ⟶ ∀ x10 : ο . x10.
Apply neq_i_sym with x3 x7, x4 x7.
Apply H7 with x7.
The subproof is completed by applying H25.
Apply H22 with λ x8 x9 . x3 x5 = x9 ⟶ ∀ x10 : ο . x10.
Apply H7 with x5.
The subproof is completed by applying H16.
Apply H27 with λ x8 x9 . x3 x5 = x9 ⟶ ∀ x10 : ο . x10.
Apply neq_i_sym with x4 x6, x3 x5.
The subproof is completed by applying H23.
...
...
...
...
...
...
...
...
■