Proofgold Proposition

∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2 ⟶ x0 x2 x1) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u3 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ x0 x2 x3)) ⟶ (∀ x1 . x1 ⊆ u18 ⟶ atleastp u6 x1 ⟶ not (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 . x3 ∈ x1 ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ not (x0 x2 x3))) ⟶ ∀ x1 . x1 ∈ u18 ⟶ ∀ x2 . x2 ∈ DirGraphOutNeighbors u18 x0 x1 ⟶ (∀ 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)) ⟶ ∀ x3 . x3 ∈ setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x2) ⟶ and (and (31e20.. x0 x1 x3 ∈ {x4 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x4) (DirGraphOutNeighbors u18 x0 x1)) u1}) (binintersect (DirGraphOutNeighbors u18 x0 (31e20.. x0 x1 x3)) (DirGraphOutNeighbors u18 x0 x1) = Sing x3)) (4b3fa.. x0 x1 (31e20.. x0 x1 x3) = x3)

type
prop

theory
HotG

name
-

proof
PUdHT..

Megalodon
-

proofgold address
TMRSk..

creator
31037 Pr4zB../33001..

owner
31037 Pr4zB../33001..

term root
319dc..