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