Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPP6../85ff6..
PUWWX../8552d..
vout
PrPP6../da666.. 0.07 bars
TMSrx../116d2.. ownership of 38cac.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKqv../da10e.. ownership of a6493.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVtX../2c116.. ownership of eda89.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXLY../f4b09.. ownership of 3c684.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFXU../7b691.. ownership of 51295.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY4f../f6914.. ownership of f7c98.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMatA../c8572.. ownership of 8e9bb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUez../5452d.. ownership of da4f3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUB1../02fc7.. ownership of 84397.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGcX../c98e6.. ownership of e3a62.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV4q../658ba.. ownership of 9fe90.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSLA../d2332.. ownership of e7310.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZzE../d19be.. ownership of babfc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS12../54ba4.. ownership of 8b663.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVW1../16417.. ownership of 5dab4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNKT../9f72b.. ownership of d7fbc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUok../1b653.. ownership of 76206.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYEW../eb12c.. ownership of 2e4d9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML42../1d74a.. ownership of 18d07.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMViW../5a409.. ownership of 35264.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTLT../8bc7c.. ownership of 45e10.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM4v../8e4e3.. ownership of e4b65.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTrm../1ec83.. ownership of fa6ce.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJy7../26942.. ownership of 116b1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMP7../e582b.. ownership of 2b614.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdiB../73c64.. ownership of 5cf7e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcHN../735b1.. ownership of 551a1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPYx../e4112.. ownership of a7cae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQRP../c1536.. ownership of 58212.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTCH../5ba47.. ownership of cce65.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQaw../289f1.. ownership of 0b595.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYZo../f711f.. ownership of 24e4a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW2C../0b38c.. ownership of 58c5d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYTA../c8845.. ownership of 0d56d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaPa../db0f7.. ownership of b6795.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV8q../3e7be.. ownership of 20f7c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM8N../674a0.. ownership of 47c39.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTDf../0384b.. ownership of dff6e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGQp../511a6.. ownership of 368c5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHfF../ef2fd.. ownership of d8f46.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSHj../6d064.. ownership of f9f27.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXGn../ff563.. ownership of 0c40f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRdd../e2476.. ownership of bf25c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdLx../a9b8d.. ownership of eb3da.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNfK../f93c4.. ownership of cbcc4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT8W../6a115.. ownership of f118e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVwD../f9529.. ownership of 9b91e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQiV../2be3f.. ownership of 5cd31.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMab4../0d524.. ownership of 327d7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb8o../88b10.. ownership of 4a758.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFgy../eed0b.. ownership of c5221.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQMc../09cbf.. ownership of 20efa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZvh../1cd5c.. ownership of c55f3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRzT../dea27.. ownership of 77942.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbHt../84c45.. ownership of ef972.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdNa../52bc3.. ownership of 360da.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHh3../d9999.. ownership of b5313.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNFa../6ef51.. ownership of 5cbe8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVrM../450e9.. ownership of 5c481.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH3p../1f34a.. ownership of e9028.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHiD../ea373.. ownership of 97325.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWvp../e74ee.. ownership of 3201a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHAc../20027.. ownership of 85a07.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWQt../29be1.. ownership of ccff4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXQC../b887a.. ownership of f3bd7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML7p../cde51.. ownership of 443bf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZr7../1d058.. ownership of 7a21c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRze../f8188.. ownership of cebf3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT6B../05012.. ownership of fe60b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQTk../018a3.. ownership of 69bea.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYtM../f2c47.. ownership of cc96f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMic../9a246.. ownership of f22cf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSmV../262c7.. ownership of ba2a1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFqx../1103c.. ownership of 05217.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb5i../ccc21.. ownership of f6ed7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY1q../2cea3.. ownership of ab508.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKFw../01d02.. ownership of e418b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHEV../482ab.. ownership of 355c2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGUc../10ada.. ownership of e46a2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGWh../41a03.. ownership of 785de.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSns../bb8dc.. ownership of 831d4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSgm../3268f.. ownership of 50ea7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVmk../debfb.. ownership of 742c4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZrB../11211.. ownership of 7a8a0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGEG../87134.. ownership of 8782d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVBL../42e97.. ownership of b751a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFqu../ba0de.. ownership of b71d0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZqS../67152.. ownership of 299d3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFZ1../41fd8.. ownership of fb180.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbof../35bdd.. ownership of b7caf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEii../4402d.. ownership of df931.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSLm../660c4.. ownership of f008f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSef../73a8e.. ownership of 8428d.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLg9../fc135.. ownership of 8a6ab.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPVD../2b016.. ownership of 569d0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWFK../2fa2d.. ownership of 6f914.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUUWv../ae556.. doc published by PrGxv..
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Param 1216a.. : ι → (ι → ο) → ι
Param 56ded.. : ι → ι
Param e4431.. : ι → ι
Param 099f3.. : ι → ι → ο
Definition 23e07.. := λ x0 . 1216a.. (56ded.. (e4431.. x0)) (λ x1 . 099f3.. x1 x0)
Known 572ea.. : ∀ x0 . ∀ x1 : ι → ο . Subq (1216a.. x0 x1) x0
Theorem e1ffe.. : ∀ x0 . Subq (23e07.. x0) (56ded.. (e4431.. x0)) (proof)
Definition 5246e.. := λ x0 . 1216a.. (56ded.. (e4431.. x0)) (099f3.. x0)
Theorem f4ff0.. : ∀ x0 . Subq (5246e.. x0) (56ded.. (e4431.. x0)) (proof)
Param 80242.. : ι → ο
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param bc82c.. : ι → ι → ι
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)
Param 0ac37.. : ι → ι → ι
Param 94f9e.. : ι → (ι → ι) → ι
Known 9ec10.. : ∀ x0 : ι → ι → ο . (∀ x1 x2 . 80242.. x1 ⟶ 80242.. x2 ⟶ (∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ x0 x3 x2) ⟶ (∀ x3 . prim1 x3 (56ded.. (e4431.. x2)) ⟶ x0 x1 x3) ⟶ (∀ x3 . prim1 x3 (56ded.. (e4431.. x1)) ⟶ ∀ x4 . prim1 x4 (56ded.. (e4431.. x2)) ⟶ x0 x3 x4) ⟶ x0 x1 x2) ⟶ ∀ x1 x2 . 80242.. x1 ⟶ 80242.. x2 ⟶ x0 x1 x2
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Param 02a50.. : ι → ι → ι
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known 8a8cc.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ bc82c.. x0 x1 = 02a50.. (0ac37.. (94f9e.. (23e07.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0)))
Known and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
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 da962.. : ∀ x0 x1 x2 . prim1 x2 x0 ⟶ prim1 x2 (0ac37.. x0 x1)
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. 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 287ca.. : ∀ x0 x1 x2 . prim1 x2 x1 ⟶ prim1 x2 (0ac37.. x0 x1)
Known 5a5d4.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ 80242.. (02a50.. x0 x1)
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
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
Param d3786.. : ι → ι → ι
Param SNoEq_ : ι → ι → ι → ο
Definition False := ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
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
Known 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1)
Known c7cc7.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2
Known 18a76.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ prim1 x1 (5246e.. x0)
Known f5194.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ prim1 x1 (23e07.. x0)
Known b50ea.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ prim1 (e4431.. x0) (e4431.. x1) ⟶ prim1 x0 (56ded.. (e4431.. x1))
Known ordinal_TransSet : ∀ x0 . ordinal x0 ⟶ TransSet x0
Known 4c9ee.. : ∀ x0 . 80242.. x0 ⟶ ordinal (e4431.. x0)
Theorem fb180.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ and (and (and (and (and (80242.. (bc82c.. x0 x1)) (∀ x2 . prim1 x2 (23e07.. x0) ⟶ 099f3.. (bc82c.. x2 x1) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x0) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1))) (∀ x2 . prim1 x2 (23e07.. x1) ⟶ 099f3.. (bc82c.. x0 x2) (bc82c.. x0 x1))) (∀ x2 . prim1 x2 (5246e.. x1) ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x0 x2))) (02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0)))) (proof)
Theorem b71d0.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. (bc82c.. x0 x1) (proof)
Theorem 8782d.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x2 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x1) (proof)
Param fe4bb.. : ι → ι → ο
Known 817af.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ fe4bb.. x0 x1 ⟶ or (099f3.. x0 x1) (x0 = x1)
Known 8dc73.. : ∀ x0 x1 . 099f3.. x0 x1 ⟶ fe4bb.. x0 x1
Known 4c8cc.. : ∀ x0 . fe4bb.. x0 x0
Theorem 742c4.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ fe4bb.. x0 x2 ⟶ fe4bb.. (bc82c.. x0 x1) (bc82c.. x2 x1) (proof)
Theorem 831d4.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x1 x2 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x0 x2) (proof)
Theorem e46a2.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ fe4bb.. x1 x2 ⟶ fe4bb.. (bc82c.. x0 x1) (bc82c.. x0 x2) (proof)
Known c5dec.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ fe4bb.. x1 x2 ⟶ 099f3.. x0 x2
Theorem e418b.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ 099f3.. x0 x2 ⟶ fe4bb.. x1 x3 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x3) (proof)
Known 45d06.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ fe4bb.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2
Theorem f6ed7.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ fe4bb.. x0 x2 ⟶ 099f3.. x1 x3 ⟶ 099f3.. (bc82c.. x0 x1) (bc82c.. x2 x3) (proof)
Theorem 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) (proof)
Known 9787a.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ fe4bb.. x0 x1 ⟶ fe4bb.. x1 x2 ⟶ fe4bb.. x0 x2
Theorem cc96f.. : ∀ x0 x1 x2 x3 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ fe4bb.. x0 x2 ⟶ fe4bb.. x1 x3 ⟶ fe4bb.. (bc82c.. x0 x1) (bc82c.. x2 x3) (proof)
Theorem fe60b.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 02b90.. (0ac37.. (94f9e.. (23e07.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (23e07.. x1) (bc82c.. x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (5246e.. x1) (bc82c.. x0))) (proof)
Theorem 7a21c.. : ∀ x0 x1 x2 x3 . 02b90.. x0 x1 ⟶ 02b90.. x2 x3 ⟶ 02b90.. (0ac37.. (94f9e.. x0 (λ x4 . bc82c.. x4 (02a50.. x2 x3))) (94f9e.. x2 (bc82c.. (02a50.. x0 x1)))) (0ac37.. (94f9e.. x1 (λ x4 . bc82c.. x4 (02a50.. x2 x3))) (94f9e.. x3 (bc82c.. (02a50.. x0 x1)))) (proof)
Known 47e6b.. : ∀ x0 x1 . 0ac37.. x0 x1 = 0ac37.. x1 x0
Known aff96.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 94f9e.. x0 x1 = 94f9e.. x0 x2
Theorem f3bd7.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. x0 x1 = bc82c.. x1 x0 (proof)
Param 4a7ef.. : ι
Known 5ccff.. : ∀ x0 : ι → ο . (∀ x1 . 80242.. x1 ⟶ (∀ x2 . prim1 x2 (56ded.. (e4431.. x1)) ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . 80242.. x1 ⟶ x0 x1
Known ebb60.. : 80242.. 4a7ef..
Known f6a2d.. : ∀ x0 . 80242.. x0 ⟶ x0 = 02a50.. (23e07.. x0) (5246e.. x0)
Known bf919.. : 5246e.. 4a7ef.. = 4a7ef..
Known d4dbc.. : ∀ x0 : ι → ι . 94f9e.. 4a7ef.. x0 = 4a7ef..
Known 019ee.. : ∀ x0 . 0ac37.. 4a7ef.. x0 = x0
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known 3e9e2.. : 23e07.. 4a7ef.. = 4a7ef..
Theorem 85a07.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. 4a7ef.. x0 = x0 (proof)
Theorem 97325.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. x0 4a7ef.. = x0 (proof)
Param f4dc0.. : ι → ι
Known 2b8be.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ e4431.. x0 = e4431.. x1 ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ x0 = x1
Known aab4f.. : ∀ x0 . ordinal x0 ⟶ e4431.. x0 = x0
Known 40f7a.. : ordinal 4a7ef..
Known e8942.. : ∀ x0 . Subq 4a7ef.. x0
Known c1313.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . 80242.. x2 ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 x2) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x2)
Known 8948a.. : ∀ x0 . 80242.. x0 ⟶ f4dc0.. (f4dc0.. x0) = x0
Known 4d4af.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 x1 ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0)
Known 15454.. : ∀ x0 . 80242.. x0 ⟶ e4431.. (f4dc0.. x0) = e4431.. x0
Known 706f7.. : ∀ x0 . 80242.. x0 ⟶ 80242.. (f4dc0.. x0)
Theorem 5c481.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. (f4dc0.. x0) x0 = 4a7ef.. (proof)
Theorem b5313.. : ∀ x0 . 80242.. x0 ⟶ bc82c.. x0 (f4dc0.. x0) = 4a7ef.. (proof)
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
Known e3ccf.. : ∀ x0 . ordinal x0 ⟶ 80242.. x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem ef972.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ 02b90.. (0ac37.. (94f9e.. (56ded.. x0) (λ x2 . bc82c.. x2 x1)) (94f9e.. (56ded.. x1) (bc82c.. x0))) 4a7ef.. (proof)
Known bc369.. : ∀ x0 . ordinal x0 ⟶ 23e07.. x0 = 56ded.. x0
Known 44ec0.. : ∀ x0 . ordinal x0 ⟶ 5246e.. x0 = 4a7ef..
Theorem c55f3.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ bc82c.. x0 x1 = 02a50.. (0ac37.. (94f9e.. (56ded.. x0) (λ x3 . bc82c.. x3 x1)) (94f9e.. (56ded.. x1) (bc82c.. x0))) 4a7ef.. (proof)
Known 32c48.. : ∀ x0 . 80242.. x0 ⟶ (∀ x1 . prim1 x1 (56ded.. (e4431.. x0)) ⟶ 099f3.. x1 x0) ⟶ ordinal x0
Known 41905.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ or (or (099f3.. x0 x1) (x0 = x1)) (099f3.. x1 x0)
Known In_irref : ∀ x0 . nIn x0 x0
Param 4ae4a.. : ι → ι
Param a842e.. : ι → (ι → ι) → ι
Known 9b3fd.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ and (and (and (and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2))))))) (∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1))) (∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2)) (∀ x2 . 80242.. x2 ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 x2) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x2))
Theorem c5221.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ ordinal (bc82c.. x0 x1) (proof)
Known ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1
Known 4f62a.. : ∀ x0 x1 . ordinal x0 ⟶ prim1 x1 x0 ⟶ or (prim1 (4ae4a.. x1) x0) (x0 = 4ae4a.. x1)
Known 09af0.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (4ae4a.. x0) ⟶ fe4bb.. x1 x0
Known 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0)
Known f1fea.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ Subq x0 x1 ⟶ fe4bb.. x0 x1
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Known Subq_ref : ∀ x0 . Subq x0 x0
Known 44eea.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ 099f3.. x1 x0
Known 09068.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ prim1 (4ae4a.. x1) (4ae4a.. x0)
Known 5f6c1.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ 099f3.. x0 x1 ⟶ prim1 x0 x1
Known b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0)
Known ade9f.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 . prim1 x2 x0 ⟶ 1beb9.. x2 x1 ⟶ prim1 x1 (56ded.. x0)
Known 5b4d8.. : ∀ x0 . ordinal x0 ⟶ 1beb9.. x0 x0
Theorem 327d7.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ bc82c.. (4ae4a.. x0) x1 = 4ae4a.. (bc82c.. x0 x1) (proof)
Theorem 9b91e.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ bc82c.. x0 (4ae4a.. x1) = 4ae4a.. (bc82c.. x0 x1) (proof)
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Theorem cbcc4.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . ordinal x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ prim1 (bc82c.. x2 x1) (bc82c.. x0 x1) (proof)
Known dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Known c47c0.. : ∀ x0 . not (099f3.. x0 x0)
Known 6ec49.. : ∀ x0 x1 x2 x3 . 02b90.. x0 x1 ⟶ 02b90.. x2 x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 (02a50.. x2 x3)) ⟶ (∀ x4 . prim1 x4 x3 ⟶ 099f3.. (02a50.. x0 x1) x4) ⟶ fe4bb.. (02a50.. x0 x1) (02a50.. x2 x3)
Known 23b01.. : ∀ x0 . 80242.. x0 ⟶ 02b90.. (23e07.. x0) (5246e.. x0)
Known 027ee.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ or (099f3.. x0 x1) (fe4bb.. x1 x0)
Known orIL : ∀ x0 x1 : ο . x0 ⟶ or x0 x1
Known orIR : ∀ x0 x1 : ο . x1 ⟶ or x0 x1
Known bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0
Theorem bf25c.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 . prim1 x2 (23e07.. (bc82c.. x0 x1)) ⟶ or (∀ x3 : ο . (∀ x4 . and (prim1 x4 (23e07.. x0)) (fe4bb.. x2 (bc82c.. x4 x1)) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 (23e07.. x1)) (fe4bb.. x2 (bc82c.. x0 x4)) ⟶ x3) ⟶ x3) (proof)
Theorem f9f27.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 . prim1 x2 (5246e.. (bc82c.. x0 x1)) ⟶ or (∀ x3 : ο . (∀ x4 . and (prim1 x4 (5246e.. x0)) (fe4bb.. (bc82c.. x4 x1) x2) ⟶ x3) ⟶ x3) (∀ x3 : ο . (∀ x4 . and (prim1 x4 (5246e.. x1)) (fe4bb.. (bc82c.. x0 x4) x2) ⟶ x3) ⟶ x3) (proof)
Known fbd1c.. : ∀ x0 : ι → ι → ι → ο . (∀ x1 x2 x3 . 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ (∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ x0 x4 x2 x3) ⟶ (∀ x4 . prim1 x4 (56ded.. (e4431.. x2)) ⟶ x0 x1 x4 x3) ⟶ (∀ x4 . prim1 x4 (56ded.. (e4431.. x3)) ⟶ x0 x1 x2 x4) ⟶ (∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ ∀ x5 . prim1 x5 (56ded.. (e4431.. x2)) ⟶ x0 x4 x5 x3) ⟶ (∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ ∀ x5 . prim1 x5 (56ded.. (e4431.. x3)) ⟶ x0 x4 x2 x5) ⟶ (∀ x4 . prim1 x4 (56ded.. (e4431.. x2)) ⟶ ∀ x5 . prim1 x5 (56ded.. (e4431.. x3)) ⟶ x0 x1 x4 x5) ⟶ (∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ ∀ x5 . prim1 x5 (56ded.. (e4431.. x2)) ⟶ ∀ x6 . prim1 x6 (56ded.. (e4431.. x3)) ⟶ x0 x4 x5 x6) ⟶ x0 x1 x2 x3) ⟶ ∀ x1 x2 x3 . 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ x0 x1 x2 x3
Known 22361.. : ∀ x0 x1 x2 x3 . 02b90.. x0 x1 ⟶ 02b90.. x2 x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 (02a50.. x2 x3)) ⟶ (∀ x4 . prim1 x4 x1 ⟶ 099f3.. (02a50.. x2 x3) x4) ⟶ (∀ x4 . prim1 x4 x2 ⟶ 099f3.. x4 (02a50.. x0 x1)) ⟶ (∀ x4 . prim1 x4 x3 ⟶ 099f3.. (02a50.. x0 x1) x4) ⟶ 02a50.. x0 x1 = 02a50.. x2 x3
Theorem 368c5.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 (bc82c.. x1 x2) = bc82c.. (bc82c.. x0 x1) x2 (proof)
Theorem 47c39.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ bc82c.. x0 x1 = bc82c.. x0 x2 ⟶ x1 = x2 (proof)
Theorem b6795.. : f4dc0.. 4a7ef.. = 4a7ef.. (proof)
Theorem 58c5d.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ f4dc0.. (bc82c.. x0 x1) = bc82c.. (f4dc0.. x0) (f4dc0.. x1) (proof)
Param If_i : ο → ι → ι → ι
Param e6316.. : ι → ι → ι
Definition 569d0.. := λ x0 x1 . If_i (x1 = 4a7ef..) 4a7ef.. (prim0 (λ x2 . and (80242.. x2) (e6316.. x2 x1 = x0)))
Param 236dc.. : ι → ι → ι
Param ce322.. : ι → ι
Param f6a32.. : ι → ι
Definition 8428d.. := λ x0 . 236dc.. (f4dc0.. (ce322.. x0)) (f4dc0.. (f6a32.. x0))
Param 1013b.. : ι → ο
Known 746bb.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 1013b.. (236dc.. x0 x1)
Known 3a25a.. : ∀ x0 . 1013b.. x0 ⟶ 80242.. (ce322.. x0)
Known 43fc2.. : ∀ x0 . 1013b.. x0 ⟶ 80242.. (f6a32.. x0)
Theorem 0b595.. : ∀ x0 . 1013b.. x0 ⟶ 1013b.. (8428d.. x0) (proof)
Known a0d36.. : ∀ x0 . 236dc.. x0 4a7ef.. = x0
Known 55f9f.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ce322.. (236dc.. x0 x1) = x0
Theorem 58212.. : ∀ x0 . 80242.. x0 ⟶ ce322.. x0 = x0 (proof)
Known 41b27.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ f6a32.. (236dc.. x0 x1) = x1
Theorem 551a1.. : ∀ x0 . 80242.. x0 ⟶ f6a32.. x0 = 4a7ef.. (proof)
Theorem 2b614.. : ce322.. 4a7ef.. = 4a7ef.. (proof)
Theorem fa6ce.. : f6a32.. 4a7ef.. = 4a7ef.. (proof)
Known c8ed0.. : 80242.. (4ae4a.. 4a7ef..)
Theorem 45e10.. : ce322.. (4ae4a.. 4a7ef..) = 4ae4a.. 4a7ef.. (proof)
Theorem 18d07.. : f6a32.. (4ae4a.. 4a7ef..) = 4a7ef.. (proof)
Definition f8050.. := 236dc.. 4a7ef.. (4ae4a.. 4a7ef..)
Theorem 76206.. : ce322.. f8050.. = 4a7ef.. (proof)
Theorem 5dab4.. : f6a32.. f8050.. = 4ae4a.. 4a7ef.. (proof)
Definition e37c0.. := λ x0 x1 . 236dc.. (bc82c.. (ce322.. x0) (ce322.. x1)) (bc82c.. (f6a32.. x0) (f6a32.. x1))
Theorem babfc.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ bc82c.. x0 x1 = e37c0.. x0 x1 (proof)
Theorem 9fe90.. : ∀ x0 x1 . 1013b.. x0 ⟶ 1013b.. x1 ⟶ 1013b.. (e37c0.. x0 x1) (proof)
Known 501e2.. : ∀ x0 . 1013b.. x0 ⟶ x0 = 236dc.. (ce322.. x0) (f6a32.. x0)
Theorem 84397.. : ∀ x0 . 1013b.. x0 ⟶ e37c0.. 4a7ef.. x0 = x0 (proof)
Theorem 8e9bb.. : ∀ x0 . 1013b.. x0 ⟶ e37c0.. x0 4a7ef.. = x0 (proof)
Theorem 51295.. : ∀ x0 . 1013b.. x0 ⟶ e37c0.. (8428d.. x0) x0 = 4a7ef.. (proof)
Theorem eda89.. : ∀ x0 . 1013b.. x0 ⟶ e37c0.. x0 (8428d.. x0) = 4a7ef.. (proof)
Theorem 38cac.. : ∀ x0 . 80242.. x0 ⟶ f4dc0.. x0 = 8428d.. x0 (proof)
Param 7ce1c.. : ι → ι → ι
Definition df931.. := λ x0 x1 . If_i (x1 = 4a7ef..) 4a7ef.. (prim0 (λ x2 . and (1013b.. x2) (7ce1c.. x2 x1 = x0)))