vin

vout

Pr91C../c2b7f.. 0.00 bars
TMYXf../66756.. negprop ownership controlledby PrGxv.. upto 0
TMZXU../af956.. negprop ownership controlledby PrGxv.. upto 0
TMXqG../cca5a.. ownership of facc5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX4c../d2f82.. ownership of 751d6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPUn../2aa96.. ownership of 501e2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHJ9../9c8ce.. ownership of 5bfa7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWDN../84375.. ownership of 43fc2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFN2../8375c.. ownership of 29514.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWeT../5188f.. ownership of 3a25a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK2y../c40ac.. ownership of c50e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcjt../6d440.. ownership of 41b27.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcFN../c365e.. ownership of 23664.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbC2../997c2.. ownership of d89f9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRC6../c6d31.. ownership of f95c9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGij../92198.. ownership of 55f9f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRby../d409a.. ownership of af5a8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXru../afecf.. ownership of a5a32.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRqS../ce1d0.. ownership of 0aeb1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW1d../4f077.. ownership of b4a76.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWAe../72b50.. ownership of ed2cf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGZo../e40f1.. ownership of 6cab0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZL3../0f87a.. ownership of e7faf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNWz../032ce.. ownership of d7ca5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJXm../6e1b5.. ownership of 6430b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFcn../2b811.. ownership of 746bb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG5A../76694.. ownership of a11df.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN52../5e0f1.. ownership of a0d36.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaLo../599c0.. ownership of 8caab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLzh../f30fd.. ownership of d3c08.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXx8../a061f.. ownership of d96ec.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM7C../3ee46.. ownership of 21331.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKfC../80262.. ownership of 1a922.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcbr../6dd0f.. ownership of 4999f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHiH../5d831.. ownership of b9b6d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJnj../26855.. ownership of 5a16f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYMd../d9734.. ownership of 432d0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVMK../4f633.. ownership of de4dc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa3H../3d42e.. ownership of a79ea.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF9Q../a7be4.. ownership of 513aa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaSv../d66bf.. ownership of 20aee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQEf../2e34e.. ownership of cd385.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPB4../a7e4f.. ownership of 4e7c4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUfQ../8dbf2.. ownership of dd5e7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVz2../ced04.. ownership of 42480.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc8N../a55eb.. ownership of b3b5f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPtE../580d7.. ownership of e8726.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUvZ../b2716.. ownership of ada38.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJbB../e1e9e.. ownership of b460e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNWF../b970d.. ownership of aef25.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNNx../dfd7d.. ownership of a8878.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFLk../71d02.. ownership of 39b19.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLNW../4df86.. ownership of 233a0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcYW../527d9.. ownership of 6351a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN8a../fa82f.. ownership of b196f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYHg../1b217.. ownership of aee35.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU9d../d245f.. ownership of b88ac.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGt6../74a95.. ownership of 7ce1c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVik../0ec24.. ownership of 0d31d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd12../44560.. ownership of e37c0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWhU../be476.. ownership of 06b11.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEyZ../e195d.. ownership of f6a32.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKVw../2bf87.. ownership of a231d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMDz../0ff9e.. ownership of ce322.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUVH../a43e5.. ownership of c83fe.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUZt../05b7d.. ownership of f8050.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSp6../2bc64.. ownership of 025b7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTQu../98c4e.. ownership of 1013b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJGK../078aa.. ownership of c45ae.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNwK../8f438.. ownership of 236dc.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaAA../96dbc.. ownership of b6a57.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUfBi../e08b1.. doc published by PrGxv..

Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Param 91630.. : ι → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Known 3bafe.. : 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known fead7.. : ∀ x0 x1 . prim1 x1 (91630.. x0) ⟶ x1 = x0
Known e7a4c.. : ∀ x0 . prim1 x0 (91630.. x0)
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 6351a.. : not (TransSet (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Theorem 39b19.. : not (ordinal (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Param 0ac37.. : ι → ι → ι
Definition 15418.. := λ x0 x1 . 0ac37.. x0 (91630.. x1)
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Known 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem aef25.. : ∀ x0 . not (ordinal (15418.. x0 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Theorem ada38.. : ∀ x0 x1 . ordinal x0 ⟶ nIn (15418.. x1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x0 (proof)
Known 9ac87.. : 4ae4a.. 4a7ef.. = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Theorem b3b5f.. : nIn (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) (91630.. (91630.. (4ae4a.. 4a7ef..))) (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Definition 472ec.. := λ x0 . 0ac37.. x0 (94f9e.. x0 (λ x1 . 15418.. x1 (91630.. (4ae4a.. 4a7ef..))))
Param exactly1of2 : ο → ο → ο
Definition 1beb9.. := λ x0 x1 . and (Subq x1 (472ec.. x0)) (∀ x2 . prim1 x2 x0 ⟶ exactly1of2 (prim1 (15418.. x2 (91630.. (4ae4a.. 4a7ef..))) x1) (prim1 x2 x1))
Definition 80242.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (ordinal x2) (1beb9.. x2 x0) ⟶ x1) ⟶ x1
Known FalseE : False ⟶ ∀ x0 : ο . x0
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1)
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Theorem dd5e7.. : ∀ x0 x1 . 80242.. x0 ⟶ nIn (15418.. x1 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))) x0 (proof)
Definition 236dc.. := λ x0 x1 . 0ac37.. x0 (94f9e.. x1 (λ x2 . 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1)
Theorem cd385.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ Subq x0 x2 (proof)
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Theorem 513aa.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x2 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ x0 = x2 (proof)
Theorem de4dc.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) = 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ Subq x2 x3 (proof)
Theorem 5a16f.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 15418.. x2 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) = 15418.. x3 (91630.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x2 = x3 (proof)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem 4999f.. : ∀ x0 x1 x2 x3 . 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ Subq x1 x3 (proof)
Theorem 21331.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ x1 = x3 (proof)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem d3c08.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 236dc.. x0 x1 = 236dc.. x2 x3 ⟶ and (x0 = x2) (x1 = x3) (proof)
Known d4dbc.. : ∀ x0 : ι → ι . 94f9e.. 4a7ef.. x0 = 4a7ef..
Known 4d5c9.. : ∀ x0 . 0ac37.. x0 4a7ef.. = x0
Theorem a0d36.. : ∀ x0 . 236dc.. x0 4a7ef.. = x0 (proof)
Definition 1013b.. := λ x0 . ∀ x1 : ο . (∀ x2 . and (80242.. x2) (∀ x3 : ο . (∀ x4 . and (80242.. x4) (x0 = 236dc.. x2 x4) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Theorem 746bb.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 1013b.. (236dc.. x0 x1) (proof)
Theorem d7ca5.. : ∀ x0 . 1013b.. x0 ⟶ ∀ x1 : ι → ο . (∀ x2 x3 . 80242.. x2 ⟶ 80242.. x3 ⟶ x0 = 236dc.. x2 x3 ⟶ x1 (236dc.. x2 x3)) ⟶ x1 x0 (proof)
Known ebb60.. : 80242.. 4a7ef..
Theorem 6cab0.. : ∀ x0 . 80242.. x0 ⟶ 1013b.. x0 (proof)
Definition f8050.. := 236dc.. 4a7ef.. (4ae4a.. 4a7ef..)
Known c8ed0.. : 80242.. (4ae4a.. 4a7ef..)
Theorem b4a76.. : 1013b.. f8050.. (proof)
Definition ce322.. := λ x0 . prim0 (λ x1 . and (80242.. x1) (∀ x2 : ο . (∀ x3 . and (80242.. x3) (x0 = 236dc.. x1 x3) ⟶ x2) ⟶ x2))
Definition f6a32.. := λ x0 . prim0 (λ x1 . and (80242.. x1) (x0 = 236dc.. (ce322.. x0) x1))
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2 ⟶ x1) ⟶ x1) ⟶ x0 (prim0 x0)
Theorem a5a32.. : ∀ x0 . 1013b.. x0 ⟶ and (80242.. (ce322.. x0)) (∀ x1 : ο . (∀ x2 . and (80242.. x2) (x0 = 236dc.. (ce322.. x0) x2) ⟶ x1) ⟶ x1) (proof)
Theorem 55f9f.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ce322.. (236dc.. x0 x1) = x0 (proof)
Theorem d89f9.. : ∀ x0 . 1013b.. x0 ⟶ and (80242.. (f6a32.. x0)) (x0 = 236dc.. (ce322.. x0) (f6a32.. x0)) (proof)
Theorem 41b27.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ f6a32.. (236dc.. x0 x1) = x1 (proof)
Theorem 3a25a.. : ∀ x0 . 1013b.. x0 ⟶ 80242.. (ce322.. x0) (proof)
Theorem 43fc2.. : ∀ x0 . 1013b.. x0 ⟶ 80242.. (f6a32.. x0) (proof)
Theorem 501e2.. : ∀ x0 . 1013b.. x0 ⟶ x0 = 236dc.. (ce322.. x0) (f6a32.. x0) (proof)
Theorem facc5.. : ∀ x0 x1 . 1013b.. x0 ⟶ 1013b.. x1 ⟶ ce322.. x0 = ce322.. x1 ⟶ f6a32.. x0 = f6a32.. x1 ⟶ x0 = x1 (proof)
Param bc82c.. : ι → ι → ι
Definition e37c0.. := λ x0 x1 . 236dc.. (bc82c.. (ce322.. x0) (ce322.. x1)) (bc82c.. (f6a32.. x0) (f6a32.. x1))
Param e6316.. : ι → ι → ι
Param f4dc0.. : ι → ι
Definition 7ce1c.. := λ x0 x1 . 236dc.. (bc82c.. (e6316.. (ce322.. x0) (ce322.. x1)) (f4dc0.. (e6316.. (f6a32.. x0) (f6a32.. x1)))) (bc82c.. (e6316.. (ce322.. x0) (f6a32.. x1)) (e6316.. (f6a32.. x0) (ce322.. x1)))
Param 3b429.. : ι → (ι → ι) → (ι → ι → ο) → CT2 ι
Param f74bd.. : ι
Param True : ο
Definition aee35.. := 3b429.. f74bd.. (λ x0 . f74bd..) (λ x0 x1 . True) 236dc..

Proofgold Signed Transaction