Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ (∀ x2 . x2 ∈ x1 ⟶ add_SNo (ordsucc x0) x2 = ordsucc (add_SNo x0 x2)) ⟶ SNo x0 ⟶ SNo x1 ⟶ ordinal (add_SNo x0 x1) ⟶ ordinal (ordsucc x0) ⟶ SNo (ordsucc x0) ⟶ ordinal (add_SNo (ordsucc x0) x1) ⟶ ordsucc (add_SNo x0 x1) ∈ add_SNo (ordsucc x0) x1 ⟶ not (ordinal (ordsucc (add_SNo x0 x1)))

as obj
-

as prop
8c732..^{Conj_add_SNo_ordinal_SL__11__9}

theory
HotG

stx
b740c..

address
TMS81..^{Conj_add_SNo_ordinal_SL__11__9}