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 ∈ DirGraphOutNeighbors u18 x0 x1.
Assume H5: ∀ x3 . x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1} ⟶ not (x0 x2 x3).
Let x3 of type ι be given.
Assume H6: x3 ∈ setminus {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2} (DirGraphOutNeighbors u18 x0 x2).
Apply setminusE with {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2}, DirGraphOutNeighbors u18 x0 x2, x3, x0 (31e20.. x0 x1 (4b3fa.. x0 x1 x3)) (31e20.. x0 x1 (f14ce.. x0 x1 x3)) leaving 2 subgoals.
The subproof is completed by applying H6.
Assume H7: x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2}.
Assume H8: nIn x3 (DirGraphOutNeighbors u18 x0 x2).
Apply SepE with setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)), λ x4 . equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u2, x3, x0 (31e20.. x0 x1 (4b3fa.. x0 x1 x3)) (31e20.. x0 x1 (f14ce.. x0 x1 x3)) leaving 2 subgoals.
The subproof is completed by applying H7.
Assume H9: x3 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1)).
Assume H10: equip (binintersect (DirGraphOutNeighbors u18 x0 x3) (DirGraphOutNeighbors u18 x0 x1)) u2.
Apply setminusE with u18, binunion (DirGraphOutNeighbors u18 ... ...) ..., ..., ... leaving 2 subgoals.
...
...
■