Here is a derivation of the three-base {Syl, Simp, Hilbert} for HI from {Frege', Simp}:

 
 



 

          1. CCpqCCqCqrCpr                                             [Frege']
          2. CpCqp                                                             [Simp]
D1.1   =  3. CCCCpCpqCrqCCCpCpqCrqsCCrps
D2.1   =  4. CpCCqrCCrCrsCqs
D1.2   =  5. CCCpqCCpqrCqr
D2.2   =  6. CpCqCrq
D2.3   =  7. CpCCCCqCqrCsrCCCqCqrCsrtCCsqt
D2.5   =  8. CpCCCqrCCqrsCrs
D5.4   =  9. CpCCpCpqCrq
D3.6   = 10. CCpqCrCCqCqsCps
D5.7   = 11. CCCCpCpqCrqsCCrps
D5.8   = 12. CCCpqrCqr
D1.9   = 13. CCCCpCpqCrqCCCpCpqCrqsCps
D10.9  = 14. CpCCCCqCqrCsrCCCqCqrCsrtCqt
D11.12 = 15. CCpqCCqrCpr                                             [Syl]
D13.14 = 16. CCpCpqCpq                                                 [Hilbert]
 

 

  Dolph Ulrich, 2007