Proofgold Term Root Disambiguation

λ x0 . ∃ x1 . and (x1 ∈ omega) (∃ x3 . and (and (and (and (∀ x5 . x5 ∈ ordsucc x1 ⟶ Group (ap x3 x5)) (∀ x5 . x5 ∈ x1 ⟶ normal_subgroup (ap x3 (ordsucc x5)) (ap x3 x5))) (∀ x5 . x5 ∈ x1 ⟶ abelian_Group (quotient_Group (ap x3 x5) (ap x3 (ordsucc x5))))) (x0 = ap x3 0)) (trivial_Group_p (ap x3 x1)))

as obj
da0c1..^{solvable_Group_p}

as prop
-

theory
HotG

stx
6b5ba..

address
TMX5X..^{solvable_Group_p}