Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrDfv../cc248..
PURDZ../586a6..
vout
PrDfv../63e0f.. 5.87 bars
TMTcV../70d4e.. ownership of e70f1.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMZr2../44a83.. ownership of f7f47.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUMBm../1a766.. doc published by Pr4zB..
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param setminussetminus : ιιι
Param SingSing : ιι
Param 0e688.. : (ιιο) → ιιιιιιιιιιιο
Param d1f25.. : (ιιο) → ιιιιιιιιιιιιο
Param 9f2b5.. : (ιιο) → ιιιιιιιιιιιιο
Param f55c6.. : (ιιο) → ιιιιιιιιιιιιο
Param 79b8d.. : (ιιο) → ιιιιιιιιιιιιο
Param 2e358.. : (ιιο) → ιιιιιιιιιιιιο
Param 91ad9.. : (ιιο) → ιιιιιιιιιιιιο
Param e4d70.. : (ιιο) → ιιιιιιιιιιιιο
Param 07080.. : (ιιο) → ιιιιιιιιιιιιο
Param f3db1.. : (ιιο) → ιιιιιιιιιιιιο
Param 43d0f.. : (ιιο) → ιιιιιιιιιιιιο
Param 0118b.. : (ιιο) → ιιιιιιιιιιιιο
Param ac9f0.. : (ιιο) → ιιιιιιιιιιιιο
Definition 50e24.. := λ x0 . λ x1 : ι → ι → ο . ∀ x2 : ο . (∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0d1f25.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x09f2b5.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0f55c6.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x079b8d.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x02e358.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x091ad9.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0e4d70.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x007080.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0f3db1.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x043d0f.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x00118b.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)(∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0ac9f0.. x1 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14x2)x2
Known c6fe1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x00e688.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14∀ x15 : ο . (∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0∀ x23 . x23x0∀ x24 . x24x0∀ x25 . x25x0∀ x26 . x26x0f3db1.. x2 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x3 x26x15)(∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0∀ x23 . x23x0∀ x24 . x24x0∀ x25 . x25x0∀ x26 . x26x0ac9f0.. x2 x16 x17 x18 x19 x20 x21 x22 x23 x24 x3 x25 x26x15)x15
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Theorem e70f1.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3setminus x0 (Sing x2)∀ x4 . x4x3∀ x5 . x5x3∀ x6 . x6x3∀ x7 . x7x3∀ x8 . x8x3∀ x9 . x9x3∀ x10 . x10x3∀ x11 . x11x3∀ x12 . x12x3∀ x13 . x13x3∀ x14 . x14x30e688.. x1 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x1450e24.. x0 x1 (proof)