Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrHSC../84764..
PUYgU../80851..
vout
PrHSC../47c0d.. 9.98 bars
TMdfr../8786f.. ownership of 9d144.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUxq../2b415.. ownership of c7c01.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN5V../aa508.. ownership of 16ffc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTbC../701d3.. ownership of e3bc9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM4b../6f48f.. ownership of d704c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZrP../221f1.. ownership of e43a2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMzm../e90b6.. ownership of aabb3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd35../50e36.. ownership of 50206.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMc7V../ba294.. ownership of 0328a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFkY../ad086.. ownership of 5a706.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWNj../5f167.. ownership of 7af5a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaTs../ac6c7.. ownership of 46441.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKh9../949c6.. ownership of 7e158.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcte../75128.. ownership of 1c101.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLV6../04d2f.. ownership of 61696.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaLf../b39fa.. ownership of 3942a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFzG../a1cf3.. ownership of 63e29.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFFd../2a155.. ownership of cd131.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdsk../7c1c4.. ownership of 3799b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMEy../67ae6.. ownership of 5dc5e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcTN../0cdb9.. ownership of 4a13b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbKW../5720f.. ownership of 52108.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNvz../77861.. ownership of 61558.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRv1../22200.. ownership of d2499.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSuJ../29883.. ownership of 7bd1f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTR5../61b9b.. ownership of 4e842.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN7U../b4c0a.. ownership of 69a7d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNBB../510fc.. ownership of fb456.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcyd../16dfb.. ownership of 0c12c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGF9../10d4c.. ownership of 36c42.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPHH../e43ad.. ownership of 3461b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNjP../60f58.. ownership of ff649.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUK5../44fdc.. ownership of 8d675.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTFr../c2f9d.. ownership of 0a0ba.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWhe../e7003.. ownership of 4d4c5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZm8../78681.. ownership of 4e533.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMP8../7ba12.. ownership of 3bcdc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHam../f0ce7.. ownership of 174d6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRJM../0d310.. ownership of 24fe3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH2T../6e23a.. ownership of a3022.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcwM../8b914.. ownership of 32733.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcj1../301a5.. ownership of 4750f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZw5../67340.. ownership of c4a94.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFgV../8c355.. ownership of 86248.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPkp../14fd5.. ownership of db7ec.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMfF../a6e57.. ownership of 4e57c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYbC../45ee9.. ownership of a4816.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKQW../f716e.. ownership of 9cdb4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKMj../95ee6.. ownership of 4f7a6.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUoU../0c321.. ownership of 86854.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWL4../3021e.. ownership of 93da0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSRA../cece8.. ownership of 78ffa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTZV../f60c8.. ownership of efc45.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYpX../75776.. ownership of 01ea1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP2P../4efb0.. ownership of 0a008.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNhD../7c914.. ownership of 2e5a3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYLK../c6531.. ownership of d5534.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJxB../b6453.. ownership of 148aa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV3H../4d354.. ownership of ac959.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQP5../58223.. ownership of 5503c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKPE../ec2fb.. ownership of 3541c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcP1../1608b.. ownership of 36751.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ2M../aee3e.. ownership of 59d0c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS3e../384a8.. ownership of 31e61.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR2t../3de06.. ownership of cfdca.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMaMY../c7d8c.. ownership of adea0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJYo../a873a.. ownership of 17fc0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPh5../253bc.. ownership of de7f1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMExH../e521d.. ownership of 931eb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbL8../0fefd.. ownership of c83af.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK6H../ffd96.. ownership of c282a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMpg../672bc.. ownership of 0e163.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFxr../ba2e7.. ownership of 24dbe.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMN2x../710ae.. ownership of a2ea1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMV4w../8bc86.. ownership of 99505.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY6N../0ac95.. ownership of 02381.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKe5../64645.. ownership of f5883.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMVz../ed973.. ownership of f8fc4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKDm../a7a11.. ownership of 378d1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ76../83857.. ownership of a30f2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdvg../582f4.. ownership of dba9c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX3A../7b92c.. ownership of 97501.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdbK../da11b.. ownership of e53a5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcKw../b853c.. ownership of ea68f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHMa../6b289.. ownership of 6f41d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMU3V../4a996.. ownership of 3553e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMExy../33f04.. ownership of 8873d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdcw../eaf19.. ownership of 6240d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcXC../39658.. ownership of 2da5e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSeg../ad031.. ownership of 9f15e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNPr../2ba1b.. ownership of 522c4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHeK../8dd64.. ownership of 8158c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLNj../745d4.. ownership of 89cf7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQz2../e0398.. ownership of 85c98.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcRB../c3e53.. ownership of 6301b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMbY../923f3.. ownership of d3b5a.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYKF../c1d89.. ownership of c1c1f.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRu9../7c5b5.. ownership of 939b3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcX4../f6d23.. ownership of 668b5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbWK../b03ff.. ownership of 4f8aa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQnv../d2997.. ownership of 368fb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMd2m../95e92.. ownership of c44bd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWbH../b9318.. ownership of b1359.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVCB../4d1ba.. ownership of 686ed.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRYH../b4d0c.. ownership of f09cb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSDE../0b187.. ownership of b4faa.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTeX../78190.. ownership of 12642.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFYd../ea390.. ownership of 36ab7.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMdxh../cf1f8.. ownership of a44f4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWq2../4a451.. ownership of c6dcd.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbKS../369c6.. ownership of 8b690.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMR4N../b6ce8.. ownership of bd1a4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNMg../171a9.. ownership of a5c5d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWG1../61a90.. ownership of ce65b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNh7../17382.. ownership of 55876.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQx8../af6b1.. ownership of 4854e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXkD../f79cb.. ownership of 8be55.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMadr../9a583.. ownership of d90cb.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUqd../f9e22.. ownership of e20c4.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJYF../44f1e.. ownership of 3bd77.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFaM../63f48.. ownership of 5e96d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ8X../63b6c.. ownership of d91c9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKKs../c0017.. ownership of 320f0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMFqW../5e3e1.. ownership of 2c54d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMWU../a4eb8.. ownership of 72a00.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMM4U../b084c.. ownership of ff453.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYuB../1c148.. ownership of adf33.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK8M../a2f07.. ownership of 9b5e3.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJfW../6bd20.. ownership of 02f73.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMagP../b763b.. ownership of 8f65d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJPe../0e963.. ownership of eb96c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbvH../105fd.. ownership of 0b87e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMMaM../ac530.. ownership of 65b34.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUn2../20e37.. ownership of 67a0e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMYt4../d18ba.. ownership of 63f68.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEvz../d646e.. ownership of b7bd9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQAE../331ff.. ownership of 58abf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUED../29d57.. ownership of 3a354.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGBY../7c36c.. ownership of 22eb2.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHn4../88a29.. ownership of 7ca98.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGcB../d36e3.. ownership of c3940.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMda3../d7c3e.. ownership of f011b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLuR../673de.. ownership of b08f5.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRnT../5de12.. ownership of 04e3c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVYA../e9c46.. ownership of 429e9.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPbo../26f57.. ownership of 6e02c.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZvp../448ed.. ownership of 0821e.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPxV../ddf42.. ownership of 469b0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMZRs../f4056.. ownership of 3896b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMSQK../590b5.. ownership of 019fc.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbsx../1dd22.. ownership of 559b0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNx5../269ca.. ownership of 2eb06.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMS3b../7e8d8.. ownership of 5c88b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMLLj../cdeb8.. ownership of d86f1.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWtY../3b0f1.. ownership of b579b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWQL../a1143.. ownership of 683bf.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTW4../7946e.. ownership of 7f14b.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPCV../1dc69.. ownership of e59f0.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMVLm../4ce94.. ownership of 572ce.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRt6../40c53.. ownership of b585d.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcGa../56487.. ownership of 4f989.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMF9x../f65ae.. ownership of 58638.. as prop with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMP2f../b4f15.. ownership of cc976.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHJi../713da.. ownership of 3ef10.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT5q../c0846.. ownership of 41669.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK4E../35b19.. ownership of d9e55.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUcH../3214e.. ownership of 0ee11.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMScd../94fd7.. ownership of ca3bc.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKqV../08348.. ownership of 8f64a.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTLf../56d60.. ownership of f1040.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNmE../f1a36.. ownership of 851fe.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX4T../2b832.. ownership of 0c373.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPPA../82f52.. ownership of b2ca5.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMHMA../ef891.. ownership of dde42.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMGBd../558a1.. ownership of 17cf8.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMKkM../cebde.. ownership of 993ee.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRYd../d1b97.. ownership of 64302.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMbsD../33aec.. ownership of 7dee3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQXo../b7faa.. ownership of 824ea.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTzT../c0c01.. ownership of 7ea86.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMEra../06e2e.. ownership of 98d5c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRDH../6944c.. ownership of cd21b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMX5n../a8792.. ownership of 74f92.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcNt../d06cc.. ownership of 28758.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXSE../f490a.. ownership of a255b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWS4../c8d7f.. ownership of 5b45c.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT2F../a3bc0.. ownership of 6a70f.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMK6V../001cb.. ownership of de033.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMT8y../b185f.. ownership of 02be0.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMTzM../f4dd5.. ownership of 1efea.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMWCk../9c1e0.. ownership of 56cd3.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMNE7../ca4c0.. ownership of 47255.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMJRZ../2e26e.. ownership of 7c612.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUAT../f3f80.. ownership of 0ca0d.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMRBJ../89be3.. ownership of 7a422.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMUWY../436d7.. ownership of 202e1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMcPP../6c564.. ownership of bbb33.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMH2Z../fcd2b.. ownership of 0715e.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMPum../ddb47.. ownership of 7f5b4.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMY9Z../1a6e8.. ownership of f7963.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMXBp../65479.. ownership of c42e1.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
TMQ8c../3758c.. ownership of 18d0b.. as obj with payaddr PrGxv.. rightscost 0.00 controlledby PrGxv.. upto 0
PUa7P../52d11.. doc published by PrGxv..
Param 0fc90.. : ι → (ι → ι) → ι
Param 4ae4a.. : ι → ι
Param 4a7ef.. : ι
Param If_i : ο → ι → ι → ι
Param e0e40.. : ι → ((ι → ο) → ο) → ι
Param 1216a.. : ι → (ι → ο) → ι
Definition c42e1.. := λ x0 . λ x1 : (ι → ο) → ο . λ x2 : ι → ο . λ x3 . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (e0e40.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (1216a.. x0 x2) x3)))
Param f482f.. : ι → ι → ι
Known 9f6be.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) 4a7ef.. = x0
Theorem 4f989.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ο . ∀ x4 . x0 = c42e1.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 572ce.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . ∀ x3 . x0 = f482f.. (c42e1.. x0 x1 x2 x3) 4a7ef.. (proof)
Param decode_c : ι → (ι → ο) → ο
Known 8a328.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. 4a7ef..) = x1
Known 81500.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . (∀ x3 . x2 x3 ⟶ prim1 x3 x0) ⟶ decode_c (e0e40.. x0 x1) x2 = x1 x2
Theorem 7f14b.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ο . ∀ x4 . x0 = c42e1.. x1 x2 x3 x4 ⟶ ∀ x5 : ι → ο . (∀ x6 . x5 x6 ⟶ prim1 x6 x1) ⟶ x2 x5 = decode_c (f482f.. x0 (4ae4a.. 4a7ef..)) x5 (proof)
Theorem b579b.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . ∀ x3 . ∀ x4 : ι → ο . (∀ x5 . x4 x5 ⟶ prim1 x5 x0) ⟶ x1 x4 = decode_c (f482f.. (c42e1.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 (proof)
Param decode_p : ι → ι → ο
Known 142e6.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. 4a7ef..)) = x2
Known 931fe.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0 ⟶ decode_p (1216a.. x0 x1) x2 = x1 x2
Theorem 5c88b.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ο . ∀ x4 . x0 = c42e1.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x3 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 (proof)
Theorem 559b0.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . ∀ x3 x4 . prim1 x4 x0 ⟶ x2 x4 = decode_p (f482f.. (c42e1.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 (proof)
Known 62a6b.. : ∀ x0 x1 x2 x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) = x3
Theorem 3896b.. : ∀ x0 x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ο . ∀ x4 . x0 = c42e1.. x1 x2 x3 x4 ⟶ x4 = f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Theorem 0821e.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . ∀ x3 . x3 = f482f.. (c42e1.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (proof)
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Known and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem 429e9.. : ∀ x0 x1 . ∀ x2 x3 : (ι → ο) → ο . ∀ x4 x5 : ι → ο . ∀ x6 x7 . c42e1.. x0 x2 x4 x6 = c42e1.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 : ι → ο . (∀ x9 . x8 x9 ⟶ prim1 x9 x0) ⟶ x2 x8 = x3 x8)) (∀ x8 . prim1 x8 x0 ⟶ x4 x8 = x5 x8)) (x6 = x7) (proof)
Param iff : ο → ο → ο
Known ee7ef.. : ∀ x0 . ∀ x1 x2 : ι → ο . (∀ x3 . prim1 x3 x0 ⟶ iff (x1 x3) (x2 x3)) ⟶ 1216a.. x0 x1 = 1216a.. x0 x2
Known fe043.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . (∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3)) ⟶ e0e40.. x0 x1 = e0e40.. x0 x2
Theorem b08f5.. : ∀ x0 . ∀ x1 x2 : (ι → ο) → ο . ∀ x3 x4 : ι → ο . ∀ x5 . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x0) ⟶ iff (x1 x6) (x2 x6)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ iff (x3 x6) (x4 x6)) ⟶ c42e1.. x0 x1 x3 x5 = c42e1.. x0 x2 x4 x5 (proof)
Definition 7f5b4.. := λ x0 . ∀ x1 : ι → ο . (∀ x2 . ∀ x3 : (ι → ο) → ο . ∀ x4 : ι → ο . ∀ x5 . prim1 x5 x2 ⟶ x1 (c42e1.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem c3940.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . ∀ x3 . prim1 x3 x0 ⟶ 7f5b4.. (c42e1.. x0 x1 x2 x3) (proof)
Theorem 22eb2.. : ∀ x0 . ∀ x1 : (ι → ο) → ο . ∀ x2 : ι → ο . ∀ x3 . 7f5b4.. (c42e1.. x0 x1 x2 x3) ⟶ prim1 x3 x0 (proof)
Known iff_refl : ∀ x0 : ο . iff x0 x0
Theorem 58abf.. : ∀ x0 . 7f5b4.. x0 ⟶ x0 = c42e1.. (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (proof)
Definition bbb33.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ο) → ι → ι . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 63f68.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ο) → ι → ι . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ο . ∀ x4 . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (x3 x7) (x6 x7)) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ bbb33.. (c42e1.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 7a422.. := λ x0 . λ x1 : ι → ((ι → ο) → ο) → (ι → ο) → ι → ο . x1 (f482f.. x0 4a7ef..) (decode_c (f482f.. x0 (4ae4a.. 4a7ef..))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))
Theorem 65b34.. : ∀ x0 : ι → ((ι → ο) → ο) → (ι → ο) → ι → ο . ∀ x1 . ∀ x2 : (ι → ο) → ο . ∀ x3 : ι → ο . ∀ x4 . (∀ x5 : (ι → ο) → ο . (∀ x6 : ι → ο . (∀ x7 . x6 x7 ⟶ prim1 x7 x1) ⟶ iff (x2 x6) (x5 x6)) ⟶ ∀ x6 : ι → ο . (∀ x7 . prim1 x7 x1 ⟶ iff (x3 x7) (x6 x7)) ⟶ x0 x1 x5 x6 x4 = x0 x1 x2 x3 x4) ⟶ 7a422.. (c42e1.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Param eb53d.. : ι → CT2 ι
Definition 7c612.. := λ x0 . λ x1 x2 x3 : ι → ι → ι . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (eb53d.. x0 x3))))
Theorem eb96c.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . x0 = 7c612.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 02f73.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . x0 = f482f.. (7c612.. x0 x1 x2 x3) 4a7ef.. (proof)
Param e3162.. : ι → ι → ι → ι
Known 35054.. : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ e3162.. (eb53d.. x0 x1) x2 x3 = x1 x2 x3
Theorem adf33.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . x0 = 7c612.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 72a00.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x4 x5 = e3162.. (f482f.. (7c612.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 320f0.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . x0 = 7c612.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 5e96d.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = e3162.. (f482f.. (7c612.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem e20c4.. : ∀ x0 x1 . ∀ x2 x3 x4 : ι → ι → ι . x0 = 7c612.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Theorem 8be55.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x3 x4 x5 = e3162.. (f482f.. (7c612.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5 (proof)
Theorem 55876.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 x6 x7 : ι → ι → ι . 7c612.. x0 x2 x4 x6 = 7c612.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x6 x8 x9 = x7 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 a5c5d.. : ∀ x0 . ∀ x1 x2 x3 x4 x5 x6 : ι → ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x1 x7 x8 = x2 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x4 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x5 x7 x8 = x6 x7 x8) ⟶ 7c612.. x0 x1 x3 x5 = 7c612.. x0 x2 x4 x6 (proof)
Definition 56cd3.. := λ 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) ⟶ x1 (7c612.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem 8b690.. : ∀ 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) ⟶ 56cd3.. (7c612.. x0 x1 x2 x3) (proof)
Theorem a44f4.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . 56cd3.. (7c612.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x4 x5) x0 (proof)
Theorem 12642.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . 56cd3.. (7c612.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x4 x5) x0 (proof)
Theorem f09cb.. : ∀ x0 . ∀ x1 x2 x3 : ι → ι → ι . 56cd3.. (7c612.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x3 x4 x5) x0 (proof)
Theorem b1359.. : ∀ x0 . 56cd3.. x0 ⟶ x0 = 7c612.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 02be0.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 368fb.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι . ∀ x1 . ∀ x2 x3 x4 : ι → ι → ι . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x4 x8 x9 = x7 x8 x9) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 02be0.. (7c612.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 6a70f.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 668b5.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ο . ∀ x1 . ∀ x2 x3 x4 : ι → ι → ι . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ι . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ x4 x8 x9 = x7 x8 x9) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 6a70f.. (7c612.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition a255b.. := λ x0 . λ x1 x2 : ι → ι → ι . λ x3 : ι → ι . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (0fc90.. x0 x3))))
Theorem c1c1f.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . x0 = a255b.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 6301b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . x0 = f482f.. (a255b.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 89cf7.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . x0 = a255b.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 522c4.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x4 x5 = e3162.. (f482f.. (a255b.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 2da5e.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . x0 = a255b.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 8873d.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = e3162.. (f482f.. (a255b.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0 ⟶ f482f.. (0fc90.. x0 x1) x2 = x1 x2
Theorem 6f41d.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . x0 = a255b.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x4 x5 = f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem e53a5.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . ∀ x4 . prim1 x4 x0 ⟶ x3 x4 = f482f.. (f482f.. (a255b.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Theorem dba9c.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι . a255b.. x0 x2 x4 x6 = a255b.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ x6 x8 = x7 x8) (proof)
Known 4402a.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0fc90.. x0 x1 = 0fc90.. x0 x2
Theorem 378d1.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ι . ∀ x5 x6 : ι → ι . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x1 x7 x8 = x2 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x4 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ x5 x7 = x6 x7) ⟶ a255b.. x0 x1 x3 x5 = a255b.. x0 x2 x4 x6 (proof)
Definition 74f92.. := λ 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) ⟶ x1 (a255b.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem f5883.. : ∀ 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) ⟶ 74f92.. (a255b.. x0 x1 x2 x3) (proof)
Theorem 99505.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . 74f92.. (a255b.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x4 x5) x0 (proof)
Theorem 24dbe.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . 74f92.. (a255b.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x4 x5) x0 (proof)
Theorem c282a.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι . 74f92.. (a255b.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x3 x4) x0 (proof)
Theorem 931eb.. : ∀ x0 . 74f92.. x0 ⟶ x0 = a255b.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 98d5c.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 17fc0.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x4 x8 = x7 x8) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 98d5c.. (a255b.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 824ea.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem cfdca.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι . (∀ x8 . prim1 x8 x1 ⟶ x4 x8 = x7 x8) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 824ea.. (a255b.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Param d2155.. : ι → (ι → ι → ο) → ι
Definition 64302.. := λ x0 . λ x1 x2 : ι → ι → ι . λ x3 : ι → ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (d2155.. x0 x3))))
Theorem 59d0c.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . x0 = 64302.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 3541c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 : ι → ι → ο . x4 x0 (f482f.. (64302.. x0 x1 x2 x3) 4a7ef..) ⟶ x4 (f482f.. (64302.. x0 x1 x2 x3) 4a7ef..) x0 (proof)
Theorem ac959.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . x0 = 64302.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem d5534.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x4 x5 = e3162.. (f482f.. (64302.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 0a008.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . x0 = 64302.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem efc45.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = e3162.. (f482f.. (64302.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 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 93da0.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . x0 = 64302.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x4 x5 x6 = 2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 x6 (proof)
Theorem 4f7a6.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x3 x4 x5 = 2b2e3.. (f482f.. (64302.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x5 (proof)
Theorem a4816.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ι → ο . 64302.. x0 x2 x4 x6 = 64302.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x6 x8 x9 = x7 x8 x9) (proof)
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 db7ec.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ι . ∀ x5 x6 : ι → ι → ο . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x1 x7 x8 = x2 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x4 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ iff (x5 x7 x8) (x6 x7 x8)) ⟶ 64302.. x0 x1 x3 x5 = 64302.. x0 x2 x4 x6 (proof)
Definition 17cf8.. := λ 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 : ι → ι → ο . x1 (64302.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem c4a94.. : ∀ 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 : ι → ι → ο . 17cf8.. (64302.. x0 x1 x2 x3) (proof)
Theorem 32733.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . 17cf8.. (64302.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x4 x5) x0 (proof)
Theorem 24fe3.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ι → ο . 17cf8.. (64302.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x4 x5) x0 (proof)
Theorem 3bcdc.. : ∀ x0 . 17cf8.. x0 ⟶ x0 = 64302.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition b2ca5.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 4d4c5.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x4 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ b2ca5.. (64302.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 851fe.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 8d675.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ι → ο . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ι → ο . (∀ x8 . prim1 x8 x1 ⟶ ∀ x9 . prim1 x9 x1 ⟶ iff (x4 x8 x9) (x7 x8 x9)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 851fe.. (64302.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition 8f64a.. := λ x0 . λ x1 x2 : ι → ι → ι . λ x3 : ι → ο . 0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) (eb53d.. x0 x1) (If_i (x4 = 4ae4a.. (4ae4a.. 4a7ef..)) (eb53d.. x0 x2) (1216a.. x0 x3))))
Theorem 3461b.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ο . x0 = 8f64a.. x1 x2 x3 x4 ⟶ x1 = f482f.. x0 4a7ef.. (proof)
Theorem 0c12c.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ο . x0 = f482f.. (8f64a.. x0 x1 x2 x3) 4a7ef.. (proof)
Theorem 69a7d.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ο . x0 = 8f64a.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x2 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. 4a7ef..)) x5 x6 (proof)
Theorem 7bd1f.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x4 x5 = e3162.. (f482f.. (8f64a.. x0 x1 x2 x3) (4ae4a.. 4a7ef..)) x4 x5 (proof)
Theorem 61558.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ο . x0 = 8f64a.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ ∀ x6 . prim1 x6 x1 ⟶ x3 x5 x6 = e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..))) x5 x6 (proof)
Theorem 4a13b.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = e3162.. (f482f.. (8f64a.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))) x4 x5 (proof)
Theorem 3799b.. : ∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ο . x0 = 8f64a.. x1 x2 x3 x4 ⟶ ∀ x5 . prim1 x5 x1 ⟶ x4 x5 = decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x5 (proof)
Theorem 63e29.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ο . ∀ x4 . prim1 x4 x0 ⟶ x3 x4 = decode_p (f482f.. (8f64a.. x0 x1 x2 x3) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) x4 (proof)
Theorem 61696.. : ∀ x0 x1 . ∀ x2 x3 x4 x5 : ι → ι → ι . ∀ x6 x7 : ι → ο . 8f64a.. x0 x2 x4 x6 = 8f64a.. x1 x3 x5 x7 ⟶ and (and (and (x0 = x1) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x2 x8 x9 = x3 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x8 x9 = x5 x8 x9)) (∀ x8 . prim1 x8 x0 ⟶ x6 x8 = x7 x8) (proof)
Theorem 7e158.. : ∀ x0 . ∀ x1 x2 x3 x4 : ι → ι → ι . ∀ x5 x6 : ι → ο . (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x1 x7 x8 = x2 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x3 x7 x8 = x4 x7 x8) ⟶ (∀ x7 . prim1 x7 x0 ⟶ iff (x5 x7) (x6 x7)) ⟶ 8f64a.. x0 x1 x3 x5 = 8f64a.. x0 x2 x4 x6 (proof)
Definition 0ee11.. := λ 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 : ι → ο . x1 (8f64a.. x2 x3 x4 x5)) ⟶ x1 x0
Theorem 7af5a.. : ∀ 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 : ι → ο . 0ee11.. (8f64a.. x0 x1 x2 x3) (proof)
Theorem 0328a.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ο . 0ee11.. (8f64a.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x1 x4 x5) x0 (proof)
Theorem aabb3.. : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 : ι → ο . 0ee11.. (8f64a.. x0 x1 x2 x3) ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ prim1 (x2 x4 x5) x0 (proof)
Theorem d704c.. : ∀ x0 . 0ee11.. x0 ⟶ x0 = 8f64a.. (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (proof)
Definition 41669.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ο) → ι . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 16ffc.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ο) → ι . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ο . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x4 x8) (x7 x8)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ 41669.. (8f64a.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)
Definition cc976.. := λ x0 . λ x1 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ο) → ο . x1 (f482f.. x0 4a7ef..) (e3162.. (f482f.. x0 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x0 (4ae4a.. (4ae4a.. 4a7ef..)))) (decode_p (f482f.. x0 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))
Theorem 9d144.. : ∀ x0 : ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ο) → ο . ∀ x1 . ∀ x2 x3 : ι → ι → ι . ∀ x4 : ι → ο . (∀ x5 : ι → ι → ι . (∀ x6 . prim1 x6 x1 ⟶ ∀ x7 . prim1 x7 x1 ⟶ x2 x6 x7 = x5 x6 x7) ⟶ ∀ x6 : ι → ι → ι . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ x3 x7 x8 = x6 x7 x8) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x4 x8) (x7 x8)) ⟶ x0 x1 x5 x6 x7 = x0 x1 x2 x3 x4) ⟶ cc976.. (8f64a.. x1 x2 x3 x4) x0 = x0 x1 x2 x3 x4 (proof)