WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys equal(Capture(),Capture()) -> True() equal(Capture(),Swap()) -> False() equal(Swap(),Capture()) -> False() equal(Swap(),Swap()) -> True() game(p1,p2,Cons(Swap(),xs)) -> game(p2,p1,xs) game(p1,p2,Nil()) -> @(p1,p2) game(p1,Cons(x',xs'),Cons(Capture(),xs)) -> game(Cons(x',p1),xs',xs) goal(p1,p2,moves) -> game(p1,p2,moves) - Signature: {@/2,equal/2,game/3,goal/3} / {Capture/0,Cons/2,False/0,Nil/0,Swap/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {@,equal,game,goal} and constructors {Capture,Cons,False ,Nil,Swap,True} + Applied Processor: NaturalPI {shape = Linear, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(Cons) = {2} Following symbols are considered usable: {@,equal,game,goal} TcT has computed the following interpretation: p(@) = 9 + 2*x1 + 2*x2 p(Capture) = 2 p(Cons) = 8 + x2 p(False) = 4 p(Nil) = 11 p(Swap) = 0 p(True) = 10 p(equal) = 11 + 10*x1 p(game) = 2*x1 + 2*x2 + x3 p(goal) = 2 + 8*x1 + 10*x2 + 3*x3 Following rules are strictly oriented: @(Cons(x,xs),ys) = 25 + 2*xs + 2*ys > 17 + 2*xs + 2*ys = Cons(x,@(xs,ys)) @(Nil(),ys) = 31 + 2*ys > ys = ys equal(Capture(),Capture()) = 31 > 10 = True() equal(Capture(),Swap()) = 31 > 4 = False() equal(Swap(),Capture()) = 11 > 4 = False() equal(Swap(),Swap()) = 11 > 10 = True() game(p1,p2,Cons(Swap(),xs)) = 8 + 2*p1 + 2*p2 + xs > 2*p1 + 2*p2 + xs = game(p2,p1,xs) game(p1,p2,Nil()) = 11 + 2*p1 + 2*p2 > 9 + 2*p1 + 2*p2 = @(p1,p2) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = 24 + 2*p1 + xs + 2*xs' > 16 + 2*p1 + xs + 2*xs' = game(Cons(x',p1),xs',xs) goal(p1,p2,moves) = 2 + 3*moves + 8*p1 + 10*p2 > moves + 2*p1 + 2*p2 = game(p1,p2,moves) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))