MAYBE * Step 1: NaturalPI MAYBE + Considered Problem: - Strict TRS: f(Cons(x,xs),y) -> h(Cons(x,xs),y) f(Nil(),y) -> g(Nil(),y) g(Cons(x,xs),y) -> Cons(x,xs) g(Nil(),y) -> h(Nil(),y) h(Cons(x,xs),y) -> f(Cons(x,xs),y) h(Nil(),y) -> h(Nil(),y) r(x,y) -> x sp1(x,y) -> f(x,y) - Signature: {f/2,g/2,h/2,r/2,sp1/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,h,r,sp1} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: none Following symbols are considered usable: {f,g,h,r,sp1} TcT has computed the following interpretation: p(Cons) = 0 p(Nil) = 1 p(f) = 6*x1 + 6*x1*x2 + 6*x1^2 + 6*x2 + 2*x2^2 p(g) = 5*x1*x2 + 4*x1^2 + 7*x2 + 2*x2^2 p(h) = x1 + 5*x1*x2 + 2*x1^2 + 6*x2 + 2*x2^2 p(r) = 3*x1 + x1*x2 + x1^2 + x2^2 p(sp1) = 4 + 7*x1 + 6*x1*x2 + 7*x1^2 + 6*x2 + 3*x2^2 Following rules are strictly oriented: f(Nil(),y) = 12 + 12*y + 2*y^2 > 4 + 12*y + 2*y^2 = g(Nil(),y) g(Nil(),y) = 4 + 12*y + 2*y^2 > 3 + 11*y + 2*y^2 = h(Nil(),y) sp1(x,y) = 4 + 7*x + 6*x*y + 7*x^2 + 6*y + 3*y^2 > 6*x + 6*x*y + 6*x^2 + 6*y + 2*y^2 = f(x,y) Following rules are (at-least) weakly oriented: f(Cons(x,xs),y) = 6*y + 2*y^2 >= 6*y + 2*y^2 = h(Cons(x,xs),y) g(Cons(x,xs),y) = 7*y + 2*y^2 >= 0 = Cons(x,xs) h(Cons(x,xs),y) = 6*y + 2*y^2 >= 6*y + 2*y^2 = f(Cons(x,xs),y) h(Nil(),y) = 3 + 11*y + 2*y^2 >= 3 + 11*y + 2*y^2 = h(Nil(),y) r(x,y) = 3*x + x*y + x^2 + y^2 >= x = x * Step 2: NaturalPI MAYBE + Considered Problem: - Strict TRS: f(Cons(x,xs),y) -> h(Cons(x,xs),y) g(Cons(x,xs),y) -> Cons(x,xs) h(Cons(x,xs),y) -> f(Cons(x,xs),y) h(Nil(),y) -> h(Nil(),y) r(x,y) -> x - Weak TRS: f(Nil(),y) -> g(Nil(),y) g(Nil(),y) -> h(Nil(),y) sp1(x,y) -> f(x,y) - Signature: {f/2,g/2,h/2,r/2,sp1/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,h,r,sp1} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: none Following symbols are considered usable: {f,g,h,r,sp1} TcT has computed the following interpretation: p(Cons) = 0 p(Nil) = 2 p(f) = 7*x1*x2 + 2*x1^2 + 2*x2^2 p(g) = 6*x1*x2 + x1^2 + 2*x2 + 2*x2^2 p(h) = x1^2 + 2*x2^2 p(r) = 2 + x1 + 2*x2 p(sp1) = 1 + x1 + 7*x1*x2 + 3*x1^2 + 2*x2^2 Following rules are strictly oriented: r(x,y) = 2 + x + 2*y > x = x Following rules are (at-least) weakly oriented: f(Cons(x,xs),y) = 2*y^2 >= 2*y^2 = h(Cons(x,xs),y) f(Nil(),y) = 8 + 14*y + 2*y^2 >= 4 + 14*y + 2*y^2 = g(Nil(),y) g(Cons(x,xs),y) = 2*y + 2*y^2 >= 0 = Cons(x,xs) g(Nil(),y) = 4 + 14*y + 2*y^2 >= 4 + 2*y^2 = h(Nil(),y) h(Cons(x,xs),y) = 2*y^2 >= 2*y^2 = f(Cons(x,xs),y) h(Nil(),y) = 4 + 2*y^2 >= 4 + 2*y^2 = h(Nil(),y) sp1(x,y) = 1 + x + 7*x*y + 3*x^2 + 2*y^2 >= 7*x*y + 2*x^2 + 2*y^2 = f(x,y) * Step 3: NaturalPI MAYBE + Considered Problem: - Strict TRS: f(Cons(x,xs),y) -> h(Cons(x,xs),y) g(Cons(x,xs),y) -> Cons(x,xs) h(Cons(x,xs),y) -> f(Cons(x,xs),y) h(Nil(),y) -> h(Nil(),y) - Weak TRS: f(Nil(),y) -> g(Nil(),y) g(Nil(),y) -> h(Nil(),y) r(x,y) -> x sp1(x,y) -> f(x,y) - Signature: {f/2,g/2,h/2,r/2,sp1/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,h,r,sp1} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: none Following symbols are considered usable: {f,g,h,r,sp1} TcT has computed the following interpretation: p(Cons) = x1 p(Nil) = 2 p(f) = 2*x1 + 2*x1^2 p(g) = 6 + x1 + x1^2 p(h) = 2*x1 + 2*x1^2 p(r) = 1 + 6*x1 + x1^2 p(sp1) = 4 + 4*x1 + x1*x2 + 2*x1^2 + 7*x2 Following rules are strictly oriented: g(Cons(x,xs),y) = 6 + x + x^2 > x = Cons(x,xs) Following rules are (at-least) weakly oriented: f(Cons(x,xs),y) = 2*x + 2*x^2 >= 2*x + 2*x^2 = h(Cons(x,xs),y) f(Nil(),y) = 12 >= 12 = g(Nil(),y) g(Nil(),y) = 12 >= 12 = h(Nil(),y) h(Cons(x,xs),y) = 2*x + 2*x^2 >= 2*x + 2*x^2 = f(Cons(x,xs),y) h(Nil(),y) = 12 >= 12 = h(Nil(),y) r(x,y) = 1 + 6*x + x^2 >= x = x sp1(x,y) = 4 + 4*x + x*y + 2*x^2 + 7*y >= 2*x + 2*x^2 = f(x,y) * Step 4: Failure MAYBE + Considered Problem: - Strict TRS: f(Cons(x,xs),y) -> h(Cons(x,xs),y) h(Cons(x,xs),y) -> f(Cons(x,xs),y) h(Nil(),y) -> h(Nil(),y) - Weak TRS: f(Nil(),y) -> g(Nil(),y) g(Cons(x,xs),y) -> Cons(x,xs) g(Nil(),y) -> h(Nil(),y) r(x,y) -> x sp1(x,y) -> f(x,y) - Signature: {f/2,g/2,h/2,r/2,sp1/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,g,h,r,sp1} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE