vin

vout

Pr91C../5b738.. 0.02 bars
TMM2T../e5bae.. ownership of 109c3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSRg../e62e7.. ownership of a7b37.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWqH../87c30.. ownership of 0ae99.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWXT../010e7.. ownership of 59185.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQuH../97f76.. ownership of b588d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKEN../2e800.. ownership of 8931c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ3j../8bda6.. ownership of c756b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKhh../222b6.. ownership of 137b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZWm../9e95d.. ownership of 9ca29.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMfg../5245a.. ownership of 8b487.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG9Q../c64b3.. ownership of 62f13.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXMX../bed2c.. ownership of 46648.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML1f../16e89.. ownership of bb32b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMqw../d21fd.. ownership of a6de6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSTn../bd393.. ownership of f97a7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVMv../4c618.. ownership of 02c4d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFac../0c52f.. ownership of 0345c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWv8../7e2ca.. ownership of 0e648.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc3C../d899e.. ownership of 896e2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXVn../6a508.. ownership of d3837.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNPZ../84e95.. ownership of bd0b9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGxN../f8eff.. ownership of 65fab.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMThN../59652.. ownership of e581a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMjs../bb2ca.. ownership of 4ae83.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUK9b../553d0.. doc published by PrGxv..

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Definition empty_p := λ x0 . ∀ x1 . nIn x1 x0
Definition e581a.. := λ x0 . not (empty_p x0)
Param 4a7ef.. : ι
Definition bd0b9.. := prim1 4a7ef..
Param If_i : ο → ι → ι → ι
Param 4ae4a.. : ι → ι
Definition 896e2.. := λ x0 : ο . If_i x0 (4ae4a.. 4a7ef..) 4a7ef..
Param 48ef8.. : ι
Known 8ee89.. : prim1 4a7ef.. 48ef8..
Theorem 0345c.. : e581a.. 48ef8.. (proof)
Param 3097a.. : ι → (ι → ι) → ι
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Param f482f.. : ι → ι → ι
Known d8d74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 (3097a.. x0 x1) ⟶ prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) (x1 x3)
Theorem f97a7.. : ∀ x0 x1 x2 . prim1 x2 (b5c9f.. x1 x0) ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (f482f.. x2 x3) x1 (proof)
Theorem bb32b.. : ∀ x0 x1 x2 x3 . prim1 x3 (b5c9f.. (b5c9f.. x2 x1) x0) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x1 ⟶ prim1 (f482f.. (f482f.. x3 x4) x5) x2 (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Theorem 62f13.. : ∀ x0 . e581a.. x0 ⟶ ∀ x1 : ο . (∀ x2 . prim1 x2 x0 ⟶ x1) ⟶ x1 (proof)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known xm : ∀ x0 : ο . or x0 (not x0)
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 9ca29.. : ∀ x0 : ο . prim1 (896e2.. x0) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known 9f6cd.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem c756b.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ bd0b9.. x0 ⟶ x0 = 4ae4a.. 4a7ef.. (proof)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Theorem b588d.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ not (bd0b9.. x0) ⟶ x0 = 4a7ef.. (proof)
Theorem 0ae99.. : ∀ x0 : ο . x0 ⟶ bd0b9.. (896e2.. x0) (proof)
Theorem 109c3.. : ∀ x0 : ο . bd0b9.. (896e2.. x0) ⟶ x0 (proof)

Proofgold Signed Transaction