Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . 62ee1.. x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x6 x7 x8 = x6 x9 x10and (x7 = x9) (x8 = x10))∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)∀ x9 . prim1 x9 (3b429.. x0 (λ x10 . x0) (λ x10 x11 . True) x6)x6 (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (x9 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))) x15)))))) (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (x9 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))) x15)))) (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))))) = x6 x11 x13)x12)x12)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x7 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x6 (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))) x13)))))) (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))) x13)))) (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (x9 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x9 = x6 x19 x21)x20)x20))) x17)))))) (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (x9 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x9 = x6 x19 x21)x20)x20))) x17)))) (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))))) = x6 x13 x15)x14)x14))) x11)))))) (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (x6 (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))) x13)))))) (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (x9 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))) x13)))) (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (x9 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x9 = x6 x19 x21)x20)x20))) x17)))))) (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (x9 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x9 = x6 x19 x21)x20)x20))) x17)))) (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))))) = x6 x13 x15)x14)x14))) x11)))) (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x7 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (x9 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))) x15)))))) (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (x9 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x9 = x6 x17 x19)x18)x18))) x15)))) (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x9 = x6 x15 x17)x16)x16))))) = x6 x11 x13)x12)x12))))) = x6 (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x7 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15)))))) (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15)))) (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x7 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))))) = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x6 (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x7 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13)))))) (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13)))) (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x7 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x7 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17)))))) (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17)))) (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x7 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))))) = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))))) (x3 (x4 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x6 (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x7 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15)))))) (x3 (x4 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) (prim0 (λ x15 . and (prim1 x15 x0) (x8 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))) x15)))) (x4 (prim0 (λ x15 . and (prim1 x15 x0) (x7 = x6 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) x15))) (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))))) = x6 x11 x13)x12)x12))) (prim0 (λ x11 . and (prim1 x11 x0) (x9 = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x9 = x6 x13 x15)x14)x14))) x11)))) (x4 (prim0 (λ x11 . and (prim1 x11 x0) (x6 (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x7 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13)))))) (x3 (x4 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x7 = x6 x13 x15)x14)x14))) (prim0 (λ x13 . and (prim1 x13 x0) (x8 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x8 = x6 x15 x17)x16)x16))) x13)))) (x4 (prim0 (λ x13 . and (prim1 x13 x0) (x7 = x6 (prim0 (λ x15 . and (prim1 x15 x0) (∀ x16 : ο . (∀ x17 . and (prim1 x17 x0) (x7 = x6 x15 x17)x16)x16))) x13))) (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x8 = x6 x13 x15)x14)x14))))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x7 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17)))))) (x3 (x4 (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x7 = x6 x17 x19)x18)x18))) (prim0 (λ x17 . and (prim1 x17 x0) (x8 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x8 = x6 x19 x21)x20)x20))) x17)))) (x4 (prim0 (λ x17 . and (prim1 x17 x0) (x7 = x6 (prim0 (λ x19 . and (prim1 x19 x0) (∀ x20 : ο . (∀ x21 . and (prim1 x21 x0) (x7 = x6 x19 x21)x20)x20))) x17))) (prim0 (λ x17 . and (prim1 x17 x0) (∀ x18 : ο . (∀ x19 . and (prim1 x19 x0) (x8 = x6 x17 x19)x18)x18))))) = x6 x13 x15)x14)x14))) x11))) (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x9 = x6 x11 x13)x12)x12)))))
as obj
-
as prop
dde2d..
theory
HoTg
stx
a993b..
address
TMZiD..