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 ∈ {x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2}.
Apply SepE with setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)), λ x3 . equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2, x2, and (f14ce.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (f14ce.. x0 x1 x2 = 4b3fa.. x0 x1 x2 ⟶ ∀ x3 : ο . x3) leaving 2 subgoals.
The subproof is completed by applying H4.
Assume H5: x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)).
Assume H6: equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u2.
Apply Eps_i_ex with λ x3 . and (x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (x3 = 4b3fa.. x0 x1 x2 ⟶ ∀ x4 : ο . x4).
Apply unknownprop_4d754b36cdd40bc8cd396c0ff8341e59d3f91fcdd920c2c29f628773f7320249 with binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1), ∃ x3 . and (x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (x3 = 4b3fa.. x0 x1 x2 ⟶ ∀ x4 : ο . x4) leaving 2 subgoals.
Apply equip_sym with binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1), u2.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H7: (λ x4 . and (x4 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (∃ x5 . and (x5 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (and (x4 = x5 ⟶ ∀ x6 : ο . x6) (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1) = UPair x4 x5)))) ....
...
■