Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr53g../9f341..
PUd8D../80e57..
vout
Pr53g../4ac5b.. 1.97 bars
TMcfs../4169d.. ownership of 81723.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWFs../ef4b3.. ownership of 9122f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdmc../af9a8.. ownership of 794ec.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMq5../0ff9f.. ownership of 623f9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUD6../dad7c.. ownership of 530f4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGJk../4ce9f.. ownership of e482e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXZy../b2dd8.. ownership of 29def.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXkv../8ce38.. ownership of e62aa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKta../f93b7.. ownership of 62a6b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc8j../fbe5f.. ownership of 1ebf3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGDk../62d91.. ownership of 142e6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNDQ../2c2d7.. ownership of 609ac.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHfv../b5144.. ownership of 8a328.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHhv../4f26f.. ownership of a1109.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXpK../2a600.. ownership of 9f6be.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWMZ../06a16.. ownership of 420bb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMasf../7d8ea.. ownership of 11d6d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdUA../12f1f.. ownership of 7a16b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMz8../f3d11.. ownership of c2bca.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYpH../7cce5.. ownership of d7d39.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZfr../62bc6.. ownership of 52da6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMby2../a7d40.. ownership of c6edf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHC1../9117a.. ownership of 2c4f9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMarQ../9421f.. ownership of 058b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFCV../dfa8d.. ownership of 3f4b4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHZ3../92dd6.. ownership of f32d4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUZR6../5cabe.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param f482f.. : ι → ι → ι
Param If_i : ο → ι → ι → ι
Known 7e4c2.. : ∀ x0 . ∀ x1 : ι → ι . 0fc90.. x0 (f482f.. (0fc90.. x0 x1)) = 0fc90.. x0 x1
Theorem 3f4b4.. : ∀ x0 x1 x2 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2)))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2)) (proof)
Theorem 2c4f9.. : ∀ x0 x1 x2 x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3))))) = 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3))) (proof)
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Known 72f77.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 52da6.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) 4a7ef.. = x0 (proof)
Known c60fe.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known 5c667.. : 4ae4a.. 4a7ef.. = 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem c2bca.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (4ae4a.. 4a7ef..) = x1 (proof)
Known 2eaee.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))
Known 3a2b6.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known f9d2f.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem 11d6d.. : ∀ x0 x1 x2 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known 77d87.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 9f6be.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) 4a7ef.. = x0 (proof)
Known 42824.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 8a328.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. 4a7ef..) = x1 (proof)
Known 68d02.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 142e6.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known 778cc.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Known 57b7e.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known daead.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 0c325.. : 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Theorem 62a6b.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Param 3097a.. : ι → (ι → ι) → ι
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Known 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) (x1 x3)) ⟶ prim1 (0fc90.. x0 x2) (3097a.. x0 x1)
Known b1d09.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 x0
Theorem 29def.. : ∀ x0 x1 x2 x3 . prim1 x0 x3 ⟶ prim1 x1 x3 ⟶ prim1 x2 x3 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (b5c9f.. x3 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Param bij : ι → ι → (ι → ι) → ο
Param ba9d8.. : ι → ο
Known aa4b6.. : ∀ x0 . ba9d8.. x0 ⟶ ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) x0) ⟶ (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3) ⟶ bij x0 x0 x1
Known 2fbbc.. : ∀ x0 . ba9d8.. x0 ⟶ ba9d8.. (4ae4a.. x0)
Known d7fe6.. : ba9d8.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 530f4.. : ∀ x0 x1 x2 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ prim1 x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ prim1 x2 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ (x0 = x1 ⟶ ∀ x3 : ο . x3) ⟶ (x0 = x2 ⟶ ∀ x3 : ο . x3) ⟶ (x1 = x2 ⟶ ∀ x3 : ο . x3) ⟶ bij (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x3 . If_i (x3 = 4a7ef..) x0 (If_i (x3 = 4ae4a.. 4a7ef..) x1 x2)))) (proof)
Known aeaf9.. : ∀ x0 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x1 : ι → ο . x1 4a7ef.. ⟶ x1 (4ae4a.. 4a7ef..) ⟶ x1 (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ x1 x0
Theorem 794ec.. : ∀ x0 x1 x2 x3 x4 . prim1 x0 x4 ⟶ prim1 x1 x4 ⟶ prim1 x2 x4 ⟶ prim1 x3 x4 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (b5c9f.. x4 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Theorem 81723.. : ∀ x0 x1 x2 x3 . prim1 x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ prim1 x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ prim1 x2 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ prim1 x3 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ (x0 = x1 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x0 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x2 ⟶ ∀ x4 : ο . x4) ⟶ (x1 = x3 ⟶ ∀ x4 : ο . x4) ⟶ (x2 = x3 ⟶ ∀ x4 : ο . x4) ⟶ bij (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3))))) (proof)