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    DefIff("DefIff Def. biconditional")13    T6("T6 Addition (orI)")14    T7("T7 Simplification (andE)")15    T8("T8 Simplification (andE)")16    T9("T9 Conjunction (andI)")17    T10("T10 Material impl.")18    T11("T11 De Morgan (1)")19    T12("T12 De Morgan (2)")20    A1 --> T121    A2 --> T122    MP --> T123    A3 --> T224    T1 --> T225    MP --> T226    A1 --> T327    A3 --> T328    MP --> T329    A3 --> T430    T2 --> T431    T3 --> T432    MP --> T433    A1 --> DefOr34    A2 --> DefOr35    A3 --> DefOr36    MP --> DefOr37    DefOr --> DefAnd38    A3 --> DefAnd39    MP --> DefAnd40    DefAnd --> DefIff41    T9 --> DefIff42    MP --> DefIff43    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 --> T1058    T4 --> T1059    MP --> T1060    DefAnd --> T1161    DefOr --> T1162    T4 --> T1163    T6 --> T1164    MP --> T1165    DefAnd --> T1266    DefOr --> T1267    T4 --> T1268    MP --> T1269    classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b70    classDef definition fill:#3498db,color:#fff,stroke:#2980b971    classDef theorem fill:#1abc9c,color:#fff,stroke:#16a08572    class A1,A2,A3,MP axiom73    class DefOr,DefAnd,DefIff definition74    class T1,T2,T3,T4,T6,T7,T8,T9,T10,T11,T12 theorem