Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../8fbc9..
PUUSC../545e2..
vout
PrCit../5dda1.. 5.95 bars
TMcB3../c2d5d.. ownership of 85fe9.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHJN../23bbc.. ownership of a6731.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMYjo../8ba2f.. ownership of 1e494.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMJuJ../7a0df.. ownership of b16b3.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMcJE../83d06.. ownership of db65d.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVcg../0accd.. ownership of 5a98f.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdbk../ba2d3.. ownership of 92c84.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNnU../60623.. ownership of 3d728.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSum../3f05c.. ownership of 6d980.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMFyZ../b3279.. ownership of d1f68.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPG2../c69ce.. ownership of 091d5.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVEz../9fbcb.. ownership of 4af87.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMNdC../36772.. ownership of 9e4f1.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TML9i../99f30.. ownership of a1ac5.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPS1../499d7.. ownership of 30073.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUwL../95cca.. ownership of 7da4c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMHKK../71f6f.. ownership of d457e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMYXJ../37dc4.. ownership of 0ee26.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKiW../4c4b3.. ownership of ab802.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMP9s../d7f4a.. ownership of b4ef9.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMQao../fb95e.. ownership of a3398.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdyu../df117.. ownership of eab76.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZLm../6e635.. ownership of 099c4.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZKm../c02a0.. ownership of 1d3b7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVU9../ac821.. ownership of f2e7a.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSVq../1c75a.. ownership of b9177.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSkG../63cf2.. ownership of fcba1.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLxR../7ee42.. ownership of af602.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMRHR../be9b4.. ownership of e5bf1.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMb9W../ea941.. ownership of bc15f.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZ7b../39c92.. ownership of 983da.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMQK../8333a.. ownership of e82c5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMXVQ../17db2.. ownership of ca92e.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMati../427e7.. ownership of c56c5.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMpX../3826e.. ownership of 15d4c.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMau9../cf770.. ownership of 53e57.. as obj with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUgD2../b1e44.. doc published by Pr4zB..
Definition Church13_p := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x14) ⟶ x1 x0
Theorem fe032.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0) (proof)
Theorem 19e27.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x1) (proof)
Theorem f85ed.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x2) (proof)
Theorem 82a17.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x3) (proof)
Theorem 59a5f.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x4) (proof)
Theorem 5ca83.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x5) (proof)
Theorem 40dec.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x6) (proof)
Theorem 41eb8.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x7) (proof)
Theorem 42638.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x8) (proof)
Theorem 34c89.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x9) (proof)
Theorem bf246.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x10) (proof)
Theorem 7e49d.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x11) (proof)
Theorem cc205.. : Church13_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x12) (proof)
Definition TwoRamseyGraph_3_5_Church13 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3 x3) (x1 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2 x3) (x1 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x3 x3 x2 x3 x3 x3 x2 x3)
Definition Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x8 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7
Theorem 099c4.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 x0) (proof)
Theorem a3398.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 x0) (Church13_perm_7_8_9_10_11_12_0_1_2_3_4_5_6 x1) (proof)
Definition Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x9 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8
Theorem ab802.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x0) (proof)
Theorem d457e.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x0) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x1) (proof)
Definition Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x10 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9
Theorem 30073.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 x0) (proof)
Theorem 9e4f1.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 x0) (Church13_perm_9_10_11_12_0_1_2_3_4_5_6_7_8 x1) (proof)
Definition Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x11 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10
Theorem 091d5.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 x0) (proof)
Theorem 6d980.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 x0) (Church13_perm_10_11_12_0_1_2_3_4_5_6_7_8_9 x1) (proof)
Definition Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x12 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11
Theorem 92c84.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 x0) (proof)
Theorem db65d.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 x0) (Church13_perm_11_12_0_1_2_3_4_5_6_7_8_9_10 x1) (proof)
Definition Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x13 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12
Theorem 1e494.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p (Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 x0) (proof)
Theorem 85fe9.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church13_p x0 ⟶ Church13_p x1 ⟶ TwoRamseyGraph_3_5_Church13 x0 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 x0) (Church13_perm_12_0_1_2_3_4_5_6_7_8_9_10_11 x1) (proof)