(A) m n
comment:
(=) m 0
(add1) n
(=) n 0
(A) (sub1) m 1
#true
(A) (sub1) m (A) m (sub1) n
(003) "+" n 1
(sub1) n
(003) "-" n 1
(=) n1 n2
(003) "=" n1 n2