Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrD1n../d4d80..
PUQNg../cdbfd..
vout
PrD1n../85e9f.. 5.10 bars
TMcW5../41e8c.. ownership of 7a7b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJHg../0e101.. ownership of c854a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLSk../ba5e9.. ownership of 33c62.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXPd../04e61.. ownership of 965f3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdEk../f9c9b.. ownership of 85552.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZek../3ad10.. ownership of a6b2d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWpG../f3d78.. ownership of bb257.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPbC../61d6f.. ownership of ab67c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP3n../95ebd.. ownership of 3daa5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbKk../e57be.. ownership of f63b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZgp../99fd0.. ownership of 31081.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVGa../3dcf4.. ownership of 96653.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVVa../150ed.. ownership of 9619e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXUM../f217c.. ownership of 52fd8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcM3../5ce13.. ownership of 7039d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUca../edef0.. ownership of 7172a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTMP../54da2.. ownership of e2ad4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZQR../94426.. ownership of 6577f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQLM../e7e09.. ownership of c9d91.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFxK../965e5.. ownership of 35e56.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTrH../6ec13.. ownership of 3956e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXua../68f00.. ownership of 66441.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHFW../6618a.. ownership of df2aa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR5X../b8c03.. ownership of 08a13.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTxB../7f85e.. ownership of d842e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPGy../c79a7.. ownership of 22e40.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKYF../0becc.. ownership of ffdcd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGdN../613c1.. ownership of 9081f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbH8../2a75d.. ownership of 431f3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSVh../18277.. ownership of abc63.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdfL../50a2f.. ownership of fb20c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbRs../e221c.. ownership of 51dd0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZi2../2d72d.. ownership of 504a8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ9g../db148.. ownership of 77f68.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPB4../5b5b1.. ownership of 7d2e2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWW9../0859f.. ownership of df289.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUSsj../7b80d.. doc published by PrGxv..
Param f482f.. : ι → ι → ι
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Known 03651.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem 7d2e2.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) 4a7ef.. = x0 (proof)
Known ff451.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (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 504a8.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. 4a7ef..) = x1 (proof)
Known a7963.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known 3a2b6.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known f9d2f.. : 4ae4a.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Theorem fb20c.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known 9044c.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (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 431f3.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Known 3b34e.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Known 37f0a.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known d1b49.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 05e02.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known 2f510.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0
Theorem ffdcd.. : ∀ x0 x1 x2 x3 x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x6 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x4 (proof)
Known 652a2.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem d842e.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) 4a7ef.. = x0 (proof)
Known 71fcb.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem df2aa.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. 4a7ef..) = x1 (proof)
Known 7f899.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 3956e.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known d88ba.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem c9d91.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Known 15e7b.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem e2ad4.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x4 (proof)
Known 98e34.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Known 3dae7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known a82a2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 7fa57.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known 67cbd.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0
Known e25a7.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0
Theorem 7039d.. : ∀ x0 x1 x2 x3 x4 x5 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x7 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x5 (proof)
Known b9890.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 9619e.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) 4a7ef.. = x0 (proof)
Known 102c8.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 31081.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. 4a7ef..) = x1 (proof)
Known 28cca.. : prim1 (4ae4a.. (4ae4a.. 4a7ef..)) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 3daa5.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2 (proof)
Known 57aad.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem bb257.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3 (proof)
Known ea5d5.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 85552.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) = x4 (proof)
Known 1ceed.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Theorem 33c62.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x5 (proof)
Known 57cc6.. : prim1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))))
Known cdcd4.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 31e4d.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. 4a7ef.. ⟶ ∀ x0 : ο . x0
Known 5ccd2.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. 4a7ef..) ⟶ ∀ x0 : ο . x0
Known 7357c.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)) ⟶ ∀ x0 : ο . x0
Known d13e3.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) ⟶ ∀ x0 : ο . x0
Known 2d896.. : 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) ⟶ ∀ x0 : ο . x0
Theorem 7a7b6.. : ∀ x0 x1 x2 x3 x4 x5 x6 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))) (λ x8 . If_i (x8 = 4a7ef..) x0 (If_i (x8 = 4ae4a.. 4a7ef..) x1 (If_i (x8 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (If_i (x8 = 4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6))))))) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) = x6 (proof)