Notation:
a(x,y)=x+y
s(x)="the increment of x"

A1	a(x,s(y))=s(a(x,y))	AXIOM	x+sy=s(x+y)
T2	a(1,s(y))=s(a(1,y))	FROM A1	1+sy=s(1+y)
T3	a(1,s(0))=s(a(1,0))	FROM T2	1+s0=s(1+0)
A4	a(x,0)=x	AXIOM	x+0=x
T5	a(1,0)=1	FROM A4	1+0=1
T6	a(1,s(0))=s(1)	FROM T3 AND T5	1+s0=s1
D7	s(0)=1	DEFINITION	s0=1
T8	a(1,1)=s(1)	FROM T6 AND D7	1+1=s1
D9	s(1)=2	DEFINITION	s1=2
T10	a(1,1)=2	FROM T8 AND D9	1+1=2

Expression tree of this proof structure

Notation:
a(x,y)=x+y
i(x)="the increment of x"
d(x)="the decrement of x"

A1	a(x,y)=a(i(x),d(y))	AXIOM
T2	a(1,y)=a(i(1),d(y))	FROM A1
T3	a(1,1)=a(i(1),d(1))	FROM T2
D4	i(1)=2	DEFINITION
T5	a(1,1)=a(2,d(1))	FROM T3 AND D4
D6	i(0)=1	DEFINITION
T7	a(1,1)=a(2,d(i(0)))	FROM T5 AND D6
A8	d(i(x))=x	AXIOM
T9	d(i(0))=0	AXIOM
T10	a(1,1)=a(2,0)	FROM T7 AND D9
A11	a(x,0)=x	AXIOM
T12	a(2,0)=2	FROM A11
T13	a(1,1)=2	FROM T10 AND T12

• Two proofs of "eight plus three equals eleven"
• Graph Theory
• Expression trees