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] |
||
|