WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),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: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(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: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: @(y,z){y -> Cons(x,y)} = @(Cons(x,y),z) ->^+ Cons(x,@(y,z)) = C[@(y,z) = @(y,z){}] ** Step 1.b: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 = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + 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(@) = x1 + 2*x2 p(Capture) = 4 p(Cons) = x1 + x2 p(False) = 15 p(Nil) = 4 p(Swap) = 6 p(True) = 0 p(equal) = 7 + x1 + 3*x2 p(game) = 1 + 2*x1 + 2*x2 + 4*x3 p(goal) = 8 + 8*x1 + 2*x2 + 9*x3 Following rules are strictly oriented: @(Nil(),ys) = 4 + 2*ys > ys = ys equal(Capture(),Capture()) = 23 > 0 = True() equal(Capture(),Swap()) = 29 > 15 = False() equal(Swap(),Capture()) = 25 > 15 = False() equal(Swap(),Swap()) = 31 > 0 = True() game(p1,p2,Cons(Swap(),xs)) = 25 + 2*p1 + 2*p2 + 4*xs > 1 + 2*p1 + 2*p2 + 4*xs = game(p2,p1,xs) game(p1,p2,Nil()) = 17 + 2*p1 + 2*p2 > p1 + 2*p2 = @(p1,p2) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = 17 + 2*p1 + 2*x' + 4*xs + 2*xs' > 1 + 2*p1 + 2*x' + 4*xs + 2*xs' = game(Cons(x',p1),xs',xs) goal(p1,p2,moves) = 8 + 9*moves + 8*p1 + 2*p2 > 1 + 4*moves + 2*p1 + 2*p2 = game(p1,p2,moves) Following rules are (at-least) weakly oriented: @(Cons(x,xs),ys) = x + xs + 2*ys >= x + xs + 2*ys = Cons(x,@(xs,ys)) ** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) - Weak TRS: @(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 = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + 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(@) = 8*x1 + 2*x2 p(Capture) = 0 p(Cons) = 2 + x2 p(False) = 0 p(Nil) = 0 p(Swap) = 0 p(True) = 0 p(equal) = 0 p(game) = 8*x1 + 8*x2 p(goal) = 8*x1 + 8*x2 Following rules are strictly oriented: @(Cons(x,xs),ys) = 16 + 8*xs + 2*ys > 2 + 8*xs + 2*ys = Cons(x,@(xs,ys)) Following rules are (at-least) weakly oriented: @(Nil(),ys) = 2*ys >= ys = ys equal(Capture(),Capture()) = 0 >= 0 = True() equal(Capture(),Swap()) = 0 >= 0 = False() equal(Swap(),Capture()) = 0 >= 0 = False() equal(Swap(),Swap()) = 0 >= 0 = True() game(p1,p2,Cons(Swap(),xs)) = 8*p1 + 8*p2 >= 8*p1 + 8*p2 = game(p2,p1,xs) game(p1,p2,Nil()) = 8*p1 + 8*p2 >= 8*p1 + 2*p2 = @(p1,p2) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = 16 + 8*p1 + 8*xs' >= 16 + 8*p1 + 8*xs' = game(Cons(x',p1),xs',xs) goal(p1,p2,moves) = 8*p1 + 8*p2 >= 8*p1 + 8*p2 = game(p1,p2,moves) ** Step 1.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))