Search for blocks/addresses/...

Proofgold Asset

asset id
208b64dd6afb719df44832b1532bf6b16d729b6b0d62570756bfe87702bc3e7a
asset hash
18337572d22d535faa544a2d57d0d8817d5608159799bd0f872572c150921458
bday / block
27822
tx
0e794..
preasset
doc published by PrQUS..
Param SNoSNo : ιο
Param SNoLtSNoLt : ιιο
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param recip_SNo_posrecip_SNo_pos : ιι
Param mul_SNomul_SNo : ιιι
Param ordsuccordsucc : ιι
Param SNoS_SNoS_ : ιι
Param SNoLevSNoLev : ιι
Known SNoLev_indSNoLev_ind : ∀ x0 : ι → ο . (∀ x1 . SNo x1(∀ x2 . x2SNoS_ (SNoLev x1)x0 x2)x0 x1)∀ x1 . SNo x1x0 x1
Param SNoCutSNoCut : ιιι
Param famunionfamunion : ι(ιι) → ι
Param omegaomega : ι
Param apap : ιιι
Param SNo_recipauxSNo_recipaux : ι(ιι) → ιι
Known recip_SNo_pos_eqrecip_SNo_pos_eq : ∀ x0 . SNo x0recip_SNo_pos x0 = SNoCut (famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 0)) (famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 1))
Definition SNoCutPSNoCutP := λ x0 x1 . and (and (∀ x2 . x2x0SNo x2) (∀ x2 . x2x1SNo x2)) (∀ x2 . x2x0∀ x3 . x3x1SNoLt x2 x3)
Known SNo_recipaux_lem2SNo_recipaux_lem2 : ∀ x0 . SNo x0SNoLt 0 x0∀ x1 : ι → ι . (∀ x2 . x2SNoS_ (SNoLev x0)SNoLt 0 x2and (SNo (x1 x2)) (mul_SNo x2 (x1 x2) = 1))SNoCutP (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 0)) (famunion omega (λ x2 . ap (SNo_recipaux x0 x1 x2) 1))
Param binunionbinunion : ιιι
Param SubqSubq : ιιο
Param SNoEq_SNoEq_ : ιιιο
Known SNoCutP_SNoCut_impredSNoCutP_SNoCut_impred : ∀ x0 x1 . SNoCutP x0 x1∀ x2 : ο . (SNo (SNoCut x0 x1)SNoLev (SNoCut x0 x1)ordsucc (binunion (famunion x0 (λ x3 . ordsucc (SNoLev x3))) (famunion x1 (λ x3 . ordsucc (SNoLev x3))))(∀ x3 . x3x0SNoLt x3 (SNoCut x0 x1))(∀ x3 . x3x1SNoLt (SNoCut x0 x1) x3)(∀ x3 . SNo x3(∀ x4 . x4x0SNoLt x4 x3)(∀ x4 . x4x1SNoLt x3 x4)and (SNoLev (SNoCut x0 x1)SNoLev x3) (SNoEq_ (SNoLev (SNoCut x0 x1)) (SNoCut x0 x1) x3))x2)x2
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known SNoLt_trichotomy_or_impredSNoLt_trichotomy_or_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 : ο . (SNoLt x0 x1x2)(x0 = x1x2)(SNoLt x1 x0x2)x2
Known SNo_1SNo_1 : SNo 1
Param SNoLeSNoLe : ιιο
Param add_SNoadd_SNo : ιιι
Param minus_SNominus_SNo : ιι
Param SNoRSNoR : ιι
Param SNoLSNoL : ιι
Known mul_SNo_SNoR_interpolate_impredmul_SNo_SNoR_interpolate_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoR (mul_SNo x0 x1)∀ x3 : ο . (∀ x4 . x4SNoL x0∀ x5 . x5SNoR x1SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo x2 (mul_SNo x4 x5))x3)(∀ x4 . x4SNoR x0∀ x5 . x5SNoL x1SNoLe (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) (add_SNo x2 (mul_SNo x4 x5))x3)x3
Known SNoR_ISNoR_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x1SNoR x0
Param ordinalordinal : ιο
Known ordinal_SNoLevordinal_SNoLev : ∀ x0 . ordinal x0SNoLev x0 = x0
Known ordinal_1ordinal_1 : ordinal 1
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known ordinal_In_Or_Subqordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0ordinal x1or (x0x1) (x1x0)
Known SNoLev_ordinalSNoLev_ordinal : ∀ x0 . SNo x0ordinal (SNoLev x0)
Known FalseEFalseE : False∀ x0 : ο . x0
Known pos_low_eq_onepos_low_eq_one : ∀ x0 . SNo x0SNoLt 0 x0SNoLev x01x0 = 1
Known mul_SNo_pos_posmul_SNo_pos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt 0 x1SNoLt 0 (mul_SNo x0 x1)
Known SNoL_ESNoL_E : ∀ x0 . SNo x0∀ x1 . x1SNoL x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x2)x2
Known SNoR_ESNoR_E : ∀ x0 . SNo x0∀ x1 . x1SNoR x0∀ x2 : ο . (SNo x1SNoLev x1SNoLev x0SNoLt x0 x1x2)x2
Known SNoR_SNoCutP_exSNoR_SNoCutP_ex : ∀ x0 x1 . SNoCutP x0 x1∀ x2 . x2SNoR (SNoCut x0 x1)∀ x3 : ο . (∀ x4 . and (x4x1) (SNoLe x4 x2)x3)x3
Known SNoS_I2SNoS_I2 : ∀ x0 x1 . SNo x0SNo x1SNoLev x0SNoLev x1x0SNoS_ (SNoLev x1)
Known famunionE_impredfamunionE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2famunion x0 x1∀ x3 : ο . (∀ x4 . x4x0x2x1 x4x3)x3
Known famunionIfamunionI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2x0x3x1 x2x3famunion x0 x1
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Param nat_pnat_p : ιο
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
Param SNo_recipauxsetSNo_recipauxset : ιιι(ιι) → ι
Param SepSep : ι(ιο) → ι
Definition SNoL_posSNoL_pos := λ x0 . Sep (SNoL x0) (SNoLt 0)
Known SNo_recipaux_SSNo_recipaux_S : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2SNo_recipaux x0 x1 (ordsucc x2) = lam 2 (λ x4 . If_i (x4 = 0) (binunion (binunion (ap (SNo_recipaux x0 x1 x2) 0) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 0) x0 (SNoR x0) x1)) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 1) x0 (SNoL_pos x0) x1)) (binunion (binunion (ap (SNo_recipaux x0 x1 x2) 1) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 0) x0 (SNoL_pos x0) x1)) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 1) x0 (SNoR x0) x1)))
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SNo_recipauxset_ISNo_recipauxset_I : ∀ x0 x1 x2 . ∀ x3 : ι → ι . ∀ x4 . x4x0∀ x5 . x5x2mul_SNo (add_SNo 1 (mul_SNo (add_SNo x5 (minus_SNo x1)) x4)) (x3 x5)SNo_recipauxset x0 x1 x2 x3
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known nonneg_mul_SNo_Lenonneg_mul_SNo_Le : ∀ x0 x1 x2 . SNo x0SNoLe 0 x0SNo x1SNo x2SNoLe x1 x2SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known SNo_minus_SNoSNo_minus_SNo : ∀ x0 . SNo x0SNo (minus_SNo x0)
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
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 SNo_0SNo_0 : SNo 0
Known add_SNo_0Ladd_SNo_0L : ∀ x0 . SNo x0add_SNo 0 x0 = x0
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known SNoLt_irrefSNoLt_irref : ∀ x0 . not (SNoLt x0 x0)
Known SNoLtLe_traSNoLtLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLe x1 x2SNoLt x0 x2
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known SNo_recipaux_lem1SNo_recipaux_lem1 : ∀ x0 . SNo x0SNoLt 0 x0∀ x1 : ι → ι . (∀ x2 . x2SNoS_ (SNoLev x0)SNoLt 0 x2and (SNo (x1 x2)) (mul_SNo x2 (x1 x2) = 1))∀ x2 . nat_p x2and (∀ x3 . x3ap (SNo_recipaux x0 x1 x2) 0and (SNo x3) (SNoLt (mul_SNo x0 x3) 1)) (∀ x3 . x3ap (SNo_recipaux x0 x1 x2) 1and (SNo x3) (SNoLt 1 (mul_SNo x0 x3)))
Known SNoLe_traSNoLe_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLe x1 x2SNoLe x0 x2
Known add_SNo_Le1add_SNo_Le1 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x2SNoLe (add_SNo x0 x1) (add_SNo x2 x1)
Known mul_SNo_nonpos_negmul_SNo_nonpos_neg : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 0SNoLt x1 0SNoLe 0 (mul_SNo x0 x1)
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
Known mul_SNo_distrLmul_SNo_distrL : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2mul_SNo x0 (add_SNo x1 x2) = add_SNo (mul_SNo x0 x1) (mul_SNo x0 x2)
Known add_SNo_com_3b_1_2add_SNo_com_3b_1_2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo (add_SNo x0 x1) x2 = add_SNo (add_SNo x0 x2) x1
Known add_SNo_minus_Le2add_SNo_minus_Le2 : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x2 (add_SNo x0 (minus_SNo x1))SNoLe (add_SNo x2 x1) x0
Known mul_SNo_minus_distrRmul_minus_SNo_distrR : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 (minus_SNo x1) = minus_SNo (mul_SNo x0 x1)
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known SNoL_SNoCutP_exSNoL_SNoCutP_ex : ∀ x0 x1 . SNoCutP x0 x1∀ x2 . x2SNoL (SNoCut x0 x1)∀ x3 : ο . (∀ x4 . and (x4x0) (SNoLe x2 x4)x3)x3
Known SNoLt_traSNoLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt x0 x1SNoLt x1 x2SNoLt x0 x2
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known nonpos_mul_SNo_Lenonpos_mul_SNo_Le : ∀ x0 x1 x2 . SNo x0SNoLe x0 0SNo x1SNo x2SNoLe x2 x1SNoLe (mul_SNo x0 x1) (mul_SNo x0 x2)
Known add_SNo_0Radd_SNo_0R : ∀ x0 . SNo x0add_SNo x0 0 = 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 SNoLt_minus_posSNoLt_minus_pos : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 x1SNoLt 0 (add_SNo x1 (minus_SNo x0))
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
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_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Known minus_add_SNo_distrminus_add_SNo_distr : ∀ x0 x1 . SNo x0SNo x1minus_SNo (add_SNo x0 x1) = add_SNo (minus_SNo x0) (minus_SNo 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 add_SNo_minus_SNo_prop2add_SNo_minus_SNo_prop2 : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 (add_SNo (minus_SNo x0) x1) = x1
Known mul_SNo_minus_distrLmul_SNo_minus_distrL : ∀ x0 x1 . SNo x0SNo x1mul_SNo (minus_SNo x0) x1 = minus_SNo (mul_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)
Known add_SNo_assocadd_SNo_assoc : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 (add_SNo x1 x2) = add_SNo (add_SNo x0 x1) x2
Known mul_SNo_SNoL_interpolate_impredmul_SNo_SNoL_interpolate_impred : ∀ x0 x1 . SNo x0SNo x1∀ x2 . x2SNoL (mul_SNo x0 x1)∀ x3 : ο . (∀ x4 . x4SNoL x0∀ x5 . x5SNoL x1SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5))x3)(∀ x4 . x4SNoR x0∀ x5 . x5SNoR x1SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5))x3)x3
Known SNoL_ISNoL_I : ∀ x0 . SNo x0∀ x1 . SNo x1SNoLev x1SNoLev x0SNoLt x1 x0x1SNoL x0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known mul_SNo_nonpos_posmul_SNo_nonpos_pos : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 0SNoLt 0 x1SNoLe (mul_SNo x0 x1) 0
Known add_SNo_minus_Lt2badd_SNo_minus_Lt2b : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt (add_SNo x2 x1) x0SNoLt x2 (add_SNo x0 (minus_SNo x1))
Known mul_SNo_pos_negmul_SNo_pos_neg : ∀ x0 x1 . SNo x0SNo x1SNoLt 0 x0SNoLt x1 0SNoLt (mul_SNo x0 x1) 0
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
Known nat_0nat_0 : nat_p 0
Param SingSing : ιι
Known SNo_recipaux_0SNo_recipaux_0 : ∀ x0 . ∀ x1 : ι → ι . SNo_recipaux x0 x1 0 = lam 2 (λ x3 . If_i (x3 = 0) (Sing 0) 0)
Known SingISingI : ∀ x0 . x0Sing x0
Theorem recip_SNo_pos_prop1recip_SNo_pos_prop1 : ∀ x0 . SNo x0SNoLt 0 x0and (SNo (recip_SNo_pos x0)) (mul_SNo x0 (recip_SNo_pos x0) = 1) (proof)