Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrAa9../f429d..
PUdjC../0a482..
vout
PrAa9../26282.. 5.43 bars
TMHCM../07bbb.. ownership of 43f21.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcrt../f169a.. ownership of 86cb7.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMaXG../760f2.. ownership of 5a91e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMUig../5d3f8.. ownership of c1341.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMTHq../b30c5.. ownership of 075c5.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMV9x../212ac.. ownership of cc8b4.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZPm../a6da6.. ownership of ff328.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVmA../d7776.. ownership of 2cb45.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMTWt../7de2e.. ownership of 24a12.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMX5a../1b42e.. ownership of fdad6.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYoU../be0ff.. ownership of 31403.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMXMf../1ece9.. ownership of a1961.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNjM../75a8c.. ownership of 74594.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMc5q../d5a00.. ownership of f2329.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNea../9df16.. ownership of de0dc.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFbR../9b837.. ownership of c8356.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPzg../3ade4.. ownership of 45365.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMQSt../09eaf.. ownership of 1bfd9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMWqr../3f622.. ownership of 7a734.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMXsH../65924.. ownership of d2ba3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMGyh../fdeec.. ownership of 641ca.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TManQ../f4528.. ownership of 6940e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMP3w../136db.. ownership of f7ed5.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNUj../9eeff.. ownership of 63d0a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMREP../a3ab1.. ownership of 503ac.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMaeZ../e7170.. ownership of c375c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMRf../70e3a.. ownership of e6d5e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZHQ../c837c.. ownership of 22806.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZAN../915c1.. ownership of 7be79.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJ4b../844fb.. ownership of d2b48.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMLaw../50d06.. ownership of d7b62.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMKTt../9ad46.. ownership of 32efd.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMLot../444db.. ownership of 30e88.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMGk7../78638.. ownership of 6ecbe.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMXoU../bd6d3.. ownership of afa83.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVLc../2d1a5.. ownership of f2d4e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMH9F../e48cc.. ownership of 1b2e4.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMQFw../0e490.. ownership of 553d3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMie../053f5.. ownership of ab0f3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMU9R../ea5b7.. ownership of 46cea.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYgW../07694.. ownership of c240f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVw6../07c48.. ownership of ec385.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMTr4../3a750.. ownership of a8c31.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMV91../2faec.. ownership of 60d24.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMSas../29a83.. ownership of 6c6f7.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMgS../916e9.. ownership of e1e21.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPkb../d52d1.. ownership of a33b6.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFNt../75506.. ownership of 72b21.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMYD../b0517.. ownership of 8b8a9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHHs../c507a.. ownership of 30d03.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJwW../c058c.. ownership of 96e70.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMUB1../591a4.. ownership of eda78.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMbas../37151.. ownership of 9d4e1.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMRaq../10d42.. ownership of 805f3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVkH../dd50a.. ownership of 1634a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHiC../49668.. ownership of ee225.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHJQ../cdcaa.. ownership of acdf7.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMWnS../939e6.. ownership of 429f8.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMN2B../f0ec7.. ownership of a4275.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMdvj../b3db1.. ownership of 822f9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFGu../375c4.. ownership of c5a67.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHA1../fec76.. ownership of 7c326.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMLbU../f5ad1.. ownership of 34a9f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHnR../44070.. ownership of 7cb4b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJTc../680ab.. ownership of 70471.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMQeM../41afe.. ownership of fa83c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMUd3../36ad8.. ownership of 037b6.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPZh../59a6f.. ownership of efd41.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMaFs../3912d.. ownership of bdad1.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcFd../d1360.. ownership of 32583.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcce../09807.. ownership of 3ba1a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJJz../06663.. ownership of b72da.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMScT../e0b5d.. ownership of 6b961.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPY2../7dd0e.. ownership of ba958.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJzu../f10f8.. ownership of 24435.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMRNW../8472e.. ownership of 1fd42.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVSz../d2f0c.. ownership of ef15c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYZB../dedc8.. ownership of 3bc60.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMbT3../d88e2.. ownership of 06c4f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMQAX../f3a67.. ownership of 7a0a1.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMbaB../40d57.. ownership of ef027.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNf4../389b0.. ownership of f403b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMRfn../e017c.. ownership of 7f9d6.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMLmc../8bbb6.. ownership of 144bc.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMaU8../a7739.. ownership of 65828.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMdjM../38c38.. ownership of a783d.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMKH6../ec106.. ownership of 2987b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TML6u../63e8a.. ownership of 7811e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHV6../3b5f2.. ownership of 7e8a0.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMW89../4a68d.. ownership of fb982.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNAz../a2fbc.. ownership of 99370.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZHo../f806e.. ownership of d924b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMkA../54490.. ownership of 385a8.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMWS4../5b1b7.. ownership of 47512.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFDS../1e59b.. ownership of f7342.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMRmc../c7525.. ownership of 663f2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFqN../2d3b9.. ownership of c50dc.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFYR../c221f.. ownership of ac973.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMHdw../29213.. ownership of 44d11.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVCS../4c68f.. ownership of 09ea0.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVyZ../6c23f.. ownership of 20ea2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFXQ../b64b6.. ownership of 0e721.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPwb../47649.. ownership of 068aa.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMG2k../b77a1.. ownership of afda4.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMGr5../e5361.. ownership of 22e9e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMden../3bb44.. ownership of 15305.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPs1../b1d72.. ownership of 3d6c4.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNA7../1a6c5.. ownership of 154d2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMSBq../b6ed4.. ownership of e214f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPs8../954f4.. ownership of 3c768.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFrK../80721.. ownership of 83656.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZug../76ba9.. ownership of 93136.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZvX../3da32.. ownership of 3eed7.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVwr../28657.. ownership of c6600.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYgZ../63700.. ownership of 128a5.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMYKP../1f682.. ownership of d0e82.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMRz7../cb1ce.. ownership of fc0c5.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMUWX../4b821.. ownership of 657d0.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMUL6../9ef8f.. ownership of 67024.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMRzg../c2919.. ownership of db57e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMX2C../c8735.. ownership of 6831b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVKq../39ea5.. ownership of ba42d.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMU1z../40d69.. ownership of bbdc7.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMdPi../6564f.. ownership of 483ab.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMWnC../39698.. ownership of cebfe.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMViF../cdc2a.. ownership of 647ec.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPym../e730d.. ownership of d1d81.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMdgJ../71dc6.. ownership of fdf58.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMJJ3../7dd09.. ownership of 1d55a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMFrE../e203e.. ownership of 33e66.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMU1j../f6dfb.. ownership of 8454f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMKJS../42091.. ownership of b83dd.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMbjn../f01aa.. ownership of 3841c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMcjD../19f66.. ownership of 50a25.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMdh5../3361a.. ownership of 2555f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMXQn../d5466.. ownership of f54c0.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMbpN../bfb85.. ownership of 1fe00.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMd3i../c96bd.. ownership of a06f9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMKJ3../35c21.. ownership of 6c866.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMY7j../94ba7.. ownership of e749b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMPYU../7ec48.. ownership of de9e9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMda3../5d38d.. ownership of 4b8d1.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMSZG../81c76.. ownership of 2fffd.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMZ5j../67c26.. ownership of 96890.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNXG../fdd51.. ownership of 6ee59.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMM9Z../b4b26.. ownership of b7b29.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVk9../76fc5.. ownership of a4026.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMNSy../dfe93.. ownership of bfc1c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMK91../beda2.. ownership of bc000.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMVrn../b3d2a.. ownership of 55de5.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMMZD../a244d.. ownership of 81c99.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMV97../9de59.. ownership of f8cd2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMUix../57df6.. ownership of 547c4.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
TMbxo../85ae0.. ownership of 39e81.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0
PUdSf../52e41.. doc published by Pr5Zc..
Theorem 547c4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x2 (x1 x3 (x1 x4 x5)) x6 = x1 (x2 x3 x6) (x1 (x2 x4 x6) (x2 x5 x6)) (proof)
Known e11b7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x2 (x1 x3 x4))
Theorem 81c99.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) x7 = x1 (x2 x3 x7) (x1 (x2 x4 x7) (x1 (x2 x5 x7) (x2 x6 x7))) (proof)
Known 25618.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 x5)))
Theorem bc000.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) x8 = x1 (x2 x3 x8) (x1 (x2 x4 x8) (x1 (x2 x5 x8) (x1 (x2 x6 x8) (x2 x7 x8)))) (proof)
Known b9f0e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 x6))))
Theorem a4026.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) x9 = x1 (x2 x3 x9) (x1 (x2 x4 x9) (x1 (x2 x5 x9) (x1 (x2 x6 x9) (x1 (x2 x7 x9) (x2 x8 x9))))) (proof)
Known 2a50e.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))))
Theorem 6ee59.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) x10 = x1 (x2 x3 x10) (x1 (x2 x4 x10) (x1 (x2 x5 x10) (x1 (x2 x6 x10) (x1 (x2 x7 x10) (x1 (x2 x8 x10) (x2 x9 x10)))))) (proof)
Known 948ae.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))))
Theorem 2fffd.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) x11 = x1 (x2 x3 x11) (x1 (x2 x4 x11) (x1 (x2 x5 x11) (x1 (x2 x6 x11) (x1 (x2 x7 x11) (x1 (x2 x8 x11) (x1 (x2 x9 x11) (x2 x10 x11))))))) (proof)
Known 18faf.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))))
Theorem de9e9.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))) x12 = x1 (x2 x3 x12) (x1 (x2 x4 x12) (x1 (x2 x5 x12) (x1 (x2 x6 x12) (x1 (x2 x7 x12) (x1 (x2 x8 x12) (x1 (x2 x9 x12) (x1 (x2 x10 x12) (x2 x11 x12)))))))) (proof)
Known 880a1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))))
Theorem 6c866.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))) x13 = x1 (x2 x3 x13) (x1 (x2 x4 x13) (x1 (x2 x5 x13) (x1 (x2 x6 x13) (x1 (x2 x7 x13) (x1 (x2 x8 x13) (x1 (x2 x9 x13) (x1 (x2 x10 x13) (x1 (x2 x11 x13) (x2 x12 x13))))))))) (proof)
Known 737fb.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))))
Theorem 1fe00.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))) x14 = x1 (x2 x3 x14) (x1 (x2 x4 x14) (x1 (x2 x5 x14) (x1 (x2 x6 x14) (x1 (x2 x7 x14) (x1 (x2 x8 x14) (x1 (x2 x9 x14) (x1 (x2 x10 x14) (x1 (x2 x11 x14) (x1 (x2 x12 x14) (x2 x13 x14)))))))))) (proof)
Known f7821.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))))
Theorem 2555f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) x15 = x1 (x2 x3 x15) (x1 (x2 x4 x15) (x1 (x2 x5 x15) (x1 (x2 x6 x15) (x1 (x2 x7 x15) (x1 (x2 x8 x15) (x1 (x2 x9 x15) (x1 (x2 x10 x15) (x1 (x2 x11 x15) (x1 (x2 x12 x15) (x1 (x2 x13 x15) (x2 x14 x15))))))))))) (proof)
Known 2c5ad.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))))
Theorem 3841c.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))) x16 = x1 (x2 x3 x16) (x1 (x2 x4 x16) (x1 (x2 x5 x16) (x1 (x2 x6 x16) (x1 (x2 x7 x16) (x1 (x2 x8 x16) (x1 (x2 x9 x16) (x1 (x2 x10 x16) (x1 (x2 x11 x16) (x1 (x2 x12 x16) (x1 (x2 x13 x16) (x1 (x2 x14 x16) (x2 x15 x16)))))))))))) (proof)
Known ea7b1.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))))
Theorem 8454f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))) x17 = x1 (x2 x3 x17) (x1 (x2 x4 x17) (x1 (x2 x5 x17) (x1 (x2 x6 x17) (x1 (x2 x7 x17) (x1 (x2 x8 x17) (x1 (x2 x9 x17) (x1 (x2 x10 x17) (x1 (x2 x11 x17) (x1 (x2 x12 x17) (x1 (x2 x13 x17) (x1 (x2 x14 x17) (x1 (x2 x15 x17) (x2 x16 x17))))))))))))) (proof)
Known 6cd80.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))))
Theorem 1d55a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))))))))))) x18 = x1 (x2 x3 x18) (x1 (x2 x4 x18) (x1 (x2 x5 x18) (x1 (x2 x6 x18) (x1 (x2 x7 x18) (x1 (x2 x8 x18) (x1 (x2 x9 x18) (x1 (x2 x10 x18) (x1 (x2 x11 x18) (x1 (x2 x12 x18) (x1 (x2 x13 x18) (x1 (x2 x14 x18) (x1 (x2 x15 x18) (x1 (x2 x16 x18) (x2 x17 x18)))))))))))))) (proof)
Known 855a7.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι → ι . (∀ x2 x3 . x0 x2 ⟶ x0 x3 ⟶ x0 (x1 x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x2 ⟶ x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 (x1 x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))))
Theorem d1d81.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x0 x19 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))))))))))) x19 = x1 (x2 x3 x19) (x1 (x2 x4 x19) (x1 (x2 x5 x19) (x1 (x2 x6 x19) (x1 (x2 x7 x19) (x1 (x2 x8 x19) (x1 (x2 x9 x19) (x1 (x2 x10 x19) (x1 (x2 x11 x19) (x1 (x2 x12 x19) (x1 (x2 x13 x19) (x1 (x2 x14 x19) (x1 (x2 x15 x19) (x1 (x2 x16 x19) (x1 (x2 x17 x19) (x2 x18 x19))))))))))))))) (proof)
Theorem cebfe.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x2 x6 (x1 x3 (x1 x4 x5)) = x1 (x2 x6 x3) (x1 (x2 x6 x4) (x2 x6 x5)) (proof)
Theorem bbdc7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 x7 (x1 x3 (x1 x4 (x1 x5 x6))) = x1 (x2 x7 x3) (x1 (x2 x7 x4) (x1 (x2 x7 x5) (x2 x7 x6))) (proof)
Theorem 6831b.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 x8 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) = x1 (x2 x8 x3) (x1 (x2 x8 x4) (x1 (x2 x8 x5) (x1 (x2 x8 x6) (x2 x8 x7)))) (proof)
Theorem 67024.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 x9 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) = x1 (x2 x9 x3) (x1 (x2 x9 x4) (x1 (x2 x9 x5) (x1 (x2 x9 x6) (x1 (x2 x9 x7) (x2 x9 x8))))) (proof)
Theorem fc0c5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 x10 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) = x1 (x2 x10 x3) (x1 (x2 x10 x4) (x1 (x2 x10 x5) (x1 (x2 x10 x6) (x1 (x2 x10 x7) (x1 (x2 x10 x8) (x2 x10 x9)))))) (proof)
Theorem 128a5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 x11 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) = x1 (x2 x11 x3) (x1 (x2 x11 x4) (x1 (x2 x11 x5) (x1 (x2 x11 x6) (x1 (x2 x11 x7) (x1 (x2 x11 x8) (x1 (x2 x11 x9) (x2 x11 x10))))))) (proof)
Theorem 3eed7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 x12 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))))) = x1 (x2 x12 x3) (x1 (x2 x12 x4) (x1 (x2 x12 x5) (x1 (x2 x12 x6) (x1 (x2 x12 x7) (x1 (x2 x12 x8) (x1 (x2 x12 x9) (x1 (x2 x12 x10) (x2 x12 x11)))))))) (proof)
Theorem 83656.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 x13 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))))) = x1 (x2 x13 x3) (x1 (x2 x13 x4) (x1 (x2 x13 x5) (x1 (x2 x13 x6) (x1 (x2 x13 x7) (x1 (x2 x13 x8) (x1 (x2 x13 x9) (x1 (x2 x13 x10) (x1 (x2 x13 x11) (x2 x13 x12))))))))) (proof)
Theorem e214f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 x14 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))))))) = x1 (x2 x14 x3) (x1 (x2 x14 x4) (x1 (x2 x14 x5) (x1 (x2 x14 x6) (x1 (x2 x14 x7) (x1 (x2 x14 x8) (x1 (x2 x14 x9) (x1 (x2 x14 x10) (x1 (x2 x14 x11) (x1 (x2 x14 x12) (x2 x14 x13)))))))))) (proof)
Theorem 3d6c4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 x15 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))))))) = x1 (x2 x15 x3) (x1 (x2 x15 x4) (x1 (x2 x15 x5) (x1 (x2 x15 x6) (x1 (x2 x15 x7) (x1 (x2 x15 x8) (x1 (x2 x15 x9) (x1 (x2 x15 x10) (x1 (x2 x15 x11) (x1 (x2 x15 x12) (x1 (x2 x15 x13) (x2 x15 x14))))))))))) (proof)
Theorem 22e9e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 x16 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))))))))) = x1 (x2 x16 x3) (x1 (x2 x16 x4) (x1 (x2 x16 x5) (x1 (x2 x16 x6) (x1 (x2 x16 x7) (x1 (x2 x16 x8) (x1 (x2 x16 x9) (x1 (x2 x16 x10) (x1 (x2 x16 x11) (x1 (x2 x16 x12) (x1 (x2 x16 x13) (x1 (x2 x16 x14) (x2 x16 x15)))))))))))) (proof)
Theorem 068aa.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 x17 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))))))))) = x1 (x2 x17 x3) (x1 (x2 x17 x4) (x1 (x2 x17 x5) (x1 (x2 x17 x6) (x1 (x2 x17 x7) (x1 (x2 x17 x8) (x1 (x2 x17 x9) (x1 (x2 x17 x10) (x1 (x2 x17 x11) (x1 (x2 x17 x12) (x1 (x2 x17 x13) (x1 (x2 x17 x14) (x1 (x2 x17 x15) (x2 x17 x16))))))))))))) (proof)
Theorem 20ea2.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x2 x18 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))))))))))) = x1 (x2 x18 x3) (x1 (x2 x18 x4) (x1 (x2 x18 x5) (x1 (x2 x18 x6) (x1 (x2 x18 x7) (x1 (x2 x18 x8) (x1 (x2 x18 x9) (x1 (x2 x18 x10) (x1 (x2 x18 x11) (x1 (x2 x18 x12) (x1 (x2 x18 x13) (x1 (x2 x18 x14) (x1 (x2 x18 x15) (x1 (x2 x18 x16) (x2 x18 x17)))))))))))))) (proof)
Theorem 44d11.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x0 x19 ⟶ x2 x19 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))))))))))) = x1 (x2 x19 x3) (x1 (x2 x19 x4) (x1 (x2 x19 x5) (x1 (x2 x19 x6) (x1 (x2 x19 x7) (x1 (x2 x19 x8) (x1 (x2 x19 x9) (x1 (x2 x19 x10) (x1 (x2 x19 x11) (x1 (x2 x19 x12) (x1 (x2 x19 x13) (x1 (x2 x19 x14) (x1 (x2 x19 x15) (x1 (x2 x19 x16) (x1 (x2 x19 x17) (x2 x19 x18))))))))))))))) (proof)
Theorem c50dc.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x2 (x1 x3 x4) (x1 x5 x6) = x1 (x1 (x2 x3 x5) (x2 x3 x6)) (x1 (x2 x4 x5) (x2 x4 x6)) (proof)
Theorem f7342.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 x7)) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x2 x3 x7))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x2 x4 x7))) (proof)
Theorem 385a8.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 x8))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x2 x3 x8)))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x2 x4 x8)))) (proof)
Theorem 99370.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9))))) (proof)
Theorem 7e8a0.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10)))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10)))))) (proof)
Theorem 2987b.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))))))) (proof)
Theorem 65828.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 x4) (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))))) = x1 (x1 (x2 x3 x5) (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))))))) (x1 (x2 x4 x5) (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))))))) (proof)
Theorem 7f9d6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 x7) = x1 (x1 (x2 x3 x6) (x2 x3 x7)) (x1 (x1 (x2 x4 x6) (x2 x4 x7)) (x1 (x2 x5 x6) (x2 x5 x7))) (proof)
Theorem ef027.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 x8)) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x2 x3 x8))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x2 x4 x8))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x2 x5 x8)))) (proof)
Theorem 06c4f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 x9))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9)))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9)))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x2 x5 x9))))) (proof)
Theorem ef15c.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10)))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10)))))) (proof)
Theorem 24435.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11)))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11)))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))))))) (proof)
Theorem 6b961.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12)))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))))))) (proof)
Theorem 3ba1a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 x5)) (x1 x6 (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13))))))) = x1 (x1 (x2 x3 x6) (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))))))) (x1 (x1 (x2 x4 x6) (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))))))) (x1 (x2 x5 x6) (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))))))) (proof)
Theorem bdad1.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 x8) = x1 (x1 (x2 x3 x7) (x2 x3 x8)) (x1 (x1 (x2 x4 x7) (x2 x4 x8)) (x1 (x1 (x2 x5 x7) (x2 x5 x8)) (x1 (x2 x6 x7) (x2 x6 x8)))) (proof)
Theorem 037b6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 x9)) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x2 x3 x9))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x2 x4 x9))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x2 x5 x9))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x2 x6 x9))))) (proof)
Theorem 70471.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 x10))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10)))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10)))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10)))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x2 x6 x10)))))) (proof)
Theorem 34a9f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 x11)))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11))))))) (proof)
Theorem c5a67.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12)))))))) (proof)
Theorem a4275.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))))))))) (proof)
Theorem acdf7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 x6))) (x1 x7 (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))))) = x1 (x1 (x2 x3 x7) (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))))))) (x1 (x1 (x2 x4 x7) (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))))))) (x1 (x1 (x2 x5 x7) (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))))))) (x1 (x2 x6 x7) (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))))))))) (proof)
Theorem 1634a.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 x9) = x1 (x1 (x2 x3 x8) (x2 x3 x9)) (x1 (x1 (x2 x4 x8) (x2 x4 x9)) (x1 (x1 (x2 x5 x8) (x2 x5 x9)) (x1 (x1 (x2 x6 x8) (x2 x6 x9)) (x1 (x2 x7 x8) (x2 x7 x9))))) (proof)
Theorem 9d4e1.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 x10)) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x2 x3 x10))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x2 x4 x10))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x2 x5 x10))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x2 x6 x10))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x2 x7 x10)))))) (proof)
Theorem 96e70.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 x11))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11)))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11)))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11)))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11)))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x2 x7 x11))))))) (proof)
Theorem 8b8a9.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 x12)))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12)))))))) (proof)
Theorem a33b6.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13)))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13)))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))))))))) (proof)
Theorem 6c6f7.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14)))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14))))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14))))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14))))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14))))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))))))))) (proof)
Theorem a8c31.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 x7)))) (x1 x8 (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15))))))) = x1 (x1 (x2 x3 x8) (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15)))))))) (x1 (x1 (x2 x4 x8) (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15)))))))) (x1 (x1 (x2 x5 x8) (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15)))))))) (x1 (x1 (x2 x6 x8) (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15)))))))) (x1 (x2 x7 x8) (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))))))))) (proof)
Theorem c240f.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 x10) = x1 (x1 (x2 x3 x9) (x2 x3 x10)) (x1 (x1 (x2 x4 x9) (x2 x4 x10)) (x1 (x1 (x2 x5 x9) (x2 x5 x10)) (x1 (x1 (x2 x6 x9) (x2 x6 x10)) (x1 (x1 (x2 x7 x9) (x2 x7 x10)) (x1 (x2 x8 x9) (x2 x8 x10)))))) (proof)
Theorem ab0f3.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 x11)) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x2 x3 x11))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x2 x4 x11))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x2 x5 x11))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x2 x6 x11))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x2 x7 x11))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x2 x8 x11))))))) (proof)
Theorem 1b2e4.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 x12))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12)))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12)))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12)))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12)))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12)))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x2 x8 x12)))))))) (proof)
Theorem afa83.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 x13)))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13))))))))) (proof)
Theorem 30e88.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14)))))))))) (proof)
Theorem d7b62.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15))))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15))))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15))))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15))))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15))))))))))) (proof)
Theorem 7be79.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 x8))))) (x1 x9 (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))))) = x1 (x1 (x2 x3 x9) (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16)))))))) (x1 (x1 (x2 x4 x9) (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16)))))))) (x1 (x1 (x2 x5 x9) (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16)))))))) (x1 (x1 (x2 x6 x9) (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16)))))))) (x1 (x1 (x2 x7 x9) (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16)))))))) (x1 (x2 x8 x9) (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16)))))))))))) (proof)
Theorem e6d5e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 x11) = x1 (x1 (x2 x3 x10) (x2 x3 x11)) (x1 (x1 (x2 x4 x10) (x2 x4 x11)) (x1 (x1 (x2 x5 x10) (x2 x5 x11)) (x1 (x1 (x2 x6 x10) (x2 x6 x11)) (x1 (x1 (x2 x7 x10) (x2 x7 x11)) (x1 (x1 (x2 x8 x10) (x2 x8 x11)) (x1 (x2 x9 x10) (x2 x9 x11))))))) (proof)
Theorem 503ac.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 x12)) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x2 x3 x12))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x2 x4 x12))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x2 x5 x12))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x2 x6 x12))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x2 x7 x12))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x2 x8 x12))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x2 x9 x12)))))))) (proof)
Theorem f7ed5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 x13))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13)))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13)))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13)))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13)))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13)))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13)))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x2 x9 x13))))))))) (proof)
Theorem 641ca.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 x14)))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x2 x9 x14)))))))))) (proof)
Theorem 7a734.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15)))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15)))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15)))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15)))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15)))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15)))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x2 x9 x15))))))))))) (proof)
Theorem 45365.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16)))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16))))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16))))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16))))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16))))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16))))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16))))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x2 x9 x16)))))))))))) (proof)
Theorem de0dc.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 x9)))))) (x1 x10 (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17))))))) = x1 (x1 (x2 x3 x10) (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x2 x3 x17)))))))) (x1 (x1 (x2 x4 x10) (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x2 x4 x17)))))))) (x1 (x1 (x2 x5 x10) (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x2 x5 x17)))))))) (x1 (x1 (x2 x6 x10) (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x2 x6 x17)))))))) (x1 (x1 (x2 x7 x10) (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x2 x7 x17)))))))) (x1 (x1 (x2 x8 x10) (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x2 x8 x17)))))))) (x1 (x2 x9 x10) (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x2 x9 x17))))))))))))) (proof)
Theorem 74594.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 x12) = x1 (x1 (x2 x3 x11) (x2 x3 x12)) (x1 (x1 (x2 x4 x11) (x2 x4 x12)) (x1 (x1 (x2 x5 x11) (x2 x5 x12)) (x1 (x1 (x2 x6 x11) (x2 x6 x12)) (x1 (x1 (x2 x7 x11) (x2 x7 x12)) (x1 (x1 (x2 x8 x11) (x2 x8 x12)) (x1 (x1 (x2 x9 x11) (x2 x9 x12)) (x1 (x2 x10 x11) (x2 x10 x12)))))))) (proof)
Theorem 31403.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 x13)) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x2 x3 x13))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x2 x4 x13))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x2 x5 x13))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x2 x6 x13))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x2 x7 x13))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x2 x8 x13))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x2 x9 x13))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x2 x10 x13))))))))) (proof)
Theorem 24a12.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 x14))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x2 x3 x14)))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x2 x4 x14)))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x2 x5 x14)))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x2 x6 x14)))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x2 x7 x14)))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x2 x8 x14)))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x2 x9 x14)))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x2 x10 x14)))))))))) (proof)
Theorem ff328.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 x15)))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x2 x3 x15))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x2 x4 x15))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x2 x5 x15))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x2 x6 x15))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x2 x7 x15))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x2 x8 x15))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x2 x9 x15))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x2 x10 x15))))))))))) (proof)
Theorem 075c5.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 x16))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x2 x3 x16)))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x2 x4 x16)))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x2 x5 x16)))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x2 x6 x16)))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x2 x7 x16)))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x2 x8 x16)))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x2 x9 x16)))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x2 x10 x16)))))))))))) (proof)
Theorem 5a91e.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 x17)))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x2 x3 x17))))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x2 x4 x17))))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x2 x5 x17))))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x2 x6 x17))))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x2 x7 x17))))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x2 x8 x17))))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x2 x9 x17))))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x1 (x2 x10 x16) (x2 x10 x17))))))))))))) (proof)
Theorem 43f21.. : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ι . (∀ x3 x4 . x0 x3 ⟶ x0 x4 ⟶ x0 (x1 x3 x4)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 x3 (x1 x4 x5) = x1 (x2 x3 x4) (x2 x3 x5)) ⟶ (∀ x3 x4 x5 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x2 (x1 x3 x4) x5 = x1 (x2 x3 x5) (x2 x4 x5)) ⟶ ∀ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 . x0 x3 ⟶ x0 x4 ⟶ x0 x5 ⟶ x0 x6 ⟶ x0 x7 ⟶ x0 x8 ⟶ x0 x9 ⟶ x0 x10 ⟶ x0 x11 ⟶ x0 x12 ⟶ x0 x13 ⟶ x0 x14 ⟶ x0 x15 ⟶ x0 x16 ⟶ x0 x17 ⟶ x0 x18 ⟶ x2 (x1 x3 (x1 x4 (x1 x5 (x1 x6 (x1 x7 (x1 x8 (x1 x9 x10))))))) (x1 x11 (x1 x12 (x1 x13 (x1 x14 (x1 x15 (x1 x16 (x1 x17 x18))))))) = x1 (x1 (x2 x3 x11) (x1 (x2 x3 x12) (x1 (x2 x3 x13) (x1 (x2 x3 x14) (x1 (x2 x3 x15) (x1 (x2 x3 x16) (x1 (x2 x3 x17) (x2 x3 x18)))))))) (x1 (x1 (x2 x4 x11) (x1 (x2 x4 x12) (x1 (x2 x4 x13) (x1 (x2 x4 x14) (x1 (x2 x4 x15) (x1 (x2 x4 x16) (x1 (x2 x4 x17) (x2 x4 x18)))))))) (x1 (x1 (x2 x5 x11) (x1 (x2 x5 x12) (x1 (x2 x5 x13) (x1 (x2 x5 x14) (x1 (x2 x5 x15) (x1 (x2 x5 x16) (x1 (x2 x5 x17) (x2 x5 x18)))))))) (x1 (x1 (x2 x6 x11) (x1 (x2 x6 x12) (x1 (x2 x6 x13) (x1 (x2 x6 x14) (x1 (x2 x6 x15) (x1 (x2 x6 x16) (x1 (x2 x6 x17) (x2 x6 x18)))))))) (x1 (x1 (x2 x7 x11) (x1 (x2 x7 x12) (x1 (x2 x7 x13) (x1 (x2 x7 x14) (x1 (x2 x7 x15) (x1 (x2 x7 x16) (x1 (x2 x7 x17) (x2 x7 x18)))))))) (x1 (x1 (x2 x8 x11) (x1 (x2 x8 x12) (x1 (x2 x8 x13) (x1 (x2 x8 x14) (x1 (x2 x8 x15) (x1 (x2 x8 x16) (x1 (x2 x8 x17) (x2 x8 x18)))))))) (x1 (x1 (x2 x9 x11) (x1 (x2 x9 x12) (x1 (x2 x9 x13) (x1 (x2 x9 x14) (x1 (x2 x9 x15) (x1 (x2 x9 x16) (x1 (x2 x9 x17) (x2 x9 x18)))))))) (x1 (x2 x10 x11) (x1 (x2 x10 x12) (x1 (x2 x10 x13) (x1 (x2 x10 x14) (x1 (x2 x10 x15) (x1 (x2 x10 x16) (x1 (x2 x10 x17) (x2 x10 x18)))))))))))))) (proof)