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    T5("T5 Hyp. syllogism")11    DefOr("DefOr Def. disjunction")12    DefAnd("DefAnd Def. conjunction")13    DefIff("DefIff Def. biconditional")14    T6("T6 Addition (orI)")15    T7("T7 Simplification (andE)")16    T8("T8 Simplification (andE)")17    T9("T9 Conjunction (andI)")18    T10("T10 Material impl.")19    T11("T11 De Morgan (1)")20    T12("T12 De Morgan (2)")21    T13("T13 Excluded middle")22    T14("T14 Non-contradiction")23    T15("T15 Explosion")24    T16("T16 Commutation (or)")25    T17("T17 Commutation (and)")26    T18("T18 Distribution")27    T19("T19 Deduction thm")28    A1 --> T129    A2 --> T130    MP --> T131    A3 --> T232    T1 --> T233    MP --> T234    A1 --> T335    A3 --> T336    MP --> T337    A3 --> T438    T2 --> T439    T3 --> T440    MP --> T441    A2 --> T542    T1 --> T543    MP --> T544    A1 --> DefOr45    A2 --> DefOr46    A3 --> DefOr47    MP --> DefOr48    DefOr --> DefAnd49    A3 --> DefAnd50    MP --> DefAnd51    DefAnd --> DefIff52    T9 --> DefIff53    MP --> DefIff54    DefOr --> T655    A1 --> T656    MP --> T657    DefAnd --> T758    A1 --> T759    A3 --> T760    MP --> T761    DefAnd --> T862    A1 --> T863    A3 --> T864    MP --> T865    A1 --> T966    A2 --> T967    MP --> T968    DefOr --> T1069    T4 --> T1070    MP --> T1071    DefAnd --> T1172    DefOr --> T1173    T4 --> T1174    T6 --> T1175    MP --> T1176    DefAnd --> T1277    DefOr --> T1278    T4 --> T1279    MP --> T1280    DefOr --> T1381    T2 --> T1382    T3 --> T1383    MP --> T1384    DefAnd --> T1485    T4 --> T1486    MP --> T1487    DefAnd --> T1588    A1 --> T1589    A2 --> T1590    MP --> T1591    DefOr --> T1692    T4 --> T1693    MP --> T1694    DefAnd --> T1795    T9 --> T1796    MP --> T1797    DefAnd --> T1898    DefOr --> T1899    T6 --> T18100    T7 --> T18101    T8 --> T18102    T9 --> T18103    MP --> T18104    A1 --> T19105    A2 --> T19106    MP --> T19107    classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b108    classDef definition fill:#3498db,color:#fff,stroke:#2980b9109    classDef theorem fill:#1abc9c,color:#fff,stroke:#16a085110    class A1,A2,A3,MP axiom111    class DefOr,DefAnd,DefIff definition112    class T1,T2,T3,T4,T5,T6,T7,T8,T9,T10,T11,T12,T13,T14,T15,T16,T17,T18,T19 theorem