Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNHZ../2723b..
PUPbB../eb11d..
vout
PrNHZ../283e1.. 63.93 bars
TMdxU../c5b09.. ownership of 680b2.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMPHC../6c8d3.. ownership of a25be.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbch../7ed43.. ownership of 7929c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMVpW../cfec7.. ownership of 7f1de.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMLKH../28d65.. ownership of 1af62.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMa7j../9be96.. ownership of 26314.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMMQa../29f4c.. ownership of 02125.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbAz../b56d3.. ownership of 3c7c0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMNYM../e2f87.. ownership of 16a34.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMMym../8ac26.. ownership of 80723.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWgx../a0d61.. ownership of d0bc5.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMWwY../42eec.. ownership of 6914a.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMEtW../67a7a.. ownership of 6d267.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMF6e../7f388.. ownership of 31c42.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMYFW../42fcb.. ownership of 2749c.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMUER../59742.. ownership of 0691e.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMc3W../ccd77.. ownership of 694b2.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMG6C../549c3.. ownership of e4a86.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMYeH../947d3.. ownership of 412d0.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMJDi../21b01.. ownership of 94724.. as prop with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMbJv../2ac25.. ownership of 89fb5.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
TMVWB../8195d.. ownership of 4f6fe.. as obj with payaddr PrQUS.. rights free controlledby PrQUS.. upto 0
PUcxH../aa19c.. doc published by PrQUS..
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param intint : ι
Param SNoS_SNoS_ : ιι
Param omegaomega : ι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Param mul_SNomul_SNo : ιιι
Param eps_eps_ : ιι
Definition diadic_rational_pdiadic_rational_p := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2omega) (∀ x3 : ο . (∀ x4 . and (x4int) (x0 = mul_SNo (eps_ x2) x4)x3)x3)x1)x1
Known diadic_rational_p_SNoS_omegadiadic_rational_p_SNoS_omega : ∀ x0 . diadic_rational_p x0x0SNoS_ omega
Known int_diadic_rational_pint_diadic_rational_p : ∀ x0 . x0intdiadic_rational_p x0
Theorem Subq_int_SNoS_omegaSubq_int_SNoS_omega : intSNoS_ omega (proof)
Param SepSep : ι(ιο) → ι
Param realreal : ι
Param setminussetminus : ιιι
Param SingSing : ιι
Param recip_SNorecip_SNo : ιι
Definition div_SNodiv_SNo := λ x0 x1 . mul_SNo x0 (recip_SNo x1)
Definition rationalrational := {x0 ∈ real|∀ x1 : ο . (∀ x2 . and (x2int) (∀ x3 : ο . (∀ x4 . and (x4setminus omega (Sing 0)) (x0 = div_SNo x2 x4)x3)x3)x1)x1}
Known SNoS_omega_diadic_rational_pSNoS_omega_diadic_rational_p : ∀ x0 . x0SNoS_ omegadiadic_rational_p x0
Param nat_pnat_p : ιο
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known SNoS_omega_realSNoS_omega_real : SNoS_ omegareal
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Param exp_SNo_natexp_SNo_nat : ιιι
Param ordsuccordsucc : ιι
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition nInnIn := λ x0 x1 . not (x0x1)
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known nat_p_omeganat_p_omega : ∀ x0 . nat_p x0x0omega
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
Known neq_1_0neq_1_0 : 1 = 0∀ x0 : ο . x0
Known mul_SNo_eps_power_2mul_SNo_eps_power_2 : ∀ x0 . nat_p x0mul_SNo (eps_ x0) (exp_SNo_nat 2 x0) = 1
Param SNoSNo : ιο
Known mul_SNo_zeroRmul_SNo_zeroR : ∀ x0 . SNo x0mul_SNo x0 0 = 0
Known SNo_eps_SNo_eps_ : ∀ x0 . x0omegaSNo (eps_ x0)
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known recip_SNo_pow_2recip_SNo_pow_2 : ∀ x0 . nat_p x0recip_SNo (exp_SNo_nat 2 x0) = eps_ x0
Known mul_SNo_commul_SNo_com : ∀ x0 x1 . SNo x0SNo x1mul_SNo x0 x1 = mul_SNo x1 x0
Known int_SNoint_SNo : ∀ x0 . x0intSNo x0
Known omega_nat_pomega_nat_p : ∀ x0 . x0omeganat_p x0
Theorem Subq_SNoS_omega_rationalSubq_SNoS_omega_rational : SNoS_ omegarational (proof)
Known Sep_SubqSep_Subq : ∀ x0 . ∀ x1 : ι → ο . Sep x0 x1x0
Theorem Subq_rational_realSubq_rational_real : rationalreal (proof)
Param minus_SNominus_SNo : ιι
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known real_minus_SNoreal_minus_SNo : ∀ x0 . x0realminus_SNo x0real
Known int_minus_SNoint_minus_SNo : ∀ x0 . x0intminus_SNo x0int
Known mul_SNo_nonzero_cancelmul_SNo_nonzero_cancel_L : ∀ x0 x1 x2 . SNo x0(x0 = 0∀ x3 : ο . x3)SNo x1SNo x2mul_SNo x0 x1 = mul_SNo x0 x2x1 = x2
Known real_SNoreal_SNo : ∀ x0 . x0realSNo x0
Known SNo_div_SNoSNo_div_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (div_SNo x0 x1)
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 mul_div_SNo_invRmul_div_SNo_invR : ∀ x0 x1 . SNo x0SNo x1(x1 = 0∀ x2 : ο . x2)mul_SNo x1 (div_SNo x0 x1) = x0
Known SingISingI : ∀ x0 . x0Sing x0
Known omega_SNoomega_SNo : ∀ x0 . x0omegaSNo x0
Theorem rational_minus_SNorational_minus_SNo : ∀ x0 . x0rationalminus_SNo x0rational (proof)
Param add_SNoadd_SNo : ιιι
Definition nat_pairnat_pair := λ x0 x1 . mul_SNo (exp_SNo_nat 2 x0) (add_SNo (mul_SNo 2 x1) 1)
Known mul_SNo_In_omegamul_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegamul_SNo x0 x1omega
Known add_SNo_In_omegaadd_SNo_In_omega : ∀ x0 . x0omega∀ x1 . x1omegaadd_SNo x0 x1omega
Known nat_1nat_1 : nat_p 1
Theorem nat_pair_In_omeganat_pair_In_omega : ∀ x0 . x0omega∀ x1 . x1omeganat_pair x0 x1omega (proof)
Param even_nateven_nat : ιο
Param mul_natmul_nat : ιιι
Known mul_nat_mul_SNomul_nat_mul_SNo : ∀ x0 . x0omega∀ x1 . x1omegamul_nat x0 x1 = mul_SNo x0 x1
Known even_nat_doubleeven_nat_double : ∀ x0 . nat_p x0even_nat (mul_nat 2 x0)
Theorem even_nat_2x : ∀ x0 . x0omegaeven_nat (mul_SNo 2 x0) (proof)
Param odd_natodd_nat : ιο
Param ordinalordinal : ιο
Known ordinal_ordsucc_SNo_eqordinal_ordsucc_SNo_eq : ∀ x0 . ordinal x0ordsucc x0 = add_SNo 1 x0
Known nat_p_ordinalnat_p_ordinal : ∀ x0 . nat_p x0ordinal x0
Known even_nat_odd_nat_Seven_nat_odd_nat_S : ∀ x0 . even_nat x0odd_nat (ordsucc x0)
Theorem odd_nat_1p2x : ∀ x0 . x0omegaodd_nat (add_SNo 1 (mul_SNo 2 x0)) (proof)
Known add_SNo_comadd_SNo_com : ∀ x0 x1 . SNo x0SNo x1add_SNo x0 x1 = add_SNo x1 x0
Known SNo_mul_SNoSNo_mul_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (mul_SNo x0 x1)
Known SNo_2SNo_2 : SNo 2
Known SNo_1SNo_1 : SNo 1
Theorem odd_nat_2xp1 : ∀ x0 . x0omegaodd_nat (add_SNo (mul_SNo 2 x0) 1) (proof)
Known nat_complete_indnat_complete_ind : ∀ x0 : ι → ο . (∀ x1 . nat_p x1(∀ x2 . x2x1x0 x2)x0 x1)∀ x1 . nat_p x1x0 x1
Known nat_inv_imprednat_inv_impred : ∀ x0 : ι → ο . x0 0(∀ x1 . nat_p x1x0 (ordsucc x1))∀ x1 . nat_p x1x0 x1
Known FalseEFalseE : False∀ x0 : ο . x0
Known even_nat_not_odd_nateven_nat_not_odd_nat : ∀ x0 . even_nat x0not (odd_nat x0)
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)
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 SNo_exp_SNo_natSNo_exp_SNo_nat : ∀ x0 . SNo x0∀ x1 . nat_p x1SNo (exp_SNo_nat x0 x1)
Known SNo_add_SNoSNo_add_SNo : ∀ x0 x1 . SNo x0SNo x1SNo (add_SNo x0 x1)
Known nat_p_SNonat_p_SNo : ∀ x0 . nat_p x0SNo x0
Known exp_SNo_nat_0exp_SNo_nat_0 : ∀ x0 . SNo x0exp_SNo_nat x0 0 = 1
Known mul_SNo_oneLmul_SNo_oneL : ∀ x0 . SNo x0mul_SNo 1 x0 = x0
Param SNoLtSNoLt : ιιο
Known ordinal_SNoLt_Inordinal_SNoLt_In : ∀ x0 x1 . ordinal x0ordinal x1SNoLt x0 x1x0x1
Known pos_mul_SNo_Lt'pos_mul_SNo_Lt : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLt 0 x2SNoLt x0 x1SNoLt (mul_SNo x0 x2) (mul_SNo x1 x2)
Known nat_ordsuccnat_ordsucc : ∀ x0 . nat_p x0nat_p (ordsucc x0)
Param SNoLeSNoLe : ιιο
Known SNoLeLt_traSNoLeLt_tra : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2SNoLe x0 x1SNoLt x1 x2SNoLt x0 x2
Known SNo_0SNo_0 : SNo 0
Known mul_SNo_nonneg_nonnegmul_SNo_nonneg_nonneg : ∀ x0 x1 . SNo x0SNo x1SNoLe 0 x0SNoLe 0 x1SNoLe 0 (mul_SNo x0 x1)
Known SNoLtLeSNoLtLe : ∀ x0 x1 . SNoLt x0 x1SNoLe x0 x1
Known SNoLt_0_2SNoLt_0_2 : SNoLt 0 2
Known omega_nonnegomega_nonneg : ∀ x0 . x0omegaSNoLe 0 x0
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_0_1SNoLt_0_1 : SNoLt 0 1
Known exp_SNo_nat_posexp_SNo_nat_pos : ∀ x0 . SNo x0SNoLt 0 x0∀ x1 . nat_p x1SNoLt 0 (exp_SNo_nat x0 x1)
Known SNoLt_1_2SNoLt_1_2 : SNoLt 1 2
Known neq_2_0neq_2_0 : 2 = 0∀ x0 : ο . x0
Theorem nat_pair_0nat_pair_0 : ∀ x0 . x0omega∀ x1 . x1omega∀ x2 . x2omega∀ x3 . x3omeganat_pair x0 x1 = nat_pair x2 x3x0 = x2 (proof)
Known add_SNo_cancel_Radd_SNo_cancel_R : ∀ x0 x1 x2 . SNo x0SNo x1SNo x2add_SNo x0 x1 = add_SNo x2 x1x0 = x2
Theorem nat_pair_1nat_pair_1 : ∀ x0 . x0omega∀ x1 . x1omega∀ x2 . x2omega∀ x3 . x3omeganat_pair x0 x1 = nat_pair x2 x3x1 = x3 (proof)
Param equipequip : ιιο
Definition injinj := λ x0 x1 . λ x2 : ι → ι . and (∀ x3 . x3x0x2 x3x1) (∀ x3 . x3x0∀ x4 . x4x0x2 x3 = x2 x4x3 = x4)
Definition atleastpatleastp := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . inj x0 x1 x3x2)x2
Known 2c48a..atleastp_antisym_equip : ∀ x0 x1 . atleastp x0 x1atleastp x1 x0equip x0 x1
Known Subq_atleastpSubq_atleastp : ∀ x0 x1 . x0x1atleastp x0 x1
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known Subq_omega_intSubq_omega_int : omegaint
Param If_iIf_i : οιιι
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known SNoLtLe_orSNoLtLe_or : ∀ x0 x1 . SNo x0SNo x1or (SNoLt x0 x1) (SNoLe x1 x0)
Known minus_SNo_Lt_contra2minus_SNo_Lt_contra2 : ∀ x0 x1 . SNo x0SNo x1SNoLt x0 (minus_SNo x1)SNoLt x1 (minus_SNo x0)
Known minus_SNo_0minus_SNo_0 : minus_SNo 0 = 0
Known nat_0nat_0 : nat_p 0
Known minus_SNo_involminus_SNo_invol : ∀ x0 . SNo x0minus_SNo (minus_SNo x0) = x0
Known neq_0_1neq_0_1 : 0 = 1∀ x0 : ο . x0
Known If_i_0If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0If_i x0 x1 x2 = x2
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 If_i_1If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0If_i x0 x1 x2 = x1
Known Eps_i_exEps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Known int_3_casesint_3_cases : ∀ x0 . x0int∀ x1 : ο . (∀ x2 . x2omegax0 = minus_SNo (ordsucc x2)x1)(x0 = 0x1)(∀ x2 . x2omegax0 = ordsucc x2x1)x1
Known mul_SNo_zeroLmul_SNo_zeroL : ∀ x0 . SNo x0mul_SNo 0 x0 = 0
Known SNo_recip_SNoSNo_recip_SNo : ∀ x0 . SNo x0SNo (recip_SNo x0)
Known recip_SNo_of_pos_is_posrecip_SNo_of_pos_is_pos : ∀ x0 . SNo x0SNoLt 0 x0SNoLt 0 (recip_SNo x0)
Known SNoLeESNoLeE : ∀ x0 x1 . SNo x0SNo x1SNoLe x0 x1or (SNoLt x0 x1) (x0 = x1)
Known minus_SNo_Lt_contra1minus_SNo_Lt_contra1 : ∀ x0 x1 . SNo x0SNo x1SNoLt (minus_SNo x0) x1SNoLt (minus_SNo x1) x0
Known omega_ordsuccomega_ordsucc : ∀ x0 . x0omegaordsucc x0omega
Known ordinal_In_SNoLtordinal_In_SNoLt : ∀ x0 . ordinal x0∀ x1 . x1x0SNoLt x1 x0
Known nat_0_in_ordsuccnat_0_in_ordsucc : ∀ x0 . nat_p x00ordsucc x0
Theorem form100_3form100_3 : equip omega rational (proof)