* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + 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:
            { 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:
            { S(x),y -> S(y)} =
            monus(S(x),S(y)) ->^+ monus(x,y)
              = C[monus(x,y) = monus(x,y){}]

WORST_CASE(Omega(n^1),?)