Proofgold Signed Transaction

vin
PrEvg../ea7c2.. PUQ3t../5ab52..

vout

PrEvg../ea1c9.. 0.38 bars
TMUWd../6f6a7.. BOUNTY 1.00 bars
TMUWd../2298b.. BOUNTY 2.00 bars
TMYFw../67791.. ownership of 553b7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZV2../be569.. ownership of 30845.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTW9../751f9.. ownership of a95d2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPJ2../85ae0.. ownership of 23502.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSwG../700db.. ownership of 3d3ad.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSEp../b8a9d.. ownership of 8bc73.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUqc../115cb.. ownership of 03c76.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG2Y../07ccb.. ownership of b6c97.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKxE../01f64.. ownership of d6b7f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbUh../012fe.. ownership of 385ff.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSxB../ff859.. ownership of 8d17d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMG19../8983d.. ownership of 2f012.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGkk../ac5ca.. ownership of 1868b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJnj../544c2.. ownership of bbc4b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGf1../ee05b.. ownership of a286a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM6k../3c75f.. ownership of 74df3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT5Y../3c1f3.. ownership of 39a1f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNvA../c8e2c.. ownership of 1f078.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVLV../6a9aa.. ownership of c4cc0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZkt../c7aa2.. ownership of 3a6ab.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMjr../028fb.. ownership of 0e197.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLHe../11623.. ownership of 77f57.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSzA../80aaa.. ownership of f8636.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTxQ../a314c.. ownership of 75289.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEx9../3890a.. ownership of 8a0cb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTfT../250fb.. ownership of 9b00f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMNv../1c2af.. ownership of fed74.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWSS../0d408.. ownership of 3629c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF5K../b0337.. ownership of c99f6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSeq../f4c7b.. ownership of cea6d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFRG../b5226.. ownership of b7449.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYhi../d1e4b.. ownership of 660f1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRbb../03733.. ownership of 9a3a3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMoi../05da7.. ownership of 51bac.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNi4../68a40.. ownership of 45772.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ44../8380e.. ownership of 926cc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJne../31ea0.. ownership of 2da01.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRAj../b9f72.. ownership of 8ec5e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNVv../a62ff.. ownership of 62e33.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKFH../e8e3c.. ownership of 48bdd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRRs../fdb62.. ownership of 05f2a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX4o../75b2a.. ownership of 97cd0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZtQ../e1239.. ownership of 59827.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZRv../486df.. ownership of e2e6b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMmi../e672b.. ownership of c2c0d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWcb../a102c.. ownership of 02e04.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQLH../90549.. ownership of 456ec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcYM../e9729.. ownership of 4b415.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN5y../be334.. ownership of f2c23.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMctb../9f915.. ownership of 1558c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbJ2../f0a98.. ownership of 148f8.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX6d../fae23.. ownership of 72aa2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKrv../f352b.. ownership of f558c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaQ5../87ed0.. ownership of ebc21.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUMw../ab9a0.. ownership of d701e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTqG../4a345.. ownership of 41f06.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHRQ../d0393.. ownership of df3ca.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbA5../c8650.. ownership of 2d3cc.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPc4../4e29d.. ownership of 316b1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaZm../201ee.. ownership of 8d3ae.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHWj../4f170.. ownership of 8e91b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVQx../cc1fe.. ownership of c33c2.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMW4M../5c892.. ownership of 4b3e1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWp3../15364.. ownership of a06c3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRiA../c57d9.. ownership of 707bb.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJMw../a05ff.. ownership of 99150.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHfe../ae9a3.. ownership of 56103.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLB8../dc857.. ownership of a5d29.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMREE../7f663.. ownership of 57d6a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX3L../eb717.. ownership of 12416.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZWV../8f842.. ownership of 236c6.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaTZ../1ddd0.. ownership of aab3e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUf2B../620a8.. doc published by PrGxv..

Definition 236c6.. := prim1 (λ x0 . x0)
Known 9aea6.. : ∀ x0 x1 . ∀ x2 : ι → ι . prim0 x0 x1 = prim1 x2 ⟶ ∀ x3 : ο . x3
Theorem f558c.. : ∀ x0 x1 . 236c6.. = prim0 x0 x1 ⟶ ∀ x2 : ο . x2 (proof)
Known b4755.. : ∀ x0 x1 : ι → ι . prim1 x0 = prim1 x1 ⟶ x0 = x1
Theorem 148f8.. : ∀ x0 : ι → ι → ι . 236c6.. = prim1 (λ x2 . prim1 (x0 x2)) ⟶ ∀ x1 : ο . x1 (proof)
Theorem f2c23.. : ∀ x0 x1 : ι → ι . 236c6.. = prim1 (λ x3 . prim0 (x0 x3) (x1 x3)) ⟶ ∀ x2 : ο . x2 (proof)
Definition 57d6a.. := λ x0 x1 . prim0 236c6.. (prim0 x0 x1)
Definition 56103.. := λ x0 : ι → ι . prim0 236c6.. (prim1 x0)
Known 128d8.. : ∀ x0 x1 x2 x3 . prim0 x0 x1 = prim0 x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4
Theorem 456ec.. : ∀ x0 x1 x2 x3 . 57d6a.. x0 x1 = 57d6a.. x2 x3 ⟶ ∀ x4 : ο . (x0 = x2 ⟶ x1 = x3 ⟶ x4) ⟶ x4 (proof)
Theorem c2c0d.. : ∀ x0 x1 : ι → ι . 56103.. x0 = 56103.. x1 ⟶ x0 = x1 (proof)
Theorem 59827.. : ∀ x0 x1 . ∀ x2 : ι → ι . 57d6a.. x0 x1 = 56103.. x2 ⟶ ∀ x3 : ο . x3 (proof)
Param de327.. : (ι → ο) → ι → ι → ο
Definition 707bb.. := λ x0 : ι → ο . λ x1 . ∀ x2 : (ι → ο) → ι → ο . (∀ x3 : ι → ο . ∀ x4 . x3 x4 ⟶ x2 x3 x4) ⟶ (∀ x3 : ι → ο . ∀ x4 : ι → ι . (∀ x5 . x2 (de327.. x3 x5) (x4 x5)) ⟶ x2 x3 (56103.. x4)) ⟶ (∀ x3 : ι → ο . ∀ x4 x5 . x2 x3 x4 ⟶ x2 x3 x5 ⟶ x2 x3 (57d6a.. x4 x5)) ⟶ x2 x0 x1
Theorem 05f2a.. : ∀ x0 : ι → ο . ∀ x1 . x0 x1 ⟶ 707bb.. x0 x1 (proof)
Theorem 62e33.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . (∀ x2 . 707bb.. (de327.. x0 x2) (x1 x2)) ⟶ 707bb.. x0 (56103.. x1) (proof)
Theorem 2da01.. : ∀ x0 : ι → ο . ∀ x1 x2 . 707bb.. x0 x1 ⟶ 707bb.. x0 x2 ⟶ 707bb.. x0 (57d6a.. x1 x2) (proof)
Definition 4b3e1.. := λ x0 : ι → ο . λ x1 x2 . ∀ x3 : (ι → ο) → ι → ι → ο . (∀ x4 : ι → ο . ∀ x5 : ι → ι . ∀ x6 . (∀ x7 . 707bb.. (de327.. x4 x7) (x5 x7)) ⟶ 707bb.. x4 x6 ⟶ x3 x4 (57d6a.. (56103.. x5) x6) (x5 x6)) ⟶ (∀ x4 : ι → ο . ∀ x5 x6 : ι → ι . (∀ x7 . x3 (de327.. x4 x7) (x5 x7) (x6 x7)) ⟶ x3 x4 (56103.. x5) (56103.. x6)) ⟶ (∀ x4 : ι → ο . ∀ x5 x6 x7 . x3 x4 x5 x7 ⟶ 707bb.. x4 x6 ⟶ x3 x4 (57d6a.. x5 x6) (57d6a.. x7 x6)) ⟶ (∀ x4 : ι → ο . ∀ x5 x6 x7 . x3 x4 x6 x7 ⟶ 707bb.. x4 x5 ⟶ x3 x4 (57d6a.. x5 x6) (57d6a.. x5 x7)) ⟶ x3 x0 x1 x2
Theorem 45772.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ 4b3e1.. x0 (57d6a.. (56103.. x1) x2) (x1 x2) (proof)
Theorem 9a3a3.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι . (∀ x3 . 4b3e1.. (de327.. x0 x3) (x1 x3) (x2 x3)) ⟶ 4b3e1.. x0 (56103.. x1) (56103.. x2) (proof)
Theorem b7449.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . 4b3e1.. x0 x1 x3 ⟶ 707bb.. x0 x2 ⟶ 4b3e1.. x0 (57d6a.. x1 x2) (57d6a.. x3 x2) (proof)
Theorem c99f6.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . 4b3e1.. x0 x2 x3 ⟶ 707bb.. x0 x1 ⟶ 4b3e1.. x0 (57d6a.. x1 x2) (57d6a.. x1 x3) (proof)
Definition 8e91b.. := λ x0 : ι → ι → ο . λ x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x0 x4 x5 ⟶ x3 x4 x5) ⟶ (∀ x4 x5 x6 . x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6) ⟶ x3 x1 x2
Theorem fed74.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 . x0 x1 x2 ⟶ 8e91b.. x0 x1 x2 (proof)
Theorem 8a0cb.. : ∀ x0 : ι → ι → ο . ∀ x1 x2 x3 . 8e91b.. x0 x1 x2 ⟶ 8e91b.. x0 x2 x3 ⟶ 8e91b.. x0 x1 x3 (proof)
Definition 316b1.. := λ x0 : ι → ο . 8e91b.. (4b3e1.. x0)
Theorem f8636.. : ∀ x0 : ι → ο . ∀ x1 x2 . 4b3e1.. x0 x1 x2 ⟶ 316b1.. x0 x1 x2 (proof)
Theorem 0e197.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ 316b1.. x0 (57d6a.. (56103.. x1) x2) (x1 x2) (proof)
Theorem c4cc0.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . 316b1.. x0 x1 x2 ⟶ 316b1.. x0 x2 x3 ⟶ 316b1.. x0 x1 x3 (proof)
Definition df3ca.. := λ x0 : ι → ο . λ x1 : ι → ι → ο . λ x2 x3 . ∀ x4 : ι → ι → ο . (∀ x5 x6 . x1 x5 x6 ⟶ x4 x5 x6) ⟶ (∀ x5 . x0 x5 ⟶ x4 x5 x5) ⟶ (∀ x5 x6 . x4 x5 x6 ⟶ x4 x6 x5) ⟶ (∀ x5 x6 x7 . x4 x5 x6 ⟶ x4 x6 x7 ⟶ x4 x5 x7) ⟶ x4 x2 x3
Theorem 39a1f.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 x3 . x1 x2 x3 ⟶ df3ca.. x0 x1 x2 x3 (proof)
Theorem a286a.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 . x0 x2 ⟶ df3ca.. x0 x1 x2 x2 (proof)
Theorem 1868b.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 x3 . df3ca.. x0 x1 x2 x3 ⟶ df3ca.. x0 x1 x3 x2 (proof)
Theorem 8d17d.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ο . ∀ x2 x3 x4 . df3ca.. x0 x1 x2 x3 ⟶ df3ca.. x0 x1 x3 x4 ⟶ df3ca.. x0 x1 x2 x4 (proof)
Definition d701e.. := λ x0 : ι → ο . df3ca.. (707bb.. x0) (4b3e1.. x0)
Theorem d6b7f.. : ∀ x0 : ι → ο . ∀ x1 x2 . 4b3e1.. x0 x1 x2 ⟶ d701e.. x0 x1 x2 (proof)
Theorem 03c76.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . 707bb.. (de327.. x0 x3) (x1 x3)) ⟶ 707bb.. x0 x2 ⟶ d701e.. x0 (57d6a.. (56103.. x1) x2) (x1 x2) (proof)
Theorem 3d3ad.. : ∀ x0 : ι → ο . ∀ x1 . 707bb.. x0 x1 ⟶ d701e.. x0 x1 x1 (proof)
Theorem a95d2.. : ∀ x0 : ι → ο . ∀ x1 x2 . d701e.. x0 x1 x2 ⟶ d701e.. x0 x2 x1 (proof)
Theorem 553b7.. : ∀ x0 : ι → ο . ∀ x1 x2 x3 . d701e.. x0 x1 x2 ⟶ d701e.. x0 x2 x3 ⟶ d701e.. x0 x1 x3 (proof)
Param and : ο → ο → ο
Param 8ac9a.. : ι → ο
Conjecture 90489.. : ∀ x0 : ο . (∀ x1 . and (707bb.. 8ac9a.. x1) (∀ x2 . d701e.. (de327.. 8ac9a.. x2) (57d6a.. x1 x2) x2) ⟶ x0) ⟶ x0
Conjecture 1dd60.. : ∀ x0 : ο . (∀ x1 . and (707bb.. 8ac9a.. x1) (∀ x2 . d701e.. (de327.. 8ac9a.. x2) (57d6a.. x1 x2) (57d6a.. x2 (57d6a.. x1 x2))) ⟶ x0) ⟶ x0