Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../fcca8..
PUcK1../1e19c..
vout
PrCit../315bb.. 6.22 bars
TMGtF../ebda1.. ownership of a6047.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMP15../78226.. ownership of 7f4cc.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMbXb../2aab3.. ownership of 5b991.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMX8p../1a46c.. ownership of 51bec.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJ7Y../c84f3.. ownership of 256ca.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLMR../a0124.. ownership of a056e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRdr../ea363.. ownership of 2eeb3.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMf6../a0cb8.. ownership of 8bd16.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWkA../ae0dd.. ownership of c88e0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNKn../cf394.. ownership of 80fb4.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMcL3../8d0e1.. ownership of 020b9.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFwM../7f92e.. ownership of a6105.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNM3../d7515.. ownership of e8bc0.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMYgT../9d05a.. ownership of eab19.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUYm../ee1fb.. ownership of eb0c4.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFKV../f1569.. ownership of 20fce.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPCZ../d1925.. ownership of c5737.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTmW../de454.. ownership of b1ab5.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMU34../fc57c.. ownership of cb57f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPb3../7f28c.. ownership of 6b767.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMH7y../d895a.. ownership of 1c73f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMSK../a5a4e.. ownership of 3ec05.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPjb../79452.. ownership of 29ffa.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRKA../b18e2.. ownership of 0135c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWrd../f314c.. ownership of 86ed7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUJg../5e5e7.. ownership of e980f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMX9T../ed065.. ownership of c01ee.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUQi../97fb9.. ownership of 3dc3c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUXp3../b1454.. doc published by Pr4zB..
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Known set_extset_ext : ∀ x0 x1 . x0x1x1x0x0 = x1
Theorem c01ee.. : ∀ x0 x1 . x1x0∀ x2 . x2x0(∀ x3 . x3x0x3x1x3x2)(∀ x3 . x3x0x3x2x3x1)x1 = x2 (proof)
Param ordsuccordsucc : ιι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known cases_3cases_3 : ∀ x0 . x03∀ x1 : ι → ο . x1 0x1 1x1 2x1 x0
Definition FalseFalse := ∀ x0 : ο . x0
Known FalseEFalseE : False∀ x0 : ο . x0
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Known In_2_3In_2_3 : 23
Known orILorIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIRorIR : ∀ x0 x1 : ο . x1or x0 x1
Known In_1_3In_1_3 : 13
Known In_0_3In_0_3 : 03
Theorem 86ed7.. : ∀ x0 . x03∀ x1 . x13(x0 = x1∀ x2 : ο . x2)∀ x2 : ο . (∀ x3 . and (x33) (∀ x4 . x43(x4 = x3∀ x5 : ο . x5)or (x4 = x0) (x4 = x1))x2)x2 (proof)
Definition notnot := λ x0 : ο . x0False
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known prop_ext_2prop_ext_2 : ∀ x0 x1 : ο . (x0x1)(x1x0)x0 = x1
Theorem 29ffa.. : ∀ x0 x1 : ο . (x0 = x1∀ x2 : ο . x2)∀ x2 : ο . or (x2 = x0) (x2 = x1) (proof)
Param bijbij : ιι(ιι) → ο
Definition equipequip := λ x0 x1 . ∀ x2 : ο . (∀ x3 : ι → ι . bij x0 x1 x3x2)x2
Param apap : ιιι
Param lamSigma : ι(ιι) → ι
Param If_iIf_i : οιιι
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 cases_2cases_2 : ∀ x0 . x02∀ x1 : ι → ο . x1 0x1 1x1 x0
Known tuple_2_0_eqtuple_2_0_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 0 = x0
Known tuple_2_1_eqtuple_2_1_eq : ∀ x0 x1 . ap (lam 2 (λ x3 . If_i (x3 = 0) x0 x1)) 1 = x1
Known In_0_2In_0_2 : 02
Known In_1_2In_1_2 : 12
Theorem 1c73f.. : ∀ x0 x1 . x1x0∀ x2 . x2x0(x1 = x2∀ x3 : ο . x3)(∀ x3 . x3x0or (x3 = x1) (x3 = x2))equip 2 x0 (proof)
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
Definition nInnIn := λ x0 x1 . not (x0x1)
Known Empty_eqEmpty_eq : ∀ x0 . (∀ x1 . nIn x1 x0)x0 = 0
Known EmptyEEmptyE : ∀ x0 . nIn x0 0
Theorem cb57f.. : ∀ x0 . atleastp x0 0x0 = 0 (proof)
Known equip_atleastpequip_atleastp : ∀ x0 x1 . equip x0 x1atleastp x0 x1
Known equip_symequip_sym : ∀ x0 x1 . equip x0 x1equip x1 x0
Theorem c5737.. : ∀ x0 . equip 0 x0x0 = 0 (proof)
Param binunionbinunion : ιιι
Param setminussetminus : ιιι
Param SingSing : ιι
Known binunionI2binunionI2 : ∀ x0 x1 x2 . x2x1x2binunion x0 x1
Known SingISingI : ∀ x0 . x0Sing x0
Known binunionI1binunionI1 : ∀ x0 x1 x2 . x2x0x2binunion x0 x1
Known setminusIsetminusI : ∀ x0 x1 x2 . x2x0nIn x2 x1x2setminus x0 x1
Known SingESingE : ∀ x0 x1 . x1Sing x0x1 = x0
Known binunionEbinunionE : ∀ x0 x1 x2 . x2binunion x0 x1or (x2x0) (x2x1)
Known setminusE1setminusE1 : ∀ x0 x1 x2 . x2setminus x0 x1x2x0
Theorem eb0c4..binunion_remove1_eq : ∀ x0 x1 . x1x0x0 = binunion (setminus x0 (Sing x1)) (Sing x1) (proof)
Known bijEbijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2∀ x3 : ο . ((∀ x4 . x4x0x2 x4x1)(∀ x4 . x4x0∀ x5 . x5x0x2 x4 = x2 x5x4 = x5)(∀ x4 . x4x1∀ x5 : ο . (∀ x6 . and (x6x0) (x2 x6 = x4)x5)x5)x3)x3
Known ordsuccEordsuccE : ∀ x0 x1 . x1ordsucc x0or (x1x0) (x1 = x0)
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 In_irrefIn_irref : ∀ x0 . nIn x0 x0
Known ordsuccI1ordsuccI1 : ∀ x0 . x0ordsucc x0
Known ordsuccI2ordsuccI2 : ∀ x0 . x0ordsucc x0
Theorem e8bc0..equip_adjoin_ordsucc : ∀ x0 x1 x2 . nIn x2 x1equip x0 x1equip (ordsucc x0) (binunion x1 (Sing x2)) (proof)
Param setsumsetsum : ιιι
Param Inj1Inj1 : ιι
Param Inj0Inj0 : ιι
Known setsum_Inj_invsetsum_Inj_inv : ∀ x0 x1 x2 . x2setsum x0 x1or (∀ x3 : ο . (∀ x4 . and (x4x0) (x2 = Inj0 x4)x3)x3) (∀ x3 : ο . (∀ x4 . and (x4x1) (x2 = Inj1 x4)x3)x3)
Known Inj0_setsumInj0_setsum : ∀ x0 x1 x2 . x2x0Inj0 x2setsum x0 x1
Known Inj1_setsumInj1_setsum : ∀ x0 x1 x2 . x2x1Inj1 x2setsum x0 x1
Known ReplIReplI : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2x0x1 x2prim5 x0 x1
Known ReplE_impredReplE_impred : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2prim5 x0 x1∀ x3 : ο . (∀ x4 . x4x0x2 = x1 x4x3)x3
Theorem 020b9.. : ∀ x0 x1 x2 . setsum x0 (binunion x1 x2) = binunion (setsum x0 x1) (prim5 x2 Inj1) (proof)
Param nat_pnat_p : ιο
Param add_natadd_nat : ιιι
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 equip_traequip_tra : ∀ x0 x1 x2 . equip x0 x1equip x1 x2equip x0 x2
Known Inj0_injInj0_inj : ∀ x0 x1 . Inj0 x0 = Inj0 x1x0 = x1
Known add_nat_SRadd_nat_SR : ∀ x0 x1 . nat_p x1add_nat x0 (ordsucc x1) = ordsucc (add_nat x0 x1)
Known Repl_SingRepl_Sing : ∀ x0 : ι → ι . ∀ x1 . prim5 (Sing x1) x0 = Sing (x0 x1)
Known Inj0_Inj1_neqInj0_Inj1_neq : ∀ x0 x1 . Inj0 x0 = Inj1 x1∀ x2 : ο . x2
Known setminusE2setminusE2 : ∀ x0 x1 x2 . x2setminus x0 x1nIn x2 x1
Known Inj1_injInj1_inj : ∀ x0 x1 . Inj1 x0 = Inj1 x1x0 = x1
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Theorem c88e0.. : ∀ x0 x1 x2 x3 . nat_p x0nat_p x1equip x0 x2equip x1 x3equip (add_nat x0 x1) (setsum x2 x3) (proof)
Known nat_0nat_0 : nat_p 0
Theorem 2eeb3.. : add_nat 2 1 = 3 (proof)
Known nat_1nat_1 : nat_p 1
Theorem 256ca.. : add_nat 2 2 = 4 (proof)
Known nat_2nat_2 : nat_p 2
Known equip_refequip_ref : ∀ x0 . equip x0 x0
Theorem 5b991.. : equip 4 (setsum 2 2) (proof)
Known PowerEPowerE : ∀ x0 x1 . x1prim4 x0x1x0
Known dnegdneg : ∀ x0 : ο . not (not x0)x0
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known In_0_1In_0_1 : 01
Theorem a6047.. : ∀ x0 . x0prim4 3∀ x1 . x1prim4 3(∀ x2 . x2x0∀ x3 . x3x1∀ x4 : ο . (∀ x5 . and (x53) (∀ x6 : ο . (∀ x7 . and (x73) (and (and (x5 = x7∀ x8 : ο . x8) (x5x2 = x5x3)) (x7x2 = x7x3))x6)x6)x4)x4)∀ x2 : ο . (atleastp x0 1x2)(atleastp x1 1x2)(equip 2 x0equip 2 x1x2)x2 (proof)