Notation:
a(x,y)=x+y
s(x)="the successor of x"
| D1 | s(zero)=one | DEFINITION | s0=1 |
| D2 | s(one)=two | DEFINITION | s1=2 |
| D3 | s(two)=three | DEFINITION | s2=3 |
| s(three)=four | DEFINITION | s3=4 | |
| s(four)=five | DEFINITION | s4=5 | |
| s(five)=six | DEFINITION | s5=6 | |
| s(six)=seven | DEFINITION | s6=7 | |
| s(seven)=eight | DEFINITION | s7=8 | |
| D4 | s(eight)=nine | DEFINITION | s8=9 |
| D5 | s(nine)=ten | DEFINITION | s9=10 |
| D6 | s(ten)=eleven | DEFINITION | s10=11 |
| A7 | a(x,s(y))=s(a(x,y)) | AXIOM | x+sy=s(x+y) |
| T8 | a(eight,s(y))=s(a(eight,y)) | FROM A7 | 8+sy=s(8+y) |
| A9 | a(x,zero)=x | AXIOM | x+0=x |
| T10 | a(eight,zero)=eight | FROM A9 | 8+0=8 |
| T11 | a(eight,s(zero))=s(a(eight,zero)) | FROM T8 | 8+s0=s(8+0) |
| T12 | a(eight,s(zero))=s(eight) | FROM T11 AND T10 | 8+s0=s8 |
| T13 | a(eight,s(zero))=nine | FROM T12 AND D4 | 8+s0=9 |
| T14 | a(eight,one)=nine | FROM T13 AND D1 | 8+1=9 |
| T15 | a(eight,s(one)=s(a(eight,one)) | FROM T8 | 8+s1=s(8+1) |
| T16 | a(eight,s(one))=s(nine) | FROM T15 AND T14 | 8+s1=s9 |
| T17 | a(eight,s(one))=ten | FROM T16 AND D5 | 8+s1=10 |
| T18 | a(eight,two)=ten | FROM T17 AND D2 | 8+2=10 |
| T19 | a(eight,s(two))=s(a(eight,two)) | FROM T8 | 8+s2=s(8+2) |
| T20 | a(eight,s(two))=s(ten) | FROM T19 AND T18 | 8+s2=s10 |
| T21 | a(eight,s(two))=eleven | FROM T20 AND D6 | 8+s2=11 |
| T22 | a(eight,three)=eleven | FROM T21 AND D3 | 8+3=11 |
Notation:
a(x,y)=x+y
i(x)="the increment of x"
d(x)="the decrement of x"
| D1 | i(zero)=one | DEFINITION |
| D2 | i(one)=two | DEFINITION |
| D3 | i(two)=three | DEFINITION |
| i(three)=four | DEFINITION | |
| i(four)=five | DEFINITION | |
| i(five)=six | DEFINITION | |
| i(six)=seven | DEFINITION | |
| i(seven)=eight | DEFINITION | |
| D4 | i(eight)=nine | DEFINITION |
| D5 | i(nine)=ten | DEFINITION |
| D6 | i(ten)=eleven | DEFINITION |
| A7 | d(i(x))=x | AXIOM |
| T8 | d(i(two))=two | FROM A7 |
| T9 | d(three)=two | FROM T8 AND D3 |
| T10 | d(i(one))=one | FROM A7 |
| T11 | d(two)=one | FROM T10 AND D2 |
| T12 | d(i(zero))=zero | FROM A7 |
| T13 | d(one)=zero | FROM T10 AND D1 |
| A14 | a(x,y)=a(i(x),d(y)) | AXIOM |
| T15 | a(eight,y)=a(i(eight),d(y)) | FROM A14 |
| T16 | a(eight,three)=a(i(eight),d(three)) | FROM T15 |
| T17 | a(eight,three)=a(nine,d(three)) | FROM T16 AND D4 |
| T18 | a(eight,three)=a(nine,two) | FROM T17 AND T9 |
| T19 | a(nine,y)=a(i(nine),d(y)) | FROM A14 |
| T20 | a(nine,two)=a(i(nine),d(two)) | FROM T19 |
| T21 | a(nine,two)=a(ten,d(two)) | FROM T20 AND D5 |
| T22 | a(nine,two)=a(ten,one) | FROM T21 AND T11 |
| T23 | a(eight,three)=a(ten,one) | FROM T18 AND T22 |
| T24 | a(ten,y)=a(i(ten),d(y)) | FROM A14 |
| T25 | a(ten,one)=a(i(ten),d(one)) | FROM T24 |
| T26 | a(ten,one)=a(eleven,d(one)) | FROM T25 AND D6 |
| T27 | a(ten,one)=a(eleven,zero) | FROM T26 AND D13 |
| T28 | a(eight,three)=a(eleven,zero) | FROM T23 AND T27 |
| A29 | a(x,zero)=x | AXIOM |
| T30 | a(eleven,zero)=eleven | FROM A29 |
| T31 | a(eight,three)=eleven | FROM T25 AND T27 |