Here's a derivation of the C3 base {Syl, Hilbert, Weak Irrelevance} from the single axiom CCCCpCpqCCrsCpqCCCtuCCvwCCCxxCwyCvyzz:

 
   
                       1 . CCCCpCpqCCrsCpqCCCtuCCvwCCCxxCwyCvyzz
D1.1        =   2 . CCpqCCCrrCqsCps                                                    [The BC011I axiom]
D1.2       =   3 . CCpCpqCCCrrCCpqsCCtus
D2.2       =  4 . CCCppCCCCqqCrsCtsuCCtru
D1.3       =   5 . CCpqCCCrrCCstuCCsCstu
D2.3      =   6 . CCCppCCCCqqCCrstCCuvtwCCrCrsw
D4.1       =   7 . CCpqCCrsCCCttCsuCru
D4.2      =   8 . CCpqCpq
D2.4      =   9 . CCCppCCCqrstCCCuuCCCCvvCrwCqwst
D4.4      = 10 . CCpqCCCrrCCpstCCCuuCqst
D5.1      =  11 . CCCppCCqrsCCqCqrs
D1.7       = 12 . CCCppCCCqrCCCssCrtCqtuCCvwu
D4.9      = 13 . CCCCCppCqrCsrtCCsqt
D9.10    = 14 . CCCppCCCCqqCrsCrsCCtuvCCCwwCtuv
D11.8    = 15 . CCpCpqCpq                                                              [Hilbert]
D13.13  = 16 . CCpqCCqrCpr                                                          [Syl]
D12.14  = 17 . CCpqCrr                                                                   [Weak-Irrel]
 


© Dolph Ulrich, 2007