| vout |
|---|
PrFKo../0e209.. 375.00 barsTMRRm../2e611.. ownership of 76a14.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMJmP../8cfdf.. ownership of d2baa.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMH1g../e30b2.. ownership of 9a7a2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMNdk../515c0.. ownership of debf9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMPWw../eedcb.. ownership of 27d68.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMaGp../108cd.. ownership of fbde3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMb1U../d84b3.. ownership of 97776.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMNgq../b72a5.. ownership of 4a640.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMKeu../0d853.. ownership of 11d87.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMSMY../c3cb1.. ownership of b2851.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMXzQ../253f1.. ownership of 41b33.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMVUL../cacf4.. ownership of 71fd4.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMNBL../182e7.. ownership of 3c98f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMZ7W../ee769.. ownership of 2bb7e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMcyu../356e7.. ownership of 9b301.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMZK6../a948f.. ownership of 5ea5e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMFbB../d9a35.. ownership of a2d04.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMMaL../a4662.. ownership of 21c06.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMRA2../c75f2.. ownership of b1aaf.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMKNy../e55da.. ownership of 46d31.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMGkf../16a48.. ownership of 8e732.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMQd7../2f154.. ownership of 20e3d.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMPF8../3aac5.. ownership of 53a15.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMMRW../5f30e.. ownership of 0521d.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMNJh../8ffa2.. ownership of 7d7de.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMV75../f3940.. ownership of 26c80.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMZJC../59a58.. ownership of 16021.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMMpN../5f169.. ownership of 83a89.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMSjb../5a629.. ownership of 2e61c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMNDV../801bc.. ownership of 881ed.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMMrS../630b0.. ownership of 3b9d7.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMUGV../c2048.. ownership of f4261.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMcRR../8f141.. ownership of da964.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMSGR../d0819.. ownership of c48c2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMWbp../eb8ac.. ownership of 596bd.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMF9m../416d9.. ownership of 86856.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMUVS../818dc.. ownership of f7a78.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMN7m../fabae.. ownership of 1ffc9.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMXSj../abb7e.. ownership of b6264.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMN7y../d571c.. ownership of 49730.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMbxo../e9ad0.. ownership of 4723f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMQ2c../d773f.. ownership of 216c2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMb7N../0c873.. ownership of 6deab.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMQJe../59553.. ownership of b1aab.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMJYG../78367.. ownership of 8811b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMKtE../b0dd9.. ownership of a7053.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMUZq../59a3a.. ownership of 843a6.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMQ1d../e2285.. ownership of 8971d.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMYRs../e3f43.. ownership of 114a2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMGxv../eac48.. ownership of ee7da.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMZij../e5b16.. ownership of 36187.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMKty../a37b5.. ownership of b8e8c.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMZ7v../da1bf.. ownership of a1479.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMX9s../83394.. ownership of 89fd8.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMGo4../4a44b.. ownership of 45c54.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMPNd../8f44a.. ownership of 369fd.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMUSu../19321.. ownership of b4c6e.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMVyK../ce24f.. ownership of 393bb.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMZJv../ed52d.. ownership of 92d58.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMQQ5../ec4de.. ownership of 2bdb4.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMLdD../a4bb5.. ownership of 573cc.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMTdm../f27fc.. ownership of 7c73a.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMM6H../b8077.. ownership of ef9bb.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMMtq../ffe4d.. ownership of 4c737.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMTBa../efbf9.. ownership of 69433.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMRzK../86d41.. ownership of 08626.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMW7T../cf341.. ownership of 554db.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMbai../d8bc3.. ownership of 88502.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMXsX../61175.. ownership of f2d8f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMT2h../54d1b.. ownership of a9fbb.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMGgo../df47d.. ownership of 0e17d.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMJqM../c2881.. ownership of f3ee2.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMa7Z../ae71a.. ownership of b99b8.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMY1i../85f3b.. ownership of 6998f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMSGc../ae712.. ownership of 10d52.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMHMT../176df.. ownership of f9dac.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMJaC../f86d2.. ownership of 2948f.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMZQr../a2897.. ownership of 9df00.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMSJH../e15fb.. ownership of 31050.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMa1i../5bcd0.. ownership of f50d3.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMVGT../a92f0.. ownership of 7d951.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMEqz../98049.. ownership of ab418.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMGLE../b0428.. ownership of b56a1.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMMun../34ce1.. ownership of 726ef.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMF9a../2497d.. ownership of 0c348.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0TMGNW../299e4.. ownership of dd12b.. as prop with payaddr Pr5Zc.. rights free controlledby Pr5Zc.. upto 0PUS1o../2d9c3.. doc published by Pr5Zc..Theorem 0c348.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x0 (x3 (x2 x4)) (proof)Theorem b56a1.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ ∀ x5 . x0 x5 ⟶ x0 (x4 (x3 (x2 x5))) (proof)Theorem 7d951.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ ∀ x6 . x0 x6 ⟶ x0 (x5 (x4 (x3 (x2 x6)))) (proof)Theorem 31050.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ ∀ x7 . x0 x7 ⟶ x0 (x6 (x5 (x4 (x3 (x2 x7))))) (proof)Theorem 2948f.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ ∀ x8 . x0 x8 ⟶ x0 (x7 (x6 (x5 (x4 (x3 (x2 x8)))))) (proof)Theorem 10d52.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ ∀ x9 . x0 x9 ⟶ x0 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x9))))))) (proof)Theorem b99b8.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ ∀ x10 . x0 x10 ⟶ x0 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x10)))))))) (proof)Theorem 0e17d.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ ∀ x11 . x0 x11 ⟶ x0 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x11))))))))) (proof)Theorem f2d8f.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ x1 x11 ⟶ ∀ x12 . x0 x12 ⟶ x0 (x11 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x12)))))))))) (proof)Theorem 554db.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ x1 x11 ⟶ x1 x12 ⟶ ∀ x13 . x0 x13 ⟶ x0 (x12 (x11 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x13))))))))))) (proof)Theorem 69433.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : ι → ι . 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 . x0 x14 ⟶ x0 (x13 (x12 (x11 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x14)))))))))))) (proof)Theorem ef9bb.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : ι → ι . 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 . x0 x15 ⟶ x0 (x14 (x13 (x12 (x11 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x15))))))))))))) (proof)Theorem 573cc.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 : ι → ι . 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 . x0 x16 ⟶ x0 (x15 (x14 (x13 (x12 (x11 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x16)))))))))))))) (proof)Theorem 92d58.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 : ι → ι . 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 ⟶ x1 x16 ⟶ ∀ x17 . x0 x17 ⟶ x0 (x16 (x15 (x14 (x13 (x12 (x11 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x17))))))))))))))) (proof)Theorem b4c6e.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : ι → ι . 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 ⟶ x1 x16 ⟶ x1 x17 ⟶ ∀ x18 . x0 x18 ⟶ x0 (x17 (x16 (x15 (x14 (x13 (x12 (x11 (x10 (x9 (x8 (x7 (x6 (x5 (x4 (x3 (x2 x18)))))))))))))))) (proof)Theorem 45c54.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ ∀ x5 . x0 x5 ⟶ x2 (x3 (x4 x5)) = x3 (x2 (x4 x5)) (proof)Theorem a1479.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ ∀ x6 . x0 x6 ⟶ x2 (x3 (x4 (x5 x6))) = x3 (x2 (x4 (x5 x6))) (proof)Theorem 36187.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ ∀ x7 . x0 x7 ⟶ x2 (x3 (x4 (x5 (x6 x7)))) = x3 (x2 (x4 (x5 (x6 x7)))) (proof)Theorem 114a2.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ ∀ x8 . x0 x8 ⟶ x2 (x3 (x4 (x5 (x6 (x7 x8))))) = x3 (x2 (x4 (x5 (x6 (x7 x8))))) (proof)Theorem 843a6.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ ∀ x9 . x0 x9 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 x9)))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 x9)))))) (proof)Theorem 8811b.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ ∀ x10 . x0 x10 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 x10))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 x10))))))) (proof)Theorem 6deab.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ ∀ x11 . x0 x11 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 x11)))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 x11)))))))) (proof)Theorem 4723f.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ x1 x11 ⟶ ∀ x12 . x0 x12 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 x12))))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 x12))))))))) (proof)Theorem b6264.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ x1 x11 ⟶ x1 x12 ⟶ ∀ x13 . x0 x13 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 x13)))))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 x13)))))))))) (proof)Theorem f7a78.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : ι → ι . 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 . x0 x14 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 x14))))))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 x14))))))))))) (proof)Theorem 596bd.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : ι → ι . 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 . x0 x15 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 x15)))))))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 x15)))))))))))) (proof)Theorem da964.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 : ι → ι . 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 . x0 x16 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 x16))))))))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 x16))))))))))))) (proof)Theorem 3b9d7.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 : ι → ι . 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 ⟶ x1 x16 ⟶ ∀ x17 . x0 x17 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 (x16 x17)))))))))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 (x16 x17)))))))))))))) (proof)Theorem 2e61c.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : ι → ι . 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 ⟶ x1 x16 ⟶ x1 x17 ⟶ ∀ x18 . x0 x18 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 (x16 (x17 x18))))))))))))))) = x3 (x2 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 (x16 (x17 x18))))))))))))))) (proof)Theorem 16021.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ ∀ x5 . x0 x5 ⟶ x2 (x3 (x4 x5)) = x4 (x2 (x3 x5)) (proof)Theorem 7d7de.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ ∀ x6 . x0 x6 ⟶ x2 (x3 (x4 (x5 x6))) = x5 (x2 (x3 (x4 x6))) (proof)Theorem 53a15.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ ∀ x7 . x0 x7 ⟶ x2 (x3 (x4 (x5 (x6 x7)))) = x6 (x2 (x3 (x4 (x5 x7)))) (proof)Theorem 8e732.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ ∀ x8 . x0 x8 ⟶ x2 (x3 (x4 (x5 (x6 (x7 x8))))) = x7 (x2 (x3 (x4 (x5 (x6 x8))))) (proof)Theorem b1aaf.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ ∀ x9 . x0 x9 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 x9)))))) = x8 (x2 (x3 (x4 (x5 (x6 (x7 x9)))))) (proof)Theorem a2d04.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ ∀ x10 . x0 x10 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 x10))))))) = x9 (x2 (x3 (x4 (x5 (x6 (x7 (x8 x10))))))) (proof)Theorem 9b301.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ ∀ x11 . x0 x11 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 x11)))))))) = x10 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 x11)))))))) (proof)Theorem 3c98f.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ x1 x11 ⟶ ∀ x12 . x0 x12 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 x12))))))))) = x11 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 x12))))))))) (proof)Theorem 41b33.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ x1 x4 ⟶ x1 x5 ⟶ x1 x6 ⟶ x1 x7 ⟶ x1 x8 ⟶ x1 x9 ⟶ x1 x10 ⟶ x1 x11 ⟶ x1 x12 ⟶ ∀ x13 . x0 x13 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 x13)))))))))) = x12 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 x13)))))))))) (proof)Theorem 11d87.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 : ι → ι . 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 . x0 x14 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 x14))))))))))) = x13 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 x14))))))))))) (proof)Theorem 97776.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 : ι → ι . 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 . x0 x15 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 x15)))))))))))) = x14 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 x15)))))))))))) (proof)Theorem 27d68.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 : ι → ι . 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 . x0 x16 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 x16))))))))))))) = x15 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 x16))))))))))))) (proof)Theorem 9a7a2.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 : ι → ι . 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 ⟶ x1 x16 ⟶ ∀ x17 . x0 x17 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 (x16 x17)))))))))))))) = x16 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 x17)))))))))))))) (proof)Theorem 76a14.. : ∀ x0 : ι → ο . ∀ x1 : (ι → ι) → ο . (∀ x2 : ι → ι . x1 x2 ⟶ ∀ x3 . x0 x3 ⟶ x0 (x2 x3)) ⟶ (∀ x2 x3 : ι → ι . x1 x2 ⟶ x1 x3 ⟶ ∀ x4 . x0 x4 ⟶ x2 (x3 x4) = x3 (x2 x4)) ⟶ ∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 : ι → ι . 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 ⟶ x1 x16 ⟶ x1 x17 ⟶ ∀ x18 . x0 x18 ⟶ x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 (x16 (x17 x18))))))))))))))) = x17 (x2 (x3 (x4 (x5 (x6 (x7 (x8 (x9 (x10 (x11 (x12 (x13 (x14 (x15 (x16 x18))))))))))))))) (proof) |
|