Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ι → ο be given.
Assume H0: ∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1.
Assume H1: ∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3).
Assume H2: ∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3)).
Let x1 of type ι be given.
Assume H3: x1 ∈ u18.
Let x2 of type ι be given.
Assume H4: x2 ∈ u18.
Assume H5: x1 = x2 ⟶ ∀ x3 : ο . x3.
Assume H6: not (x0 x1 x2).
Apply unknownprop_45d11dce2d0b092bd17c01d64c29c5885c90b43dc7cb762c6d6ada999ea508c5 with 2, binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2), atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2 leaving 3 subgoals.
The subproof is completed by applying nat_2.
Assume H7: atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) 2.
The subproof is completed by applying H7.
Assume H7: atleastp u3 (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)).
Claim L8: ...
...
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Apply L11 with x0, atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2 leaving 3 subgoals.
The subproof is completed by applying H0.
Assume H12: ∃ x3 . and (x3 ⊆ setminus u18 (binunion (binunion (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) (UPair x1 x2))) (and (equip u3 x3) (∀ x4 . x4 ∈ x3 ⟶ ∀ x5 . x5 ∈ x3 ⟶ (x4 = x5 ⟶ ∀ x6 : ο . x6) ⟶ x0 x4 x5)).
Apply H12 with atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2.
Let x3 of type ι be given.
Assume H13: (λ x4 . and (x4 ⊆ setminus u18 (binunion (binunion (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) (UPair x1 x2))) (and (equip u3 x4) (∀ x5 . x5 ∈ x4 ⟶ ∀ x6 . x6 ∈ x4 ⟶ (x5 = x6 ⟶ ∀ x7 : ο . x7) ⟶ x0 x5 x6))) x3.
Apply H13 with atleastp (binintersect (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) u2.
Assume H14: x3 ⊆ setminus u18 (binunion (binunion (DirGraphOutNeighbors u18 x0 x1) (DirGraphOutNeighbors u18 x0 x2)) (UPair x1 x2)).
Assume H15: and (equip u3 x3) (∀ x4 . ... ⟶ ∀ x5 . ... ⟶ ... ⟶ x0 x4 ...).
...
...
■