Spaces:
Running
Running
File size: 1,515 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 | graph TD
A5["A5\nInduction"]
DefAdd["DefAdd\nDefinition of +"]
T5["T5\nAssociativity of +"]
T6["T6\nLeft identity"]
T7["T7\nSuccessor and add"]
T8["T8\nCommutativity of +"]
T9["T9\nCancellation for +"]
DefMul["DefMul\nDefinition of ·"]
T10["T10\nMul well-defined"]
T11["T11\nZero times"]
T12["T12\nZero from left"]
T13["T13\nSuccessor and mul"]
T14["T14\nCommutativity of ·"]
T15["T15\nAssociativity of ·"]
T16["T16\nDistributivity"]
T17["T17\nDistributivity (right)"]
A5 --> DefAdd
DefAdd --> T5
A5 --> T5
DefAdd --> T6
A5 --> T6
DefAdd --> T7
T6 --> T7
A5 --> T7
DefAdd --> T8
T5 --> T8
T6 --> T8
T7 --> T8
A5 --> T8
DefAdd --> T9
T8 --> T9
A5 --> T9
DefAdd --> DefMul
A5 --> DefMul
DefMul --> T10
A5 --> T10
DefMul --> T11
DefMul --> T12
T6 --> T12
A5 --> T12
DefMul --> T13
T8 --> T13
A5 --> T13
DefMul --> T14
T12 --> T14
T13 --> T14
A5 --> T14
DefMul --> T15
T5 --> T15
T8 --> T15
A5 --> T15
DefMul --> T16
T5 --> T16
T8 --> T16
T15 --> T16
A5 --> T16
T16 --> T17
T8 --> T17
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 A5 axiom
class DefAdd,DefMul definition
class T5,T6,T7,T8,T9,T10,T11,T12,T13,T14,T15,T16,T17 theorem |