Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5∀ x6 : ο . ((∀ x7 . x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})})x1{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}{x7 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x7 = x1∀ x8 : ο . x8}{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}x0(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}∀ x8 : ο . (explicit_Field_minus x0 x1 x2 x3 x4 x7{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}x8)(x7 = x1x8)(x7{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}x8)x8)x2{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}explicit_Field_minus x0 x1 x2 x3 x4 x2{x7 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9}) (x7 = x1)) (x7{x8 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x8 = x1∀ x9 : ο . x9})}(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}explicit_Field_minus x0 x1 x2 x3 x4 x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})})(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}∀ x8 . 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})}x3 x7 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})})(∀ x7 . x7{x8 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10}) (x8 = x1)) (x8{x9 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x9 = x1∀ x10 : ο . x10})}∀ x8 . 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})}x4 x7 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})})x6)x6
as obj
-
as prop
5d739..explicit_OrderedField_Z_props
theory
HotG
stx
b2e5e..
address
TMXcg..explicit_OrderedField_Z_props