MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: gcd(x,0()) -> x gcd(0(),y) -> y gcd(s(x),s(y)) -> if(<(x,y),gcd(s(x),-(y,x)),gcd(-(x,y),s(y))) - Signature: {gcd/2} / {-/2,0/0,