Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr8bR../34e89..
PUSo6../7f8ba..
vout
Pr8bR../09643.. 0.07 bars
TMGCb../9bc11.. ownership of ed5b9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaXQ../82a8e.. ownership of 54bb6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXKG../4f2e7.. ownership of ca858.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTzA../b3fe5.. ownership of f4c47.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXPb../f07dd.. ownership of 4a843.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNou../57477.. ownership of e1c00.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFZF../27c4c.. ownership of ad682.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYWr../9fc94.. ownership of 7b7fb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEn5../2c206.. ownership of 073b4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMbY../d4460.. ownership of aac19.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRnd../f29d8.. ownership of fa00b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGoA../434c9.. ownership of 9ca49.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKxQ../6f8ca.. ownership of 70f5e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKNB../7baa0.. ownership of 97106.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH8o../63b33.. ownership of 3350d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTb4../70c34.. ownership of 403e0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHiB../e041f.. ownership of 1038f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdAi../70cd4.. ownership of a489d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUDC../32e0e.. ownership of 8b23b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH6m../137b4.. ownership of 3c675.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHiP../a6cd7.. ownership of 2a18c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZN4../1b83f.. ownership of bdbe4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXJM../9fd10.. ownership of 65db8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcGK../78903.. ownership of 72a10.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTzH../a5974.. ownership of baee2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaPP../51544.. ownership of 87e2f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdYA../d2177.. ownership of 5d9d4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXM6../4b42f.. ownership of 11672.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH1J../b54bb.. ownership of 5144e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYAc../656e9.. ownership of 4e34a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZpX../23472.. ownership of 40681.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPo4../f957a.. ownership of 30c79.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQUN../44704.. ownership of cba25.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSHG../a3001.. ownership of b2e39.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVCG../17595.. ownership of 1906a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSzi../1c37a.. ownership of ab3e7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEhR../774fe.. ownership of eb5ba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdNE../5eace.. ownership of 3341a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX9d../90973.. ownership of f24af.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMafy../c09e8.. ownership of 15201.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXyX../8d413.. ownership of 08d14.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGzF../d4b0f.. ownership of 36f11.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFwd../f2571.. ownership of e7471.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbjN../f4692.. ownership of 2dabd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLm8../9f6f7.. ownership of 7abb3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPt9../6f556.. ownership of 4f5a0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJRc../5ec0f.. ownership of 6f4d6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN6y../e7e86.. ownership of 5b79c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSqR../a2a1c.. ownership of b846f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbyF../aac7b.. ownership of 7c0f0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUbD9../7d134.. doc published by PrGxv..
Param ordinal : ι → ο
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known ordinal_trichotomy_or : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (or (prim1 x0 x1) (x0 = x1)) (prim1 x1 x0)
Theorem ordinal_trichotomy_or_impred : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ∀ x2 : ο . (prim1 x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (prim1 x1 x0 ⟶ x2) ⟶ x2 (proof)
Param 80242.. : ι → ο
Param 099f3.. : ι → ι → ο
Param 23e07.. : ι → ι
Param 5246e.. : ι → ι
Param e4431.. : ι → ι
Param d3786.. : ι → ι → ι
Param SNoEq_ : ι → ι → ι → ο
Param nIn : ι → ι → ο
Known 36ff9.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . 80242.. x3 ⟶ prim1 (e4431.. x3) (d3786.. (e4431.. x0) (e4431.. x1)) ⟶ SNoEq_ (e4431.. x3) x3 x0 ⟶ SNoEq_ (e4431.. x3) x3 x1 ⟶ 099f3.. x0 x3 ⟶ 099f3.. x3 x1 ⟶ nIn (e4431.. x3) x0 ⟶ prim1 (e4431.. x3) x1 ⟶ x2) ⟶ (prim1 (e4431.. x0) (e4431.. x1) ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ prim1 (e4431.. x0) x1 ⟶ x2) ⟶ (prim1 (e4431.. x1) (e4431.. x0) ⟶ SNoEq_ (e4431.. x1) x0 x1 ⟶ nIn (e4431.. x1) x0 ⟶ x2) ⟶ x2
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1)
Known f5194.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ prim1 x1 (23e07.. x0)
Known 18a76.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ prim1 x1 (5246e.. x0)
Theorem 6f4d6.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 x1 ⟶ ∀ x2 : ο . (∀ x3 . prim1 x3 (23e07.. x1) ⟶ prim1 x3 (5246e.. x0) ⟶ x2) ⟶ (prim1 x0 (23e07.. x1) ⟶ x2) ⟶ (prim1 x1 (5246e.. x0) ⟶ x2) ⟶ x2 (proof)
Known bbdbf.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 : ο . (099f3.. x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (099f3.. x1 x0 ⟶ x2) ⟶ x2
Theorem 7abb3.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 : ο . (x0 = x1 ⟶ x2) ⟶ (∀ x3 . prim1 x3 (23e07.. x1) ⟶ prim1 x3 (5246e.. x0) ⟶ x2) ⟶ (prim1 x0 (23e07.. x1) ⟶ x2) ⟶ (prim1 x1 (5246e.. x0) ⟶ x2) ⟶ (∀ x3 . prim1 x3 (5246e.. x1) ⟶ prim1 x3 (23e07.. x0) ⟶ x2) ⟶ (prim1 x0 (5246e.. x1) ⟶ x2) ⟶ (prim1 x1 (23e07.. x0) ⟶ x2) ⟶ x2 (proof)
Param bc82c.. : ι → ι → ι
Param f4dc0.. : ι → ι
Known 368c5.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 (bc82c.. x1 x2) = bc82c.. (bc82c.. x0 x1) x2
Known 706f7.. : ∀ x0 . 80242.. x0 ⟶ 80242.. (f4dc0.. x0)
Param 4a7ef.. : ι
Known b5313.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. x0 (f4dc0.. x0) = 4a7ef..
Known 97325.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. x0 4a7ef.. = x0
Theorem e7471.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. (bc82c.. x0 x1) (f4dc0.. x1) = x0 (proof)
Known 8782d.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x2 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1)
Known b71d0.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. (bc82c.. x0 x1)
Theorem 08d14.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1) ⟶ 099f3.. x0 x2 (proof)
Theorem f24af.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ bc82c.. x0 (bc82c.. x1 (bc82c.. x2 x3)) = bc82c.. (bc82c.. x0 (bc82c.. x1 x2)) x3 (proof)
Known f3bd7.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. x0 x1 = bc82c.. x1 x0
Theorem eb5ba.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 (bc82c.. x1 x2) = bc82c.. x1 (bc82c.. x0 x2) (proof)
Theorem 1906a.. : ∀ x0 x1 x2 x3 . 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ bc82c.. x0 (bc82c.. x1 (bc82c.. x2 x3)) = bc82c.. x0 (bc82c.. x2 (bc82c.. x1 x3)) (proof)
Theorem cba25.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. (bc82c.. x0 x1) x2 = bc82c.. (bc82c.. x0 x2) x1 (proof)
Theorem 40681.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ bc82c.. (bc82c.. x0 x1) (bc82c.. x2 x3) = bc82c.. (bc82c.. x0 x2) (bc82c.. x1 x3) (proof)
Theorem 5144e.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 (bc82c.. x1 x2) = bc82c.. x2 (bc82c.. x0 x1) (proof)
Known 5c481.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. (f4dc0.. x0) x0 = 4a7ef..
Known 85a07.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. 4a7ef.. x0 = x0
Theorem 5d9d4.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. (f4dc0.. x0) (bc82c.. x0 x1) = x1 (proof)
Theorem baee2.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. x0 (bc82c.. (f4dc0.. x0) x1) = x1 (proof)
Theorem 65db8.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ bc82c.. (bc82c.. x0 (bc82c.. x1 x2)) (bc82c.. (f4dc0.. x2) x3) = bc82c.. x0 (bc82c.. x1 x3) (proof)
Theorem 2a18c.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ bc82c.. (bc82c.. x0 (bc82c.. x1 x2)) (bc82c.. x3 (f4dc0.. x2)) = bc82c.. x0 (bc82c.. x1 x3) (proof)
Known 8948a.. : ∀ x0 . 80242.. x0 ⟶ f4dc0.. (f4dc0.. x0) = x0
Theorem 8b23b.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ bc82c.. (bc82c.. x0 (bc82c.. x1 (f4dc0.. x2))) (bc82c.. x2 x3) = bc82c.. x0 (bc82c.. x1 x3) (proof)
Theorem 1038f.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. (bc82c.. x0 (f4dc0.. x1)) x2 ⟶ 099f3.. x0 (bc82c.. x2 x1) (proof)
Theorem 3350d.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x2 (bc82c.. x0 (f4dc0.. x1)) ⟶ 099f3.. (bc82c.. x2 x1) x0 (proof)
Known ba2a1.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 099f3.. x0 x2 ⟶ 099f3.. x1 x3 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x3)
Theorem 70f5e.. : ∀ x0 x1 x2 x3 x4 x5 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 80242.. x5 ⟶ 099f3.. (bc82c.. x0 x4) (bc82c.. x2 x5) ⟶ 099f3.. (bc82c.. x1 x5) (bc82c.. x3 x4) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x3) (proof)
Known c7cc7.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2
Known 831d4.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x1 x2 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x0 x2)
Theorem fa00b.. : ∀ x0 x1 x2 x3 x4 x5 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 80242.. x5 ⟶ 099f3.. (bc82c.. x0 x2) (bc82c.. x3 x5) ⟶ 099f3.. (bc82c.. x1 x5) x4 ⟶ 099f3.. (bc82c.. x0 (bc82c.. x1 x2)) (bc82c.. x3 x4) (proof)
Known ebb60.. : 80242.. 4a7ef..
Theorem 073b4.. : ∀ x0 x1 x2 x3 x4 x5 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 80242.. x5 ⟶ 099f3.. (bc82c.. x0 x5) (bc82c.. x2 x4) ⟶ 099f3.. x1 (bc82c.. x5 x3) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 (bc82c.. x3 x4)) (proof)
Theorem ad682.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 80242.. x5 ⟶ 80242.. x6 ⟶ 80242.. x7 ⟶ 099f3.. (bc82c.. x0 x5) (bc82c.. x6 x7) ⟶ 099f3.. (bc82c.. x1 x7) x4 ⟶ 099f3.. (bc82c.. x6 x2) (bc82c.. x3 x5) ⟶ 099f3.. (bc82c.. x0 (bc82c.. x1 x2)) (bc82c.. x3 x4) (proof)
Theorem 4a843.. : ∀ x0 x1 x2 x3 x4 x5 x6 x7 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 80242.. x4 ⟶ 80242.. x5 ⟶ 80242.. x6 ⟶ 80242.. x7 ⟶ 099f3.. (bc82c.. x0 x5) (bc82c.. x6 x4) ⟶ 099f3.. x1 (bc82c.. x7 x3) ⟶ 099f3.. (bc82c.. x6 x7) (bc82c.. x2 x5) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 (bc82c.. x3 x4)) (proof)
Param e6316.. : ι → ι → ι
Param 02a50.. : ι → ι → ι
Param 0ac37.. : ι → ι → ι
Param 94f9e.. : ι → (ι → ι) → ι
Param 0fc90.. : ι → (ι → ι) → ι
Definition ac767.. := λ x0 x1 . 0fc90.. x0 (λ x2 . x1)
Param f482f.. : ι → ι → ι
Param 4ae4a.. : ι → ι
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
Known 33e74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 4a7ef..) x0
Known 35b50.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (0fc90.. x0 x1) ⟶ prim1 (f482f.. x2 (4ae4a.. 4a7ef..)) (x1 (f482f.. x2 4a7ef..))
Known da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1)
Param If_i : ο → ι → ι → ι
Known 6f2e8.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) 4a7ef.. = x0
Known 15d37.. : ∀ x0 x1 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x3 . If_i (x3 = 4a7ef..) x0 x1)) (4ae4a.. 4a7ef..) = x1
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Known d5115.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ prim1 (0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x4 . If_i (x4 = 4a7ef..) x2 x3)) (ac767.. x0 x1)
Known 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1)
Known 6381b.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ e6316.. x0 x1 = 02a50.. (0ac37.. (94f9e.. (ac767.. (23e07.. x0) (23e07.. x1)) (λ x3 . bc82c.. (e6316.. (f482f.. x3 4a7ef..) x1) (bc82c.. (e6316.. x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (e6316.. (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x0) (5246e.. x1)) (λ x3 . bc82c.. (e6316.. (f482f.. x3 4a7ef..) x1) (bc82c.. (e6316.. x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (e6316.. (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)))))))) (0ac37.. (94f9e.. (ac767.. (23e07.. x0) (5246e.. x1)) (λ x3 . bc82c.. (e6316.. (f482f.. x3 4a7ef..) x1) (bc82c.. (e6316.. x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (e6316.. (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x0) (23e07.. x1)) (λ x3 . bc82c.. (e6316.. (f482f.. x3 4a7ef..) x1) (bc82c.. (e6316.. x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (e6316.. (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..))))))))
Theorem ca858.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 : ο . (∀ x3 x4 . (∀ x5 . prim1 x5 x3 ⟶ ∀ x6 : ο . (∀ x7 . prim1 x7 (23e07.. x0) ⟶ ∀ x8 . prim1 x8 (23e07.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ (∀ x7 . prim1 x7 (5246e.. x0) ⟶ ∀ x8 . prim1 x8 (5246e.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x3) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x3) ⟶ (∀ x5 . prim1 x5 x4 ⟶ ∀ x6 : ο . (∀ x7 . prim1 x7 (23e07.. x0) ⟶ ∀ x8 . prim1 x8 (5246e.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ (∀ x7 . prim1 x7 (5246e.. x0) ⟶ ∀ x8 . prim1 x8 (23e07.. x1) ⟶ x5 = bc82c.. (e6316.. x7 x1) (bc82c.. (e6316.. x0 x8) (f4dc0.. (e6316.. x7 x8))) ⟶ x6) ⟶ x6) ⟶ (∀ x5 . prim1 x5 (23e07.. x0) ⟶ ∀ x6 . prim1 x6 (5246e.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x4) ⟶ (∀ x5 . prim1 x5 (5246e.. x0) ⟶ ∀ x6 . prim1 x6 (23e07.. x1) ⟶ prim1 (bc82c.. (e6316.. x5 x1) (bc82c.. (e6316.. x0 x6) (f4dc0.. (e6316.. x5 x6)))) x4) ⟶ e6316.. x0 x1 = 02a50.. x3 x4 ⟶ x2) ⟶ x2 (proof)
Param 56ded.. : ι → ι
Known 5ccff.. : ∀ x0 : ι → ο . (∀ x1 . 80242.. x1 ⟶ (∀ x2 . prim1 x2 (56ded.. (e4431.. x1)) ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . 80242.. x1 ⟶ x0 x1
Definition 02b90.. := λ x0 x1 . and (and (∀ x2 . prim1 x2 x0 ⟶ 80242.. x2) (∀ x2 . prim1 x2 x1 ⟶ 80242.. x2)) (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3)
Known cbec9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ x2) ⟶ x2
Known 0888b.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1)
Known e76d1.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ x2) ⟶ x2
Known 9c8cc.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2
Known 5a5d4.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ 80242.. (02a50.. x0 x1)
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known 63df9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ prim1 x1 (56ded.. (e4431.. x0))
Known 54843.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ prim1 x1 (56ded.. (e4431.. x0))
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Known ordinal_TransSet : ∀ x0 . ordinal x0 ⟶ TransSet x0
Known 4c9ee.. : ∀ x0 . 80242.. x0 ⟶ ordinal (e4431.. x0)
Known b50ea.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ prim1 (e4431.. x0) (e4431.. x1) ⟶ prim1 x0 (56ded.. (e4431.. x1))
Param 1beb9.. : ι → ι → ο
Known bfaa9.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 (56ded.. x0) ⟶ ∀ x2 : ο . (prim1 (e4431.. x1) x0 ⟶ ordinal (e4431.. x1) ⟶ 80242.. x1 ⟶ 1beb9.. (e4431.. x1) x1 ⟶ x2) ⟶ x2
Theorem ed5b9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ ∀ x2 : ο . (80242.. (e6316.. x0 x1) ⟶ (∀ x3 . prim1 x3 (23e07.. x0) ⟶ ∀ x4 . prim1 x4 (23e07.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4)) (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4))) ⟶ (∀ x3 . prim1 x3 (5246e.. x0) ⟶ ∀ x4 . prim1 x4 (5246e.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4)) (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4))) ⟶ (∀ x3 . prim1 x3 (23e07.. x0) ⟶ ∀ x4 . prim1 x4 (5246e.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4)) (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4))) ⟶ (∀ x3 . prim1 x3 (5246e.. x0) ⟶ ∀ x4 . prim1 x4 (23e07.. x1) ⟶ 099f3.. (bc82c.. (e6316.. x0 x1) (e6316.. x3 x4)) (bc82c.. (e6316.. x3 x1) (e6316.. x0 x4))) ⟶ x2) ⟶ x2 (proof)