Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (explicit_Reals x0 x1 x2 x3 x4 x5explicit_OrderedField x0 x1 x2 x3 x4 x5(∀ x7 . x7x0∀ x8 . x8x0lt x0 x1 x2 x3 x4 x5 x1 x7x5 x1 x8∀ x9 : ο . (∀ x10 . and (x10Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)) (x5 x8 (x4 x10 x7))x9)x9)(∀ x7 . x7setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))∀ x8 . x8setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))(∀ x9 . x9Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (and (x5 (ap x7 x9) (ap x8 x9)) (x5 (ap x7 x9) (ap x7 (x3 x9 x2)))) (x5 (ap x8 (x3 x9 x2)) (ap x8 x9)))∀ x9 : ο . (∀ x10 . and (x10x0) (∀ x11 . x11Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (x5 (ap x7 x11) x10) (x5 x10 (ap x8 x11)))x9)x9)x6)explicit_Reals x0 x1 x2 x3 x4 x5x6
as obj
-
as prop
4da66..explicit_Reals_E
theory
HotG
stx
788c2..
address
TMGdZ..explicit_Reals_E