Proofgold Object

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∃ x7 . and (x7 ∈ {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 . and (x9 ∈ {x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1 ⟶ ∀ x12 : ο . x12}) (x4 x9 x6 = x7))

type
ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ο

theory
HotG

name
explicit_OrderedField_rationalp

definition
PUa4W..

Megalodon
explicit_OrderedField_rationalp

proofgold address
TMdsi..^{explicit_OrderedField_rationalp}

creator
5731 Pr6Pc../28609..

owner
5731 Pr6Pc../28609..

term root
bacde..