(A) m n
comment:
(=) m 0
(add1) n

(A) m n
comment:
(=) n 0
(A) (sub1) m 1

(A) m n
comment:
#true
(A) (sub1) m (A) m (sub1) n

(add1) n
comment:
#true
(003) "+" n 1

(sub1) n
comment:
#true
(003) "-" n 1

(=) n1 n2
comment:
#true
(003) "=" n1 n2