Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . and (and (explicit_OrderedField x0 x1 x2 x3 x4 x5) (∀ x6 . x6x0∀ x7 . x7x0lt x0 x1 x2 x3 x4 x5 x1 x6x5 x1 x7∀ x8 : ο . (∀ x9 . and (x9Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)) (x5 x7 (x4 x9 x6))x8)x8)) (∀ x6 . x6setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))∀ x7 . x7setexp x0 (Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))(∀ x8 . x8Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (and (x5 (ap x6 x8) (ap x7 x8)) (x5 (ap x6 x8) (ap x6 (x3 x8 x2)))) (x5 (ap x7 (x3 x8 x2)) (ap x7 x8)))∀ x8 : ο . (∀ x9 . and (x9x0) (∀ x10 . x10Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)and (x5 (ap x6 x10) x9) (x5 x9 (ap x7 x10)))x8)x8)
as obj
f814a..explicit_Reals
as prop
-
theory
HotG
stx
788c2..
address
TMNQk..explicit_Reals