Search for blocks/addresses/...

Proofgold Address

address
PUU3EMsFwhorNe1K8HAYz2PwaXbBTXNefcn
total
0
mg
-
conjpub
-
current assets
b275b../1530e.. bday: 4946 doc published by Pr6Pc..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param ordsuccordsucc : ιι
Definition bijbij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Definition TwoRamseyPropTwoRamseyProp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5x3 x5 x4)or (∀ x4 : ο . (∀ x5 . and (x5x2) (and (equip x0 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)x3 x6 x7))x4)x4) (∀ x4 : ο . (∀ x5 . and (x5x2) (and (equip x1 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)not (x3 x6 x7)))x4)x4)
Conjecture not_TwoRamseyProp_3_3_5not_TwoRamseyProp_3_3_5 : not (TwoRamseyProp 3 3 5)
Conjecture TwoRamseyProp_3_3_6TwoRamseyProp_3_3_6 : TwoRamseyProp 3 3 6
Conjecture not_TwoRamseyProp_3_4_8not_TwoRamseyProp_3_4_8 : not (TwoRamseyProp 3 4 8)
Conjecture not_TwoRamseyProp_3_5_13not_TwoRamseyProp_3_5_13 : not (TwoRamseyProp 3 5 13)
Conjecture not_TwoRamseyProp_3_6_17not_TwoRamseyProp_3_6_17 : not (TwoRamseyProp 3 6 17)
Conjecture not_TwoRamseyProp_3_7_22not_TwoRamseyProp_3_7_22 : not (TwoRamseyProp 3 7 22)
Conjecture 828bc..not_TwoRamseyProp_3_8_27 : not (TwoRamseyProp 3 8 27)
Conjecture ad1c8..not_TwoRamseyProp_3_9_35 : not (TwoRamseyProp 3 9 35)
Conjecture cbbd3..not_TwoRamseyProp_3_10_39 : not (TwoRamseyProp 3 10 39)
Conjecture not_TwoRamseyProp_4_4_17not_TwoRamseyProp_4_4_17 : not (TwoRamseyProp 4 4 17)
Conjecture not_TwoRamseyProp_4_5_24not_TwoRamseyProp_4_5_24 : not (TwoRamseyProp 4 5 24)
Conjecture not_TwoRamseyProp_4_6_35not_TwoRamseyProp_4_6_35 : not (TwoRamseyProp 4 6 35)
Conjecture 7db35..not_TwoRamseyProp_4_7_48 : not (TwoRamseyProp 4 7 48)
Conjecture 2044f..not_TwoRamseyProp_4_8_58 : not (TwoRamseyProp 4 8 58)
Conjecture cecb1..not_TwoRamseyProp_4_9_72 : not (TwoRamseyProp 4 9 72)
Conjecture c7463..not_TwoRamseyProp_5_5_42 : not (TwoRamseyProp 5 5 42)
Conjecture 580f9..not_TwoRamseyProp_5_6_57 : not (TwoRamseyProp 5 6 57)
Conjecture 6a818..not_TwoRamseyProp_5_7_79 : not (TwoRamseyProp 5 7 79)
Conjecture 10514..not_TwoRamseyProp_5_8_100 : not (TwoRamseyProp 5 8 100)
Conjecture ccd3e..not_TwoRamseyProp_6_6_101 : not (TwoRamseyProp 6 6 101)
Conjecture d6f6b..not_TwoRamseyProp_6_7_114 : not (TwoRamseyProp 6 7 114)
Conjecture TwoRamseyProp_3_4_9TwoRamseyProp_3_4_9 : TwoRamseyProp 3 4 9
Conjecture TwoRamseyProp_3_5_14TwoRamseyProp_3_5_14 : TwoRamseyProp 3 5 14
Conjecture TwoRamseyProp_3_6_18TwoRamseyProp_3_6_18 : TwoRamseyProp 3 6 18
Conjecture 2265c..TwoRamseyProp_3_7_23 : TwoRamseyProp 3 7 23
Conjecture a89ea..TwoRamseyProp_3_8_28 : TwoRamseyProp 3 8 28
Conjecture 5b30b..TwoRamseyProp_3_9_36 : TwoRamseyProp 3 9 36
Conjecture 6f9cf..TwoRamseyProp_3_10_42 : TwoRamseyProp 3 10 42
Conjecture TwoRamseyProp_4_4_18TwoRamseyProp_4_4_18 : TwoRamseyProp 4 4 18
Conjecture cc749..TwoRamseyProp_4_5_25 : TwoRamseyProp 4 5 25
Conjecture 8ecff..TwoRamseyProp_4_6_41 : TwoRamseyProp 4 6 41
Conjecture 019f1..TwoRamseyProp_4_7_61 : TwoRamseyProp 4 7 61
Conjecture ae49e..TwoRamseyProp_4_8_84 : TwoRamseyProp 4 8 84
Conjecture 0df9d..TwoRamseyProp_4_9_115 : TwoRamseyProp 4 9 115
Conjecture 4c756..TwoRamseyProp_5_5_48 : TwoRamseyProp 5 5 48
Conjecture bfcef..TwoRamseyProp_5_6_87 : TwoRamseyProp 5 6 87
Conjecture 67a94..TwoRamseyProp_5_7_143 : TwoRamseyProp 5 7 143
Conjecture f57af..TwoRamseyProp_5_8_216 : TwoRamseyProp 5 8 216
Conjecture 184bf..TwoRamseyProp_6_6_165 : TwoRamseyProp 6 6 165
Conjecture 6bc28..TwoRamseyProp_6_7_298 : TwoRamseyProp 6 7 298
Conjecture 6bca8..not_TwoRamseyProp_3_5_Power_3 : not (TwoRamseyProp 3 5 (prim4 3))
Conjecture ff590..not_TwoRamseyProp_3_6_Power_3 : not (TwoRamseyProp 3 6 (prim4 3))
Conjecture 4618e..not_TwoRamseyProp_3_6_Power_4 : not (TwoRamseyProp 3 6 (prim4 4))
Conjecture 54668..not_TwoRamseyProp_3_7_Power_3 : not (TwoRamseyProp 3 7 (prim4 3))
Conjecture 1d99f..not_TwoRamseyProp_3_7_Power_4 : not (TwoRamseyProp 3 7 (prim4 4))
Conjecture df26e..not_TwoRamseyProp_3_8_Power_3 : not (TwoRamseyProp 3 8 (prim4 3))
Conjecture b6366..not_TwoRamseyProp_3_8_Power_4 : not (TwoRamseyProp 3 8 (prim4 4))
Conjecture 69d43..not_TwoRamseyProp_3_9_Power_3 : not (TwoRamseyProp 3 9 (prim4 3))
Conjecture f990b..not_TwoRamseyProp_3_9_Power_4 : not (TwoRamseyProp 3 9 (prim4 4))
Conjecture 976d2..not_TwoRamseyProp_3_9_Power_5 : not (TwoRamseyProp 3 9 (prim4 5))
Conjecture 7f909..not_TwoRamseyProp_3_10_Power_3 : not (TwoRamseyProp 3 10 (prim4 3))
Conjecture a1e0f..not_TwoRamseyProp_3_10_Power_4 : not (TwoRamseyProp 3 10 (prim4 4))
Conjecture 0c824..not_TwoRamseyProp_3_10_Power_5 : not (TwoRamseyProp 3 10 (prim4 5))
Conjecture ce62b..not_TwoRamseyProp_4_4_Power_3 : not (TwoRamseyProp 4 4 (prim4 3))
Conjecture 485cd..not_TwoRamseyProp_4_4_Power_4 : not (TwoRamseyProp 4 4 (prim4 4))
Conjecture fe972..not_TwoRamseyProp_4_5_Power_3 : not (TwoRamseyProp 4 5 (prim4 3))
Conjecture 5b30a..not_TwoRamseyProp_4_5_Power_4 : not (TwoRamseyProp 4 5 (prim4 4))
Conjecture 33278..not_TwoRamseyProp_4_6_Power_3 : not (TwoRamseyProp 4 6 (prim4 3))
Conjecture f5ebc..not_TwoRamseyProp_4_6_Power_4 : not (TwoRamseyProp 4 6 (prim4 4))
Conjecture not_TwoRamseyProp_4_6_Power_5not_TwoRamseyProp_4_6_Power_5 : not (TwoRamseyProp 4 6 (prim4 5))
Conjecture e1864..not_TwoRamseyProp_4_7_Power_3 : not (TwoRamseyProp 4 7 (prim4 3))
Conjecture a1968..not_TwoRamseyProp_4_7_Power_4 : not (TwoRamseyProp 4 7 (prim4 4))
Conjecture not_TwoRamseyProp_4_7_Power_5not_TwoRamseyProp_4_7_Power_5 : not (TwoRamseyProp 4 7 (prim4 5))
Conjecture 95a55..not_TwoRamseyProp_4_8_Power_3 : not (TwoRamseyProp 4 8 (prim4 3))
Conjecture fa29b..not_TwoRamseyProp_4_8_Power_4 : not (TwoRamseyProp 4 8 (prim4 4))
Conjecture not_TwoRamseyProp_4_8_Power_5not_TwoRamseyProp_4_8_Power_5 : not (TwoRamseyProp 4 8 (prim4 5))
Conjecture 8b769..not_TwoRamseyProp_4_9_Power_3 : not (TwoRamseyProp 4 9 (prim4 3))
Conjecture 5914c..not_TwoRamseyProp_4_9_Power_4 : not (TwoRamseyProp 4 9 (prim4 4))
Conjecture not_TwoRamseyProp_4_9_Power_5not_TwoRamseyProp_4_9_Power_5 : not (TwoRamseyProp 4 9 (prim4 5))
Conjecture aaf47..not_TwoRamseyProp_4_9_Power_6 : not (TwoRamseyProp 4 9 (prim4 6))
Conjecture cd2fd..not_TwoRamseyProp_5_5_Power_3 : not (TwoRamseyProp 5 5 (prim4 3))
Conjecture not_TwoRamseyProp_5_5_Power_4not_TwoRamseyProp_5_5_Power_4 : not (TwoRamseyProp 5 5 (prim4 4))
Conjecture 181da..not_TwoRamseyProp_5_5_Power_5 : not (TwoRamseyProp 5 5 (prim4 5))
Conjecture eff2c..not_TwoRamseyProp_5_6_Power_3 : not (TwoRamseyProp 5 6 (prim4 3))
Conjecture c0836..not_TwoRamseyProp_5_6_Power_4 : not (TwoRamseyProp 5 6 (prim4 4))
Conjecture not_TwoRamseyProp_5_6_Power_5not_TwoRamseyProp_5_6_Power_5 : not (TwoRamseyProp 5 6 (prim4 5))
Conjecture 73405..not_TwoRamseyProp_5_7_Power_3 : not (TwoRamseyProp 5 7 (prim4 3))
Conjecture c6b25..not_TwoRamseyProp_5_7_Power_4 : not (TwoRamseyProp 5 7 (prim4 4))
Conjecture not_TwoRamseyProp_5_7_Power_5not_TwoRamseyProp_5_7_Power_5 : not (TwoRamseyProp 5 7 (prim4 5))
Conjecture 5b9e1..not_TwoRamseyProp_5_7_Power_6 : not (TwoRamseyProp 5 7 (prim4 6))
Conjecture 41978..not_TwoRamseyProp_5_8_Power_3 : not (TwoRamseyProp 5 8 (prim4 3))
Conjecture f4df6..not_TwoRamseyProp_5_8_Power_4 : not (TwoRamseyProp 5 8 (prim4 4))
Conjecture not_TwoRamseyProp_5_8_Power_5not_TwoRamseyProp_5_8_Power_5 : not (TwoRamseyProp 5 8 (prim4 5))
Conjecture cd9fa..not_TwoRamseyProp_5_8_Power_6 : not (TwoRamseyProp 5 8 (prim4 6))
Conjecture 3de2e..not_TwoRamseyProp_6_6_Power_3 : not (TwoRamseyProp 6 6 (prim4 3))
Conjecture 3ce96..not_TwoRamseyProp_6_6_Power_4 : not (TwoRamseyProp 6 6 (prim4 4))
Conjecture not_TwoRamseyProp_6_6_Power_5not_TwoRamseyProp_6_6_Power_5 : not (TwoRamseyProp 6 6 (prim4 5))
Conjecture 129ce..not_TwoRamseyProp_6_6_Power_6 : not (TwoRamseyProp 6 6 (prim4 6))
Conjecture 84f84..not_TwoRamseyProp_6_7_Power_3 : not (TwoRamseyProp 6 7 (prim4 3))
Conjecture c642e..not_TwoRamseyProp_6_7_Power_4 : not (TwoRamseyProp 6 7 (prim4 4))
Conjecture not_TwoRamseyProp_6_7_Power_5not_TwoRamseyProp_6_7_Power_5 : not (TwoRamseyProp 6 7 (prim4 5))
Conjecture 65eeb..not_TwoRamseyProp_6_7_Power_6 : not (TwoRamseyProp 6 7 (prim4 6))
Conjecture TwoRamseyProp_3_4_Power_4TwoRamseyProp_3_4_Power_4 : TwoRamseyProp 3 4 (prim4 4)
Conjecture TwoRamseyProp_3_4_Power_5TwoRamseyProp_3_4_Power_5 : TwoRamseyProp 3 4 (prim4 5)
Conjecture TwoRamseyProp_3_4_Power_6TwoRamseyProp_3_4_Power_6 : TwoRamseyProp 3 4 (prim4 6)
Conjecture TwoRamseyProp_3_4_Power_7TwoRamseyProp_3_4_Power_7 : TwoRamseyProp 3 4 (prim4 7)
Conjecture TwoRamseyProp_3_4_Power_8TwoRamseyProp_3_4_Power_8 : TwoRamseyProp 3 4 (prim4 8)
Conjecture TwoRamseyProp_3_5_Power_4TwoRamseyProp_3_5_Power_4 : TwoRamseyProp 3 5 (prim4 4)
Conjecture TwoRamseyProp_3_5_Power_5TwoRamseyProp_3_5_Power_5 : TwoRamseyProp 3 5 (prim4 5)
Conjecture TwoRamseyProp_3_5_Power_6TwoRamseyProp_3_5_Power_6 : TwoRamseyProp 3 5 (prim4 6)
Conjecture TwoRamseyProp_3_5_Power_7TwoRamseyProp_3_5_Power_7 : TwoRamseyProp 3 5 (prim4 7)
Conjecture TwoRamseyProp_3_5_Power_8TwoRamseyProp_3_5_Power_8 : TwoRamseyProp 3 5 (prim4 8)
Conjecture TwoRamseyProp_3_6_Power_5TwoRamseyProp_3_6_Power_5 : TwoRamseyProp 3 6 (prim4 5)
Conjecture TwoRamseyProp_3_6_Power_6TwoRamseyProp_3_6_Power_6 : TwoRamseyProp 3 6 (prim4 6)
Conjecture TwoRamseyProp_3_6_Power_7TwoRamseyProp_3_6_Power_7 : TwoRamseyProp 3 6 (prim4 7)
Conjecture TwoRamseyProp_3_6_Power_8TwoRamseyProp_3_6_Power_8 : TwoRamseyProp 3 6 (prim4 8)
Conjecture TwoRamseyProp_3_7_Power_5TwoRamseyProp_3_7_Power_5 : TwoRamseyProp 3 7 (prim4 5)
Conjecture TwoRamseyProp_3_7_Power_6TwoRamseyProp_3_7_Power_6 : TwoRamseyProp 3 7 (prim4 6)
Conjecture TwoRamseyProp_3_7_Power_7TwoRamseyProp_3_7_Power_7 : TwoRamseyProp 3 7 (prim4 7)
Conjecture TwoRamseyProp_3_7_Power_8TwoRamseyProp_3_7_Power_8 : TwoRamseyProp 3 7 (prim4 8)
Conjecture 73684..TwoRamseyProp_3_8_Power_5 : TwoRamseyProp 3 8 (prim4 5)
Conjecture TwoRamseyProp_3_8_Power_6TwoRamseyProp_3_8_Power_6 : TwoRamseyProp 3 8 (prim4 6)
Conjecture TwoRamseyProp_3_8_Power_7TwoRamseyProp_3_8_Power_7 : TwoRamseyProp 3 8 (prim4 7)
Conjecture TwoRamseyProp_3_8_Power_8TwoRamseyProp_3_8_Power_8 : TwoRamseyProp 3 8 (prim4 8)
Conjecture TwoRamseyProp_3_9_Power_6TwoRamseyProp_3_9_Power_6 : TwoRamseyProp 3 9 (prim4 6)
Conjecture TwoRamseyProp_3_9_Power_7TwoRamseyProp_3_9_Power_7 : TwoRamseyProp 3 9 (prim4 7)
Conjecture TwoRamseyProp_3_9_Power_8TwoRamseyProp_3_9_Power_8 : TwoRamseyProp 3 9 (prim4 8)
Conjecture TwoRamseyProp_3_10_Power_6TwoRamseyProp_3_10_Power_6 : TwoRamseyProp 3 10 (prim4 6)
Conjecture TwoRamseyProp_3_10_Power_7TwoRamseyProp_3_10_Power_7 : TwoRamseyProp 3 10 (prim4 7)
Conjecture TwoRamseyProp_3_10_Power_8TwoRamseyProp_3_10_Power_8 : TwoRamseyProp 3 10 (prim4 8)
Conjecture TwoRamseyProp_4_4_Power_5TwoRamseyProp_4_4_Power_5 : TwoRamseyProp 4 4 (prim4 5)
Conjecture TwoRamseyProp_4_4_Power_6TwoRamseyProp_4_4_Power_6 : TwoRamseyProp 4 4 (prim4 6)
Conjecture TwoRamseyProp_4_4_Power_7TwoRamseyProp_4_4_Power_7 : TwoRamseyProp 4 4 (prim4 7)
Conjecture TwoRamseyProp_4_4_Power_8TwoRamseyProp_4_4_Power_8 : TwoRamseyProp 4 4 (prim4 8)
Conjecture TwoRamseyProp_4_5_Power_5TwoRamseyProp_4_5_Power_5 : TwoRamseyProp 4 5 (prim4 5)
Conjecture TwoRamseyProp_4_5_Power_6TwoRamseyProp_4_5_Power_6 : TwoRamseyProp 4 5 (prim4 6)
Conjecture TwoRamseyProp_4_5_Power_7TwoRamseyProp_4_5_Power_7 : TwoRamseyProp 4 5 (prim4 7)
Conjecture TwoRamseyProp_4_5_Power_8TwoRamseyProp_4_5_Power_8 : TwoRamseyProp 4 5 (prim4 8)
Conjecture 1e5e4..TwoRamseyProp_4_6_Power_6 : TwoRamseyProp 4 6 (prim4 6)
Conjecture TwoRamseyProp_4_6_Power_7TwoRamseyProp_4_6_Power_7 : TwoRamseyProp 4 6 (prim4 7)
Conjecture TwoRamseyProp_4_6_Power_8TwoRamseyProp_4_6_Power_8 : TwoRamseyProp 4 6 (prim4 8)
Conjecture 0ea3e..TwoRamseyProp_4_7_Power_6 : TwoRamseyProp 4 7 (prim4 6)
Conjecture TwoRamseyProp_4_7_Power_7TwoRamseyProp_4_7_Power_7 : TwoRamseyProp 4 7 (prim4 7)
Conjecture TwoRamseyProp_4_7_Power_8TwoRamseyProp_4_7_Power_8 : TwoRamseyProp 4 7 (prim4 8)
Conjecture TwoRamseyProp_4_8_Power_7TwoRamseyProp_4_8_Power_7 : TwoRamseyProp 4 8 (prim4 7)
Conjecture TwoRamseyProp_4_8_Power_8TwoRamseyProp_4_8_Power_8 : TwoRamseyProp 4 8 (prim4 8)
Conjecture 75d1d..TwoRamseyProp_4_9_Power_7 : TwoRamseyProp 4 9 (prim4 7)
Conjecture TwoRamseyProp_4_9_Power_8TwoRamseyProp_4_9_Power_8 : TwoRamseyProp 4 9 (prim4 8)
Conjecture TwoRamseyProp_5_5_Power_6TwoRamseyProp_5_5_Power_6 : TwoRamseyProp 5 5 (prim4 6)
Conjecture TwoRamseyProp_5_5_Power_7TwoRamseyProp_5_5_Power_7 : TwoRamseyProp 5 5 (prim4 7)
Conjecture TwoRamseyProp_5_5_Power_8TwoRamseyProp_5_5_Power_8 : TwoRamseyProp 5 5 (prim4 8)
Conjecture 4005b..TwoRamseyProp_5_6_Power_7 : TwoRamseyProp 5 6 (prim4 7)
Conjecture TwoRamseyProp_5_6_Power_8TwoRamseyProp_5_6_Power_8 : TwoRamseyProp 5 6 (prim4 8)
Conjecture c6e22..TwoRamseyProp_5_7_Power_8 : TwoRamseyProp 5 7 (prim4 8)
Conjecture 31b50..TwoRamseyProp_5_8_Power_8 : TwoRamseyProp 5 8 (prim4 8)
Conjecture c30d4..TwoRamseyProp_6_6_Power_8 : TwoRamseyProp 6 6 (prim4 8)
Conjecture f3e4e..TwoRamseyProp_3_10_40 : TwoRamseyProp 3 10 40
Conjecture 47305..TwoRamseyProp_3_10_41 : TwoRamseyProp 3 10 41
Conjecture 9cb5e..TwoRamseyProp_4_6_36 : TwoRamseyProp 4 6 36
Conjecture 130f8..TwoRamseyProp_4_6_40 : TwoRamseyProp 4 6 40
Conjecture 9a8e3..TwoRamseyProp_4_7_49 : TwoRamseyProp 4 7 49
Conjecture 937b9..TwoRamseyProp_4_7_60 : TwoRamseyProp 4 7 60
Conjecture 750bb..TwoRamseyProp_4_8_59 : TwoRamseyProp 4 8 59
Conjecture faf2b..TwoRamseyProp_4_8_83 : TwoRamseyProp 4 8 83
Conjecture 0b30c..TwoRamseyProp_4_9_73 : TwoRamseyProp 4 9 73
Conjecture beb3c..TwoRamseyProp_4_9_114 : TwoRamseyProp 4 9 114
Conjecture e5b63..TwoRamseyProp_5_5_43 : TwoRamseyProp 5 5 43
Conjecture e1165..TwoRamseyProp_5_5_47 : TwoRamseyProp 5 5 47
Conjecture b5144..TwoRamseyProp_5_6_58 : TwoRamseyProp 5 6 58
Conjecture dba4b..TwoRamseyProp_5_6_86 : TwoRamseyProp 5 6 86
Conjecture c8d15..TwoRamseyProp_5_7_80 : TwoRamseyProp 5 7 80
Conjecture 89daf..TwoRamseyProp_5_7_142 : TwoRamseyProp 5 7 142
Conjecture 11f94..TwoRamseyProp_5_8_101 : TwoRamseyProp 5 8 101
Conjecture 3f085..TwoRamseyProp_5_8_215 : TwoRamseyProp 5 8 215
Conjecture 13553..TwoRamseyProp_6_6_102 : TwoRamseyProp 6 6 102
Conjecture 54fb4..TwoRamseyProp_6_6_164 : TwoRamseyProp 6 6 164
Conjecture 9c5ae..TwoRamseyProp_6_7_115 : TwoRamseyProp 6 7 115
Conjecture bb403..TwoRamseyProp_6_7_297 : TwoRamseyProp 6 7 297

previous assets