Search for blocks/addresses/...

Proofgold Asset

asset id
375765d3136bd3cd2e76a10ace9971fe78b0a21b29f5126332c0dec57e986f4e
asset hash
985e17aeba9ce7a65e058c8fa95290949fb60f9ec51179819e13470d3328e0ac
bday / block
30499
tx
de20d..
preasset
doc published by Pr5Zc..
Known 60e4a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2x0 x3x0 (x1 x2 x3))(∀ x2 x3 x4 . x0 x2x0 x3x0 x4x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)(∀ x2 x3 . x0 x2x0 x3x1 x2 x3 = x1 x3 x2)∀ x2 x3 x4 x5 . x0 x2x0 x3x0 x4x0 x5x1 x2 (x1 x3 (x1 x4 x5)) = x1 x3 (x1 x4 (x1 x2 x5))
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param omegaomega : ι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Param add_natadd_nat : ιιι
Param mul_natmul_nat : ιιι
Definition b3e62..equiv_nat_mod := λ x0 x1 x2 . and (and (and (x0omega) (x1omega)) (x2omega)) (or (∀ x3 : ο . (∀ x4 . and (x4omega) (add_nat x0 (mul_nat x4 x2) = x1)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4omega) (add_nat x1 (mul_nat x4 x2) = x0)x3)x3))
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param ordsuccordsucc : ιι
Definition divides_natdivides_nat := λ x0 x1 . and (and (x0omega) (x1omega)) (∀ x2 : ο . (∀ x3 . and (x3omega) (mul_nat x0 x3 = x1)x2)x2)
Definition prime_natprime_nat := λ x0 . and (and (x0omega) (1x0)) (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))
Param nat_pnat_p : ιο
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_2nat_2 : nat_p 2
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Known nat_4nat_4 : nat_p 4
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known c3da7.. : mul_nat 2 2 = 4
Known neq_2_1neq_2_1 : 2 = 1∀ x0 : ο . x0
Known neq_4_2neq_4_2 : 4 = 2∀ x0 : ο . x0
Theorem c14f2.. : not (prime_nat 4) (proof)
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 ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Theorem d8085.. : ∀ x0 x1 . nat_p x1x0ordsucc (add_nat x0 x1) (proof)
Known nat_invnat_inv : ∀ x0 . nat_p x0or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2)x1)x1)
Known FalseEFalseE : False∀ x0 : ο . x0
Definition nInnIn := λ x0 x1 . not (x0x1)
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Theorem 46720.. : ∀ x0 x1 . nat_p x0nat_p x1add_nat x0 x1x0x1 = 0 (proof)
Known Subq_refSubq_ref : ∀ x0 . x0x0
Theorem ab486.. : ∀ x0 x1 . nat_p x0nat_p x1x0 = add_nat x0 x1x1 = 0 (proof)
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known f3fbb..mul_nat_0_inv : ∀ x0 . nat_p x0∀ x1 . nat_p x1mul_nat x0 x1 = 0or (x0 = 0) (x1 = 0)
Known mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
Known ordsucc_injordsucc_inj : ∀ x0 x1 . ordsucc x0 = ordsucc x1x0 = x1
Known add_nat_SLadd_nat_SL : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat (ordsucc x0) x1 = ordsucc (add_nat x0 x1)
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Theorem 92637.. : ∀ x0 . nat_p x0mul_nat x0 x0 = x0or (x0 = 0) (x0 = 1) (proof)
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 lamSigma : ι(ιι) → ι
Definition setprodsetprod := λ x0 x1 . lam x0 (λ x2 . x1)
Known 63881.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (mul_nat x0 x1) (setprod x2 x3)
Param PiPi : ι(ιι) → ι
Definition setexpsetexp := λ x0 x1 . Pi x1 (λ x2 . x0)
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 In_0_1In_0_1 : 01
Param apap : ιιι
Known Pi_extPi_ext : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2Pi x0 x1∀ x3 . x3Pi x0 x1(∀ x4 . x4x0ap x2 x4 = ap x3 x4)x2 = x3
Param pair_ppair_p : ιο
Known PiIPiI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . x3x2and (pair_p x3) (ap x3 0x0))(∀ x3 . x3x0ap x2 x3x1 x3)x2Pi x0 x1
Known cases_1cases_1 : ∀ x0 . x01∀ x1 : ι → ο . x1 0x1 x0
Theorem 1032b.. : ∀ x0 . equip (setexp x0 0) 1 (proof)
Param exp_natexp_nat : ιιι
Known 856b4..exp_nat_0 : ∀ x0 . exp_nat x0 0 = 1
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known caaf4..exp_nat_S : ∀ x0 x1 . nat_p x1exp_nat x0 (ordsucc x1) = mul_nat x0 (exp_nat x0 x1)
Known equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2
Known 4f402..exp_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (exp_nat x0 x1)
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Param If_iIf_i : οιιι
Known tuple_2_setprodtuple_2_setprod : ∀ x0 x1 x2 . x2x0∀ x3 . x3x1lam 2 (λ x4 . If_i (x4 = 0) x2 x3)setprod x0 x1
Known ap_Piap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2Pi x0 x1x3x0ap x2 x3x1 x3
Known lam_Pilam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3x0x2 x3x1 x3)lam x0 x2Pi x0 x1
Known tuple_2_injtuple_2_inj : ∀ x0 x1 x2 x3 . lam 2 (λ x5 . If_i (x5 = 0) x0 x1) = lam 2 (λ x5 . If_i (x5 = 0) x2 x3)and (x0 = x2) (x1 = x3)
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known betabeta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0ap (lam x0 x1) x2 = x1 x2
Param invinv : ι(ιι) → ιι
Known surj_rinvsurj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x5x0) (x2 x5 = x3)x4)x4)∀ x3 . x3x1and (inv x0 x2 x3x0) (x2 (inv x0 x2 x3) = x3)
Known ap1_Sigmaap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 1x1 (ap x2 0)
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 tuple_Sigma_etatuple_Sigma_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1lam 2 (λ x4 . If_i (x4 = 0) (ap x2 0) (ap x2 1)) = x2
Known ap0_Sigmaap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 0x0
Theorem 17a87.. : ∀ x0 . nat_p x0∀ x1 . nat_p x1equip (exp_nat x0 x1) (setexp x0 x1) (proof)
Param even_nateven_nat : ιο
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known even_nat_0even_nat_0 : even_nat 0
Definition odd_natodd_nat := λ x0 . and (x0omega) (∀ x1 . x1omegax0 = mul_nat 2 x1∀ x2 : ο . x2)
Known odd_nat_even_nat_Sodd_nat_even_nat_S : ∀ x0 . odd_nat x0even_nat (ordsucc x0)
Known even_nat_odd_nat_Seven_nat_odd_nat_S : ∀ x0 . even_nat x0odd_nat (ordsucc x0)
Param setminussetminus : ιιι
Param UPairUPair : ιιι
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known UPairEUPairE : ∀ x0 x1 x2 . x0UPair x1 x2or (x0 = x1) (x0 = x2)
Known In_no2cycleIn_no2cycle : ∀ x0 x1 . x0x1x1x0False
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 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 nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known UPairI1UPairI1 : ∀ x0 x1 . x0UPair x0 x1
Known UPairI2UPairI2 : ∀ x0 x1 . x1UPair x0 x1
Known ordinal_ordsucc_In_Subqordinal_ordsucc_In_Subq : ∀ x0 . ordinal x0∀ x1 . x1x0ordsucc x1x0
Known nat_ordsucc_in_ordsuccnat_ordsucc_in_ordsucc : ∀ x0 . nat_p x0∀ x1 . x1x0ordsucc x1ordsucc x0
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Theorem 63511.. : ∀ x0 . nat_p x0∀ x1 . equip x0 x1∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x1)(∀ x3 . x3x1x2 (x2 x3) = x3)(∀ x3 . x3x1x2 x3 = x3∀ x4 : ο . x4)even_nat x0 (proof)
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known even_nat_not_odd_nateven_nat_not_odd_nat : ∀ x0 . even_nat x0not (odd_nat x0)
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Theorem d3cb5.. : ∀ x0 x1 . odd_nat x1equip x0 x1∀ x2 : ι → ι . (∀ x3 . x3x0x2 x3x0)(∀ x3 . x3x0x2 (x2 x3) = x3)∀ x3 : ο . (∀ x4 . and (x4x0) (x2 x4 = x4)x3)x3 (proof)
Param SingSing : ιι
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known SingISingI : ∀ x0 . x0Sing x0
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Theorem 74e07.. : ∀ x0 . nat_p x0∀ x1 . equip x0 x1∀ x2 : ι → ι . (∀ x3 . x3x1x2 x3x1)(∀ x3 . x3x1x2 (x2 x3) = x3)(∀ x3 : ο . (∀ x4 . and (x4x1) (and (x2 x4 = x4) (∀ x5 . x5x1x2 x5 = x5x4 = x5))x3)x3)odd_nat x0 (proof)
Param SNoSNo : ιο
Param mul_SNomul_SNo : ιιι
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known mul_SNo_assocmul_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo (mul_SNo x0 x1) x2
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Theorem 24b4c.. : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo x0 (mul_SNo x1 (mul_SNo x2 x3)) = mul_SNo x1 (mul_SNo x2 (mul_SNo x0 x3)) (proof)
Known mul_SNo_oneRmul_SNo_oneR : ∀ x0 . SNo x0mul_SNo x0 1 = x0
Known SNo_1SNo_1 : SNo 1
Theorem e032f.. : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (mul_SNo x1 x2) = mul_SNo x1 (mul_SNo x2 x0) (proof)
Param add_SNoadd_SNo : ιιι
Known 547c4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3x0 x4x0 (x1 x3 x4))(∀ x3 x4 x5 . x0 x3x0 x4x0 x5x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5))∀ x3 x4 x5 x6 . x0 x3x0 x4x0 x5x0 x6x2 (x1 x3 (x1 x4 x5)) x6 = x1 (x2 x3 x6) (x1 (x2 x4 x6) (x2 x5 x6))
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known mul_SNo_distrRmul_SNo_distrR : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo (add_SNo x0 x1) x2 = add_SNo (mul_SNo x0 x2) (mul_SNo x1 x2)
Theorem 7bd74.. : ∀ x0 x1 x2 x3 . SNo x0SNo x1SNo x2SNo x3mul_SNo (add_SNo x0 (add_SNo x1 x2)) x3 = add_SNo (mul_SNo x0 x3) (add_SNo (mul_SNo x1 x3) (mul_SNo x2 x3)) (proof)
Param SNoLtSNoLt : ιιο
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Known In_1_4In_1_4 : 14
Theorem c188a.. : SNoLt 1 4 (proof)