Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrLbx../3e125..
PUMcF../076b7..
vout
PrLbx../07743.. 5.96 bars
TMHoG../160a8.. ownership of 90ebb.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVP9../a8cc4.. ownership of a7284.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVMy../614a0.. ownership of 305fb.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMURu../caa5c.. ownership of e08ec.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMGx7../8daca.. ownership of 19bdf.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMTiV../05235.. ownership of 3a476.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWPz../043f8.. ownership of 5e850.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPbU../e2c3c.. ownership of e1c22.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMa5w../603eb.. ownership of 288e6.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMJ4../19ec0.. ownership of aa5dd.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMd1E../c5854.. ownership of 9c478.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMLVJ../b788d.. ownership of d9149.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMdVT../67b30.. ownership of d584c.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMUsR../f2dcd.. ownership of 5465d.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKmk../cc027.. ownership of 5a1b8.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMVWS../ce8af.. ownership of eac44.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMSd7../66f33.. ownership of 1def7.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZXg../b1be8.. ownership of cb11a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMMNd../b71fa.. ownership of a154e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMKEB../8fe35.. ownership of c6cbd.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUZwD../6d09a.. doc published by Pr4zB..
Param 80df3.. : (ιιο) → ιιιιιο
Param notnot : οο
Definition af3c4.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (80df3.. x0 x1 x2 x3 x4 x5(x1 = x6∀ x8 : ο . x8)(x2 = x6∀ x8 : ο . x8)(x3 = x6∀ x8 : ο . x8)(x4 = x6∀ x8 : ο . x8)(x5 = x6∀ x8 : ο . x8)x0 x1 x6x0 x2 x6x0 x3 x6x0 x4 x6not (x0 x5 x6)x7)x7
Known eb3c8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x080df3.. x1 x2 x3 x4 x5 x680df3.. x1 x4 x3 x2 x5 x6
Theorem a154e.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0af3c4.. x1 x2 x3 x4 x5 x6 x7af3c4.. x1 x4 x3 x2 x5 x6 x7 (proof)
Known 803b6.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x080df3.. x1 x2 x3 x4 x5 x680df3.. x1 x2 x4 x3 x5 x6
Theorem 1def7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0af3c4.. x1 x2 x3 x4 x5 x6 x7af3c4.. x1 x2 x4 x3 x5 x6 x7 (proof)
Known 3ee71.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x080df3.. x1 x2 x3 x4 x5 x680df3.. x1 x5 x3 x4 x2 x6
Theorem 5a1b8.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0af3c4.. x1 x2 x3 x4 x5 x6 x7af3c4.. x1 x5 x3 x4 x2 x6 x7 (proof)
Known 389b5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x080df3.. x1 x2 x3 x4 x5 x680df3.. x1 x2 x5 x4 x3 x6
Theorem d584c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0af3c4.. x1 x2 x3 x4 x5 x6 x7af3c4.. x1 x2 x5 x4 x3 x6 x7 (proof)
Definition 2bd79.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (af3c4.. x0 x1 x2 x3 x4 x5 x6(x1 = x7∀ x9 : ο . x9)(x2 = x7∀ x9 : ο . x9)(x3 = x7∀ x9 : ο . x9)(x4 = x7∀ x9 : ο . x9)(x5 = x7∀ x9 : ο . x9)(x6 = x7∀ x9 : ο . x9)x0 x1 x7x0 x2 x7x0 x3 x7x0 x4 x7not (x0 x5 x7)not (x0 x6 x7)x8)x8
Theorem 9c478.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x02bd79.. x1 x2 x3 x4 x5 x6 x7 x82bd79.. x1 x4 x3 x2 x5 x6 x7 x8 (proof)
Theorem 288e6.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x02bd79.. x1 x2 x3 x4 x5 x6 x7 x82bd79.. x1 x2 x4 x3 x5 x6 x7 x8 (proof)
Theorem 5e850.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x02bd79.. x1 x2 x3 x4 x5 x6 x7 x82bd79.. x1 x5 x3 x4 x2 x6 x7 x8 (proof)
Theorem 19bdf.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x02bd79.. x1 x2 x3 x4 x5 x6 x7 x82bd79.. x1 x2 x5 x4 x3 x6 x7 x8 (proof)
Theorem 305fb.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x02bd79.. x1 x2 x3 x4 x5 x6 x7 x82bd79.. x1 x4 x5 x2 x3 x6 x7 x8 (proof)
Theorem 90ebb.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x02bd79.. x1 x2 x3 x4 x5 x6 x7 x82bd79.. x1 x5 x4 x3 x2 x6 x7 x8 (proof)