Search for blocks/addresses/...

Proofgold Asset

asset id
dc86598753f2a51aecd29485f9ee2f2bed59e92e411526bd2c7a82400e04e562
asset hash
325602aab7aa6e8ccb47a13ca6b6479be81b81b84c0a03e1d1a4e08064871783
bday / block
19339
tx
36e89..
preasset
doc published by Pr4zB..
Param lamSigma : ι(ιι) → ι
Definition setprodsetprod := λ x0 x1 . lam x0 (λ x2 . x1)
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Param apap : ιιι
Param ordsuccordsucc : ιι
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Known ap1_Sigmaap1_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 1x1 (ap x2 0)
Theorem a9232.. : ∀ x0 . setprod x0 0 = 0 (proof)
Param nat_pnat_p : ιο
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 mul_natmul_nat : ιιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known mul_nat_0Rmul_nat_0R : ∀ x0 . mul_nat x0 0 = 0
Known c5737.. : ∀ x0 . equip 0 x0x0 = 0
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Param add_natadd_nat : ιιι
Known mul_nat_SRmul_nat_SR : ∀ x0 x1 . nat_p x1mul_nat x0 (ordsucc x1) = add_nat x0 (mul_nat x0 x1)
Param setsumsetsum : ιιι
Param setminussetminus : ιιι
Param SingSing : ιι
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 mul_nat_pmul_nat_p : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (mul_nat x0 x1)
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 setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known FalseEFalseE : False∀ x0 : ο . x0
Known SingISingI : ∀ x0 . x0Sing x0
Param combine_funcscombine_funcs : ιι(ιι) → (ιι) → ιι
Param If_iIf_i : οιιι
Param Inj0Inj0 : ιι
Param Inj1Inj1 : ιι
Known f4c7c.. : ∀ x0 x1 . ∀ x2 : ι → ο . (∀ x3 . x3x0x2 (Inj0 x3))(∀ x3 . x3x1x2 (Inj1 x3))∀ x3 . x3setsum x0 x1x2 x3
Known combine_funcs_eq1combine_funcs_eq1 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj0 x4) = x2 x4
Known tuple_2_setprodtuple_2_setprod : ∀ x0 x1 x2 . x2x0∀ x3 . x3x1lam 2 (λ x4 . If_i (x4 = 0) x2 x3)setprod x0 x1
Known combine_funcs_eq2combine_funcs_eq2 : ∀ x0 x1 . ∀ x2 x3 : ι → ι . ∀ x4 . combine_funcs x0 x1 x2 x3 (Inj1 x4) = x3 x4
Known setprod_mon1setprod_mon1 : ∀ x0 x1 x2 . x1x2setprod x0 x1setprod x0 x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known Inj0_setsumInj0_setsum : ∀ x0 x1 x2 . x2x0Inj0 x2setsum x0 x1
Known ap0_Sigmaap0_Sigma : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2lam x0 x1ap x2 0x0
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 Inj1_setsumInj1_setsum : ∀ x0 x1 x2 . x2x1Inj1 x2setsum x0 x1
Theorem 63881.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (mul_nat x0 x1) (setprod x2 x3) (proof)
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition u4 := ordsucc u3
Definition u5 := ordsucc u4
Definition u6 := ordsucc u5
Definition u7 := ordsucc u6
Definition u8 := ordsucc u7
Definition u9 := ordsucc u8
Definition u10 := ordsucc u9
Definition u11 := ordsucc u10
Definition u12 := ordsucc u11
Definition u13 := ordsucc u12
Definition u14 := ordsucc u13
Definition u15 := ordsucc u14
Definition u16 := ordsucc u15
Definition u17 := ordsucc u16
Definition u18 := ordsucc u17
Definition u19 := ordsucc u18
Definition u20 := ordsucc u19
Definition u21 := ordsucc u20
Definition u22 := ordsucc u21
Definition u23 := ordsucc u22
Definition u24 := ordsucc u23
Definition u25 := ordsucc u24
Definition u26 := ordsucc u25
Definition u27 := ordsucc u26
Definition u28 := ordsucc u27
Definition u29 := ordsucc u28
Definition u30 := ordsucc u29
Definition u31 := ordsucc u30
Definition u32 := ordsucc u31
Definition u33 := ordsucc u32
Definition u34 := ordsucc u33
Definition u35 := ordsucc u34
Definition u36 := ordsucc u35
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known nat_5nat_5 : nat_p 5
Known nat_4nat_4 : nat_p 4
Known 2cf95.. : add_nat 6 4 = 10
Theorem f1303.. : add_nat u6 u6 = u12 (proof)
Known nat_1nat_1 : nat_p 1
Known mul_nat_1Rmul_nat_1R : ∀ x0 . mul_nat x0 1 = x0
Theorem fbd5e.. : mul_nat u6 u2 = u12 (proof)
Known nat_11nat_11 : nat_p 11
Known add_nat_comadd_nat_com : ∀ x0 . nat_p x0∀ x1 . nat_p x1add_nat x0 x1 = add_nat x1 x0
Known nat_6nat_6 : nat_p 6
Known 91a85.. : add_nat 11 6 = 17
Theorem a2682.. : add_nat u6 u12 = u18 (proof)
Known nat_2nat_2 : nat_p 2
Theorem 176e9.. : mul_nat u6 u3 = u18 (proof)
Known nat_17nat_17 : nat_p 17
Known nat_16nat_16 : nat_p 16
Known f5339.. : add_nat 16 6 = 22
Theorem 67f29.. : add_nat u6 u18 = u24 (proof)
Known nat_3nat_3 : nat_p 3
Theorem 4603a.. : mul_nat u6 u4 = u24 (proof)
Known 2a2ab.. : add_nat 24 6 = 30
Theorem b6d70.. : mul_nat u6 u5 = u30 (proof)
Known 73189.. : nat_p u24
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Theorem d5180.. : nat_p u25 (proof)
Theorem 24234.. : nat_p u26 (proof)
Theorem e06fe.. : nat_p u27 (proof)
Theorem 5c78e.. : nat_p u28 (proof)
Theorem 7e1a8.. : nat_p u29 (proof)
Theorem a9ae2.. : nat_p u30 (proof)
Theorem 74918.. : nat_p u31 (proof)
Theorem 1f846.. : nat_p u32 (proof)
Theorem ffdd1.. : nat_p u33 (proof)
Theorem 183e4.. : nat_p u34 (proof)
Theorem 966a2.. : nat_p u35 (proof)
Theorem 4aca7.. : nat_p u36 (proof)
Known nat_0nat_0 : nat_p 0
Known add_nat_0Radd_nat_0R : ∀ x0 . add_nat x0 0 = x0
Theorem ac6b6.. : add_nat u6 u30 = u36 (proof)
Theorem 66577.. : mul_nat u6 u6 = u36 (proof)
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Theorem 9bff1.. : equip (setprod u6 u6) u36 (proof)
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Theorem bc60b.. : ∀ x0 x1 x2 . x2x0∀ x3 : ι → ι . bij x0 x1 x3bij (setminus x0 (Sing x2)) (setminus x1 (Sing (x3 x2))) x3 (proof)
Known 8ac0e.. : ∀ x0 . nat_p x0∀ x1 . x1ordsucc x0equip x0 (setminus (ordsucc x0) (Sing x1))
Known In_5_6In_5_6 : 56
Theorem 903ea.. : equip (setminus (setprod u6 u6) (Sing (lam 2 (λ x0 . If_i (x0 = 0) u5 u5)))) u35 (proof)