Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∀ x7 : ο . (∀ x8 . and (x8{x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11}) (x9 = x1)) (x9{x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1∀ x11 : ο . x11})}) (∀ x9 : ο . (∀ x10 . and (x10{x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1∀ x12 : ο . x12}) (x4 x10 x6 = x8)x9)x9)x7)x7
as obj
6449a..explicit_OrderedField_rationalp
as prop
-
theory
HotG
stx
b2e5e..
address
TMS9J..explicit_OrderedField_rationalp