Runtime Complexity TRS:
The TRS R consists of the following rules:

@(Cons(x, xs), ys) → Cons(x, @(xs, ys))
@(Nil, ys) → ys
game(p1, p2, Cons(Capture, xs)) → game[Ite][False][Ite][False][Ite](True, p1, p2, Cons(Capture, xs))
game(p1, p2, Cons(Swap, xs)) → game(p2, p1, xs)
equal(Capture, Capture) → True
equal(Capture, Swap) → False
equal(Swap, Capture) → False
equal(Swap, Swap) → True
game(p1, p2, Nil) → @(p1, p2)
goal(p1, p2, moves) → game(p1, p2, moves)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

@'(Cons'(x, xs), ys) → Cons'(x, @'(xs, ys))
@'(Nil', ys) → ys
game'(p1, p2, Cons'(Capture', xs)) → game[Ite][False][Ite][False][Ite]'(True', p1, p2, Cons'(Capture', xs))
game'(p1, p2, Cons'(Swap', xs)) → game'(p2, p1, xs)
equal'(Capture', Capture') → True'
equal'(Capture', Swap') → False'
equal'(Swap', Capture') → False'
equal'(Swap', Swap') → True'
game'(p1, p2, Nil') → @'(p1, p2)
goal'(p1, p2, moves) → game'(p1, p2, moves)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
game[Ite][False][Ite][False][Ite]'/0
game[Ite][False][Ite][False][Ite]'/1
game[Ite][False][Ite][False][Ite]'/2
game[Ite][False][Ite][False][Ite]'/3

Runtime Complexity TRS:
The TRS R consists of the following rules:

@'(Cons'(x, xs), ys) → Cons'(x, @'(xs, ys))
@'(Nil', ys) → ys
game'(p1, p2, Cons'(Capture', xs)) → game[Ite][False][Ite][False][Ite]'
game'(p1, p2, Cons'(Swap', xs)) → game'(p2, p1, xs)
equal'(Capture', Capture') → True'
equal'(Capture', Swap') → False'
equal'(Swap', Capture') → False'
equal'(Swap', Swap') → True'
game'(p1, p2, Nil') → @'(p1, p2)
goal'(p1, p2, moves) → game'(p1, p2, moves)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
@'(Cons'(x, xs), ys) → Cons'(x, @'(xs, ys))
@'(Nil', ys) → ys
game'(p1, p2, Cons'(Capture', xs)) → game[Ite][False][Ite][False][Ite]'
game'(p1, p2, Cons'(Swap', xs)) → game'(p2, p1, xs)
equal'(Capture', Capture') → True'
equal'(Capture', Swap') → False'
equal'(Swap', Capture') → False'
equal'(Swap', Swap') → True'
game'(p1, p2, Nil') → @'(p1, p2)
goal'(p1, p2, moves) → game'(p1, p2, moves)

Types:
@' :: Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]'
Cons' :: Capture':Swap' → Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]'
Nil' :: Cons':Nil':game[Ite][False][Ite][False][Ite]'
game' :: Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]'
Capture' :: Capture':Swap'
game[Ite][False][Ite][False][Ite]' :: Cons':Nil':game[Ite][False][Ite][False][Ite]'
Swap' :: Capture':Swap'
equal' :: Capture':Swap' → Capture':Swap' → True':False'
True' :: True':False'
False' :: True':False'
goal' :: Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]' → Cons':Nil':game[Ite][False][Ite][False][Ite]'
_hole_Cons':Nil':game[Ite][False][Ite][False][Ite]'1 :: Cons':Nil':game[Ite][False][Ite][False][Ite]'
_hole_Capture':Swap'2 :: Capture':Swap'
_hole_True':False'3 :: True':False'
_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4 :: Nat → Cons':Nil':game[Ite][False][Ite][False][Ite]'

Heuristically decided to analyse the following defined symbols:
@', game'

They will be analysed ascendingly in the following order:
@' < game'

Generator Equations:
_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(0) ⇔ Nil'
_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(+(x, 1)) ⇔ Cons'(Capture', _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(x))

The following defined symbols remain to be analysed:
@', game'

They will be analysed ascendingly in the following order:
@' < game'

Proved the following rewrite lemma:
@'(_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(_n6), _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(b)) → _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(+(_n6, b)), rt ∈ Ω(1 + _n6)

Induction Base:
@'(_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(0), _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(b)) →_R^Ω(1)
_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(b)

Induction Step:
@'(_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(+(_$n7, 1)), _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(_b146)) →_R^Ω(1)
Cons'(Capture', @'(_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(_$n7), _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(_b146))) →_IH
Cons'(Capture', _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(+(_$n7, _b146)))

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

Lemmas:
@'(_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(_n6), _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(b)) → _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(+(_n6, b)), rt ∈ Ω(1 + _n6)

The following defined symbols remain to be analysed:
game'

Could not prove a rewrite lemma for the defined symbol game'.

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
@'(_gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(_n6), _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(b)) → _gen_Cons':Nil':game[Ite][False][Ite][False][Ite]'4(+(_n6, b)), rt ∈ Ω(1 + _n6)