Search for blocks/addresses/...

Proofgold Address

address
PUgHR7rjCWSwejyXCGJAUTuvBKNDvzzYuRU
total
0
mg
-
conjpub
-
current assets
3e775../3a724.. bday: 29749 doc published by PrQUS..
Param omegaomega : ι
Param add_SNoadd_SNo : ιιι
Param ordsuccordsucc : ιι
Param add_natadd_nat : ιιι
Known add_nat_add_SNoadd_nat_add_SNo : ∀ x0 . x0omega∀ x1 . x1omegaadd_nat x0 x1 = add_SNo x0 x1
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Param nat_pnat_p : ιο
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Theorem add_SNo_omega_SR : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 (ordsucc x1) = ordsucc (add_SNo x0 x1) (proof)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
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
Definition finitefinite := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2omega) (equip x0 x2)x1)x1
Definition infiniteinfinite := λ x0 . not (finite x0)
Param atleastpatleastp : ιιο
Known 4fb58..Pigeonhole_not_atleastp_ordsucc : ∀ x0 . nat_p x0not (atleastp (ordsucc x0) x0)
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known Subq_atleastpSubq_atleastp : ∀ x0 x1 . x0x1atleastp x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Theorem atleastp_omega_infiniteatleastp_omega_infinite : ∀ x0 . atleastp omega x0infinite x0 (proof)
Param setminussetminus : ιιι
Param SingSing : ιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Param binunionbinunion : ιιι
Known eb0c4..binunion_remove1_eq : ∀ x0 x1 . x1x0x0 = binunion (setminus x0 (Sing x1)) (Sing x1)
Known binunion_finitebinunion_finite : ∀ x0 . finite x0∀ x1 . finite x1finite (binunion x0 x1)
Known 28148..Sing_finite : ∀ x0 . finite (Sing x0)
Definition nInnIn := λ x0 x1 . not (x0x1)
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Theorem infinite_remove1infinite_remove1 : ∀ x0 . infinite x0∀ x1 . infinite (setminus x0 (Sing x1)) (proof)
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known Subq_EmptySubq_Empty : ∀ x0 . 0x0
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Param If_iIf_i : οιιι
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SingISingI : ∀ x0 . x0Sing x0
Theorem infinite_Finite_Subq_exinfinite_Finite_Subq_ex : ∀ x0 . infinite x0∀ x1 . nat_p x1∀ x2 : ο . (∀ x3 . and (x3x0) (equip x3 x1)x2)x2 (proof)

previous assets