Proofgold Term Root Disambiguation

λ x0 x1 . ∃ x2 . and (x2 ∈ omega) (∃ x4 . and (and (and (ap x4 0 = x0) (ap x4 x2 = x1)) (∀ x6 . x6 ∈ ordsucc x2 ⟶ Field (ap x4 x6))) (∀ x6 . x6 ∈ x2 ⟶ ∃ x7 . and (x7 ∈ field0 (ap x4 (ordsucc x6))) (∃ x9 . and (x9 ∈ omega) (and (CRing_with_id_omega_exp (ap x4 (ordsucc x6)) x7 x9 ∈ field0 (ap x4 x6)) (Field_extension_by_1 (ap x4 x6) (ap x4 (ordsucc x6)) x7)))))

as obj
816f6..^{radical_field_extension}

as prop
-

theory
HotG

stx
6b5ba..

address
TMchE..^{radical_field_extension}