Search for blocks/addresses/...

Proofgold Proposition

∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0prim1 (x3 x7 x8) x0)prim1 x1 x0(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0prim1 (x4 x7 x8) x0)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x4 x7 (x4 x8 x9) = x4 (x4 x7 x8) x9)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 x7 x8 = x4 x8 x7)prim1 x2 x0(∀ x7 . prim1 x7 x0(x7 = x1∀ x8 : ο . x8)∀ x8 : ο . (∀ x9 . and (prim1 x9 x0) (x4 x7 x9 = x2)x8)x8)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x4 x7 (x3 x8 x9) = x3 (x4 x7 x8) (x4 x7 x9))(∀ x7 . prim1 x7 x0prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x7) x0)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x4 (x3 x7 x8) x9 = x3 (x4 x7 x9) (x4 x8 x9))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0explicit_Field_minus x0 x1 x2 x3 x4 (x3 x7 x8) = x3 (explicit_Field_minus x0 x1 x2 x3 x4 x7) (explicit_Field_minus x0 x1 x2 x3 x4 x8))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 (explicit_Field_minus x0 x1 x2 x3 x4 x7) x8 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x7 x8))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 x7 (explicit_Field_minus x0 x1 x2 x3 x4 x8) = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x7 x8))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)prim1 (prim0 (λ x8 . and (prim1 x8 x0) (∀ x9 : ο . (∀ x10 . and (prim1 x10 x0) (x7 = x6 x8 x10)x9)x9))) x0)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)prim1 (prim0 (λ x8 . and (prim1 x8 x0) (x7 = x6 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) x8))) x0)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11)) = prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))prim0 (λ x10 . and (prim1 x10 x0) (x7 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) x10)) = prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))x7 = x8)(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (x6 (x3 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9)))))) (x3 (x4 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9)))) (x4 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10)))))) (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x6 (x3 (x4 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x14 x16)x15)x15))) (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x14 x16)x15)x15)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x14 . and (prim1 x14 x0) (x7 = x6 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x16 x18)x17)x17))) x14))) (prim0 (λ x14 . and (prim1 x14 x0) (x8 = x6 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x16 x18)x17)x17))) x14)))))) (x3 (x4 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x14 x16)x15)x15))) (prim0 (λ x14 . and (prim1 x14 x0) (x8 = x6 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x16 x18)x17)x17))) x14)))) (x4 (prim0 (λ x14 . and (prim1 x14 x0) (x7 = x6 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x16 x18)x17)x17))) x14))) (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x14 x16)x15)x15))))) = x6 x10 x12)x11)x11)) = x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x7 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))))))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . and (prim1 x10 x0) (x6 (x3 (x4 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x12 . and (prim1 x12 x0) (x7 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x14 x16)x15)x15))) x12))) (prim0 (λ x12 . and (prim1 x12 x0) (x8 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x14 x16)x15)x15))) x12)))))) (x3 (x4 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) (prim0 (λ x12 . and (prim1 x12 x0) (x8 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x14 x16)x15)x15))) x12)))) (x4 (prim0 (λ x12 . and (prim1 x12 x0) (x7 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x14 x16)x15)x15))) x12))) (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))))) = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (x4 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x16 x18)x17)x17))) (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x16 x18)x17)x17)))) (explicit_Field_minus x0 x1 x2 x3 x4 (x4 (prim0 (λ x16 . and (prim1 x16 x0) (x7 = x6 (prim0 (λ x18 . and (prim1 x18 x0) (∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x18 x20)x19)x19))) x16))) (prim0 (λ x16 . and (prim1 x16 x0) (x8 = x6 (prim0 (λ x18 . and (prim1 x18 x0) (∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x18 x20)x19)x19))) x16)))))) (x3 (x4 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x16 x18)x17)x17))) (prim0 (λ x16 . and (prim1 x16 x0) (x8 = x6 (prim0 (λ x18 . and (prim1 x18 x0) (∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x18 x20)x19)x19))) x16)))) (x4 (prim0 (λ x16 . and (prim1 x16 x0) (x7 = x6 (prim0 (λ x18 . and (prim1 x18 x0) (∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x18 x20)x19)x19))) x16))) (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x16 x18)x17)x17))))) = x6 x12 x14)x13)x13))) x10)) = x3 (x4 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10)))) (x4 (prim0 (λ x10 . and (prim1 x10 x0) (x7 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11)))))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim1 (x6 (x3 (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x7 = x6 x9 x11)x10)x10))) (prim0 (λ x9 . and (prim1 x9 x0) (∀ x10 : ο . (∀ x11 . and (prim1 x11 x0) (x8 = x6 x9 x11)x10)x10)))) (x3 (prim0 (λ x9 . and (prim1 x9 x0) (x7 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x7 = x6 x11 x13)x12)x12))) x9))) (prim0 (λ x9 . and (prim1 x9 x0) (x8 = x6 (prim0 (λ x11 . and (prim1 x11 x0) (∀ x12 : ο . (∀ x13 . and (prim1 x13 x0) (x8 = x6 x11 x13)x12)x12))) x9))))) (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x6 (x3 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x14 x16)x15)x15))) (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x14 x16)x15)x15)))) (x3 (prim0 (λ x14 . and (prim1 x14 x0) (x7 = x6 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x16 x18)x17)x17))) x14))) (prim0 (λ x14 . and (prim1 x14 x0) (x8 = x6 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x16 x18)x17)x17))) x14)))) = x6 x10 x12)x11)x11)) = x3 (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x7 = x6 x10 x12)x11)x11))) (prim0 (λ x10 . and (prim1 x10 x0) (∀ x11 : ο . (∀ x12 . and (prim1 x12 x0) (x8 = x6 x10 x12)x11)x11))))(∀ x7 . prim1 x7 (3b429.. x0 (λ x8 . x0) (λ x8 x9 . True) x6)∀ x8 . prim1 x8 (3b429.. x0 (λ x9 . x0) (λ x9 x10 . True) x6)prim0 (λ x10 . and (prim1 x10 x0) (x6 (x3 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13)))) (x3 (prim0 (λ x12 . and (prim1 x12 x0) (x7 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x7 = x6 x14 x16)x15)x15))) x12))) (prim0 (λ x12 . and (prim1 x12 x0) (x8 = x6 (prim0 (λ x14 . and (prim1 x14 x0) (∀ x15 : ο . (∀ x16 . and (prim1 x16 x0) (x8 = x6 x14 x16)x15)x15))) x12)))) = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x6 (x3 (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x7 = x6 x16 x18)x17)x17))) (prim0 (λ x16 . and (prim1 x16 x0) (∀ x17 : ο . (∀ x18 . and (prim1 x18 x0) (x8 = x6 x16 x18)x17)x17)))) (x3 (prim0 (λ x16 . and (prim1 x16 x0) (x7 = x6 (prim0 (λ x18 . and (prim1 x18 x0) (∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x7 = x6 x18 x20)x19)x19))) x16))) (prim0 (λ x16 . and (prim1 x16 x0) (x8 = x6 (prim0 (λ x18 . and (prim1 x18 x0) (∀ x19 : ο . (∀ x20 . and (prim1 x20 x0) (x8 = x6 x18 x20)x19)x19))) x16)))) = x6 x12 x14)x13)x13))) x10)) = x3 (prim0 (λ x10 . and (prim1 x10 x0) (x7 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x7 = x6 x12 x14)x13)x13))) x10))) (prim0 (λ x10 . and (prim1 x10 x0) (x8 = x6 (prim0 (λ x12 . and (prim1 x12 x0) (∀ x13 : ο . (∀ x14 . and (prim1 x14 x0) (x8 = x6 x12 x14)x13)x13))) x10))))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0∀ x10 . prim1 x10 x0x3 (x3 x7 x8) (x3 x9 x10) = x3 (x3 x7 x9) (x3 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 (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)))) (x3 (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)))) = 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 (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)))) (x3 (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)))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (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)))) (x3 (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)))) = 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 (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)))) (x3 (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)))) = x6 (prim0 (λ x13 . and (prim1 x13 x0) (∀ x14 : ο . (∀ x15 . and (prim1 x15 x0) (x6 (x3 (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)))) (x3 (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)))) = 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 (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)))) (x3 (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)))) = x6 x11 x13)x12)x12))))) = x6 (x3 (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) (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) (x9 = 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) (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) (x7 = 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) (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) (x9 = x6 x15 x17)x16)x16))))) = x6 x11 x13)x12)x12)))) (x3 (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) (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) (x9 = 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) (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) (x7 = 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) (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) (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) (x7 = 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) (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) (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) (x7 = 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) (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) (x9 = x6 x17 x19)x18)x18))))) = x6 x13 x15)x14)x14))) x11))))
type
prop
theory
HoTg
name
-
proof
PUZBg..
Megalodon
-
proofgold address
TMYnv..
creator
3834 PrGxv../03f37..
owner
3834 PrGxv../03f37..
term root
e65ea..