Spaces:
Running
Running
| graph TD | |
| A1("A1 Weakening") | |
| A2("A2 Distrib. of impl.") | |
| A3("A3 Contraposition") | |
| MP("MP MP") | |
| T1("T1 Self-implication") | |
| T2("T2 Double neg. elim") | |
| T3("T3 Double neg. intro") | |
| T4("T4 Transposition") | |
| DefOr("DefOr Def. disjunction") | |
| DefAnd("DefAnd Def. conjunction") | |
| DefIff("DefIff Def. biconditional") | |
| T6("T6 Addition (orI)") | |
| T7("T7 Simplification (andE)") | |
| T8("T8 Simplification (andE)") | |
| T9("T9 Conjunction (andI)") | |
| T10("T10 Material impl.") | |
| T11("T11 De Morgan (1)") | |
| T12("T12 De Morgan (2)") | |
| A1 --> T1 | |
| A2 --> T1 | |
| MP --> T1 | |
| A3 --> T2 | |
| T1 --> T2 | |
| MP --> T2 | |
| A1 --> T3 | |
| A3 --> T3 | |
| MP --> T3 | |
| A3 --> T4 | |
| T2 --> T4 | |
| T3 --> T4 | |
| MP --> T4 | |
| A1 --> DefOr | |
| A2 --> DefOr | |
| A3 --> DefOr | |
| MP --> DefOr | |
| DefOr --> DefAnd | |
| A3 --> DefAnd | |
| MP --> DefAnd | |
| DefAnd --> DefIff | |
| T9 --> DefIff | |
| MP --> DefIff | |
| DefOr --> T6 | |
| A1 --> T6 | |
| MP --> T6 | |
| DefAnd --> T7 | |
| A1 --> T7 | |
| A3 --> T7 | |
| MP --> T7 | |
| DefAnd --> T8 | |
| A1 --> T8 | |
| A3 --> T8 | |
| MP --> T8 | |
| A1 --> T9 | |
| A2 --> T9 | |
| MP --> T9 | |
| DefOr --> T10 | |
| T4 --> T10 | |
| MP --> T10 | |
| DefAnd --> T11 | |
| DefOr --> T11 | |
| T4 --> T11 | |
| T6 --> T11 | |
| MP --> T11 | |
| DefAnd --> T12 | |
| DefOr --> T12 | |
| T4 --> T12 | |
| MP --> T12 | |
| classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b | |
| classDef definition fill:#3498db,color:#fff,stroke:#2980b9 | |
| classDef theorem fill:#1abc9c,color:#fff,stroke:#16a085 | |
| class A1,A2,A3,MP axiom | |
| class DefOr,DefAnd,DefIff definition | |
| class T1,T2,T3,T4,T6,T7,T8,T9,T10,T11,T12 theorem |