Search for blocks/addresses/...

Proofgold Asset

asset id
df132acfd84775e5b038c8c5cd6e6bc3bb44caea4bf0fce2fe78c374c5da87a0
asset hash
3098d9a95cde32ebfab9d3ae6f78031319231a8af2310ed80144488c4dec1720
bday / block
8134
tx
71eda..
preasset
doc published by PrFVW..
Param nat_pnat_p : ιο
Param nat_primrecnat_primrec : ι(ιιι) → ιι
Param ordsuccordsucc : ιι
Param mul_natmul_nat : ιιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known nat_primrec_0nat_primrec_0 : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known nat_1nat_1 : nat_p 1
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)
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem 6523a.. : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2x0nat_p (x1 x2))nat_p (nat_primrec 1 (λ x2 . mul_nat (x1 x2)) x0) (proof)
Param add_natadd_nat : ιιι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known nat_invnat_inv : ∀ x0 . nat_p x0or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2)x1)x1)
Known add_nat_0Ladd_nat_0L : ∀ x0 . nat_p x0add_nat 0 x0 = x0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known add_nat_SLadd_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known neq_ordsucc_0neq_ordsucc_0 : ∀ x0 . ordsucc x0 = 0∀ x1 : ο . x1
Theorem 93901.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = 0and (x0 = 0) (x1 = 0) (proof)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known mul_nat_SLmul_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat (ordsucc x0) x1 = add_nat (mul_nat x0 x1) x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Theorem f3fbb..mul_nat_0_inv : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = 0or (x0 = 0) (x1 = 0) (proof)
Param setminussetminus : ιιι
Param omegaomega : ι
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known In_0_1In_0_1 : 01
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Theorem a0ed2.. : ∀ x0 . x0setminus omega 1∀ x1 . x1setminus omega 1mul_nat x0 x1setminus omega 1 (proof)
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
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
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
Theorem f11bb.. : ∀ x0 . nat_p x0mul_nat 1 x0 = x0 (proof)
Param ordinalordinal : ιο
Known ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0)
Known ordinal_ordsuccordinal_ordsucc : ∀ x0 . ordinal x0ordinal (ordsucc x0)
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Theorem f0633.. : ∀ x0 x1 . ordinal x0ordinal x1x0x1ordsucc x0ordsucc x1 (proof)
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known add_nat_padd_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (add_nat x0 x1)
Theorem 116d8.. : ∀ x0 x1 . nat_p x0nat_p x1x0x1∀ x2 . nat_p x2add_nat x0 x2add_nat x1 x2 (proof)
Known add_nat_comadd_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = add_nat x1 x0
Theorem abb9e.. : ∀ x0 x1 . nat_p x0nat_p x1x0x1∀ x2 . nat_p x2add_nat x2 x0add_nat x2 x1 (proof)
Known Subq_refSubq_ref : ∀ x0 . x0x0
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Theorem 4324d..mul_nat_Subq_R : ∀ x0 x1 . nat_p x0nat_p x1x0x1∀ x2 . nat_p x2mul_nat x0 x2mul_nat x1 x2 (proof)
Theorem df9cc..mul_nat_Subq_L : ∀ x0 x1 . nat_p x0nat_p x1x0x1∀ x2 . nat_p x2mul_nat x2 x0mul_nat x2 x1 (proof)
Theorem 6899f.. : ∀ x0 . x0setminus omega 1∀ x1 : ο . (∀ x2 . x2omegax0 = ordsucc x2x1)x1 (proof)
Known ordinal_ordsucc_Inordinal_ordsucc_In : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known ordinal_1ordinal_1 : ordinal 1
Known Subq_1_2Subq_1_2 : 12
Theorem ee3ec.. : ∀ x0 . x0setminus omega 2∀ x1 : ο . (∀ x2 . x2omegax0 = ordsucc (ordsucc x2)x1)x1 (proof)
Theorem add_nat_Subq_Ladd_nat_Subq_R : ∀ x0 . nat_p x0∀ x1 . nat_p x1x0add_nat x0 x1 (proof)
Theorem 3b460.. : ∀ x0 . nat_p x0∀ x1 . x1setminus omega 1x0mul_nat x0 x1 (proof)
Theorem e5f18.. : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2x0x1 x2setminus omega 1)nat_primrec 1 (λ x2 . mul_nat (x1 x2)) x0setminus omega 1 (proof)
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Theorem 39880.. : ∀ x0 . nat_p x0∀ x1 . x1setminus omega 1x0mul_nat x1 x0 (proof)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Theorem d1a0b.. : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2x0x1 x2setminus omega 1)∀ x2 . x2x0x1 x2nat_primrec 1 (λ x3 . mul_nat (x1 x3)) x0 (proof)
Definition divides_natdivides_nat := λ x0 x1 . and (and (x0omega) (x1omega)) (∀ x2 : ο . (∀ x3 . and (x3omega) (mul_nat x0 x3 = x1)x2)x2)
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Theorem 9baed.. : ∀ x0 . x0omegadivides_nat x0 x0 (proof)
Known and3Eand3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2∀ x3 : ο . (x0x1x2x3)x3
Known mul_nat_assomul_nat_asso : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2mul_nat (mul_nat x0 x1) x2 = mul_nat x0 (mul_nat x1 x2)
Theorem e4e38..divides_nat_tra : ∀ x0 x1 x2 . divides_nat x0 x1divides_nat x1 x2divides_nat x0 x2 (proof)
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Theorem 4c147.. : ∀ x0 . nat_p x0∀ x1 : ι → ι . (∀ x2 . x2x0nat_p (x1 x2))∀ x2 . x2x0divides_nat (x1 x2) (nat_primrec 1 (λ x3 . mul_nat (x1 x3)) x0) (proof)
Theorem 01ac5.. : ∀ x0 . nat_p x0∀ x1 : ι → ο . x1 0(∀ x2 . x2setminus omega 1x1 x2)x1 x0 (proof)
Known cases_2cases_2 : ∀ x0 . x02∀ x1 : ι → ο . x1 0x1 1x1 x0
Known ordsucc_inj_contraordsucc_inj_contra : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)ordsucc x0 = ordsucc x1∀ x2 : ο . x2
Theorem 3aff2.. : ∀ x0 . nat_p x0∀ x1 : ι → ο . x1 0x1 1(∀ x2 . x2setminus omega 2x1 x2)x1 x0 (proof)
Theorem 6a866.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1or (x1 = 0) (x0add_nat x0 x1) (proof)
Theorem 20225.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1or (x1 = 0) (x0add_nat x1 x0) (proof)
Known neq_0_1neq_0_1 : 0 = 1∀ x0 : ο . x0
Known mul_nat_0Lmul_nat_0L : ∀ x0 . nat_p x0mul_nat 0 x0 = 0
Theorem 7092d.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = 1and (x0 = 1) (x1 = 1) (proof)
Definition prime_natprime_nat := λ x0 . and (and (x0omega) (1x0)) (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known In_0_2In_0_2 : 02
Known ordinal_trichotomy_or_impredordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0ordinal x1∀ x2 : ο . (x0x1x2)(x0 = x1x2)(x1x0x2)x2
Known In_1_2In_1_2 : 12
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Theorem b513d.. : ∀ x0 . x0setminus omega 2∀ x1 : ο . (∀ x2 . and (x2omega) (and (prime_nat x2) (divides_nat x2 x0))x1)x1 (proof)
Theorem 4e482.. : ∀ x0 . prime_nat x0x0setminus omega 2 (proof)
Theorem f7d6d.. : ∀ x0 x1 . (x1 = 0∀ x2 : ο . x2)divides_nat x0 x1x0x1 (proof)
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Theorem 3ed2c.. : ∀ x0 x1 . (x1 = 0∀ x2 : ο . x2)divides_nat x0 x1or (x0x1) (x0 = x1) (proof)
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Theorem a9ab4.. : ∀ x0 . nat_p x0∀ x1 . x1x0∀ x2 : ο . (∀ x3 . and (x3omega) (add_nat x1 x3 = x0)x2)x2 (proof)
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Theorem c6e57.. : ∀ x0 x1 . nat_p x0nat_p x1∀ x2 . nat_p x2add_nat x0 x2 = add_nat x1 x2x0 = x1 (proof)
Theorem 0d850.. : ∀ x0 x1 x2 . nat_p x0nat_p x1nat_p x2add_nat x0 x1 = add_nat x0 x2x1 = x2 (proof)
Known mul_add_nat_distrLmul_add_nat_distrL : ∀ x0 . nat_p x0∀ x1 . nat_p x1∀ x2 . nat_p x2mul_nat x0 (add_nat x1 x2) = add_nat (mul_nat x0 x1) (mul_nat x0 x2)
Theorem 6ce5b.. : ∀ x0 . x0setminus omega 2∀ x1 . divides_nat x0 x1not (divides_nat x0 (ordsucc x1)) (proof)
Definition surjsurj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)
Param SepSep : ι(ιο) → ι
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Known neq_0_ordsuccneq_0_ordsucc : ∀ x0 . 0 = ordsucc x0∀ x1 : ο . x1
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Theorem 3a99b.. : ∀ x0 . nat_p x0∀ x1 : ι → ι . not (surj x0 (Sep omega prime_nat) x1) (proof)
Param bijbij : ιι(ιι) → ο
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)
Known bij_surjbij_surj : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2surj x0 x1 x2
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Theorem form100_11_infinite_primesform100_11_infinite_primes : infinite (Sep omega prime_nat) (proof)