Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3 ⟶ x1 x3 x2) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u3 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ x1 x3 x4)) ⟶ (∀ x2 . x2 ⊆ x0 ⟶ atleastp u6 x2 ⟶ not (∀ x3 . x3 ∈ x2 ⟶ ∀ x4 . x4 ∈ x2 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4))) ⟶ ∀ x2 . nat_p x2 ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ (x3 = x4 ⟶ ∀ x5 : ο . x5) ⟶ not (x1 x3 x4) ⟶ or (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) x2) (equip (binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x4)) (ordsucc x2))) ⟶ ∀ x3 x4 . x3 ∈ x0 ⟶ x4 ∈ DirGraphOutNeighbors x0 x1 x3 ⟶ (∀ x5 . x5 ∈ {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) x2} ⟶ not (x1 x4 x5)) ⟶ binunion (setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3)) (setminus {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) (ordsucc x2)} (setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x3))) = {x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x3)) (ordsucc x2)}

type
prop

theory
HotG

name
-

proof
PUTao..

Megalodon
-

proofgold address
TMUjz..

creator
25989 Pr4zB../97727..

owner
25991 Pr4zB../aaa5d..

term root
74300..