Search for blocks/addresses/...

Proofgold Asset

asset id
3f75bc9411348996534447cd5d65445cd5a3bfba4e4c16954ffd8e38e98c3bee
asset hash
6d95ae2083bfd1d1e82441f9f0c04a2038eb0dd328457f892c06818fa5a7345b
bday / block
29779
tx
ec879..
preasset
doc published by PrQUS..
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 exp_SNo_natexp_SNo_nat : ιιι
Param ordsuccordsucc : ιι
Known nat_indnat_ind : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known equip_0_Emptyequip_0_Empty : ∀ x0 . equip x0 0x0 = 0
Param SNoSNo : ιο
Known exp_SNo_nat_0exp_SNo_nat_0 : ∀ x0 . SNo x0exp_SNo_nat x0 0 = 1
Known SNo_2SNo_2 : SNo 2
Param SingSing : ιι
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
Param mul_SNomul_SNo : ιιι
Known exp_SNo_nat_Sexp_SNo_nat_S : ∀ x0 . SNo x0∀ x1 . nat_p x1exp_SNo_nat x0 (ordsucc x1) = mul_SNo x0 (exp_SNo_nat x0 x1)
Param add_SNoadd_SNo : ιιι
Known add_SNo_1_1_2add_SNo_1_1_2 : add_SNo 1 1 = 2
Param omegaomega : ι
Param ordinalordinal : ιο
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)
Known SNo_1SNo_1 : SNo 1
Known mul_SNo_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Param setminussetminus : ιιι
Known 9c223..equip_ordsucc_remove1 : ∀ x0 x1 x2 . x2x0equip x0 (ordsucc x1)equip (setminus x0 (Sing x2)) x1
Param If_iIf_i : οιιι
Known and3Iand3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Param SNoLtSNoLt : ιιο
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known add_SNo_Lt2add_SNo_Lt2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x1 x2SNoLt (add_SNo x0 x1) (add_SNo x0 x2)
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known PowerIPowerI : ∀ x0 x1 . x1x0x1prim4 x0
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 PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
Known nat_transnat_trans : ∀ x0 . nat_p x0∀ x1 . x1x0x1x0
Param SNoLeSNoLe : ιιο
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Known ordinal_SNoordinal_SNo : ∀ x0 . ordinal x0SNo x0
Known ordinal_ordsuccordinal_ordsucc : ∀ x0 . ordinal x0ordinal (ordsucc x0)
Known nat_p_SNonat_p_SNo : ∀ x0 . nat_p x0SNo x0
Known ordinal_ordsucc_SNo_eqordinal_ordsucc_SNo_eq : ∀ x0 . ordinal x0ordsucc x0 = add_SNo 1 x0
Known add_SNo_Le1add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x2SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Known exp_SNo_1_bdexp_SNo_1_bd : ∀ x0 . SNo x0SNoLe 1 x0∀ x1 . nat_p x1SNoLe 1 (exp_SNo_nat x0 x1)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNoLt_1_2SNoLt_1_2 : SNoLt 1 2
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Known add_SNo_cancel_Ladd_SNo_cancel_L : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 x1 = add_SNo x0 x2x1 = x2
Known FalseEFalseE : False∀ x0 : ο . x0
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = x0
Known add_SNo_Le2add_SNo_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x1 x2SNoLe (add_SNo x0 x1) (add_SNo x0 x2)
Known SNo_0SNo_0 : SNo 0
Known omega_nonnegomega_nonneg : ∀ x0 . x0omegaSNoLe 0 x0
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known SingISingI : ∀ x0 . x0Sing x0
Param minus_SNominus_SNo : ιι
Param intint : ι
Known aa7e8..nonneg_int_nat_p : ∀ x0 . x0intSNoLe 0 x0nat_p x0
Known int_add_SNoint_add_SNo : ∀ x0 . x0int∀ x1 . x1intadd_SNo x0 x1int
Known Subq_omega_intSubq_omega_int : omegaint
Known int_minus_SNoint_minus_SNo : ∀ x0 . x0intminus_SNo x0int
Known add_SNo_minus_Le2badd_SNo_minus_Le2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe (add_SNo x2 x1) x0SNoLe x2 (add_SNo x0 (minus_SNo x1))
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known add_SNo_minus_Lt1badd_SNo_minus_Lt1b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 (add_SNo x2 x1)SNoLt (add_SNo x0 (minus_SNo x1)) x2
Param binunionbinunion : ιιι
Known binunion_Subq_minbinunion_Subq_min : ∀ x0 x1 x2 . x0x2x1x2binunion x0 x1x2
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known add_SNo_rotate_3_1add_SNo_rotate_3_1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo x2 (add_SNo x0 x1)
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known add_SNo_minus_L2add_SNo_minus_L2 : ∀ x0 x1 . SNo x0SNo x1add_SNo (minus_SNo x0) (add_SNo x0 x1) = x1
Known nat_p_transnat_p_trans : ∀ x0 . nat_p x0∀ x1 . x1x0nat_p x1
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known add_SNo_In_omegaadd_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 x1omega
Known nat_exp_SNo_natnat_exp_SNo_nat : ∀ x0 . nat_p x0∀ x1 . nat_p x1nat_p (exp_SNo_nat x0 x1)
Known nat_2nat_2 : nat_p 2
Theorem equip_finite_Power : ∀ x0 . nat_p x0∀ x1 . equip x1 x0equip (prim4 x1) (exp_SNo_nat 2 x0) (proof)