Proof-for-the-LC-I-axiom

Here is a derivation of the four-base {Syl, Simp, Hilbert, Dummett} for C-pure LC from the single axiom:
		1. CCCpCqpCCCCCCrstCCCsrttCuCuvCwvxCCwux D1.1 = 2. CCpqCrCsr D2.1 = 3. *CpCqp* [Simp] D1.2 = 4. CCpqCrCCCCCstuCCCtsuuCqCqvCpv D1.4 = 5. CCpqCCCCCrstCCCsrttCCuvCCuvwCvw D4.3 = 6. CpCCCCCqrsCCCrqssCCtuCCtuvCuv D5.1 = 7. CCCCCpqrCCCqprrCCstCCstuCtu D3.6 = 8. CpCqCCCCCrstCCCsrttCCuvCCuvwCvw D7.4 = 9. CCCCCpqrrCCCCpqrrsCCCqprs D7.8 = 10. CCCpqCCpqrCqr D9.3 = 11. *CCCpqrCCCqprr* [Dummett] D3.10 = 12. CpCCCqrCCqrsCrs D10.11 = 13. Cpp D10.12 = 14. CCCpqrCqr D4.13 = 15. CpCCCCCqrsCCCrqssCtCtuCtu D3.14 = 16. CpCCCqrsCrs D10.15 = 17. *CCpCpqCpq* [Hilbert] D1.16 = 18. CCpqCCqCqrCpr D18.18 = 19. CCCCpCpqCrqCCCpCpqCrqsCCrps D19.16 = 20. *CCpqCCqrCpr* [SYL] There is an even shorter derivation of the three-base {Frege', Simp, Dummett}: space 1. *CCCpCqpCCCCCCrstCCCsrttCuCuvCwvxCCwux* D1.1 = 2. CCpqCrCsr D2.1 = 3. *CpCqp* [Simp] D1.2 = 4. CCpqCrCCCCCstuCCCtsuuCqCqvCpv D1.4 = 5. CCpqCCCCCrstCCCsrttCCuvCCuvwCvw D4.3 = 6. CpCCCCCqrsCCCrqssCCtuCCtuvCuv D5.1 = 7. CCCCCpqrCCCqprrCCstCCstuCtu D3.6 = 8. CpCqCCCCCrstCCCsrttCCuvCCuvwCvw D7.4 = 9. CCCCCpqrrCCCCpqrrsCCCqprs D7.8 = 10. CCCpqCCpqrCqr D9.3 = 11. *CCCpqrCCCqprr* [Dummett] D3.10 = 12. CpCCCqrCCqrsCrs D10.12 = 13. CCCpqrCqr D3.13 = 14. CpCCCqrsCrs D1.14 = 15. CCpqCCqCqrCpr [Frege']
		© Dolph Ulrich, 2007