Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrA9L../626eb..
PUUJ5../ca30b..
vout
PrA9L../b6438.. 24.98 bars
TMT3q../b6736.. ownership of e3f76.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLS8../5b067.. ownership of 7792b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMnz../2f66c.. ownership of 9119e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJVr../4fd31.. ownership of 98dc7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZ2N../2c4b3.. ownership of c309c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTcv../25bb5.. ownership of 2df40.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUNp../ba285.. ownership of 50e1c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNE7../c127b.. ownership of 169e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJLB../b38bc.. ownership of f20e8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVni../914da.. ownership of ba801.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXAb../44db3.. ownership of 86de4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKuC../2aff6.. ownership of 9a3a5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMV95../96333.. ownership of 2b7cd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVNj../03af4.. ownership of e6496.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYwS../0f06d.. ownership of 121e6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMX6f../a5e26.. ownership of 593dd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEj4../2373c.. ownership of ee4fc.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVhZ../6b5f5.. ownership of 23f15.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUFL../c70b5.. ownership of 09398.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYT9../80dec.. ownership of 64c40.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS1K../15d81.. ownership of eda5f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRdC../584bd.. ownership of a4579.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLKH../cf528.. ownership of 7317d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKQj../41e33.. ownership of 9b67d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMRM../388e2.. ownership of ffd4f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEix../c3885.. ownership of 0af29.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNXW../c951f.. ownership of 87536.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUQ7../ba7ef.. ownership of e23c7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMT8X../dc866.. ownership of 91639.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRbD../a8627.. ownership of bd515.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPk1../7ab2d.. ownership of e2b9c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTmZ../5d581.. ownership of fb186.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFsz../0f811.. ownership of 9c391.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLes../54fe4.. ownership of 2f915.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaun../4b5e8.. ownership of 6ab76.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUuZ../a917b.. ownership of 8e68b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMpi../64a92.. ownership of 00522.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUG7../c80e5.. ownership of 93afd.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXKW../6f50d.. ownership of dccff.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMau7../39599.. ownership of ebcd6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZUS../a22a7.. ownership of ed400.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRyu../a8964.. ownership of 13ca6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG3K../3af97.. ownership of 6c77d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRz3../a1936.. ownership of 3b387.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcrg../ffba9.. ownership of f788e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXRK../ab03b.. ownership of fe6eb.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUCA../56d79.. ownership of 57c76.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbXV../aeba8.. ownership of 373f6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTok../b805a.. ownership of 1c47d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMG6P../3f057.. ownership of a6e59.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYUS../95d5b.. ownership of c33e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQis../2f2ca.. ownership of cf689.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPyk../c4c72.. ownership of 7a66d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMY2X../8b525.. ownership of 68668.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb1j../b3288.. ownership of fb682.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWKN../400a8.. ownership of 2ea6f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKeE../b96d2.. ownership of 5b944.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYyz../07eac.. ownership of 97f1f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMPm../500e2.. ownership of 3c050.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFNm../aa58d.. ownership of c9b23.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbqy../c0643.. ownership of ee1d2.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQFU../c23b6.. ownership of 21b1a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXyk../3778b.. ownership of e66ce.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNZm../73a89.. ownership of e3dd3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRg5../9cf05.. ownership of b9b42.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaZU../27183.. ownership of f9155.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRq9../0c1a6.. ownership of d5f6d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMRkp../df22c.. ownership of 2cec6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcuQ../f6b84.. ownership of 07bb5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFtG../d7390.. ownership of 02f0c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPXG../4597c.. ownership of 16b9f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTnC../c41e8.. ownership of 6ef01.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbAz../2a245.. ownership of 1283d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUfN../807a1.. ownership of 5151c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMR9f../1f554.. ownership of 7a018.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTRv../61307.. ownership of 36621.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbT2../f1b4e.. ownership of ff222.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJP1../a8c8c.. ownership of 8ebce.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXZi../907c4.. ownership of 4108c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLNQ../26799.. ownership of a918e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMccy../798a2.. ownership of 67912.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVM5../ccaa4.. ownership of d914d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMS2z../3e8de.. ownership of 71832.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJMJ../7fe1e.. ownership of 84db5.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNiJ../96ca6.. ownership of 44294.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWeT../5c030.. ownership of 74c45.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPve../237ea.. ownership of eb01a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVNz../bab5b.. ownership of 72906.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEsZ../34a7b.. ownership of 8569e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdyk../a4a9e.. ownership of 5375e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKHA../1fadc.. ownership of 6e26a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWwW../85be3.. ownership of 87949.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMW7y../c23d5.. ownership of 7e4a4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSvv../d5c90.. ownership of a7429.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGML../541e6.. ownership of f1f54.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTME../db847.. ownership of 57767.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdK9../9580e.. ownership of 4b5da.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGfe../2f6ff.. ownership of d478b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJqw../445ac.. ownership of 94c28.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTTU../be43c.. ownership of abf32.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVPm../06c33.. ownership of c8f7f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQDu../611ef.. ownership of bf3a8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGZd../db3f1.. ownership of 6e35b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdNB../476de.. ownership of b0049.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSxx../c3f18.. ownership of fffe9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPhs../5e28b.. ownership of e3028.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU73../aac4d.. ownership of e0b1d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMwQ../02858.. ownership of 7f04e.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbww../644a6.. ownership of 2349c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMb3t../abb16.. ownership of 21805.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMc4x../8dcf6.. ownership of 31e00.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMKeS../b8dad.. ownership of c8bd7.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMJtw../8d72a.. ownership of f7bea.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWvy../6a12f.. ownership of f71e3.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLPo../ea949.. ownership of 02e09.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXqf../33aca.. ownership of 1ead9.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPV1../fb7e9.. ownership of bb5c0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMctu../35b88.. ownership of cbb6d.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMVmg../95b03.. ownership of d075f.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPhT../41fb8.. ownership of 09486.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXmj../a161e.. ownership of ba288.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXko../3e0e8.. ownership of cf983.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZTE../0639a.. ownership of db6e8.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP7x../7f845.. ownership of 4bdaf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMSDd../2dcd1.. ownership of ead03.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGMo../798b9.. ownership of e5086.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUbj../f7bb3.. ownership of 07fdf.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaSK../77652.. ownership of 93a24.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYNm../aea3b.. ownership of bab90.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TML5h../dc9ad.. ownership of 9ae7a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHNn../a5f9e.. ownership of 6af8a.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXhb../c26c9.. ownership of 7e3b0.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbks../360e6.. ownership of 38ec6.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMXwA../d0754.. ownership of e9fe4.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbLh../c91cb.. ownership of e8070.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMNVn../35477.. ownership of dff0b.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMYcq../ee729.. ownership of c523c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGnu../1e1df.. ownership of 9f82c.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFki../ae96c.. ownership of 440ae.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMdje../fc1b1.. ownership of 95938.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWSe../211ce.. ownership of 20346.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHKm../88b00.. ownership of f2429.. as prop with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLjt../989e0.. ownership of 008b9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPg2../b4369.. ownership of 97905.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMaEQ../1daaa.. ownership of 0ca1b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTuR../33650.. ownership of f2224.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQki../65482.. ownership of c19ad.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcZu../7c6b5.. ownership of f2777.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMcAn../2ef78.. ownership of 97f57.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMP3D../aedf8.. ownership of 2f519.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTTg../d3634.. ownership of f5144.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMTvX../f1765.. ownership of 93264.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLHQ../64a9c.. ownership of 6cae4.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMFDw../d60b6.. ownership of 0cbfd.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWKP../30784.. ownership of b0aa9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUXP../d3d07.. ownership of 757d8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMHFt../0a180.. ownership of 363b9.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUaX../22704.. ownership of b2e97.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMZdv../32f03.. ownership of 45090.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMMRd../be2d4.. ownership of 5cc00.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMWBu../52683.. ownership of d6ebe.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMGJp../86f62.. ownership of d57b8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMU4v../d5c8b.. ownership of 8f2ce.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUzT../cd60a.. ownership of 30e85.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMQf8../d6793.. ownership of 0d9e7.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMM7y../0a7d0.. ownership of 83331.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUft../e016f.. ownership of d768a.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMUmg../84235.. ownership of 7a679.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMLgU../b288d.. ownership of cc817.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbec../5b304.. ownership of b14be.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMEjr../8ad96.. ownership of d469f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMbCQ../dc251.. ownership of 20b7b.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMPLF../5886e.. ownership of 3d68f.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
TMH5t../bcce8.. ownership of 535e8.. as obj with payaddr PrGxv.. rights free controlledby PrGxv.. upto 0
PUNse../64dda.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param d2155.. : ι → (ι → ι → ο) → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition 3d68f.. := λ x0 . λ x1 x2 : ι → ι → ο . λ x3 : ι → ο . λ x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (1216a.. 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 20346.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = 3d68f.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 440ae.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x0 = f482f.. (3d68f.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Param 2b2e3.. : ι → ι → ι → ο
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 67416.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ 2b2e3.. (d2155.. x0 x1) x2 x3 = x1 x2 x3
Theorem c523c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = 3d68f.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem e8070.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = 2b2e3.. (f482f.. (3d68f.. 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 38ec6.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = 3d68f.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem 6af8a.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. (3d68f.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Param decode_p : ι → ι → ο
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
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem bab90.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = 3d68f.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (proof)
Theorem 07fdf.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . prim1 x5 x0 ⟶ x3 x5 = decode_p (f482f.. (3d68f.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (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 ead03.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . x0 = 3d68f.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem db6e8.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . x4 = f482f.. (3d68f.. 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 ba288.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . ∀ x6 x7 : ι → ο . ∀ x8 x9 . 3d68f.. x0 x2 x4 x6 x8 = 3d68f.. 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)) (x8 = x9) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
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 d075f.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 x6 : ι → ο . ∀ x7 . (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ iff (x1 x8 x9) (x2 x8 x9)) ⟶ (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ iff (x3 x8 x9) (x4 x8 x9)) ⟶ (∀ x8 . prim1 x8 x0 ⟶ iff (x5 x8) (x6 x8)) ⟶ 3d68f.. x0 x1 x3 x5 x7 = 3d68f.. x0 x2 x4 x6 x7 (proof)
Definition d469f.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . ∀ x5 : ι → ο . ∀ x6 . prim1 x6 x2 ⟶ x1 (3d68f.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem bb5c0.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ d469f.. (3d68f.. x0 x1 x2 x3 x4) (proof)
Theorem 02e09.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 . d469f.. (3d68f.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem f7bea.. : ∀ x0 . d469f.. x0 ⟶ x0 = 3d68f.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition cc817.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 31e00.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ι → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x3 x8 x9) (x7 x8 x9)) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ cc817.. (3d68f.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition d768a.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 2349c.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → (ι → ο) → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x3 x8 x9) (x7 x8 x9)) ⟶ ∀ x8 : ι → ο . (∀ x9 . prim1 x9 x1 ⟶ iff (x4 x9) (x8 x9)) ⟶ x0 x1 x6 x7 x8 x5 = x0 x1 x2 x3 x4 x5) ⟶ d768a.. (3d68f.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 0d9e7.. := λ x0 . λ x1 x2 : ι → ι → ο . λ x3 x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (d2155.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))
Theorem e0b1d.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . x0 = 0d9e7.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem fffe9.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . x0 = f482f.. (0d9e7.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem 6e35b.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . x0 = 0d9e7.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem c8f7f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = 2b2e3.. (f482f.. (0d9e7.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 94c28.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . x0 = 0d9e7.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x3 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 x7 (proof)
Theorem 4b5da.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 x6 = 2b2e3.. (f482f.. (0d9e7.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem f1f54.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . x0 = 0d9e7.. x1 x2 x3 x4 x5 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 7e4a4.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . x3 = f482f.. (0d9e7.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 6e26a.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . x0 = 0d9e7.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 8569e.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . x4 = f482f.. (0d9e7.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem eb01a.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ο . ∀ x6 x7 x8 x9 . 0d9e7.. x0 x2 x4 x6 x8 = 0d9e7.. 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)) (x6 = x7)) (x8 = x9) (proof)
Theorem 44294.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ο . ∀ x5 x6 . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x1 x7 x8) (x2 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x3 x7 x8) (x4 x7 x8)) ⟶ 0d9e7.. x0 x1 x3 x5 x6 = 0d9e7.. x0 x2 x4 x5 x6 (proof)
Definition 8f2ce.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ι → ο . ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (0d9e7.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 71832.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ 8f2ce.. (0d9e7.. x0 x1 x2 x3 x4) (proof)
Theorem 67912.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . 8f2ce.. (0d9e7.. x0 x1 x2 x3 x4) ⟶ prim1 x3 x0 (proof)
Theorem 4108c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 . 8f2ce.. (0d9e7.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem ff222.. : ∀ x0 . 8f2ce.. x0 ⟶ x0 = 0d9e7.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition d6ebe.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 7a018.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x3 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ d6ebe.. (0d9e7.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 45090.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 1283d.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x3 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ 45090.. (0d9e7.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 363b9.. := λ x0 . λ x1 : ι → ι → ο . λ x2 : ι → ο . λ x3 x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (d2155.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))
Theorem 16b9f.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 363b9.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 07bb5.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 x4 . x0 = f482f.. (363b9.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem d5f6d.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 363b9.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = 2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..)) x6 x7 (proof)
Theorem b9b42.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x1 x5 x6 = 2b2e3.. (f482f.. (363b9.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem e66ce.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 363b9.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem ee1d2.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x2 x5 = decode_p (f482f.. (363b9.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 3c050.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 363b9.. x1 x2 x3 x4 x5 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 5b944.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 x4 . x3 = f482f.. (363b9.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem fb682.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . x0 = 363b9.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 7a66d.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 x4 . x4 = f482f.. (363b9.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem c33e3.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ο . ∀ x6 x7 x8 x9 . 363b9.. x0 x2 x4 x6 x8 = 363b9.. 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 ⟶ x4 x10 = x5 x10)) (x6 = x7)) (x8 = x9) (proof)
Theorem 1c47d.. : ∀ x0 . ∀ x1 x2 : ι → ι → ο . ∀ x3 x4 : ι → ο . ∀ x5 x6 . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x1 x7 x8) (x2 x7 x8)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x3 x7) (x4 x7)) ⟶ 363b9.. x0 x1 x3 x5 x6 = 363b9.. x0 x2 x4 x5 x6 (proof)
Definition b0aa9.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : ι → ι → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (363b9.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 57c76.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ b0aa9.. (363b9.. x0 x1 x2 x3 x4) (proof)
Theorem f788e.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 x4 . b0aa9.. (363b9.. x0 x1 x2 x3 x4) ⟶ prim1 x3 x0 (proof)
Theorem 6c77d.. : ∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 : ι → ο . ∀ x3 x4 . b0aa9.. (363b9.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem ed400.. : ∀ x0 . b0aa9.. x0 ⟶ x0 = 363b9.. (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 6cae4.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ο) → ι → ι → ι . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem dccff.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ο) → ι → ι → ι . ∀ x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ 6cae4.. (363b9.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition f5144.. := λ x0 . λ x1 : ι → (ι → ι → ο) → (ι → ο) → ι → ι → ο . x1 (f482f.. x0 4a7ef..) (2b2e3.. (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 00522.. : ∀ x0 : ι → (ι → ι → ο) → (ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 : ι → ι → ο . ∀ x3 : ι → ο . ∀ x4 x5 . (∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ f5144.. (363b9.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 97f57.. := λ x0 . λ x1 x2 : ι → ο . λ x3 x4 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) (1216a.. x0 x1) (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x2) (If_i (x5 = 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) x3 x4))))
Theorem 6ab76.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . x0 = 97f57.. x1 x2 x3 x4 x5 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 9c391.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 x4 . x0 = f482f.. (97f57.. x0 x1 x2 x3 x4) 4a7ef.. (proof)
Theorem e2b9c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . x0 = 97f57.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x6 = decode_p (f482f.. x0 (4ae4a.. 4a7ef..)) x6 (proof)
Theorem 91639.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x1 x5 = decode_p (f482f.. (97f57.. x0 x1 x2 x3 x4) (4ae4a.. 4a7ef..)) x5 (proof)
Theorem 87536.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . x0 = 97f57.. x1 x2 x3 x4 x5 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x6 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x6 (proof)
Theorem ffd4f.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 x4 x5 . prim1 x5 x0 ⟶ x2 x5 = decode_p (f482f.. (97f57.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 7317d.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . x0 = 97f57.. x1 x2 x3 x4 x5 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem eda5f.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 x4 . x3 = f482f.. (97f57.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 09398.. : ∀ x0 x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . x0 = 97f57.. x1 x2 x3 x4 x5 ⟶ x5 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem ee4fc.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 x4 . x4 = f482f.. (97f57.. x0 x1 x2 x3 x4) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Theorem 121e6.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ο . ∀ x6 x7 x8 x9 . 97f57.. x0 x2 x4 x6 x8 = 97f57.. x1 x3 x5 x7 x9 ⟶ and (and (and (and (x0 = x1) (∀ x10 . prim1 x10 x0 ⟶ x2 x10 = x3 x10)) (∀ x10 . prim1 x10 x0 ⟶ x4 x10 = x5 x10)) (x6 = x7)) (x8 = x9) (proof)
Theorem 2b7cd.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ο . ∀ x5 x6 . (∀ x7 . prim1 x7 x0 ⟶ iff (x1 x7) (x2 x7)) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x3 x7) (x4 x7)) ⟶ 97f57.. x0 x1 x3 x5 x6 = 97f57.. x0 x2 x4 x5 x6 (proof)
Definition c19ad.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 x4 : ι → ο . ∀ x5 . prim1 x5 x2 ⟶ ∀ x6 . prim1 x6 x2 ⟶ x1 (97f57.. x2 x3 x4 x5 x6)) ⟶ x1 x0
Theorem 86de4.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ c19ad.. (97f57.. x0 x1 x2 x3 x4) (proof)
Theorem f20e8.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 x4 . c19ad.. (97f57.. x0 x1 x2 x3 x4) ⟶ prim1 x3 x0 (proof)
Theorem 50e1c.. : ∀ x0 . ∀ x1 x2 : ι → ο . ∀ x3 x4 . c19ad.. (97f57.. x0 x1 x2 x3 x4) ⟶ prim1 x4 x0 (proof)
Theorem c309c.. : ∀ x0 . c19ad.. x0 ⟶ x0 = 97f57.. (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 0ca1b.. := λ x0 . λ x1 : ι → (ι → ο) → (ι → ο) → ι → ι → ι . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 9119e.. : ∀ x0 : ι → (ι → ο) → (ι → ο) → ι → ι → ι . ∀ x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . (∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (x2 x7) (x6 x7)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ 0ca1b.. (97f57.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)
Definition 008b9.. := λ x0 . λ x1 : ι → (ι → ο) → (ι → ο) → ι → ι → ο . x1 (f482f.. x0 4a7ef..) (decode_p (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem e3f76.. : ∀ x0 : ι → (ι → ο) → (ι → ο) → ι → ι → ο . ∀ x1 . ∀ x2 x3 : ι → ο . ∀ x4 x5 . (∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (x2 x7) (x6 x7)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5) ⟶ 008b9.. (97f57.. x1 x2 x3 x4 x5) x0 = x0 x1 x2 x3 x4 x5 (proof)