Spaces:
Running
Running
File size: 1,936 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 75 76 77 78 79 80 81 82 83 84 85 86 | 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 ·"]
T12["T12\nZero from left"]
T13["T13\nSuccessor and mul"]
T14["T14\nCommutativity of ·"]
T15["T15\nAssociativity of ·"]
T16["T16\nDistributivity"]
T18["T18\nOrder definition"]
T19["T19\nTrichotomy"]
T20["T20\nOrder + add"]
T21["T21\nOrder + mul"]
T22["T22\nMultiplicative identity"]
T23["T23\nRight identity"]
T24["T24\nWell-ordering"]
T25["T25\nStrong induction"]
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 --> 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
DefAdd --> T18
T8 --> T18
T9 --> T18
T18 --> T19
T9 --> T19
T18 --> T20
T8 --> T20
T18 --> T21
T16 --> T21
T14 --> T21
DefMul --> T22
T6 --> T22
A5 --> T22
T14 --> T23
T22 --> T23
T18 --> T24
T19 --> T24
A5 --> T24
T18 --> T25
T24 --> T25
A5 --> T25
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,T12,T13,T14,T15,T16,T18,T19,T20,T21,T22,T23,T24,T25 theorem |