Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrEwX../f27ff..
PUX9J../67396..
vout
PrEwX../42b60.. 24.98 bars
TMYfE../cae5b.. ownership of e4b93.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPd8../e42a2.. ownership of 3d1df.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTJz../378e8.. ownership of 7c0bd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMagB../0fd03.. ownership of d3592.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdiR../21216.. ownership of 90377.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHyz../70bcc.. ownership of 1cd72.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGVx../e84e4.. ownership of c7ce6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdoC../97087.. ownership of 7cf84.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNt1../0ee77.. ownership of e7ad6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHj9../c3b60.. ownership of f2086.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPsU../c59b2.. ownership of 33ba0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdbz../ae0ad.. ownership of 5b782.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT5x../50af2.. ownership of 7d63f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRuf../be919.. ownership of bcef1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTpy../55812.. ownership of c3164.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcgy../32057.. ownership of 1203a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ6D../39872.. ownership of 28853.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQSC../2d74d.. ownership of 4d267.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSho../bc04b.. ownership of cb2b8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLR3../0aa5d.. ownership of ae503.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQvg../8ce68.. ownership of 71c44.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZnx../1df46.. ownership of b5109.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVVo../5791f.. ownership of 41435.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRuZ../f5b41.. ownership of 6fe47.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPNK../67815.. ownership of 48cf3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKNN../5fcca.. ownership of ecbf0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH37../c0685.. ownership of a411f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdUm../38b2b.. ownership of 7406e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdpH../8582b.. ownership of 9b430.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZEx../9bc39.. ownership of b0313.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQmS../d1e3b.. ownership of 7d032.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWvP../4ca75.. ownership of 0584a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcWq../e6a42.. ownership of 10e9c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRGq../6a07e.. ownership of 5b011.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWvn../b6fcd.. ownership of 96cbf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYSd../051d8.. ownership of b8b34.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUzS../da0a8.. ownership of f97c5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaej../ee9da.. ownership of 69f5a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ2V../9b838.. ownership of 6a5ab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNEt../9bb84.. ownership of d5f5c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRSs../377e2.. ownership of c1aec.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF9P../30981.. ownership of 98491.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU5e../b7e8b.. ownership of 1f70a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMavx../dbb0d.. ownership of 5bb17.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQLv../d7e24.. ownership of 1d099.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXhs../56174.. ownership of 3f07b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTot../72202.. ownership of b5aaf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPTd../9d363.. ownership of e5389.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdvs../71c4d.. ownership of 2a5bd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWB1../04b10.. ownership of 87c84.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTjS../bb986.. ownership of e0ddc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZad../5cdf9.. ownership of 70505.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcwK../02186.. ownership of 839ff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbqo../fac7b.. ownership of cc384.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRtz../de877.. ownership of 309f9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYaM../f1fbf.. ownership of a0a1d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGVE../a4efa.. ownership of a55dd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYQP../9501e.. ownership of eda74.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbze../2b366.. ownership of c42c4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLU7../ac78c.. ownership of cffd9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMReY../662eb.. ownership of c41bd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUHv../ccccc.. ownership of 0a08e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUfq../3ac22.. ownership of ba63c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUKA../ab1f3.. ownership of ead6e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWcZ../1f078.. ownership of d6f9b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ2w../84981.. ownership of 2d22d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEwf../23b32.. ownership of 64660.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMK66../679cc.. ownership of 98317.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMduw../3a522.. ownership of da4cc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUVt../85f98.. ownership of 6b836.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQgi../2f966.. ownership of dee9e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUPZ../8bee5.. ownership of ef20a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKpL../64574.. ownership of 284cf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNS5../f39fc.. ownership of b13c8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRpn../8d687.. ownership of 2847f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaK8../ee2e0.. ownership of baee9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFB3../4b682.. ownership of b091d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHYq../311b9.. ownership of 52042.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdCy../58a80.. ownership of 53862.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYqe../1c878.. ownership of 5d59e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMboi../0fa62.. ownership of 51def.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdpV../dc4d3.. ownership of f9418.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTgh../02797.. ownership of 6599b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSPN../39582.. ownership of 0b393.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHMb../0e8db.. ownership of 114ab.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJxR../f256a.. ownership of 962f7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQYt../8d6cf.. ownership of 4223b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNry../bb954.. ownership of b545f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYMg../01e16.. ownership of e6800.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdEQ../bcb93.. ownership of ee390.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFhM../be4f7.. ownership of 3c27b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQZw../afbdc.. ownership of 84899.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM2C../a73a0.. ownership of 3967a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVyT../35613.. ownership of b8c19.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWaK../c2631.. ownership of c5fe9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbxw../8c1e9.. ownership of eeb97.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcKn../1357e.. ownership of 3b308.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMben../d60fe.. ownership of 538cb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSYY../450ae.. ownership of 42f04.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdyy../bfbc5.. ownership of 931f2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPmh../01e18.. ownership of c1142.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdYy../a78b9.. ownership of f5d91.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ3A../7bcf1.. ownership of 9c862.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP9y../1364c.. ownership of 05809.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMUr../71241.. ownership of eea63.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRQh../c0bdd.. ownership of b1594.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMzn../dd0ef.. ownership of e008e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHLU../87839.. ownership of c6d34.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMb1../f0203.. ownership of 61aee.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSyt../04797.. ownership of 9be52.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYnD../9a68f.. ownership of d246f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSzb../c4b5d.. ownership of 874ba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPeq../681ec.. ownership of 8d6c4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGPw../ad420.. ownership of 3a664.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMasY../39deb.. ownership of 5dcde.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHKg../43209.. ownership of 61201.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLjS../2eb39.. ownership of 10d52.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX5E../a975d.. ownership of 3ce64.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdV1../4f83b.. ownership of 9aabc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEiw../0e3f5.. ownership of fdfdb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMmQ../ca9d8.. ownership of 8b133.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc6F../b2527.. ownership of 45ea3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEuX../32b49.. ownership of 53049.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGZM../850a8.. ownership of 21abc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWnc../69cce.. ownership of d8dcc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGVm../3f8e9.. ownership of 3255f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTT2../28b6c.. ownership of ae691.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXG5../66bb2.. ownership of 1ff36.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN1R../bcaf4.. ownership of 21112.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTNj../cc396.. ownership of c7710.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW2k../e25ee.. ownership of 5991f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMxh../0870d.. ownership of 7860f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdJb../365ca.. ownership of 9da8a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFuY../a3224.. ownership of 4370f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTJE../b744e.. ownership of 82ac9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPdS../ceaf0.. ownership of 6a694.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPZ8../170f6.. ownership of bc3d6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYPo../db9bf.. ownership of 7fa7a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMLy../adcc7.. ownership of 9d568.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYbF../b2663.. ownership of 3f2b3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWJf../4974a.. ownership of 9bed1.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaRc../8291b.. ownership of e54ba.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMa4M../34ae2.. ownership of 8a20d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSnt../2ccbf.. ownership of 68559.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSa7../c6898.. ownership of d4b1d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFRm../c89a2.. ownership of f31aa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLzC../0b2c9.. ownership of 81f1e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNKJ../427ea.. ownership of 46a5b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdRa../ec9d5.. ownership of d1558.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRC5../dec28.. ownership of 9b454.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLfv../24888.. ownership of 1046e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPYs../b83c7.. ownership of b818a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYAf../55295.. ownership of 5bb38.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGqb../26bc3.. ownership of 74aeb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQW3../b4362.. ownership of 62bfa.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGHD../5932a.. ownership of ed836.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQxZ../e0178.. ownership of 09b8b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWwf../87471.. ownership of 7f9eb.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMF1a../b57c6.. ownership of 0a647.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQ2n../98032.. ownership of da052.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQPD../f0d4e.. ownership of c754f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTqH../4dccf.. ownership of 5ec14.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMak5../3a0a0.. ownership of de6e8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGMA../60e9b.. ownership of ceaf4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPjp../9cbab.. ownership of c83ef.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQBy../4b5d0.. ownership of 7a1ee.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRQD../9a2a6.. ownership of 1f4f1.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU1B../b667b.. ownership of 8f962.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRmk../6d3cc.. ownership of d51b5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKRX../ed489.. ownership of af873.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG7a../6b6c9.. ownership of b1713.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbQr../7ce68.. ownership of 9a542.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNwV../1d80c.. ownership of 4314e.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMd4a../74933.. ownership of 5903b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcps../701d8.. ownership of a2e89.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYki../3b2e3.. ownership of 9df55.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQn8../1094f.. ownership of 04451.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG79../5e4cf.. ownership of b21c8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMJv../e94e8.. ownership of 37dbe.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQiE../1e202.. ownership of adb09.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVET../08b14.. ownership of 7765f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWUJ../333b2.. ownership of 95931.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLnf../87c30.. ownership of 9fbe5.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbU3../36148.. ownership of c2efd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYy5../0941f.. ownership of 23f55.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT53../0b26a.. ownership of cfcc6.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMN6b../dd8f3.. ownership of 71338.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQHr../2781b.. ownership of 91764.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUdQe../d534c.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param eb53d.. : ι → CT2 ι
Definition 71338.. := λ x0 . λ x1 x2 x3 : ι → ι → ι . λ x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (eb53d.. x0 x3) x4))))
Param f482f.. : ι → ι → ι
Known 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
Theorem 62bfa.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . ∀ x5 . x0 = 71338.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 5bb38.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . x0 = f482f.. (71338.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Param e3162.. : ι → ι → ι → ι
Known 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
Known 35054.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ e3162.. (eb53d.. x0 x1) x2 x3 = x1 x2 x3
Theorem 1046e.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . ∀ x5 . x0 = 71338.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem d1558.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (71338.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Known 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
Theorem 81f1e.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . ∀ x5 . x0 = 71338.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem d4b1d.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (71338.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Known 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
Theorem 8a20d.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . ∀ x5 . x0 = 71338.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x4 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 x7 (proof)
Theorem 9bed1.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = e3162.. (f482f.. (71338.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Known 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
Theorem 9d568.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . ∀ x5 . x0 = 71338.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem bc3d6.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . x4 = f482f.. (71338.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and5I : ∀ x0 x1 x2 x3 x4 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ and (and (and (and x0 x1) x2) x3) x4
Theorem 82ac9.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 x6 x7 : ι → ι → ι . ∀ x8 x9 . 71338.. x0 x2 x4 x6 x8 = 71338.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x2 x10 x11 = x3 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x4 x10 x11 = x5 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x6 x10 x11 = x7 x10 x11)) (x8 = x9) (proof)
Known 8fdaf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ eb53d.. x0 x1 = eb53d.. x0 x2
Theorem 9da8a.. : ∀ x0 . ∀ x1 x2 x3 x4 x5 x6 : ι → ι → ι . ∀ x7 . (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x1 x8 x9 = x2 x8 x9) ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x3 x8 x9 = x4 x8 x9) ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x5 x8 x9 = x6 x8 x9) ⟶ 71338.. x0 x1 x3 x5 x7 = 71338.. x0 x2 x4 x6 x7 (proof)
Definition 23f55.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x2 ⟶ ∀ x7 . prim1 x7 x2 ⟶ prim1 (x5 x6 x7) x2) ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (71338.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 5991f.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x3 x4 x5) x0) ⟶ ∀ x4 . prim1 x4 x0 ⟶ 23f55.. (71338.. x0 x1 x2 x3 x4) (proof)
Theorem 21112.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . 23f55.. (71338.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem ae691.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . 23f55.. (71338.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Theorem d8dcc.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . 23f55.. (71338.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x3 x5 x6) x0 (proof)
Theorem 53049.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . 23f55.. (71338.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem 8b133.. : ∀ x0 . 23f55.. x0 ⟶ x0 = 71338.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 9fbe5.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 9aabc.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ι . ∀ x1 . ∀ x2 x3 x4 : ι → ι → ι . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ x4 x9 x10 = x8 x9 x10) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 9fbe5.. (71338.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 7765f.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 10d52.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ο . ∀ x1 . ∀ x2 x3 x4 : ι → ι → ι . ∀ x5 . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι → ι . (∀ x9 . prim1 x9 x1 ⟶ ∀ x10 . prim1 x10 x1 ⟶ x4 x9 x10 = x8 x9 x10) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ 7765f.. (71338.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 37dbe.. := λ x0 . λ x1 x2 : ι → ι → ι . λ x3 x4 : ι → ι . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (0fc90.. x0 x3) (0fc90.. x0 x4)))))
Theorem 5dcde.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . x0 = 37dbe.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 8d6c4.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . x0 = f482f.. (37dbe.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem d246f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . x0 = 37dbe.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem 61aee.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (37dbe.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem e008e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . x0 = 37dbe.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem eea63.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (37dbe.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem 9c862.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . x0 = 37dbe.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem c1142.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 . prim1 x5 x0 ⟶ x3 x5 = f482f.. (f482f.. (37dbe.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 42f04.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . x0 = 37dbe.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem 3b308.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = f482f.. (f482f.. (37dbe.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 (proof)
Theorem c5fe9.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 x8 x9 : ι → ι . 37dbe.. x0 x2 x4 x6 x8 = 37dbe.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x2 x10 x11 = x3 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x4 x10 x11 = x5 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (∀ x10 . prim1 x10 x0 ⟶ x8 x10 = x9 x10) (proof)
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem 3967a.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ι . ∀ x5 x6 x7 x8 : ι → ι . (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x1 x9 x10 = x2 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x3 x9 x10 = x4 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ x5 x9 = x6 x9) ⟶ (∀ x9 . prim1 x9 x0 ⟶ x7 x9 = x8 x9) ⟶ 37dbe.. x0 x1 x3 x5 x7 = 37dbe.. x0 x2 x4 x6 x8 (proof)
Definition 04451.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 : ι → ι . (∀ x6 . prim1 x6 x2 ⟶ prim1 (x5 x6) x2) ⟶ ∀ x6 : ι → ι . (∀ x7 . prim1 x7 x2 ⟶ prim1 (x6 x7) x2) ⟶ x1 (37dbe.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 3c27b.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ prim1 (x3 x4) x0) ⟶ ∀ x4 : ι → ι . (∀ x5 . prim1 x5 x0 ⟶ prim1 (x4 x5) x0) ⟶ 04451.. (37dbe.. x0 x1 x2 x3 x4) (proof)
Theorem e6800.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . 04451.. (37dbe.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem 4223b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . 04451.. (37dbe.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Theorem 114ab.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . 04451.. (37dbe.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x3 x5) x0 (proof)
Theorem 6599b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι . 04451.. (37dbe.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x4 x5) x0 (proof)
Theorem 51def.. : ∀ x0 . 04451.. x0 ⟶ x0 = 37dbe.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition a2e89.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 53862.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ι . (∀ x10 . prim1 x10 x1 ⟶ x5 x10 = x9 x10) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ a2e89.. (37dbe.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 4314e.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem b091d.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 x5 : ι → ι . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ι . (∀ x10 . prim1 x10 x1 ⟶ x5 x10 = x9 x10) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 4314e.. (37dbe.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Param d2155.. : ι → (ι → ι → ο) → ι
Definition b1713.. := λ x0 . λ x1 x2 : ι → ι → ι . λ x3 : ι → ι . λ x4 : ι → ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (0fc90.. x0 x3) (d2155.. x0 x4)))))
Theorem 2847f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ο . x0 = b1713.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 284cf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 x5 : ι → ι → ο . x5 x0 (f482f.. (b1713.. x0 x1 x2 x3 x4) 4a7ef..) ⟶ x5 (f482f.. (b1713.. x0 x1 x2 x3 x4) 4a7ef..) x0 (proof)
Theorem dee9e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ο . x0 = b1713.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem da4cc.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (b1713.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 64660.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ο . x0 = b1713.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem d6f9b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (b1713.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem ba63c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ο . x0 = b1713.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem c41bd.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x3 x5 = f482f.. (f482f.. (b1713.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Param 2b2e3.. : ι → ι → ι → ο
Known 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem c42c4.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ο . x0 = b1713.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x5 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 x7 (proof)
Theorem a55dd.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x4 x5 x6 = 2b2e3.. (f482f.. (b1713.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 x6 (proof)
Theorem 309f9.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι . ∀ x8 x9 : ι → ι → ο . b1713.. x0 x2 x4 x6 x8 = b1713.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x2 x10 x11 = x3 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x4 x10 x11 = x5 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x8 x10 x11 = x9 x10 x11) (proof)
Param iff : ο → ο → ο
Known 62ef7.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ d2155.. x0 x1 = d2155.. x0 x2
Theorem 839ff.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ι . ∀ x5 x6 : ι → ι . ∀ x7 x8 : ι → ι → ο . (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x1 x9 x10 = x2 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x3 x9 x10 = x4 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ x5 x9 = x6 x9) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ iff (x7 x9 x10) (x8 x9 x10)) ⟶ b1713.. x0 x1 x3 x5 x7 = b1713.. x0 x2 x4 x6 x8 (proof)
Definition d51b5.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 : ι → ι . (∀ x6 . prim1 x6 x2 ⟶ prim1 (x5 x6) x2) ⟶ ∀ x6 : ι → ι → ο . x1 (b1713.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem e0ddc.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ prim1 (x3 x4) x0) ⟶ ∀ x4 : ι → ι → ο . d51b5.. (b1713.. x0 x1 x2 x3 x4) (proof)
Theorem 2a5bd.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . d51b5.. (b1713.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem b5aaf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . d51b5.. (b1713.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Theorem 1d099.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ι → ο . d51b5.. (b1713.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x3 x5) x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 1f70a.. : ∀ x0 . d51b5.. x0 ⟶ x0 = b1713.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition 1f4f1.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem c1aec.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . prim1 x10 x1 ⟶ ∀ x11 . prim1 x11 x1 ⟶ iff (x5 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 1f4f1.. (b1713.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition c83ef.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 6a5ab.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ι → ο . (∀ x10 . prim1 x10 x1 ⟶ ∀ x11 . prim1 x11 x1 ⟶ iff (x5 x10 x11) (x9 x10 x11)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ c83ef.. (b1713.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Param 1216a.. : ι → (ι → ο) → ι
Definition de6e8.. := λ x0 . λ x1 x2 : ι → ι → ι . λ x3 : ι → ι . λ x4 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (0fc90.. x0 x3) (1216a.. x0 x4)))))
Theorem f97c5.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ο . x0 = de6e8.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 96cbf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . x0 = f482f.. (de6e8.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 10e9c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ο . x0 = de6e8.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem 7d032.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = e3162.. (f482f.. (de6e8.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 9b430.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ο . x0 = de6e8.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem a411f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = e3162.. (f482f.. (de6e8.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 48cf3.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ο . x0 = de6e8.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 41435.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x3 x5 = f482f.. (f482f.. (de6e8.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Param decode_p : ι → ι → ο
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 71c44.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ο . x0 = de6e8.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x5 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x6 (proof)
Theorem cb2b8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x0 ⟶ x4 x5 = decode_p (f482f.. (de6e8.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) x5 (proof)
Theorem 28853.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι . ∀ x8 x9 : ι → ο . de6e8.. x0 x2 x4 x6 x8 = de6e8.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x2 x10 x11 = x3 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ ∀ x11 . prim1 x11 x0 ⟶ x4 x10 x11 = x5 x10 x11)) (∀ x10 . prim1 x10 x0 ⟶ x6 x10 = x7 x10)) (∀ x10 . prim1 x10 x0 ⟶ x8 x10 = x9 x10) (proof)
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Theorem c3164.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ι . ∀ x5 x6 : ι → ι . ∀ x7 x8 : ι → ο . (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x1 x9 x10 = x2 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ ∀ x10 . prim1 x10 x0 ⟶ x3 x9 x10 = x4 x9 x10) ⟶ (∀ x9 . prim1 x9 x0 ⟶ x5 x9 = x6 x9) ⟶ (∀ x9 . prim1 x9 x0 ⟶ iff (x7 x9) (x8 x9)) ⟶ de6e8.. x0 x1 x3 x5 x7 = de6e8.. x0 x2 x4 x6 x8 (proof)
Definition c754f.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ι . (∀ x4 . prim1 x4 x2 ⟶ ∀ x5 . prim1 x5 x2 ⟶ prim1 (x3 x4 x5) x2) ⟶ ∀ x4 : ι → ι → ι . (∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ prim1 (x4 x5 x6) x2) ⟶ ∀ x5 : ι → ι . (∀ x6 . prim1 x6 x2 ⟶ prim1 (x5 x6) x2) ⟶ ∀ x6 : ι → ο . x1 (de6e8.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 7d63f.. : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x2 x3 x4) x0) ⟶ ∀ x3 : ι → ι . (∀ x4 . prim1 x4 x0 ⟶ prim1 (x3 x4) x0) ⟶ ∀ x4 : ι → ο . c754f.. (de6e8.. x0 x1 x2 x3 x4) (proof)
Theorem 33ba0.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . c754f.. (de6e8.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x1 x5 x6) x0 (proof)
Theorem e7ad6.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . c754f.. (de6e8.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x2 x5 x6) x0 (proof)
Theorem c7ce6.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 : ι → ο . c754f.. (de6e8.. x0 x1 x2 x3 x4) ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x3 x5) x0 (proof)
Theorem 90377.. : ∀ x0 . c754f.. x0 ⟶ x0 = de6e8.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))) (proof)
Definition 0a647.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem 7c0bd.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 0a647.. (de6e8.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 09b8b.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))))
Theorem e4b93.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → (ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . ∀ x5 : ι → ο . (∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x2 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x3 x8 x9 = x7 x8 x9) ⟶ ∀ x8 : ι → ι . (∀ x9 . prim1 x9 x1 ⟶ x4 x9 = x8 x9) ⟶ ∀ x9 : ι → ο . (∀ x10 . prim1 x10 x1 ⟶ iff (x5 x10) (x9 x10)) ⟶ x0 x1 x6 x7 x8 x9 = x0 x1 x2 x3 x4 x5) ⟶ 09b8b.. (de6e8.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)