Search for blocks/addresses/...

Proofgold Address

address
PUKgXQUDhNEfyr8RFM5Eowxsz33m1h68k4B
total
0
mg
-
conjpub
-
current assets
10af6../e31c3.. bday: 14577 doc published by Pr4zB..
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param SubqSubq : ιιο
Param atleastpatleastp : ιιο
Param ordsuccordsucc : ιι
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known a6a5a.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9x8∀ x10 : ι → ο . x10 x0x10 x1x10 x2x10 x3x10 x4x10 x5x10 x6x10 x7x10 x9)∀ x9 . x9x8atleastp 3 x9∀ x10 : ο . (x0x9x1x9x2x9x10)(x0x9x1x9x3x9x10)(x0x9x2x9x3x9x10)(x1x9x2x9x3x9x10)(x0x9x1x9x4x9x10)(x0x9x2x9x4x9x10)(x1x9x2x9x4x9x10)(x0x9x3x9x4x9x10)(x1x9x3x9x4x9x10)(x2x9x3x9x4x9x10)(x0x9x1x9x5x9x10)(x0x9x2x9x5x9x10)(x1x9x2x9x5x9x10)(x0x9x3x9x5x9x10)(x1x9x3x9x5x9x10)(x2x9x3x9x5x9x10)(x0x9x4x9x5x9x10)(x1x9x4x9x5x9x10)(x2x9x4x9x5x9x10)(x3x9x4x9x5x9x10)(x0x9x1x9x6x9x10)(x0x9x2x9x6x9x10)(x1x9x2x9x6x9x10)(x0x9x3x9x6x9x10)(x1x9x3x9x6x9x10)(x2x9x3x9x6x9x10)(x0x9x4x9x6x9x10)(x1x9x4x9x6x9x10)(x2x9x4x9x6x9x10)(x3x9x4x9x6x9x10)(x0x9x5x9x6x9x10)(x1x9x5x9x6x9x10)(x2x9x5x9x6x9x10)(x3x9x5x9x6x9x10)(x4x9x5x9x6x9x10)(x0x9x1x9x7x9x10)(x0x9x2x9x7x9x10)(x1x9x2x9x7x9x10)(x0x9x3x9x7x9x10)(x1x9x3x9x7x9x10)(x2x9x3x9x7x9x10)(x0x9x4x9x7x9x10)(x1x9x4x9x7x9x10)(x2x9x4x9x7x9x10)(x3x9x4x9x7x9x10)(x0x9x5x9x7x9x10)(x1x9x5x9x7x9x10)(x2x9x5x9x7x9x10)(x3x9x5x9x7x9x10)(x4x9x5x9x7x9x10)(x0x9x6x9x7x9x10)(x1x9x6x9x7x9x10)(x2x9x6x9x7x9x10)(x3x9x6x9x7x9x10)(x4x9x6x9x7x9x10)(x5x9x6x9x7x9x10)x10
Known c14f6.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9x8∀ x10 : ι → ο . x10 x0x10 x1x10 x2x10 x3x10 x4x10 x5x10 x6x10 x7x10 x9)∀ x9 . x9x8atleastp 4 x9∀ x10 : ο . (x0x9x1x9x2x9x3x9x10)(x0x9x1x9x2x9x4x9x10)(x0x9x1x9x3x9x4x9x10)(x0x9x2x9x3x9x4x9x10)(x1x9x2x9x3x9x4x9x10)(x0x9x1x9x2x9x5x9x10)(x0x9x1x9x3x9x5x9x10)(x0x9x2x9x3x9x5x9x10)(x1x9x2x9x3x9x5x9x10)(x0x9x1x9x4x9x5x9x10)(x0x9x2x9x4x9x5x9x10)(x1x9x2x9x4x9x5x9x10)(x0x9x3x9x4x9x5x9x10)(x1x9x3x9x4x9x5x9x10)(x2x9x3x9x4x9x5x9x10)(x0x9x1x9x2x9x6x9x10)(x0x9x1x9x3x9x6x9x10)(x0x9x2x9x3x9x6x9x10)(x1x9x2x9x3x9x6x9x10)(x0x9x1x9x4x9x6x9x10)(x0x9x2x9x4x9x6x9x10)(x1x9x2x9x4x9x6x9x10)(x0x9x3x9x4x9x6x9x10)(x1x9x3x9x4x9x6x9x10)(x2x9x3x9x4x9x6x9x10)(x0x9x1x9x5x9x6x9x10)(x0x9x2x9x5x9x6x9x10)(x1x9x2x9x5x9x6x9x10)(x0x9x3x9x5x9x6x9x10)(x1x9x3x9x5x9x6x9x10)(x2x9x3x9x5x9x6x9x10)(x0x9x4x9x5x9x6x9x10)(x1x9x4x9x5x9x6x9x10)(x2x9x4x9x5x9x6x9x10)(x3x9x4x9x5x9x6x9x10)(x0x9x1x9x2x9x7x9x10)(x0x9x1x9x3x9x7x9x10)(x0x9x2x9x3x9x7x9x10)(x1x9x2x9x3x9x7x9x10)(x0x9x1x9x4x9x7x9x10)(x0x9x2x9x4x9x7x9x10)(x1x9x2x9x4x9x7x9x10)(x0x9x3x9x4x9x7x9x10)(x1x9x3x9x4x9x7x9x10)(x2x9x3x9x4x9x7x9x10)(x0x9x1x9x5x9x7x9x10)(x0x9x2x9x5x9x7x9x10)(x1x9x2x9x5x9x7x9x10)(x0x9x3x9x5x9x7x9x10)(x1x9x3x9x5x9x7x9x10)(x2x9x3x9x5x9x7x9x10)(x0x9x4x9x5x9x7x9x10)(x1x9x4x9x5x9x7x9x10)(x2x9x4x9x5x9x7x9x10)(x3x9x4x9x5x9x7x9x10)(x0x9x1x9x6x9x7x9x10)(x0x9x2x9x6x9x7x9x10)(x1x9x2x9x6x9x7x9x10)(x0x9x3x9x6x9x7x9x10)(x1x9x3x9x6x9x7x9x10)(x2x9x3x9x6x9x7x9x10)(x0x9x4x9x6x9x7x9x10)(x1x9x4x9x6x9x7x9x10)(x2x9x4x9x6x9x7x9x10)(x3x9x4x9x6x9x7x9x10)(x0x9x5x9x6x9x7x9x10)(x1x9x5x9x6x9x7x9x10)(x2x9x5x9x6x9x7x9x10)(x3x9x5x9x6x9x7x9x10)(x4x9x5x9x6x9x7x9x10)x10
Theorem 70922.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9x8∀ x10 : ι → ο . x10 x0x10 x1x10 x2x10 x3x10 x4x10 x5x10 x6x10 x7x10 x9)(x0 = x1∀ x9 : ο . x9)(x0 = x2∀ x9 : ο . x9)(x1 = x2∀ x9 : ο . x9)(x0 = x3∀ x9 : ο . x9)(x1 = x3∀ x9 : ο . x9)(x2 = x3∀ x9 : ο . x9)(x0 = x4∀ x9 : ο . x9)(x1 = x4∀ x9 : ο . x9)(x2 = x4∀ x9 : ο . x9)(x3 = x4∀ x9 : ο . x9)(x0 = x5∀ x9 : ο . x9)(x1 = x5∀ x9 : ο . x9)(x2 = x5∀ x9 : ο . x9)(x3 = x5∀ x9 : ο . x9)(x4 = x5∀ x9 : ο . x9)(x0 = x6∀ x9 : ο . x9)(x1 = x6∀ x9 : ο . x9)(x2 = x6∀ x9 : ο . x9)(x3 = x6∀ x9 : ο . x9)(x4 = x6∀ x9 : ο . x9)(x5 = x6∀ x9 : ο . x9)(x0 = x7∀ x9 : ο . x9)(x1 = x7∀ x9 : ο . x9)(x2 = x7∀ x9 : ο . x9)(x3 = x7∀ x9 : ο . x9)(x4 = x7∀ x9 : ο . x9)(x5 = x7∀ x9 : ο . x9)(x6 = x7∀ x9 : ο . x9)∀ x9 : ι → ι → ο . (∀ x10 : ο . x9 x0 x1x10)(∀ x10 : ο . x9 x0 x2x10)(∀ x10 : ο . x9 x1 x2x10)(∀ x10 : ο . x9 x0 x3x10)(∀ x10 : ο . x9 x1 x3x10)x9 x2 x3(∀ x10 : ο . x9 x0 x4x10)x9 x1 x4(∀ x10 : ο . x9 x2 x4x10)x9 x3 x4(∀ x10 : ο . x9 x0 x5x10)x9 x1 x5x9 x2 x5(∀ x10 : ο . x9 x3 x5x10)(∀ x10 : ο . x9 x4 x5x10)x9 x0 x6(∀ x10 : ο . x9 x1 x6x10)(∀ x10 : ο . x9 x2 x6x10)x9 x3 x6(∀ x10 : ο . x9 x4 x6x10)x9 x5 x6x9 x0 x7(∀ x10 : ο . x9 x1 x7x10)x9 x2 x7(∀ x10 : ο . x9 x3 x7x10)x9 x4 x7(∀ x10 : ο . x9 x5 x7x10)(∀ x10 : ο . x9 x6 x7x10)and (∀ x10 . x10x8atleastp 3 x10∀ x11 : ο . (∀ x12 . x12x10∀ x13 . x13x10(x12 = x13∀ x14 : ο . x14)not (x9 x12 x13)x11)x11) (∀ x10 . x10x8atleastp 4 x10∀ x11 : ο . (∀ x12 . x12x10∀ x13 . x13x10(x12 = x13∀ x14 : ο . x14)x9 x12 x13x11)x11) (proof)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition TwoRamseyProp_atleastp := λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5x3 x5 x4)or (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x0 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)x3 x6 x7))x4)x4) (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x1 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)not (x3 x6 x7)))x4)x4)
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem 052c4.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 x8 . (∀ x9 . x9x8∀ x10 : ι → ο . x10 x0x10 x1x10 x2x10 x3x10 x4x10 x5x10 x6x10 x7x10 x9)(x0 = x1∀ x9 : ο . x9)(x0 = x2∀ x9 : ο . x9)(x1 = x2∀ x9 : ο . x9)(x0 = x3∀ x9 : ο . x9)(x1 = x3∀ x9 : ο . x9)(x2 = x3∀ x9 : ο . x9)(x0 = x4∀ x9 : ο . x9)(x1 = x4∀ x9 : ο . x9)(x2 = x4∀ x9 : ο . x9)(x3 = x4∀ x9 : ο . x9)(x0 = x5∀ x9 : ο . x9)(x1 = x5∀ x9 : ο . x9)(x2 = x5∀ x9 : ο . x9)(x3 = x5∀ x9 : ο . x9)(x4 = x5∀ x9 : ο . x9)(x0 = x6∀ x9 : ο . x9)(x1 = x6∀ x9 : ο . x9)(x2 = x6∀ x9 : ο . x9)(x3 = x6∀ x9 : ο . x9)(x4 = x6∀ x9 : ο . x9)(x5 = x6∀ x9 : ο . x9)(x0 = x7∀ x9 : ο . x9)(x1 = x7∀ x9 : ο . x9)(x2 = x7∀ x9 : ο . x9)(x3 = x7∀ x9 : ο . x9)(x4 = x7∀ x9 : ο . x9)(x5 = x7∀ x9 : ο . x9)(x6 = x7∀ x9 : ο . x9)not (TwoRamseyProp_atleastp 3 4 x8) (proof)
Param TwoRamseyPropTwoRamseyProp : ιιιο
Known cases_8cases_8 : ∀ x0 . x08∀ x1 : ι → ο . x1 0x1 1x1 2x1 3x1 4x1 5x1 6x1 7x1 x0
Known neq_0_1neq_0_1 : 0 = 1∀ x0 : ο . x0
Known neq_0_2neq_0_2 : 0 = 2∀ x0 : ο . x0
Known neq_1_2neq_1_2 : 1 = 2∀ x0 : ο . x0
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known neq_3_0neq_3_0 : 3 = 0∀ x0 : ο . x0
Known neq_3_1neq_3_1 : 3 = 1∀ x0 : ο . x0
Known neq_3_2neq_3_2 : 3 = 2∀ x0 : ο . x0
Known neq_4_0neq_4_0 : 4 = 0∀ x0 : ο . x0
Known neq_4_1neq_4_1 : 4 = 1∀ x0 : ο . x0
Known neq_4_2neq_4_2 : 4 = 2∀ x0 : ο . x0
Known neq_4_3neq_4_3 : 4 = 3∀ x0 : ο . x0
Known neq_5_0neq_5_0 : 5 = 0∀ x0 : ο . x0
Known neq_5_1neq_5_1 : 5 = 1∀ x0 : ο . x0
Known neq_5_2neq_5_2 : 5 = 2∀ x0 : ο . x0
Known neq_5_3neq_5_3 : 5 = 3∀ x0 : ο . x0
Known neq_5_4neq_5_4 : 5 = 4∀ x0 : ο . x0
Known neq_6_0neq_6_0 : 6 = 0∀ x0 : ο . x0
Known neq_6_1neq_6_1 : 6 = 1∀ x0 : ο . x0
Known neq_6_2neq_6_2 : 6 = 2∀ x0 : ο . x0
Known neq_6_3neq_6_3 : 6 = 3∀ x0 : ο . x0
Known neq_6_4neq_6_4 : 6 = 4∀ x0 : ο . x0
Known neq_6_5neq_6_5 : 6 = 5∀ x0 : ο . x0
Known neq_7_0neq_7_0 : 7 = 0∀ x0 : ο . x0
Known neq_7_1neq_7_1 : 7 = 1∀ x0 : ο . x0
Known neq_7_2neq_7_2 : 7 = 2∀ x0 : ο . x0
Known neq_7_3neq_7_3 : 7 = 3∀ x0 : ο . x0
Known neq_7_4neq_7_4 : 7 = 4∀ x0 : ο . x0
Known neq_7_5neq_7_5 : 7 = 5∀ x0 : ο . x0
Known neq_7_6neq_7_6 : 7 = 6∀ x0 : ο . x0
Known TwoRamseyProp_atleastp_atleastp : ∀ x0 x1 x2 x3 x4 . TwoRamseyProp x0 x2 x4atleastp x1 x0atleastp x3 x2TwoRamseyProp_atleastp x1 x3 x4
Known atleastp_ref : ∀ x0 . atleastp x0 x0
Theorem not_TwoRamseyProp_3_4_8not_TwoRamseyProp_3_4_8 : not (TwoRamseyProp 3 4 8) (proof)
Param UPairUPair : ιιι
Param SingSing : ιι
Known In_Power_3_cases_impred : ∀ x0 . x0prim4 3∀ x1 : ο . (x0 = 0x1)(x0 = 1x1)(x0 = Sing 1x1)(x0 = 2x1)(x0 = Sing 2x1)(x0 = UPair 0 2x1)(x0 = UPair 1 2x1)(x0 = 3x1)x1
Known not_Empty_eq_Sing : ∀ x0 . 0 = Sing x0∀ x1 : ο . x1
Definition nInnIn := λ x0 x1 . not (x0x1)
Known nIn_not_eq_Sing : ∀ x0 x1 . nIn x0 x1x1 = Sing x0∀ x2 : ο . x2
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known nIn_2_1nIn_2_1 : nIn 2 1
Known neq_2_1neq_2_1 : 2 = 1∀ x0 : ο . x0
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known In_0_2In_0_2 : 02
Known not_Empty_eq_UPair : ∀ x0 x1 . 0 = UPair x0 x1∀ x2 : ο . x2
Known nIn_not_eq_UPair_2 : ∀ x0 x1 x2 . nIn x1 x2x2 = UPair x0 x1∀ x3 : ο . x3
Known nIn_not_eq_UPair_1 : ∀ x0 x1 x2 . nIn x0 x2x2 = UPair x0 x1∀ x3 : ο . x3
Known UPairEUPairE : ∀ x0 x1 x2 . x0UPair x1 x2or (x0 = x1) (x0 = x2)
Known neq_1_0neq_1_0 : 1 = 0∀ x0 : ο . x0
Known In_0_3In_0_3 : 03
Known In_1_3In_1_3 : 13
Theorem not_TwoRamseyProp_atleast_3_4_Power_3 : not (TwoRamseyProp_atleastp 3 4 (prim4 3)) (proof)
Param nat_pnat_p : ιο
Known nat_In_atleastp : ∀ x0 . nat_p x0∀ x1 . x1x0atleastp x1 x0
Known nat_5nat_5 : nat_p 5
Known In_4_5In_4_5 : 45
Theorem 6bca8..not_TwoRamseyProp_3_5_Power_3 : not (TwoRamseyProp 3 5 (prim4 3)) (proof)
Known nat_6nat_6 : nat_p 6
Known In_4_6In_4_6 : 46
Theorem ff590..not_TwoRamseyProp_3_6_Power_3 : not (TwoRamseyProp 3 6 (prim4 3)) (proof)
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Theorem nat_7nat_7 : nat_p 7 (proof)
Theorem nat_8nat_8 : nat_p 8 (proof)
Theorem nat_9nat_9 : nat_p 9 (proof)
Theorem nat_10nat_10 : nat_p 10 (proof)
Known In_4_7In_4_7 : 47
Theorem 54668..not_TwoRamseyProp_3_7_Power_3 : not (TwoRamseyProp 3 7 (prim4 3)) (proof)
Known In_4_8In_4_8 : 48
Theorem df26e..not_TwoRamseyProp_3_8_Power_3 : not (TwoRamseyProp 3 8 (prim4 3)) (proof)
Known In_4_9In_4_9 : 49
Theorem 69d43..not_TwoRamseyProp_3_9_Power_3 : not (TwoRamseyProp 3 9 (prim4 3)) (proof)
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known In_3_9In_3_9 : 39
Theorem 35ffd.. : 410 (proof)
Theorem 7f909..not_TwoRamseyProp_3_10_Power_3 : not (TwoRamseyProp 3 10 (prim4 3)) (proof)
Known nat_4nat_4 : nat_p 4
Known In_3_4In_3_4 : 34
Theorem ce62b..not_TwoRamseyProp_4_4_Power_3 : not (TwoRamseyProp 4 4 (prim4 3)) (proof)
Theorem fe972..not_TwoRamseyProp_4_5_Power_3 : not (TwoRamseyProp 4 5 (prim4 3)) (proof)
Theorem 33278..not_TwoRamseyProp_4_6_Power_3 : not (TwoRamseyProp 4 6 (prim4 3)) (proof)
Theorem e1864..not_TwoRamseyProp_4_7_Power_3 : not (TwoRamseyProp 4 7 (prim4 3)) (proof)
Theorem 95a55..not_TwoRamseyProp_4_8_Power_3 : not (TwoRamseyProp 4 8 (prim4 3)) (proof)
Theorem 8b769..not_TwoRamseyProp_4_9_Power_3 : not (TwoRamseyProp 4 9 (prim4 3)) (proof)
Known In_3_5In_3_5 : 35
Theorem cd2fd..not_TwoRamseyProp_5_5_Power_3 : not (TwoRamseyProp 5 5 (prim4 3)) (proof)
Theorem eff2c..not_TwoRamseyProp_5_6_Power_3 : not (TwoRamseyProp 5 6 (prim4 3)) (proof)
Theorem 73405..not_TwoRamseyProp_5_7_Power_3 : not (TwoRamseyProp 5 7 (prim4 3)) (proof)
Theorem 41978..not_TwoRamseyProp_5_8_Power_3 : not (TwoRamseyProp 5 8 (prim4 3)) (proof)
Known In_3_6In_3_6 : 36
Theorem 3de2e..not_TwoRamseyProp_6_6_Power_3 : not (TwoRamseyProp 6 6 (prim4 3)) (proof)
Theorem 84f84..not_TwoRamseyProp_6_7_Power_3 : not (TwoRamseyProp 6 7 (prim4 3)) (proof)

previous assets