Search for blocks/addresses/...

Proofgold Address

address
PUfqwwPuQU6jE6hTCR86az5b4U5rAwyewSa
total
0
mg
-
conjpub
-
current assets
48611../efd4f.. bday: 11789 doc published by PrGVS..
Theorem 9406c.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . In x2 x0∀ x3 . In x3 x0In (x1 x2 x3) x0)∀ x2 : ι → ι → ι → ι . (∀ x3 . In x3 x0∀ x4 . In x4 x0∀ x5 . In x5 x0In (x2 x3 x4 x5) x0)∀ x3 . In x3 x0∀ x4 . In x4 x0∀ x5 : ι → ι → ι . (∀ x6 . In x6 x0∀ x7 . In x7 x0In (x5 x6 x7) x0)∀ x6 : ι → ι → ι . (∀ x7 . In x7 x0∀ x8 . In x8 x0In (x6 x7 x8) x0)∀ x7 . In x7 x0∀ x8 : ι → ι → ι . (∀ x9 . In x9 x0∀ x10 . In x10 x0In (x8 x9 x10) x0)(∀ x9 . In x9 x0(x8 x7 x9 = x9False)False)(∀ x9 . In x9 x0(x8 x9 x7 = x9False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x6 x9 (x8 x9 x10) = x10False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x1 x9 x10 = x8 (x6 x9 x10) (x6 (x6 x9 x7) x7)False)False)(∀ x9 . In x9 x0(x6 x7 x9 = x9False)False)(∀ x9 . In x9 x0(x6 x9 x9 = x7False)False)(∀ x9 . In x9 x0(x5 x7 x9 = x9False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x2 x7 x9 x10 = x10False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0(x2 x9 x7 x10 = x10False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0∀ x11 . In x11 x0∀ x12 . In x12 x0(x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x1 x10 (x1 x9 (x2 x11 x10 x12))))))))))))))))))) = x12False)False)(∀ x9 . In x9 x0∀ x10 . In x10 x0∀ x11 . In x11 x0(x2 x9 x10 (x1 x9 (x5 x10 (x2 x9 x10 (x1 x9 (x5 x10 x11))))) = x11False)False)(x8 x3 x4 = x8 x4 x3False)False (proof)
Known b5371.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13In x4 x0((∀ x14 . In x14 x0∀ x15 . In x15 x0In (x1 x14 x15) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0In (x2 x14 x15) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0In (x3 x14 x15) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0In (x7 x14 x15) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0In (x8 x14 x15 x16) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0In (x9 x14 x15 x16) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0In (x10 x14 x15) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0In (x11 x14 x15) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0In (x12 x14 x15) x0)(∀ x14 . In x14 x0∀ x15 . In x15 x0In (x13 x14 x15) x0)(∀ x14 . In x14 x0x1 x4 x14 = x14)(∀ x14 . In x14 x0x1 x14 x4 = x14)(∀ x14 . In x14 x0∀ x15 . In x15 x0x2 x14 (x1 x14 x15) = x15)(∀ x14 . In x14 x0∀ x15 . In x15 x0x1 x14 (x2 x14 x15) = x15)(∀ x14 . In x14 x0∀ x15 . In x15 x0x3 (x1 x14 x15) x15 = x14)(∀ x14 . In x14 x0∀ x15 . In x15 x0x1 (x3 x14 x15) x15 = x14)(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0x1 x14 x15 = x1 x14 x16x15 = x16)(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0x1 x14 x15 = x1 x16 x15x14 = x16)(∀ x14 . In x14 x0∀ x15 . In x15 x0x5 x14 x15 = x2 (x1 x15 x14) (x1 x14 x15))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0x6 x14 x15 x16 = x2 (x1 x14 (x1 x15 x16)) (x1 (x1 x14 x15) x16))(∀ x14 . In x14 x0∀ x15 . In x15 x0x7 x14 x15 = x2 x14 (x1 x15 x14))(∀ x14 . In x14 x0∀ x15 . In x15 x0x10 x14 x15 = x1 x14 (x1 x15 (x2 x14 x4)))(∀ x14 . In x14 x0∀ x15 . In x15 x0x11 x14 x15 = x1 (x1 (x3 x4 x14) x15) x14)(∀ x14 . In x14 x0∀ x15 . In x15 x0x12 x14 x15 = x1 (x2 x14 x15) (x2 (x2 x14 x4) x4))(∀ x14 . In x14 x0∀ x15 . In x15 x0x13 x14 x15 = x1 (x3 x4 (x3 x4 x14)) (x3 x15 x14))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0x8 x14 x15 x16 = x2 (x1 x15 x14) (x1 x15 (x1 x14 x16)))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0x9 x14 x15 x16 = x3 (x1 (x1 x16 x14) x15) (x1 x14 x15))(∀ x14 . In x14 x0x2 x4 x14 = x14)(∀ x14 . In x14 x0x2 x14 x14 = x4)(∀ x14 . In x14 x0x3 x14 x4 = x14)(∀ x14 . In x14 x0x3 x14 x14 = x4)(∀ x14 . In x14 x0x7 x4 x14 = x14)(∀ x14 . In x14 x0x10 x4 x14 = x14)(∀ x14 . In x14 x0x11 x4 x14 = x14)(∀ x14 . In x14 x0x12 x4 x14 = x14)(∀ x14 . In x14 x0x13 x4 x14 = x14)(∀ x14 . In x14 x0∀ x15 . In x15 x0x8 x4 x14 x15 = x15)(∀ x14 . In x14 x0∀ x15 . In x15 x0x8 x14 x4 x15 = x15)(∀ x14 . In x14 x0∀ x15 . In x15 x0x9 x4 x14 x15 = x15)(∀ x14 . In x14 x0∀ x15 . In x15 x0x9 x14 x4 x15 = x15)∀ x14 . In x14 x0∀ x15 . In x15 x0x1 x14 x15 = x1 x15 x14)False
Known b4782..contra : ∀ x0 : ο . (not x0False)x0
Known notEnotE : ∀ x0 : ο . not x0x0False
Theorem 5fb94.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . ∀ x5 : ι → ι → ι . ∀ x6 : ι → ι → ι → ι . ∀ x7 : ι → ι → ι . ∀ x8 x9 : ι → ι → ι → ι . ∀ x10 x11 x12 x13 : ι → ι → ι . Loop_with_defs_cex1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13In x4 x0(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 (x9 x14 x15 (x12 x16 (x12 x14 (x9 x15 x16 x17))))))))))))))))))) = x17)(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0x9 x14 x15 (x12 x14 (x7 x15 (x9 x14 x15 (x12 x14 (x7 x15 x16))))) = x16)(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0x12 x14 (x12 x15 (x12 x16 x17)) = x12 x15 (x12 x16 (x12 x14 x17)))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0x8 x14 x15 (x10 x16 (x7 x17 x18)) = x10 x16 (x7 x17 (x8 x14 x15 x18)))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0x7 x14 (x7 x15 (x13 x16 (x12 x17 x18))) = x13 x16 (x12 x17 (x7 x14 (x7 x15 x18))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0x10 x14 (x7 x15 (x12 x16 (x10 x17 x18))) = x12 x16 (x10 x17 (x10 x14 (x7 x15 x18))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0x12 x14 (x12 x15 (x10 x16 (x10 x17 x18))) = x10 x16 (x10 x17 (x12 x14 (x12 x15 x18))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0x12 x14 (x12 x15 (x7 x16 (x10 x17 x18))) = x7 x16 (x10 x17 (x12 x14 (x12 x15 x18))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0x12 x14 (x7 x15 (x12 x16 (x10 x17 x18))) = x12 x16 (x10 x17 (x12 x14 (x7 x15 x18))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0x9 x14 x15 (x7 x16 (x12 x17 (x7 x18 x19))) = x12 x17 (x7 x18 (x9 x14 x15 (x7 x16 x19))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0x8 x14 x15 (x12 x16 (x12 x17 (x7 x18 x19))) = x12 x17 (x7 x18 (x8 x14 x15 (x12 x16 x19))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0x8 x14 x15 (x12 x16 (x8 x17 x18 (x7 x19 x20))) = x8 x17 x18 (x7 x19 (x8 x14 x15 (x12 x16 x20))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0x8 x14 x15 (x7 x16 (x9 x17 x18 (x12 x19 x20))) = x9 x17 x18 (x12 x19 (x8 x14 x15 (x7 x16 x20))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x8 x14 x15 (x12 x16 (x12 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x8 x14 x15 (x12 x16 (x12 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x9 x14 x15 (x10 x16 (x12 x17 (x9 x18 x19 (x10 x20 x21)))) = x9 x18 x19 (x10 x20 (x9 x14 x15 (x10 x16 (x12 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x8 x14 x15 (x10 x16 (x12 x17 (x9 x18 x19 (x13 x20 x21)))) = x9 x18 x19 (x13 x20 (x8 x14 x15 (x10 x16 (x12 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x8 x14 x15 (x13 x16 (x12 x17 (x8 x18 x19 (x7 x20 x21)))) = x8 x18 x19 (x7 x20 (x8 x14 x15 (x13 x16 (x12 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x8 x14 x15 (x12 x16 (x10 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x8 x14 x15 (x12 x16 (x10 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x9 x14 x15 (x13 x16 (x12 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x9 x14 x15 (x13 x16 (x12 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x8 x14 x15 (x12 x16 (x12 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x8 x14 x15 (x12 x16 (x12 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x9 x14 x15 (x12 x16 (x12 x17 (x8 x18 x19 (x10 x20 x21)))) = x8 x18 x19 (x10 x20 (x9 x14 x15 (x12 x16 (x12 x17 x21)))))(∀ x14 . In x14 x0∀ x15 . In x15 x0∀ x16 . In x16 x0∀ x17 . In x17 x0∀ x18 . In x18 x0∀ x19 . In x19 x0∀ x20 . In x20 x0∀ x21 . In x21 x0x9 x14 x15 (x12 x16 (x7 x17 (x9 x18 x19 (x12 x20 x21)))) = x9 x18 x19 (x12 x20 (x9 x14 x15 (x12 x16 (x7 x17 x21)))))False (proof)

previous assets