Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 . x2omega∀ x3 . ap x3 0 = x0ap x3 x2 = x1(∀ x4 . x4ordsucc x2Field (ap x3 x4))(∀ x4 . x4x2∀ x5 : ο . (∀ x6 . and (x6field0 (ap x3 (ordsucc x4))) (∀ x7 : ο . (∀ x8 . and (x8omega) (and (CRing_with_id_omega_exp (ap x3 (ordsucc x4)) x6 x8field0 (ap x3 x4)) (Field_extension_by_1 (ap x3 x4) (ap x3 (ordsucc x4)) x6))x7)x7)x5)x5)radical_field_extension x0 x1
as obj
-
as prop
6bd73..radical_field_extension_I
theory
HotG
stx
6b5ba..
address
TMaTm..radical_field_extension_I