Proofgold Term Root Disambiguation

∀ 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)

as obj
-

as prop
c41d6..^{SNo_idl_cycle_nonneg}

theory
HotG

stx
6036f..

address
TMLTP..^{SNo_idl_cycle_nonneg}