0 GTRS
if(true) → X if(false) → Y p(0) → 0 p(s(X)) → X leq(0, Y) → true leq(s(X), 0) → false leq(s(X), s(Y)) → leq(X, Y) diff(X, Y) → if(leq(X, Y))