Proofgold Address

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)