Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrKjC../29477..
PUUkx../36375..
vout
PrKjC../5a35b.. 0.04 bars
TMFvF../0128a.. ownership of 6381b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGEe../bdfd3.. ownership of 05539.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWfc../cbddc.. ownership of 8a8cc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLc4../679b3.. ownership of b2d3c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFsq../ea93a.. ownership of c57b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNue../50862.. ownership of 6b4cb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWa7../a3321.. ownership of 205d0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFdT../ed6a9.. ownership of 0d8c2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTBe../25704.. ownership of 542d9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZGd../52c04.. ownership of 99018.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXRt../0686c.. ownership of 9ed0c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc4Q../0d35a.. ownership of bd361.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbiJ../85635.. ownership of 681ed.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJdU../42b42.. ownership of a6868.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPXs../2060f.. ownership of 27827.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLXv../bb459.. ownership of b5b77.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNNn../a9e0e.. ownership of 26c90.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS3x../20d62.. ownership of d2ff7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVvi../6e9a5.. ownership of d4781.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGKc../ba8b5.. ownership of defdf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQXC../06e58.. ownership of 3cd4e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcZS../28fc6.. ownership of 11e65.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNBw../8e76d.. ownership of f4a7a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKdu../a8849.. ownership of afad4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTvT../36c3a.. ownership of cd88b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJRp../e7969.. ownership of 6821b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJRT../d4de3.. ownership of 2f1de.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML6u../af502.. ownership of 50863.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbYc../a1d7d.. ownership of 15454.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMczu../21f15.. ownership of 9cdec.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLaL../dfb09.. ownership of 8948a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSd6../f83ed.. ownership of 3a727.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML8N../c011d.. ownership of e1909.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN29../e5c01.. ownership of 15318.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLnd../5a0f0.. ownership of fa2f6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbyp../4396d.. ownership of 79d60.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJST../d3bc6.. ownership of a9e6a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF8Q../ce384.. ownership of 982cd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXxi../27a55.. ownership of 106e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHoV../e48bb.. ownership of 448cb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdoX../07d5f.. ownership of f735c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMW3../1eaab.. ownership of c8379.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXPv../653f9.. ownership of 4d4af.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWdf../09ee6.. ownership of 3cc82.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRRt../dc1ea.. ownership of 706f7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQTX../ade1b.. ownership of 8fbd0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJRr../ad4f2.. ownership of 2ffcf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJBw../cf250.. ownership of 91557.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZrX../5e36f.. ownership of 8810f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWyA../8326e.. ownership of cb0c4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMULc../d19d9.. ownership of 7c70f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUHW../fe05c.. ownership of e46d9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSws../50d2c.. ownership of 3ace7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUx6../15d9d.. ownership of bc4c7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMgC../bba36.. ownership of de156.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQPZ../3ed56.. ownership of 05c3e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRbv../cc5b1.. ownership of 56954.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTT6../bbf3d.. ownership of 58673.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTFK../96da9.. ownership of 8207c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVEU../19e27.. ownership of a3bf1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbGq../e8f0e.. ownership of c8ed0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPVv../945a6.. ownership of 3d71b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb86../63249.. ownership of fbd1c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNYv../e6eb5.. ownership of e9ef7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ3d../999a6.. ownership of 9ec10.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb9q../1b8aa.. ownership of 98dce.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGrx../ee79d.. ownership of 5ccff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGCE../3559f.. ownership of f04ee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLPp../c0a68.. ownership of b59b7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdUX../cbbf4.. ownership of 569cb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJgm../92bb3.. ownership of 262b2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ5D../dc463.. ownership of 800ab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSgo../d0938.. ownership of 73943.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcmH../ae216.. ownership of 6c83a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHjh../93bda.. ownership of 922f2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbfm../4dea8.. ownership of 0d078.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMXF../5b328.. ownership of 26c4a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZRb../e503a.. ownership of 24de1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWW9../0723e.. ownership of 43617.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYd9../3e095.. ownership of e0c85.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKqZ../e7a39.. ownership of c9f3d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMdQ../561ce.. ownership of 8108c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTUu../745a9.. ownership of 451cb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWZA../cacb8.. ownership of db769.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ1x../d00a0.. ownership of cb40e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQCL../54b7e.. ownership of e6397.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRgA../e1211.. ownership of 095d9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK1C../3cef9.. ownership of cad18.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYEy../60d63.. ownership of 32c48.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNP8../33773.. ownership of 02538.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPXL../8daea.. ownership of 99fb6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJri../f5dd8.. ownership of 833fc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKQi../0a8af.. ownership of bf919.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNrN../3cee3.. ownership of 897b6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXHE../2b9bc.. ownership of 3e9e2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGk6../3f63f.. ownership of f4186.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX6u../83de8.. ownership of ab02c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEkM../bc260.. ownership of 514ac.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSb2../2b66f.. ownership of ebb60.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaHi../a270e.. ownership of a66a6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVaH../09fb1.. ownership of 360d7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP1P../338d5.. ownership of dee9f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVqE../f7443.. ownership of 58b67.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVoc../05bba.. ownership of 5eb84.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYNa../03ebc.. ownership of 44ec0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcCR../7a83f.. ownership of 00543.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGaK../27669.. ownership of bc369.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXVE../848ab.. ownership of 86c21.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSGp../be730.. ownership of f4ff0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRna../8199b.. ownership of cd408.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV6M../ebfe4.. ownership of e1ffe.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVV8../cd930.. ownership of 3d9fc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFwE../6751d.. ownership of 899f5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSie../d1e26.. ownership of ac469.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYii../4f840.. ownership of 5f6c1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVWY../9e71e.. ownership of 035a7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJfy../cf03e.. ownership of 9ecaa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMStp../b81a2.. ownership of b01da.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUvn../0e2dc.. ownership of bbdbf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUcz../4279d.. ownership of 0ee89.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQgN../0ec98.. ownership of 2ed15.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLCC../16fa8.. ownership of 85d3b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcZw../9bb14.. ownership of eb51d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNeZ../f7215.. ownership of 3d848.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaJo../4b731.. ownership of 9aba9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbvP../5a1be.. ownership of ef1dc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK2D../2ceed.. ownership of 1e8ae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMRU../1e8e4.. ownership of 193bb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTtL../9c9cc.. ownership of f74bd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN8v../d1d77.. ownership of 8d0a0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJ5N../6f81f.. ownership of e6316.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUww../721e6.. ownership of 79af3.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNzW../47459.. ownership of bc82c.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUGo../343a5.. ownership of 35272.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNKt../42816.. ownership of f4dc0.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG3J../22df7.. ownership of 1dbc8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEta../6432e.. ownership of ad3ed.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPtL../7cbd7.. ownership of 3e27a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGPb../a9b2e.. ownership of fb712.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPLf../a02b0.. ownership of b16fa.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFyR../23a85.. ownership of b3303.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSN2../b7570.. ownership of 9f8e2.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUTG4../8cfaa.. doc published by PrGxv..
Theorem eq_i_tra : ∀ x0 x1 x2 . x0 = x1 ⟶ x1 = x2 ⟶ x0 = x2 (proof)
Definition Subq := λ x0 x1 . ∀ x2 . prim1 x2 x0 ⟶ prim1 x2 x1
Definition TransSet := λ x0 . ∀ x1 . prim1 x1 x0 ⟶ Subq x1 x0
Param 4ae4a.. : ι → ι
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known 958ef.. : ∀ x0 x1 . prim1 x1 (4ae4a.. x0) ⟶ or (prim1 x1 x0) (x1 = x0)
Known Subq_ref : ∀ x0 . Subq x0 x0
Theorem 9aba9.. : ∀ x0 x1 . TransSet x1 ⟶ prim1 x0 (4ae4a.. x1) ⟶ Subq x0 x1 (proof)
Param 94f9e.. : ι → (ι → ι) → ι
Known set_ext : ∀ x0 x1 . Subq x0 x1 ⟶ Subq x1 x0 ⟶ x0 = x1
Known 8c6f6.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (94f9e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . prim1 x4 x0 ⟶ x2 = x1 x4 ⟶ x3) ⟶ x3
Known 696c0.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ prim1 (x1 x2) (94f9e.. x0 x1)
Theorem eb51d.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 (x2 x3) = x3) ⟶ 94f9e.. (94f9e.. x0 x2) x1 = x0 (proof)
Theorem 2ed15.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ x1 (x1 x2) = x2) ⟶ 94f9e.. (94f9e.. x0 x1) x1 = x0 (proof)
Param 80242.. : ι → ο
Param 099f3.. : ι → ι → ο
Known 41905.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ or (or (099f3.. x0 x1) (x0 = x1)) (099f3.. x1 x0)
Theorem bbdbf.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ ∀ x2 : ο . (099f3.. x0 x1 ⟶ x2) ⟶ (x0 = x1 ⟶ x2) ⟶ (099f3.. x1 x0 ⟶ x2) ⟶ x2 (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
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 02a50.. : ι → ι → ι
Param e4431.. : ι → ι
Param 0ac37.. : ι → ι → ι
Param a842e.. : ι → (ι → ι) → ι
Param SNoEq_ : ι → ι → ι → ο
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 9ecaa.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 : ο . (80242.. (02a50.. x0 x1) ⟶ prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x3 . 4ae4a.. (e4431.. x3))) (a842e.. x1 (λ x3 . 4ae4a.. (e4431.. x3))))) ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 (02a50.. x0 x1)) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. (02a50.. x0 x1) x3) ⟶ (∀ x3 . 80242.. x3 ⟶ (∀ x4 . prim1 x4 x0 ⟶ 099f3.. x4 x3) ⟶ (∀ x4 . prim1 x4 x1 ⟶ 099f3.. x3 x4) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x3)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x3)) ⟶ x2) ⟶ x2 (proof)
Definition ordinal := λ x0 . and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1)
Known ordinal_In_Or_Subq : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ or (prim1 x0 x1) (Subq x1 x0)
Definition False := ∀ x0 : ο . x0
Known FalseE : False ⟶ ∀ x0 : ο . x0
Definition not := λ x0 : ο . x0 ⟶ False
Known c47c0.. : ∀ x0 . not (099f3.. x0 x0)
Param fe4bb.. : ι → ι → ο
Known c5dec.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ fe4bb.. x1 x2 ⟶ 099f3.. x0 x2
Known e3ccf.. : ∀ x0 . ordinal x0 ⟶ 80242.. x0
Known f1fea.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ Subq x0 x1 ⟶ fe4bb.. x0 x1
Theorem 5f6c1.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ 099f3.. x0 x1 ⟶ prim1 x0 x1 (proof)
Known 45d06.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ fe4bb.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2
Known 44eea.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ 099f3.. x1 x0
Theorem 899f5.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ fe4bb.. x0 x1 ⟶ Subq x0 x1 (proof)
Param 1216a.. : ι → (ι → ο) → ι
Param 56ded.. : ι → ι
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)
Known cbec9.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (23e07.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ x2) ⟶ x2
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
Known f5194.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x1 x0 ⟶ prim1 x1 (23e07.. x0)
Known c0742.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) x0 ⟶ 099f3.. x1 x0
Known aab4f.. : ∀ x0 . ordinal x0 ⟶ e4431.. x0 = x0
Theorem bc369.. : ∀ x0 . ordinal x0 ⟶ 23e07.. x0 = 56ded.. x0 (proof)
Param 4a7ef.. : ι
Known 3f849.. : ∀ x0 . Subq x0 4a7ef.. ⟶ x0 = 4a7ef..
Known e76d1.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (5246e.. x0) ⟶ ∀ x2 : ο . (80242.. x1 ⟶ prim1 (e4431.. x1) (e4431.. x0) ⟶ 099f3.. x0 x1 ⟶ x2) ⟶ x2
Known c7cc7.. : ∀ x0 x1 x2 . 80242.. x0 ⟶ 80242.. x1 ⟶ 80242.. x2 ⟶ 099f3.. x0 x1 ⟶ 099f3.. x1 x2 ⟶ 099f3.. x0 x2
Theorem 44ec0.. : ∀ x0 . ordinal x0 ⟶ 5246e.. x0 = 4a7ef.. (proof)
Known 23b01.. : ∀ x0 . 80242.. x0 ⟶ 02b90.. (23e07.. x0) (5246e.. x0)
Theorem 58b67.. : ∀ x0 . ordinal x0 ⟶ 02b90.. (56ded.. x0) 4a7ef.. (proof)
Known f6a2d.. : ∀ x0 . 80242.. x0 ⟶ x0 = 02a50.. (23e07.. x0) (5246e.. x0)
Theorem 360d7.. : ∀ x0 . ordinal x0 ⟶ x0 = 02a50.. (56ded.. x0) 4a7ef.. (proof)
Known 40f7a.. : ordinal 4a7ef..
Theorem ebb60.. : 80242.. 4a7ef.. (proof)
Theorem ab02c.. : e4431.. 4a7ef.. = 4a7ef.. (proof)
Definition nIn := λ x0 x1 . not (prim1 x0 x1)
Known dcd83.. : ∀ x0 . nIn x0 4a7ef..
Theorem 3e9e2.. : 23e07.. 4a7ef.. = 4a7ef.. (proof)
Theorem bf919.. : 5246e.. 4a7ef.. = 4a7ef.. (proof)
Known 817af.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ fe4bb.. x0 x1 ⟶ or (099f3.. x0 x1) (x0 = x1)
Param d3786.. : ι → ι → ι
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 ade9f.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 x2 . prim1 x2 x0 ⟶ 1beb9.. x2 x1 ⟶ prim1 x1 (56ded.. x0)
Known b0eab.. : ∀ x0 . 80242.. x0 ⟶ 1beb9.. (e4431.. x0) x0
Known In_irref : ∀ x0 . nIn x0 x0
Known 09af0.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (4ae4a.. x0) ⟶ fe4bb.. x1 x0
Known 5faa3.. : ∀ x0 . prim1 x0 (4ae4a.. x0)
Known 4c9ee.. : ∀ x0 . 80242.. x0 ⟶ ordinal (e4431.. x0)
Theorem 99fb6.. : ∀ x0 . 80242.. x0 ⟶ (∀ x1 . prim1 x1 (56ded.. (e4431.. x0)) ⟶ 099f3.. x1 x0) ⟶ e4431.. x0 = x0 (proof)
Theorem 32c48.. : ∀ x0 . 80242.. x0 ⟶ (∀ x1 . prim1 x1 (56ded.. (e4431.. x0)) ⟶ 099f3.. x1 x0) ⟶ ordinal x0 (proof)
Param 7cb9a.. : ι → ι
Known 20dcf.. : ∀ x0 x1 . prim1 (e4431.. x1) (e4431.. x0) ⟶ SNoEq_ (e4431.. x1) x0 x1 ⟶ nIn (e4431.. x1) x0 ⟶ 099f3.. x0 x1
Known 8e40c.. : ∀ x0 . 80242.. x0 ⟶ e4431.. (7cb9a.. x0) = 4ae4a.. (e4431.. x0)
Known f3f53.. : ∀ x0 . 80242.. x0 ⟶ SNoEq_ (e4431.. x0) (7cb9a.. x0) x0
Known e3722.. : ∀ x0 . 80242.. x0 ⟶ nIn (e4431.. x0) (7cb9a.. x0)
Theorem 095d9.. : ∀ x0 . 80242.. x0 ⟶ 099f3.. (7cb9a.. x0) x0 (proof)
Param 45abd.. : ι → ι
Known 151ed.. : ∀ x0 x1 . prim1 (e4431.. x0) (e4431.. x1) ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ prim1 (e4431.. x0) x1 ⟶ 099f3.. x0 x1
Known 80851.. : ∀ x0 . 80242.. x0 ⟶ e4431.. (45abd.. x0) = 4ae4a.. (e4431.. x0)
Known SNoEq_sym_ : ∀ x0 x1 x2 . SNoEq_ x0 x1 x2 ⟶ SNoEq_ x0 x2 x1
Known aa41a.. : ∀ x0 . 80242.. x0 ⟶ SNoEq_ (e4431.. x0) (45abd.. x0) x0
Known 35186.. : ∀ x0 . 80242.. x0 ⟶ prim1 (e4431.. x0) (45abd.. x0)
Theorem cb40e.. : ∀ x0 . 80242.. x0 ⟶ 099f3.. x0 (45abd.. x0) (proof)
Param In_rec_ii : (ι → (ι → ι → ι) → ι → ι) → ι → ι → ι
Param If_ii : ο → (ι → ι) → (ι → ι) → ι → ι
Param If_i : ο → ι → ι → ι
Param True : ο
Definition b3303.. := λ x0 : ι → (ι → ι) → ι . λ x1 . In_rec_ii (λ x2 . λ x3 : ι → ι → ι . If_ii (ordinal x2) (λ x4 . If_i (prim1 x4 (56ded.. (4ae4a.. x2))) (x0 x4 (λ x5 . x3 (e4431.. x5) x5)) (prim0 (λ x5 . True))) (λ x4 . prim0 (λ x5 . True))) (e4431.. x1) x1
Known In_rec_ii_eq : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_ii x0 x1 = x0 x1 (In_rec_ii x0)
Known If_ii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . x0 ⟶ If_ii x0 x1 x2 = x1
Known If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Known 98928.. : ∀ x0 . 80242.. x0 ⟶ prim1 x0 (56ded.. (4ae4a.. (e4431.. x0)))
Known xm : ∀ x0 : ο . or x0 (not x0)
Known b72a3.. : ∀ x0 . ordinal x0 ⟶ ordinal (4ae4a.. x0)
Known If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Known If_ii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι . not x0 ⟶ If_ii x0 x1 x2 = x2
Theorem 451cb.. : ∀ x0 : ι → (ι → ι) → ι . (∀ x1 . 80242.. x1 ⟶ ∀ x2 x3 : ι → ι . (∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 80242.. x1 ⟶ b3303.. x0 x1 = x0 x1 (b3303.. x0) (proof)
Param In_rec_iii : (ι → (ι → ι → ι → ι) → ι → ι → ι) → ι → ι → ι → ι
Param If_iii : ο → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Param Descr_ii : ((ι → ι) → ο) → ι → ι
Definition fb712.. := λ x0 : ι → (ι → ι → ι) → ι → ι . λ x1 . In_rec_iii (λ x2 . λ x3 : ι → ι → ι → ι . If_iii (ordinal x2) (λ x4 . If_ii (prim1 x4 (56ded.. (4ae4a.. x2))) (x0 x4 (λ x5 . x3 (e4431.. x5) x5)) (Descr_ii (λ x5 : ι → ι . True))) (λ x4 . Descr_ii (λ x5 : ι → ι . True))) (e4431.. x1) x1
Known In_rec_iii_eq : ∀ x0 : ι → (ι → ι → ι → ι) → ι → ι → ι . (∀ x1 . ∀ x2 x3 : ι → ι → ι → ι . (∀ x4 . prim1 x4 x1 ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . In_rec_iii x0 x1 = x0 x1 (In_rec_iii x0)
Known If_iii_1 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . x0 ⟶ If_iii x0 x1 x2 = x1
Known If_iii_0 : ∀ x0 : ο . ∀ x1 x2 : ι → ι → ι . not x0 ⟶ If_iii x0 x1 x2 = x2
Theorem c9f3d.. : ∀ x0 : ι → (ι → ι → ι) → ι → ι . (∀ x1 . 80242.. x1 ⟶ ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ x2 x4 = x3 x4) ⟶ x0 x1 x2 = x0 x1 x3) ⟶ ∀ x1 . 80242.. x1 ⟶ fb712.. x0 x1 = x0 x1 (fb712.. x0) (proof)
Known 1eaea.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 . prim1 x1 (56ded.. (e4431.. x0)) ⟶ x1 = x0 ⟶ ∀ x2 : ο . x2
Theorem 43617.. : ∀ x0 : ι → ι → (ι → ι → ι) → ι . (∀ x1 . 80242.. x1 ⟶ ∀ x2 . 80242.. x2 ⟶ ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 (56ded.. (e4431.. x1)) ⟶ ∀ x6 . 80242.. x6 ⟶ x3 x5 x6 = x4 x5 x6) ⟶ (∀ x5 . prim1 x5 (56ded.. (e4431.. x2)) ⟶ x3 x1 x5 = x4 x1 x5) ⟶ x0 x1 x2 x3 = x0 x1 x2 x4) ⟶ ∀ x1 . 80242.. x1 ⟶ ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 (56ded.. (e4431.. x1)) ⟶ x2 x4 = x3 x4) ⟶ ∀ x4 . 80242.. x4 ⟶ ∀ x5 x6 : ι → ι . (∀ x7 . prim1 x7 (56ded.. (e4431.. x4)) ⟶ x5 x7 = x6 x7) ⟶ x0 x1 x4 (λ x8 x9 . If_i (x8 = x1) (x5 x9) (x2 x8 x9)) = x0 x1 x4 (λ x8 x9 . If_i (x8 = x1) (x6 x9) (x3 x8 x9)) (proof)
Theorem 26c4a.. : ∀ x0 : ι → ι → (ι → ι → ι) → ι . (∀ x1 . 80242.. x1 ⟶ ∀ x2 . 80242.. x2 ⟶ ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 (56ded.. (e4431.. x1)) ⟶ ∀ x6 . 80242.. x6 ⟶ x3 x5 x6 = x4 x5 x6) ⟶ (∀ x5 . prim1 x5 (56ded.. (e4431.. x2)) ⟶ x3 x1 x5 = x4 x1 x5) ⟶ x0 x1 x2 x3 = x0 x1 x2 x4) ⟶ ∀ x1 . 80242.. x1 ⟶ ∀ x2 : ι → ι → ι . ∀ x3 . 80242.. x3 ⟶ b3303.. (λ x5 . λ x6 : ι → ι . x0 x1 x5 (λ x7 x8 . If_i (x7 = x1) (x6 x8) (x2 x7 x8))) x3 = x0 x1 x3 (λ x5 x6 . If_i (x5 = x1) (b3303.. (λ x7 . λ x8 : ι → ι . x0 x1 x7 (λ x9 x10 . If_i (x9 = x1) (x8 x10) (x2 x9 x10))) x6) (x2 x5 x6)) (proof)
Definition ad3ed.. := λ x0 : ι → ι → (ι → ι → ι) → ι . fb712.. (λ x1 . λ x2 : ι → ι → ι . λ x3 . If_i (80242.. x3) (b3303.. (λ x4 . λ x5 : ι → ι . x0 x1 x4 (λ x6 x7 . If_i (x6 = x1) (x5 x7) (x2 x6 x7))) x3) 4a7ef..)
Known ordinal_ind : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ (∀ x2 . prim1 x2 x1 ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . ordinal x1 ⟶ x0 x1
Theorem 922f2.. : ∀ x0 : ι → ι → (ι → ι → ι) → ι . (∀ x1 . 80242.. x1 ⟶ ∀ x2 . 80242.. x2 ⟶ ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 (56ded.. (e4431.. x1)) ⟶ ∀ x6 . 80242.. x6 ⟶ x3 x5 x6 = x4 x5 x6) ⟶ (∀ x5 . prim1 x5 (56ded.. (e4431.. x2)) ⟶ x3 x1 x5 = x4 x1 x5) ⟶ x0 x1 x2 x3 = x0 x1 x2 x4) ⟶ ∀ x1 . 80242.. x1 ⟶ ∀ x2 . 80242.. x2 ⟶ ad3ed.. x0 x1 x2 = x0 x1 x2 (ad3ed.. x0) (proof)
Theorem 73943.. : ∀ x0 : ι → ο . (∀ x1 . ordinal x1 ⟶ ∀ x2 . prim1 x2 (56ded.. x1) ⟶ x0 x2) ⟶ ∀ x1 . 80242.. x1 ⟶ x0 x1 (proof)
Theorem 262b2.. : ∀ x0 : ι → ι → ο . (∀ x1 . ordinal x1 ⟶ ∀ x2 . ordinal x2 ⟶ ∀ x3 . prim1 x3 (56ded.. x1) ⟶ ∀ x4 . prim1 x4 (56ded.. x2) ⟶ x0 x3 x4) ⟶ ∀ x1 x2 . 80242.. x1 ⟶ 80242.. x2 ⟶ x0 x1 x2 (proof)
Theorem b59b7.. : ∀ x0 : ι → ι → ι → ο . (∀ x1 . ordinal x1 ⟶ ∀ x2 . ordinal x2 ⟶ ∀ x3 . ordinal x3 ⟶ ∀ x4 . prim1 x4 (56ded.. x1) ⟶ ∀ x5 . prim1 x5 (56ded.. x2) ⟶ ∀ x6 . prim1 x6 (56ded.. x3) ⟶ x0 x4 x5 x6) ⟶ ∀ x1 x2 x3 . 80242.. x1 ⟶ 80242.. x2 ⟶ 80242.. x3 ⟶ x0 x1 x2 x3 (proof)
Theorem 5ccff.. : ∀ x0 : ι → ο . (∀ x1 . 80242.. x1 ⟶ (∀ x2 . prim1 x2 (56ded.. (e4431.. x1)) ⟶ x0 x2) ⟶ x0 x1) ⟶ ∀ x1 . 80242.. x1 ⟶ x0 x1 (proof)
Theorem 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 (proof)
Theorem 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 (proof)
Param ba9d8.. : ι → ο
Known f3fb5.. : ∀ x0 . ba9d8.. x0 ⟶ ordinal x0
Known 3db81.. : ba9d8.. (4ae4a.. 4a7ef..)
Theorem c8ed0.. : 80242.. (4ae4a.. 4a7ef..) (proof)
Known d7fe6.. : ba9d8.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 8207c.. : 80242.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Param 48ef8.. : ι
Known c8a5e.. : ordinal 48ef8..
Theorem 56954.. : 80242.. 48ef8.. (proof)
Known 9c410.. : ordinal (4ae4a.. 4a7ef..)
Known f1083.. : prim1 4a7ef.. (4ae4a.. 4a7ef..)
Theorem de156.. : 099f3.. 4a7ef.. (4ae4a.. 4a7ef..) (proof)
Known 5d775.. : ordinal (4ae4a.. (4ae4a.. 4a7ef..))
Known f336d.. : prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 3ace7.. : 099f3.. 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Known 0b783.. : prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..))
Theorem 7c70f.. : 099f3.. (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)) (proof)
Definition f4dc0.. := b3303.. (λ x0 . λ x1 : ι → ι . 02a50.. (94f9e.. (5246e.. x0) x1) (94f9e.. (23e07.. x0) x1))
Known aff96.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 94f9e.. x0 x1 = 94f9e.. x0 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))
Theorem 8810f.. : ∀ x0 . 80242.. x0 ⟶ f4dc0.. x0 = 02a50.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..) (proof)
Known andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Known 9c8cc.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2
Known 0888b.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1)
Known 5a5d4.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ 80242.. (02a50.. x0 x1)
Known d8827.. : ∀ x0 . 80242.. x0 ⟶ and (ordinal (e4431.. x0)) (1beb9.. (e4431.. x0) x0)
Known 3eff2.. : ∀ x0 x1 x2 . prim1 x2 (d3786.. x0 x1) ⟶ and (prim1 x2 x0) (prim1 x2 x1)
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ x1 x2 ⟶ prim1 x2 (1216a.. x0 x1)
Theorem 2ffcf.. : ∀ x0 . 80242.. x0 ⟶ and (and (and (80242.. (f4dc0.. x0)) (∀ x1 . prim1 x1 (23e07.. x0) ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1))) (∀ x1 . prim1 x1 (5246e.. x0) ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0))) (02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..)) (proof)
Theorem 706f7.. : ∀ x0 . 80242.. x0 ⟶ 80242.. (f4dc0.. x0) (proof)
Theorem 4d4af.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 x1 ⟶ 099f3.. (f4dc0.. x1) (f4dc0.. x0) (proof)
Known 8dc73.. : ∀ x0 x1 . 099f3.. x0 x1 ⟶ fe4bb.. x0 x1
Known 4c8cc.. : ∀ x0 . fe4bb.. x0 x0
Theorem f735c.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ fe4bb.. x0 x1 ⟶ fe4bb.. (f4dc0.. x1) (f4dc0.. x0) (proof)
Theorem 106e3.. : ∀ x0 . 80242.. x0 ⟶ 02b90.. (94f9e.. (5246e.. x0) f4dc0..) (94f9e.. (23e07.. x0) f4dc0..) (proof)
Theorem a9e6a.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ 02b90.. (94f9e.. x1 f4dc0..) (94f9e.. x0 f4dc0..) (proof)
Known edd11.. : ∀ x0 x1 x2 . prim1 x2 (0ac37.. x0 x1) ⟶ or (prim1 x2 x0) (prim1 x2 x1)
Known 042d7.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 (a842e.. x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . and (prim1 x4 x0) (prim1 x2 (x1 x4)) ⟶ x3) ⟶ x3
Known bba3d.. : ∀ x0 x1 . prim1 x0 x1 ⟶ nIn x1 x0
Known ordinal_Hered : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 x0 ⟶ ordinal x1
Known 4f62a.. : ∀ x0 x1 . ordinal x0 ⟶ prim1 x1 x0 ⟶ or (prim1 (4ae4a.. x1) x0) (x0 = 4ae4a.. x1)
Known 45024.. : ∀ x0 x1 . ordinal x0 ⟶ ordinal x1 ⟶ ordinal (0ac37.. x0 x1)
Known d5fb2.. : ∀ x0 . ∀ x1 : ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ordinal (x1 x2)) ⟶ ordinal (a842e.. x0 x1)
Theorem fa2f6.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 (56ded.. x0) ⟶ Subq (e4431.. (f4dc0.. x1)) (e4431.. x1) (proof)
Theorem e1909.. : ∀ x0 . 80242.. x0 ⟶ Subq (e4431.. (f4dc0.. x0)) (e4431.. x0) (proof)
Known cfea1.. : ∀ x0 : ι → ο . (∀ x1 x2 . 02b90.. x1 x2 ⟶ (∀ x3 . prim1 x3 x1 ⟶ x0 x3) ⟶ (∀ x3 . prim1 x3 x2 ⟶ x0 x3) ⟶ x0 (02a50.. x1 x2)) ⟶ ∀ x1 . 80242.. x1 ⟶ x0 x1
Known 2b8be.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ e4431.. x0 = e4431.. x1 ⟶ SNoEq_ (e4431.. x0) x0 x1 ⟶ x0 = x1
Known Subq_tra : ∀ x0 x1 x2 . Subq x0 x1 ⟶ Subq x1 x2 ⟶ Subq x0 x2
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)
Theorem 8948a.. : ∀ x0 . 80242.. x0 ⟶ f4dc0.. (f4dc0.. x0) = x0 (proof)
Theorem 15454.. : ∀ x0 . 80242.. x0 ⟶ e4431.. (f4dc0.. x0) = e4431.. x0 (proof)
Known 27bae.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 1beb9.. x0 x1 ⟶ e4431.. x1 = x0
Known 5258d.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 1beb9.. x0 x1 ⟶ 80242.. x1
Theorem 2f1de.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 1beb9.. x0 x1 ⟶ 1beb9.. x0 (f4dc0.. x1) (proof)
Theorem cd88b.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . prim1 x1 (56ded.. x0) ⟶ prim1 (f4dc0.. x1) (56ded.. x0) (proof)
Theorem f4a7a.. : ∀ x0 . 80242.. x0 ⟶ ∀ x1 x2 . 02b90.. x1 x2 ⟶ x0 = 02a50.. x1 x2 ⟶ f4dc0.. x0 = 02a50.. (94f9e.. x2 f4dc0..) (94f9e.. x1 f4dc0..) (proof)
Theorem 3cd4e.. : ∀ x0 x1 . 02b90.. x0 x1 ⟶ f4dc0.. (02a50.. x0 x1) = 02a50.. (94f9e.. x1 f4dc0..) (94f9e.. x0 f4dc0..) (proof)
Theorem d4781.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. (f4dc0.. x0) x1 ⟶ 099f3.. (f4dc0.. x1) x0 (proof)
Theorem 26c90.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. x0 (f4dc0.. x1) ⟶ 099f3.. x1 (f4dc0.. x0) (proof)
Theorem 27827.. : ∀ x0 x1 . 80242.. x0 ⟶ 80242.. x1 ⟶ 099f3.. (f4dc0.. x0) (f4dc0.. x1) ⟶ 099f3.. x1 x0 (proof)
Theorem 681ed.. : 80242.. (f4dc0.. 48ef8..) (proof)
Theorem 9ed0c.. : ∀ x0 . ordinal x0 ⟶ 80242.. (f4dc0.. x0) (proof)
Theorem 542d9.. : ∀ x0 . ordinal x0 ⟶ e4431.. (f4dc0.. x0) = x0 (proof)
Theorem 205d0.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) x0 ⟶ 099f3.. (f4dc0.. x0) x1 (proof)
Theorem c57b6.. : ∀ x0 . ordinal x0 ⟶ ∀ x1 . 80242.. x1 ⟶ prim1 (e4431.. x1) (4ae4a.. x0) ⟶ fe4bb.. (f4dc0.. x0) x1 (proof)
Definition bc82c.. := ad3ed.. (λ x0 x1 . λ x2 : ι → ι → ι . 02a50.. (0ac37.. (94f9e.. (23e07.. x0) (λ x3 . x2 x3 x1)) (94f9e.. (23e07.. x1) (x2 x0))) (0ac37.. (94f9e.. (5246e.. x0) (λ x3 . x2 x3 x1)) (94f9e.. (5246e.. x1) (x2 x0))))
Theorem 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))) (proof)
Param ac767.. : ι → ι → ι
Param f482f.. : ι → ι → ι
Definition e6316.. := ad3ed.. (λ x0 x1 . λ x2 : ι → ι → ι . 02a50.. (0ac37.. (94f9e.. (ac767.. (23e07.. x0) (23e07.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x0) (5246e.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)))))))) (0ac37.. (94f9e.. (ac767.. (23e07.. x0) (5246e.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..))))))) (94f9e.. (ac767.. (5246e.. x0) (23e07.. x1)) (λ x3 . bc82c.. (x2 (f482f.. x3 4a7ef..) x1) (bc82c.. (x2 x0 (f482f.. x3 (4ae4a.. 4a7ef..))) (f4dc0.. (x2 (f482f.. x3 4a7ef..) (f482f.. x3 (4ae4a.. 4a7ef..)))))))))
Known 9f585.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ 94f9e.. (ac767.. x0 x1) (λ x5 . x2 (f482f.. x5 4a7ef..) (f482f.. x5 (4ae4a.. 4a7ef..))) = 94f9e.. (ac767.. x0 x1) (λ x5 . x3 (f482f.. x5 4a7ef..) (f482f.. x5 (4ae4a.. 4a7ef..)))
Theorem 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..)))))))) (proof)
Param 62ee1.. : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ο
Definition f74bd.. := prim0 (λ x0 . and (∀ x1 . prim1 x1 x0 ⟶ 80242.. x1) (62ee1.. x0 4a7ef.. (4ae4a.. 4a7ef..) bc82c.. e6316.. fe4bb..))