*** 1 Progress [(O(1),O(n^1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: @(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) Weak DP Rules: Weak TRS Rules: Signature: {@/2,equal/2,game/3,goal/3} / {Capture/0,Cons/2,False/0,Nil/0,Swap/0,True/0} Obligation: Innermost basic terms: {@,equal,game,goal}/{Capture,Cons,False,Nil,Swap,True} Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} Proof: The problem is match-bounded by 2. The enriched problem is compatible with follwoing automaton. @_0(2,2) -> 1 @_1(2,2) -> 1 @_1(2,2) -> 3 @_2(2,2) -> 4 Capture_0() -> 1 Capture_0() -> 2 Capture_0() -> 3 Capture_0() -> 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 False_0() -> 1 False_0() -> 2 False_0() -> 3 False_0() -> 4 False_1() -> 1 Nil_0() -> 1 Nil_0() -> 2 Nil_0() -> 3 Nil_0() -> 4 Swap_0() -> 1 Swap_0() -> 2 Swap_0() -> 3 Swap_0() -> 4 True_0() -> 1 True_0() -> 2 True_0() -> 3 True_0() -> 4 True_1() -> 1 equal_0(2,2) -> 1 game_0(2,2,2) -> 1 game_1(2,2,2) -> 1 goal_0(2,2,2) -> 1 2 -> 1 2 -> 3 2 -> 4 *** 1.1 Progress [(O(1),O(1))] *** Considered Problem: Strict DP Rules: Strict TRS Rules: Weak DP Rules: Weak TRS Rules: @(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 basic terms: {@,equal,game,goal}/{Capture,Cons,False,Nil,Swap,True} Applied Processor: EmptyProcessor Proof: The problem is already closed. The intended complexity is O(1).