WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys 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,game/3,goal/3} / {Capture/0,Cons/2,Nil/0,Swap/0} - Obligation: innermost runtime complexity wrt. defined symbols {@,game,goal} and constructors {Capture,Cons,Nil,Swap} + 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: {@,game,goal} TcT has computed the following interpretation: p(@) = [1] x1 + [1] x2 + [10] p(Capture) = [0] p(Cons) = [1] x1 + [1] x2 + [0] p(Nil) = [12] p(Swap) = [9] p(game) = [4] x1 + [4] x2 + [2] x3 + [2] p(goal) = [4] x1 + [5] x2 + [8] x3 + [9] Following rules are strictly oriented: @(Nil(),ys) = [1] ys + [22] > [1] ys + [0] = ys game(p1,p2,Cons(Swap(),xs)) = [4] p1 + [4] p2 + [2] xs + [20] > [4] p1 + [4] p2 + [2] xs + [2] = game(p2,p1,xs) game(p1,p2,Nil()) = [4] p1 + [4] p2 + [26] > [1] p1 + [1] p2 + [10] = @(p1,p2) goal(p1,p2,moves) = [8] moves + [4] p1 + [5] p2 + [9] > [2] moves + [4] p1 + [4] p2 + [2] = game(p1,p2,moves) Following rules are (at-least) weakly oriented: @(Cons(x,xs),ys) = [1] x + [1] xs + [1] ys + [10] >= [1] x + [1] xs + [1] ys + [10] = Cons(x,@(xs,ys)) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = [4] p1 + [4] x' + [2] xs + [4] xs' + [2] >= [4] p1 + [4] x' + [2] xs + [4] xs' + [2] = game(Cons(x',p1),xs',xs) * Step 2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) game(p1,Cons(x',xs'),Cons(Capture(),xs)) -> game(Cons(x',p1),xs',xs) - Weak TRS: @(Nil(),ys) -> ys game(p1,p2,Cons(Swap(),xs)) -> game(p2,p1,xs) game(p1,p2,Nil()) -> @(p1,p2) goal(p1,p2,moves) -> game(p1,p2,moves) - Signature: {@/2,game/3,goal/3} / {Capture/0,Cons/2,Nil/0,Swap/0} - Obligation: innermost runtime complexity wrt. defined symbols {@,game,goal} and constructors {Capture,Cons,Nil,Swap} + 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: {@,game,goal} TcT has computed the following interpretation: p(@) = [2] x1 + [2] x2 + [3] p(Capture) = [13] p(Cons) = [1] x1 + [1] x2 + [0] p(Nil) = [8] p(Swap) = [1] p(game) = [2] x1 + [2] x2 + [2] x3 + [1] p(goal) = [3] x1 + [3] x2 + [8] x3 + [5] Following rules are strictly oriented: game(p1,Cons(x',xs'),Cons(Capture(),xs)) = [2] p1 + [2] x' + [2] xs + [2] xs' + [27] > [2] p1 + [2] x' + [2] xs + [2] xs' + [1] = game(Cons(x',p1),xs',xs) Following rules are (at-least) weakly oriented: @(Cons(x,xs),ys) = [2] x + [2] xs + [2] ys + [3] >= [1] x + [2] xs + [2] ys + [3] = Cons(x,@(xs,ys)) @(Nil(),ys) = [2] ys + [19] >= [1] ys + [0] = ys game(p1,p2,Cons(Swap(),xs)) = [2] p1 + [2] p2 + [2] xs + [3] >= [2] p1 + [2] p2 + [2] xs + [1] = game(p2,p1,xs) game(p1,p2,Nil()) = [2] p1 + [2] p2 + [17] >= [2] p1 + [2] p2 + [3] = @(p1,p2) goal(p1,p2,moves) = [8] moves + [3] p1 + [3] p2 + [5] >= [2] moves + [2] p1 + [2] p2 + [1] = game(p1,p2,moves) * Step 3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) - Weak TRS: @(Nil(),ys) -> ys 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,game/3,goal/3} / {Capture/0,Cons/2,Nil/0,Swap/0} - Obligation: innermost runtime complexity wrt. defined symbols {@,game,goal} and constructors {Capture,Cons,Nil,Swap} + 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: {@,game,goal} TcT has computed the following interpretation: p(@) = [4] x1 + [1] x2 + [0] p(Capture) = [0] p(Cons) = [1] x2 + [2] p(Nil) = [0] p(Swap) = [0] p(game) = [8] x1 + [8] x2 + [2] x3 + [8] p(goal) = [8] x1 + [8] x2 + [2] x3 + [13] Following rules are strictly oriented: @(Cons(x,xs),ys) = [4] xs + [1] ys + [8] > [4] xs + [1] ys + [2] = Cons(x,@(xs,ys)) Following rules are (at-least) weakly oriented: @(Nil(),ys) = [1] ys + [0] >= [1] ys + [0] = ys game(p1,p2,Cons(Swap(),xs)) = [8] p1 + [8] p2 + [2] xs + [12] >= [8] p1 + [8] p2 + [2] xs + [8] = game(p2,p1,xs) game(p1,p2,Nil()) = [8] p1 + [8] p2 + [8] >= [4] p1 + [1] p2 + [0] = @(p1,p2) game(p1,Cons(x',xs'),Cons(Capture(),xs)) = [8] p1 + [2] xs + [8] xs' + [28] >= [8] p1 + [2] xs + [8] xs' + [24] = game(Cons(x',p1),xs',xs) goal(p1,p2,moves) = [2] moves + [8] p1 + [8] p2 + [13] >= [2] moves + [8] p1 + [8] p2 + [8] = game(p1,p2,moves) * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: @(Cons(x,xs),ys) -> Cons(x,@(xs,ys)) @(Nil(),ys) -> ys 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,game/3,goal/3} / {Capture/0,Cons/2,Nil/0,Swap/0} - Obligation: innermost runtime complexity wrt. defined symbols {@,game,goal} and constructors {Capture,Cons,Nil,Swap} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))