Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrCit../6dc47..
PUWPU../2754c..
vout
PrCit../a84ec.. 5.81 bars
TMd9d../307fd.. ownership of 1c11b.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFmL../483de.. ownership of dab64.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMYoA../ec4e0.. ownership of 2bebb.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMH2A../54313.. ownership of 15a0f.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMQai../9d947.. ownership of 9c3ed.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMTvb../e5602.. ownership of a31ef.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMUZw../e5080.. ownership of bfee8.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMFqW../5274b.. ownership of f5ddb.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLLh../1f0d1.. ownership of 138c9.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWFf../79041.. ownership of 713f3.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKtx../2557a.. ownership of 3aad7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMc21../d472f.. ownership of 9faa5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMT49../fa72c.. ownership of c46f5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMMEd../bbcdb.. ownership of f510c.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMGQE../daf0d.. ownership of 7166e.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMZJt../48cfc.. ownership of 3b3a7.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMNAH../05f55.. ownership of fd1d6.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMa1c../1e658.. ownership of a97d1.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMbR5../83334.. ownership of edb63.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKhU../a0502.. ownership of e6bf5.. as prop with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLmr../7d27c.. ownership of aa942.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMXf5../cef5a.. ownership of 2d440.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMHiM../ba6b8.. ownership of 48d87.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKKw../78aa2.. ownership of 24f8e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMLiX../0c059.. ownership of 1dd2c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMH5j../476a6.. ownership of 91e94.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMKes../45afe.. ownership of 67aea.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMWcq../922e4.. ownership of 73151.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMJp4../b9406.. ownership of ac38c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
TMX1s../30e3f.. ownership of 47c3c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0
PUgrb../74824.. doc published by Pr4zB..
Definition Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4
Definition Church17_p := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . ∀ x1 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x2) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x3) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x4) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x5) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x6) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x7) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x8) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x9) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x10) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x11) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x12) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x13) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x14) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x15) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x16) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x17) ⟶ x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x18) ⟶ x1 x0
Known 51a81.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x4)
Known e224e.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x5)
Known 5d397.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x6)
Known 3b0d1.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x7)
Known e7def.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x8)
Known a8b9a.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x9)
Known 4f699.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x10)
Known 712d3.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x11)
Known d5e0f.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x12)
Known 51598.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x13)
Known 15dad.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x14)
Known 7e8b2.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x15)
Known 02267.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x16)
Known e70c8.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0)
Known 1b7f9.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x1)
Known 25b64.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x2)
Known 9e7eb.. : Church17_p (λ x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x3)
Theorem edb63.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 x0) (proof)
Definition TwoRamseyGraph_4_4_Church17 := λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x2 x3 . x0 (x1 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2) (x1 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2) (x1 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3) (x1 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2) (x1 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3) (x1 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3) (x1 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3) (x1 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2 x2) (x1 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3 x2) (x1 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3 x3) (x1 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3 x3) (x1 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2 x3) (x1 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3 x2) (x1 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2 x3) (x1 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2 x2) (x1 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3 x2) (x1 x2 x2 x3 x2 x3 x3 x3 x2 x2 x3 x3 x3 x2 x3 x2 x2 x3)
Theorem fd1d6.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 x0) (Church17_perm_4_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3 x1) (proof)
Definition Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5
Theorem 7166e.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 x0) (proof)
Theorem c46f5.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 x0) (Church17_perm_5_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4 x1) (proof)
Definition Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6
Theorem 3aad7.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 x0) (proof)
Theorem 138c9.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 x0) (Church17_perm_6_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5 x1) (proof)
Definition Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7
Theorem bfee8.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 x0) (proof)
Theorem 9c3ed.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 x0) (Church17_perm_7_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6 x1) (proof)
Definition Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 := λ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x9 x10 x11 x12 x13 x14 x15 x16 x17 x1 x2 x3 x4 x5 x6 x7 x8
Theorem 2bebb.. : ∀ x0 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p (Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 x0) (proof)
Theorem 1c11b.. : ∀ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x0 ⟶ Church17_p x1 ⟶ TwoRamseyGraph_4_4_Church17 x0 x1 = TwoRamseyGraph_4_4_Church17 (Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 x0) (Church17_perm_8_9_10_11_12_13_14_15_16_0_1_2_3_4_5_6_7 x1) (proof)