Spaces:
Running
Running
File size: 1,629 Bytes
06e4298 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 | 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 |