WORST_CASE(?,O(n^2)) * Step 1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: gcd(0(),y) -> y gcd(s(x),0()) -> s(x) gcd(s(x),s(y)) -> if_gcd(le(y,x),s(x),s(y)) if_gcd(false(),s(x),s(y)) -> gcd(minus(y,x),s(x)) if_gcd(true(),s(x),s(y)) -> gcd(minus(x,y),s(y)) le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) - Signature: {gcd/2,if_gcd/3,le/2,minus/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {gcd,if_gcd,le,minus} and constructors {0,false,s,true} + Applied Processor: NaturalPI {shape = Quadratic, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a polynomial interpretation of kind constructor-based(quadratic): The following argument positions are considered usable: uargs(gcd) = {1}, uargs(if_gcd) = {1} Following symbols are considered usable: {gcd,if_gcd,le,minus} TcT has computed the following interpretation: p(0) = 1 p(false) = 2 p(gcd) = 1 + 2*x1 + x1^2 + x2 + x2^2 p(if_gcd) = x1 + x2 + x2^2 + x3 + x3^2 p(le) = 2 + x2 p(minus) = 1 + x1 p(s) = 2 + x1 p(true) = 0 Following rules are strictly oriented: gcd(0(),y) = 4 + y + y^2 > y = y gcd(s(x),0()) = 11 + 6*x + x^2 > 2 + x = s(x) gcd(s(x),s(y)) = 15 + 6*x + x^2 + 5*y + y^2 > 14 + 6*x + x^2 + 5*y + y^2 = if_gcd(le(y,x),s(x),s(y)) if_gcd(false(),s(x),s(y)) = 14 + 5*x + x^2 + 5*y + y^2 > 10 + 5*x + x^2 + 4*y + y^2 = gcd(minus(y,x),s(x)) if_gcd(true(),s(x),s(y)) = 12 + 5*x + x^2 + 5*y + y^2 > 10 + 4*x + x^2 + 5*y + y^2 = gcd(minus(x,y),s(y)) le(0(),y) = 2 + y > 0 = true() le(s(x),0()) = 3 > 2 = false() le(s(x),s(y)) = 4 + y > 2 + y = le(x,y) minus(x,0()) = 1 + x > x = x minus(s(x),s(y)) = 3 + x > 1 + x = minus(x,y) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^2))