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: ∀ x3 . ... ⟶ ∀ x4 . ... ⟶ ∀ x5 . ... ⟶ ∀ x6 . ... ⟶ ∀ x7 . ... ⟶ ... ⟶ ... ⟶ x5 = {x8 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) ...)|...} ⟶ x7 = setminus {x8 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x8) (DirGraphOutNeighbors u18 x0 x1)) u2} x6 ⟶ ∀ x8 . x8 ∈ x5 ⟶ ∀ x9 . x9 ∈ x5 ⟶ ∀ x10 . x10 ∈ x5 ⟶ ∀ x11 . x11 ∈ x5 ⟶ x0 x8 x9 ⟶ x0 x9 x10 ⟶ x0 x10 x11 ⟶ x0 x11 x8 ⟶ (x9 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x10 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x8 ⟶ ∀ x12 : ο . x12) ⟶ (x10 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x9 ⟶ ∀ x12 : ο . x12) ⟶ (x11 = x10 ⟶ ∀ x12 : ο . x12) ⟶ not (x0 x8 x10) ⟶ not (x0 x9 x11) ⟶ x5 = SetAdjoin (SetAdjoin (UPair x8 x9) x10) x11 ⟶ (∀ x12 . x12 ∈ u18 ⟶ ∀ x13 : ο . (x12 = x1 ⟶ x13) ⟶ (x12 = x3 ⟶ x13) ⟶ (x12 ∈ x4 ⟶ x13) ⟶ (x12 ∈ x6 ⟶ x13) ⟶ (x12 ∈ x5 ⟶ x13) ⟶ (x12 ∈ x7 ⟶ x13) ⟶ x13) ⟶ (∀ x12 . x12 ∈ x5 ⟶ not (x0 x3 x12)) ⟶ equip x4 u4 ⟶ equip x5 u4 ⟶ equip x6 u4 ⟶ equip x7 u4 ⟶ (∀ x12 . x12 ∈ x6 ⟶ nIn x12 x7) ⟶ (∀ x12 . x12 ∈ x5 ⟶ ∃ x13 . and (x13 ∈ x6) (x0 x12 x13)) ⟶ (∀ x12 . x12 ∈ x6 ⟶ not (x0 x1 x12)) ⟶ (∀ x12 . x12 ∈ x6 ⟶ equip (binintersect (DirGraphOutNeighbors u18 x0 x12) (DirGraphOutNeighbors u18 x0 x1)) u2) ⟶ x2.
...
■