0 QTRS
-(0, y) → 0 -(x, 0) → x -(x, s(y)) → if(greater(x, s(y)), s(-(x, p(s(y)))), 0) p(0) → 0 p(s(x)) → x