MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: equal0(a,b) -> equal0[Ite](<(a,b),a,b) gcd(x,y) -> gcd[Ite](equal0(x,y),x,y) monus(S(x'),S(x)) -> monus(x',x) - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) equal0[Ite](False(),a,b) -> False() equal0[Ite](True(),a,b) -> equal0[True][Ite](<(b,a),a,b) equal0[True][Ite](False(),a,b) -> False() equal0[True][Ite](True(),a,b) -> True() gcd[False][Ite](False(),x,y) -> gcd(y,monus(y,x)) gcd[False][Ite](True(),x,y) -> gcd(monus(x,y),y) gcd[Ite](False(),x,y) -> gcd[False][Ite](<(x,y),x,y) gcd[Ite](True(),x,y) -> x - Signature: {