Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Apply dneg with or (∃ x1 . and (x1 ⊆ 9) (and (equip 3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3))) (∃ x1 . and (x1 ⊆ 9) (and (equip 4 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)))).
Assume H1: not (or (∃ x1 . and (x1 ⊆ u9) (and (equip u3 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3))) (∃ x1 . and (x1 ⊆ u9) (and (equip u4 x1) (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))))).
Claim L2: ...
...
Claim L3: ...
...
Apply unknownprop_4ea53c48851955e8bea31637fee475e64087a6b61ca7b79b70612b7fb5547d5f with x0, 0, False leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying L3.
Let x1 of type ι be given.
Assume H4: x1 ∈ u9.
Let x2 of type ι be given.
Assume H5: x2 ∈ u9.
Let x3 of type ι be given.
Assume H6: x3 ∈ u9.
Let x4 of type ι be given.
Assume H7: x4 ∈ u9.
Assume H8: 0 = x1 ⟶ ∀ x5 : ο . x5.
Assume H9: 0 = x2 ⟶ ∀ x5 : ο . x5.
Assume H10: 0 = x3 ⟶ ∀ x5 : ο . x5.
Assume H11: 0 = x4 ⟶ ∀ x5 : ο . x5.
Assume H12: x1 = x2 ⟶ ∀ x5 : ο . x5.
Assume H13: x1 = x3 ⟶ ∀ x5 : ο . x5.
Assume H14: x1 = x4 ⟶ ∀ x5 : ο . x5.
Assume H15: x2 = x3 ⟶ ∀ x5 : ο . x5.
Assume H16: x2 = x4 ⟶ ∀ x5 : ο . x5.
Assume H17: x3 = x4 ⟶ ∀ x5 : ο . x5.
Assume H18: x0 0 x1.
Assume H19: x0 0 x2.
Assume H20: x0 0 x3.
Assume H21: not (x0 x1 x2).
Assume H22: not (x0 x1 x3).
Assume H23: not (x0 x2 x3).
Assume H24: ∀ x5 . x5 ∈ u9 ⟶ x0 0 x5 ⟶ x5 ∈ SetAdjoin (SetAdjoin (UPair 0 x1) x2) x3.
Assume H25: x0 x4 x1.
Assume H26: x0 x4 x2.
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: ...
...
Apply unknownprop_f0014261a073154b27e42b7a2586bc3123c4455a00f08c2d90b89b2c21d8c9c7 with x0, x4, x1, x2, False leaving 11 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H7.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying L30.
The subproof is completed by applying L31.
The subproof is completed by applying H12.
The subproof is completed by applying H25.
The subproof is completed by applying H26.
Let x5 of type ι be given.
Assume H42: x5 ∈ u9.
Assume H43: x4 = x5 ⟶ ∀ x6 : ο . x6.
Assume H44: x1 = x5 ⟶ ∀ x6 : ο . x6.
Assume H45: x2 = x5 ⟶ ∀ x6 : ο . x6.
Assume H46: x0 x4 x5.
Assume H47: ....
...
■