Search for blocks/addresses/...

Proofgold Address

address
PUcCZDbCmtRmpyrkS6Q9DdiyvfAQDXEGMUy
total
0
mg
-
conjpub
-
current assets
073b7../82109.. bday: 29773 doc published by PrQUS..
Param nat_pnat_p : ιο
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param finitefinite : ιο
Definition infiniteinfinite := λ x0 . not (finite x0)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
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
Param ordsuccordsucc : ιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known FalseEFalseE : False∀ x0 : ο . x0
Known infinite_Finite_Subq_exinfinite_Finite_Subq_ex : ∀ x0 . infinite x0∀ x1 . nat_p x1∀ x2 : ο . (∀ x3 . and (x3x0) (equip x3 x1)x2)x2
Definition nInnIn := λ x0 x1 . not (x0x1)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known Subq_EmptySubq_Empty : ∀ x0 . 0x0
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Known equip_0_Emptyequip_0_Empty : ∀ x0 . equip x0 0x0 = 0
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Param binunionbinunion : ιιι
Param SingSing : ιι
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known nat_primrec_Snat_primrec_S : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Param omegaomega : ι
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition atleastpatleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3x2)x2
Known atleastp_omega_infiniteatleastp_omega_infinite : ∀ x0 . atleastp omega x0infinite x0
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Param ordinalordinal : ιο
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known least_ordinal_exleast_ordinal_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . and (ordinal x2) (x0 x2)x1)x1)∀ x1 : ο . (∀ x2 . and (and (ordinal x2) (x0 x2)) (∀ x3 . x3x2not (x0 x3))x1)x1
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Param setminussetminus : ιιι
Known eb0c4..binunion_remove1_eq : ∀ x0 x1 . x1x0x0 = binunion (setminus x0 (Sing x1)) (Sing x1)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known SingISingI : ∀ x0 . x0Sing x0
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known ordinal_ordsucc_In_Subqordinal_ordsucc_In_Subq : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1x0
Known 9c223..equip_ordsucc_remove1 : ∀ x0 x1 x2 . x2x0equip x0 (ordsucc x1)equip (setminus x0 (Sing x2)) x1
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Param SNoSNo : ιο
Param minus_SNominus_SNo : ιι
Param add_SNoadd_SNo : ιιι
Known add_SNo_rotate_3_1add_SNo_rotate_3_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x2 (add_SNo x0 x1)
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known add_SNo_minus_L2add_SNo_minus_L2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Known add_SNo_omega_SR : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 (ordsucc x1) = ordsucc (add_SNo x0 x1)
Known add_SNo_In_omegaadd_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 x1omega
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Param intint : ι
Param SNoLeSNoLe : ιιο
Known aa7e8..nonneg_int_nat_p : ∀ x0 . x0intSNoLe 0 x0nat_p x0
Known int_add_SNoint_add_SNo : ∀ x0 . x0int∀ x1 . x1intadd_SNo x0 x1int
Known Subq_omega_intSubq_omega_int : omegaint
Known int_minus_SNoint_minus_SNo : ∀ x0 . x0intminus_SNo x0int
Known add_SNo_minus_Le2badd_SNo_minus_Le2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe (add_SNo x2 x1) x0SNoLe x2 (add_SNo x0 (minus_SNo x1))
Known SNo_0SNo_0 : SNo 0
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known ordinal_Subq_SNoLeordinal_Subq_SNoLe : ∀ x0 x1 . ordinal x0ordinal x1x0x1SNoLe x0 x1
Known Eps_i_axEps_i_ax : ∀ x0 : ι → ο . ∀ x1 . x0 x1x0 (prim0 x0)
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Known finite_Emptyfinite_Empty : finite 0
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known infinite_remove1infinite_remove1 : ∀ x0 . infinite x0∀ x1 . infinite (setminus x0 (Sing x1))
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known e8bc0..equip_adjoin_ordsucc : ∀ x0 x1 x2 . nIn x2 x1equip x0 x1equip (ordsucc x0) (binunion x1 (Sing x2))
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Theorem infiniteRamseyinfiniteRamsey : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . infinite x2∀ x3 : ι → ι . (∀ x4 . x4x2equip x4 x1x3 x4x0)∀ x4 : ο . (∀ x5 . and (x5x2) (∀ x6 : ο . (∀ x7 . and (x7x0) (and (infinite x5) (∀ x8 . x8x5equip x8 x1x3 x8 = x7))x6)x6)x4)x4 (proof)

previous assets