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: Sum. 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: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: 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: NaturalMI. 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: 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(@) = [1] x2 + [10] p(Capture) = [1] p(Cons) = [1] x2 + [0] p(False) = [4] p(Nil) = [9] p(Swap) = [0] p(True) = [0] p(equal) = [1] x1 + [6] x2 + [3] p(game) = [1] x1 + [1] x2 + [2] x3 + [0] p(goal) = [1] x1 + [1] x2 + [4] x3 + [10] Following rules are strictly oriented: @(Nil(),ys) = [1] ys + [10] > [1] ys + [0] = ys equal(Capture(),Capture()) = [10] > [0] = True() equal(Swap(),Capture()) = [9] > [4] = False() equal(Swap(),Swap()) = [3] > [0] = True() game(p1,p2,Nil()) = [1] p1 + [1] p2 + [18] > [1] p2 + [10] = @(p1,p2) goal(p1,p2,moves) = [4] moves + [1] p1 + [1] p2 + [10] > [2] moves + [1] p1 + [1] p2 + [0] = game(p1,p2,moves) Following rules are (at-least) weakly oriented: @(Cons(x,xs),ys) = [1] ys + [10] >= [1] ys + [10] = Cons(x,@(xs,ys)) equal(Capture(),Swap()) = [4] >= [4] = False() game(p1,p2,Cons(Swap(),xs)) = [1] p1 + [1] p2 + [2] xs + [0] >= [1] p1 + [1] p2 + [2] xs + [0] = game(p2,p1,xs) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = [1] p1 + [2] xs + [1] xs' + [0] >= [1] p1 + [2] xs + [1] xs' + [0] = game(Cons(x',p1),xs',xs) ** Step 1.b:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) equal(Capture(),Swap()) -> False() game(p1,p2,Cons(Swap(),xs)) -> game(p2,p1,xs) game(p1,Cons(x',xs'),Cons(Capture(),xs)) -> game(Cons(x',p1),xs',xs) - Weak TRS: @(Nil(),ys) -> ys equal(Capture(),Capture()) -> True() equal(Swap(),Capture()) -> False() equal(Swap(),Swap()) -> True() game(p1,p2,Nil()) -> @(p1,p2) 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: 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(@) = [2] x1 + [1] x2 + [9] p(Capture) = [0] p(Cons) = [1] x1 + [1] x2 + [1] p(False) = [10] p(Nil) = [0] p(Swap) = [0] p(True) = [10] p(equal) = [10] p(game) = [4] x1 + [4] x2 + [8] x3 + [10] p(goal) = [5] x1 + [4] x2 + [8] x3 + [10] Following rules are strictly oriented: @(Cons(x,xs),ys) = [2] x + [2] xs + [1] ys + [11] > [1] x + [2] xs + [1] ys + [10] = Cons(x,@(xs,ys)) game(p1,p2,Cons(Swap(),xs)) = [4] p1 + [4] p2 + [8] xs + [18] > [4] p1 + [4] p2 + [8] xs + [10] = game(p2,p1,xs) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = [4] p1 + [4] x' + [8] xs + [4] xs' + [22] > [4] p1 + [4] x' + [8] xs + [4] xs' + [14] = game(Cons(x',p1),xs',xs) Following rules are (at-least) weakly oriented: @(Nil(),ys) = [1] ys + [9] >= [1] ys + [0] = ys equal(Capture(),Capture()) = [10] >= [10] = True() equal(Capture(),Swap()) = [10] >= [10] = False() equal(Swap(),Capture()) = [10] >= [10] = False() equal(Swap(),Swap()) = [10] >= [10] = True() game(p1,p2,Nil()) = [4] p1 + [4] p2 + [10] >= [2] p1 + [1] p2 + [9] = @(p1,p2) goal(p1,p2,moves) = [8] moves + [5] p1 + [4] p2 + [10] >= [8] moves + [4] p1 + [4] p2 + [10] = game(p1,p2,moves) ** Step 1.b:3: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: equal(Capture(),Swap()) -> False() - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys equal(Capture(),Capture()) -> True() 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: 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(@) = [1] x1 + [1] x2 + [0] p(Capture) = [4] p(Cons) = [1] x2 + [8] p(False) = [0] p(Nil) = [0] p(Swap) = [0] p(True) = [0] p(equal) = [5] p(game) = [1] x1 + [1] x2 + [1] x3 + [12] p(goal) = [1] x1 + [1] x2 + [1] x3 + [12] Following rules are strictly oriented: equal(Capture(),Swap()) = [5] > [0] = False() Following rules are (at-least) weakly oriented: @(Cons(x,xs),ys) = [1] xs + [1] ys + [8] >= [1] xs + [1] ys + [8] = Cons(x,@(xs,ys)) @(Nil(),ys) = [1] ys + [0] >= [1] ys + [0] = ys equal(Capture(),Capture()) = [5] >= [0] = True() equal(Swap(),Capture()) = [5] >= [0] = False() equal(Swap(),Swap()) = [5] >= [0] = True() game(p1,p2,Cons(Swap(),xs)) = [1] p1 + [1] p2 + [1] xs + [20] >= [1] p1 + [1] p2 + [1] xs + [12] = game(p2,p1,xs) game(p1,p2,Nil()) = [1] p1 + [1] p2 + [12] >= [1] p1 + [1] p2 + [0] = @(p1,p2) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = [1] p1 + [1] xs + [1] xs' + [28] >= [1] p1 + [1] xs + [1] xs' + [20] = game(Cons(x',p1),xs',xs) goal(p1,p2,moves) = [1] moves + [1] p1 + [1] p2 + [12] >= [1] moves + [1] p1 + [1] p2 + [12] = game(p1,p2,moves) ** Step 1.b:4: 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))