We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
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)
, equal(Capture(), Capture()) -> True()
, equal(Capture(), Swap()) -> False()
, equal(Swap(), Capture()) -> False()
, equal(Swap(), Swap()) -> True()
, goal(p1, p2, moves) -> game(p1, p2, moves) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The problem is match-bounded by 2. The enriched problem is
compatible with the following automaton.
{ @_0(2, 2) -> 1
, @_1(2, 2) -> 1
, @_1(2, 2) -> 3
, @_2(2, 2) -> 4
, Cons_0(2, 2) -> 1
, Cons_0(2, 2) -> 2
, Cons_0(2, 2) -> 3
, Cons_0(2, 2) -> 4
, Cons_1(2, 2) -> 1
, Cons_1(2, 2) -> 2
, Cons_1(2, 2) -> 3
, Cons_1(2, 2) -> 4
, Cons_1(2, 3) -> 1
, Cons_1(2, 3) -> 3
, Cons_1(2, 3) -> 4
, Cons_2(2, 4) -> 1
, Cons_2(2, 4) -> 3
, Cons_2(2, 4) -> 4
, Nil_0() -> 1
, Nil_0() -> 2
, Nil_0() -> 3
, Nil_0() -> 4
, game_0(2, 2, 2) -> 1
, game_1(2, 2, 2) -> 1
, Capture_0() -> 1
, Capture_0() -> 2
, Capture_0() -> 3
, Capture_0() -> 4
, Swap_0() -> 1
, Swap_0() -> 2
, Swap_0() -> 3
, Swap_0() -> 4
, equal_0(2, 2) -> 1
, True_0() -> 1
, True_0() -> 2
, True_0() -> 3
, True_0() -> 4
, True_1() -> 1
, False_0() -> 1
, False_0() -> 2
, False_0() -> 3
, False_0() -> 4
, False_1() -> 1
, goal_0(2, 2, 2) -> 1 }
Hurray, we answered YES(?,O(n^1))