Proofgold Proposition

∀ x0 . nat_p x0 ⟶ ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x1 x3)) ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNo (x2 x3)) ⟶ x1 (ordsucc x0) = x1 0 ⟶ (∀ x3 . x3 ∈ ordsucc x0 ⟶ SNoLe (add_SNo (x1 (ordsucc x3)) (minus_SNo (x1 x3))) (x2 x3)) ⟶ SNoLe 0 (finite_add_SNo (ordsucc x0) x2)

type
prop

theory
HotG

name
SNo_idl_cycle_nonneg

proof
PULfh..

Megalodon
SNo_idl_cycle_nonneg

proofgold address
TMV7M..^{SNo_idl_cycle_nonneg}

creator
16612 PrGxv../63f1c..

owner
16612 PrGxv../63f1c..

term root
e90cb..