Search for blocks/addresses/...

Proofgold Address

address
PUbWYj8nbhsJTjYWvRsquTyLPfV7wDqjXXS
total
0
mg
-
conjpub
-
current assets
b73d9../4894a.. bday: 15286 doc published by Pr4zB..
Param nat_pnat_p : ιο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param add_natadd_nat : ιιι
Param ordsuccordsucc : ιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem 4d87b.. : ∀ x0 x1 . nat_p x1x0add_nat x0 x1 (proof)
Param mul_natmul_nat : ιιι
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known nat_0nat_0 : nat_p 0
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Theorem mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0 (proof)
Known mul_nat_commul_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = mul_nat x1 x0
Known nat_1nat_1 : nat_p 1
Theorem f11bb.. : ∀ x0 . nat_p x0mul_nat 1 x0 = x0 (proof)
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Definition exp_natexp_nat := λ x0 . nat_primrec 1 (λ x1 . mul_nat x0)
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)
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Theorem 4f402..exp_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (exp_nat x0 x1) (proof)
Param setminussetminus : ιιι
Param SingSing : ιι
Known PowerIPowerI : ∀ x0 x1 . x1x0x1prim4 x0
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0
Definition nInnIn := λ x0 x1 . not (x0x1)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Theorem 39f67.. : ∀ x0 x1 . setminus x1 (Sing x0)prim4 x0x1prim4 (ordsucc x0) (proof)
Param binunionbinunion : ιιι
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Theorem 35356.. : ∀ x0 x1 . x1prim4 x0binunion x1 (Sing x0)prim4 (ordsucc x0) (proof)
Param Inj0Inj0 : ιι
Param Inj1Inj1 : ιι
Param setsumsetsum : ιιι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Known setsum_Inj_invsetsum_Inj_inv : ∀ x0 x1 x2 . x2setsum x0 x1or (∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = Inj0 x4)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4x1) (x2 = Inj1 x4)x3)x3)
Theorem f4c7c.. : ∀ x0 x1 . ∀ x2 : ι → ο . (∀ x3 . x3x0x2 (Inj0 x3))(∀ x3 . x3x1x2 (Inj1 x3))∀ x3 . x3setsum x0 x1x2 x3 (proof)
Param bijbij : ιι(ιι) → ο
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Known Power_0_Sing_0Power_0_Sing_0 : prim4 0 = Sing 0
Known eq_1_Sing0eq_1_Sing0 : 1 = Sing 0
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Known add_nat_1_1_2add_nat_1_1_2 : add_nat 1 1 = 2
Known mul_add_nat_distrRmul_add_nat_distrR : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2mul_nat (add_nat x0 x1) x2 = add_nat (mul_nat x0 x2) (mul_nat x1 x2)
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2
Known c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (add_nat x0 x1) (setsum x2 x3)
Known bijEbijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2∀ x3 : ο . ((∀ x4 . x4x0x2 x4x1)(∀ x4 . x4x0∀ x5 . x5x0x2 x4 = x2 x5x4 = x5)(∀ x4 . x4x1∀ x5 : ο . (∀ x6 . and (x6x0) (x2 x6 = x4)x5)x5)x3)x3
Param combine_funcscombine_funcs : ιι(ιι) → (ιι) → ιι
Known bijIbijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x1)(∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)(∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)bij x0 x1 x2
Known combine_funcs_eq1combine_funcs_eq1 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known Power_SubqPower_Subq : ∀ x0 x1 . x0x1prim4 x0prim4 x1
Known combine_funcs_eq2combine_funcs_eq2 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known FalseEFalseE : False∀ x0 : ο . x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SingISingI : ∀ x0 . x0Sing x0
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known Inj1_setsumInj1_setsum : ∀ x0 x1 x2 . x2x1Inj1 x2setsum x0 x1
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 ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known Inj0_setsumInj0_setsum : ∀ x0 x1 x2 . x2x0Inj0 x2setsum x0 x1
Known nat_2nat_2 : nat_p 2
Theorem 293d3.. : ∀ x0 . nat_p x0equip (prim4 x0) (exp_nat 2 x0) (proof)
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 EmptyEEmptyE : ∀ x0 . nIn x0 0
Theorem 71267.. : ∀ x0 . atleastp 0 x0 (proof)
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 nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Known nat_ordsucc_transnat_ordsucc_trans : ∀ x0 . nat_p x0∀ x1 . x1ordsucc x0x1x0
Known nat_invnat_inv : ∀ x0 . nat_p x0or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2)x1)x1)
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
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 In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
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)
Theorem 8ac0e.. : ∀ x0 . nat_p x0∀ x1 . x1ordsucc x0equip x0 (setminus (ordsucc x0) (Sing x1)) (proof)
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Known add_nat_padd_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (add_nat x0 x1)
Theorem 9da24.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 x3 . atleastp (add_nat x0 x1) (binunion x2 x3)or (atleastp x0 x2) (atleastp x1 x3) (proof)

previous assets