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)) u1}.
Apply SepE with setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)), λ x3 . equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u1, x2, and (4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ x0 x3 x2 ⟶ x3 = 4b3fa.. x0 x1 x2) 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)) u1.
Claim L7: ...
...
Apply andI with 4b3fa.. x0 x1 x2 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1), ∀ x3 . x3 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ x0 x3 x2 ⟶ x3 = 4b3fa.. x0 x1 x2 leaving 2 subgoals.
Apply Eps_i_ex with λ x3 . x3 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1).
The subproof is completed by applying L7.
Let x3 of type ι be given.
Assume H8: x3 ∈ DirGraphOutNeighbors u18 x0 x1.
Assume H9: x0 x3 x2.
Apply unknownprop_9c0575fd54374e0d0f9b0bb0395cadff0fc4a8034816c932683102f3d70ab52c with binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1), x3 = 4b3fa.. x0 x1 x2 leaving 2 subgoals.
Apply equip_sym with binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1), u1.
The subproof is completed by applying H6.
Let x4 of type ι be given.
Assume H10: (λ x5 . and (x5 ∈ binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1) = ...)) ....
...
■