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