garywelz/programming_framework

1graph TD2    A1["A1\n0 ∈ N"]3    A2["A2\n0 not a successor"]4    A3["A3\nS injective"]5    A4["A4\nN closed under S"]6    A5["A5\nInduction"]7    T1["T1\nContrapositive of A3"]8    T2["T2\nSuccessor ≠ identity"]9    T3["T3\nEvery nonzero is successor"]10    DefAdd["DefAdd\nDefinition of +"]11    T4["T4\nAdd well-defined"]12    T5["T5\nAssociativity of +"]13    T6["T6\nLeft identity"]14    T7["T7\nSuccessor and add"]15    T8["T8\nCommutativity of +"]16    T9["T9\nCancellation for +"]17    DefMul["DefMul\nDefinition of ·"]18    T10["T10\nMul well-defined"]19    T11["T11\nZero times"]20    T12["T12\nZero from left"]21    T13["T13\nSuccessor and mul"]22    T14["T14\nCommutativity of ·"]23    T15["T15\nAssociativity of ·"]24    T16["T16\nDistributivity"]25    T17["T17\nDistributivity (right)"]26    T18["T18\nOrder definition"]27    T19["T19\nTrichotomy"]28    T20["T20\nOrder + add"]29    T21["T21\nOrder + mul"]30    T22["T22\nMultiplicative identity"]31    T23["T23\nRight identity"]32    T24["T24\nWell-ordering"]33    T25["T25\nStrong induction"]34    A3 --> T135    A1 --> T236    A2 --> T237    A3 --> T238    T1 --> T239    A5 --> T240    A5 --> T341    A5 --> DefAdd42    DefAdd --> T443    A5 --> T444    DefAdd --> T545    A5 --> T546    DefAdd --> T647    A5 --> T648    DefAdd --> T749    T6 --> T750    A5 --> T751    DefAdd --> T852    T5 --> T853    T6 --> T854    T7 --> T855    A5 --> T856    DefAdd --> T957    T8 --> T958    A5 --> T959    DefAdd --> DefMul60    A5 --> DefMul61    DefMul --> T1062    A5 --> T1063    DefMul --> T1164    DefMul --> T1265    T6 --> T1266    A5 --> T1267    DefMul --> T1368    T8 --> T1369    A5 --> T1370    DefMul --> T1471    T12 --> T1472    T13 --> T1473    A5 --> T1474    DefMul --> T1575    T5 --> T1576    T8 --> T1577    A5 --> T1578    DefMul --> T1679    T5 --> T1680    T8 --> T1681    T15 --> T1682    A5 --> T1683    T16 --> T1784    T8 --> T1785    DefAdd --> T1886    T8 --> T1887    T9 --> T1888    T18 --> T1989    T9 --> T1990    T18 --> T2091    T8 --> T2092    T18 --> T2193    T16 --> T2194    T14 --> T2195    DefMul --> T2296    T6 --> T2297    A5 --> T2298    T14 --> T2399    T22 --> T23100    T18 --> T24101    T19 --> T24102    A5 --> T24103    T18 --> T25104    T24 --> T25105    A5 --> T25106    classDef axiom fill:#e74c3c,color:#fff,stroke:#c0392b107    classDef definition fill:#3498db,color:#fff,stroke:#2980b9108    classDef theorem fill:#1abc9c,color:#fff,stroke:#16a085109    class A1,A2,A3,A4,A5 axiom110    class DefAdd,DefMul definition111    class T1,T2,T3,T4,T5,T6,T7,T8,T9,T10,T11,T12,T13,T14,T15,T16,T17,T18,T19,T20,T21,T22,T23,T24,T25 theorem