graph TD
    A1["A1\n0 ∈ N"]
    A2["A2\n0 not a successor"]
    A3["A3\nS injective"]
    A4["A4\nN closed under S"]
    A5["A5\nInduction"]
    T1["T1\nContrapositive of A3"]
    T2["T2\nSuccessor ≠ identity"]
    T3["T3\nEvery nonzero is successor"]
    DefAdd["DefAdd\nDefinition of +"]
    T4["T4\nAdd well-defined"]
    T5["T5\nAssociativity of +"]
    T6["T6\nLeft identity"]
    A3 --> T1
    A1 --> T2
    A2 --> T2
    A3 --> T2
    T1 --> T2
    A5 --> T2
    A5 --> T3
    A5 --> DefAdd
    DefAdd --> T4
    A5 --> T4
    DefAdd --> T5
    A5 --> T5
    DefAdd --> T6
    A5 --> T6
    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,A4,A5 axiom
    class DefAdd definition
    class T1,T2,T3,T4,T5,T6 theorem