garywelz/programming_framework

1graph TD2    A1("A1 Weakening")3    A2("A2 Distrib. of impl.")4    A3("A3 Contraposition")5    MP("MP MP")6    T1("T1 Self-implication")7    T2("T2 Double neg. elim")8    T3("T3 Double neg. intro")9    T4("T4 Transposition")10    DefOr("DefOr Def. disjunction")11    DefAnd("DefAnd Def. conjunction")12    T6("T6 Addition (orI)")13    T7("T7 Simplification (andE)")14    T8("T8 Simplification (andE)")15    T9("T9 Conjunction (andI)")16    T13("T13 Excluded middle")17    T14("T14 Non-contradiction")18    T15("T15 Explosion")19    T16("T16 Commutation (or)")20    T17("T17 Commutation (and)")21    T18("T18 Distribution")22    T19("T19 Deduction thm")23    A1 --> T124    A2 --> T125    MP --> T126    A3 --> T227    T1 --> T228    MP --> T229    A1 --> T330    A3 --> T331    MP --> T332    A3 --> T433    T2 --> T434    T3 --> T435    MP --> T436    A1 --> DefOr37    A2 --> DefOr38    A3 --> DefOr39    MP --> DefOr40    DefOr --> DefAnd41    A3 --> DefAnd42    MP --> DefAnd43    DefOr --> T644    A1 --> T645    MP --> T646    DefAnd --> T747    A1 --> T748    A3 --> T749    MP --> T750    DefAnd --> T851    A1 --> T852    A3 --> T853    MP --> T854    A1 --> T955    A2 --> T956    MP --> T957    DefOr --> T1358    T2 --> T1359    T3 --> T1360    MP --> T1361    DefAnd --> T1462    T4 --> T1463    MP --> T1464    DefAnd --> T1565    A1 --> T1566    A2 --> T1567    MP --> T1568    DefOr --> T1669    T4 --> T1670    MP --> T1671    DefAnd --> T1772    T9 --> T1773    MP --> T1774    DefAnd --> T1875    DefOr --> T1876    T6 --> T1877    T7 --> T1878    T8 --> T1879    T9 --> T1880    MP --> T1881    A1 --> T1982    A2 --> T1983    MP --> T1984    classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b85    classDef definition fill:#3498db,color:#fff,stroke:#2980b986    classDef theorem fill:#1abc9c,color:#fff,stroke:#16a08587    class A1,A2,A3,MP axiom88    class DefOr,DefAnd definition89    class T1,T2,T3,T4,T6,T7,T8,T9,T13,T14,T15,T16,T17,T18,T19 theorem