YES Problem: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x63,x55,runParser_0(),Nil(),S(x12)) -> ParseSuccess(Nil()) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](eos(),x31,x27,x76,Cons(x60,x44),S(x28)) -> ParseFail(S(x28)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5,x4,x3,Cons(A(),x2),S(x1)) -> ParseFail(S(S(x1))) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5,x4,x3,Cons(C(),x2),S(x1)) -> ParseFail(S(S(x1))) bind'_0[6](return_x(),x11,x9,runParser_0(),x4,S(x2)) -> ParseSuccess(x4) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))),bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) main(x3) -> rec[string_0][6](bot[1](),x3) main(x3) -> rec[string_0][6](bot[3](),x3) main(x3) -> rec[string_0][6](bot[5](),x3) Proof: Matrix Interpretation Processor: dim=3 interpretation: [0] [bot[5]] = [1] [0], [0] [bot[3]] = [0] [1], [0] [bot[1]] = [0] [0], [1 1 0] [1] [main](x0) = [0 0 0]x0 + [1] [1 0 1] [1], [0] [0] = [1] [0], [1 0 0] [1 0 0] [1] [rec[string_0][6]](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [1] [0 1 1] [1 0 0] [0], [0] [bot[6]] = [0] [0], [0] [C] = [0] [0], [0] [B] = [0] [1], [0] [A] = [0] [0], [1] [return_x] = [0] [0], [1 0 0] [1 0 0] [bind_p_f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [0] [filter_0] = [0] [0], [0] [any] = [0] [0], [1 0 0] [1] [ParseFail](x0) = [0 0 1]x0 + [0] [0 0 0] [0], [1 0 0] [1 0 1] [Cons](x0, x1) = [0 0 1]x0 + [0 0 0]x1 [0 0 1] [0 0 0] , [0] [Unit] = [0] [0], [0] [bind_1] = [0] [0], [1 0 0] [ParseSuccess](x0) = [0 0 0]x0 [0 0 0] , [0] [Nil] = [0] [0], [0] [runParser_0] = [0] [0], [0] [eos] = [0] [1], [0] [bot[4]] = [0] [0], [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [bind'_0[6]](x0, x1, x2, x3, x4, x5) = [1 0 1]x0 + [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 0]x5 [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 1] [0 0 0] , [0] [bot[2]] = [0] [0], [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [bind_1[4]](x0, x1, x2, x3, x4) = [1 0 0]x0 + [0 0 0]x1 + [0 1 0]x2 + [0 0 0]x3 + [0 0 0]x4 [0 0 0] [0 0 0] [0 0 0] [1 0 1] [0 0 0] , [1 0 0] [0] [S](x0) = [0 1 0]x0 + [0] [0 0 0] [1], [1 0 1] [bind'_0](x0) = [0 0 0]x0 [1 0 0] orientation: [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 1 0]x3 + [0 0 0]x4 + [1 0 1]x5 >= [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [1 0 1]x5 = bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 1 0]x3 + [0 0 0]x4 + [1 0 1]x5 >= [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [1 0 1]x5 = bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1 0 0] [1 0 0] [1] [0] bind'_0[6](eos(),x63,x55,runParser_0(),Nil(),S(x12)) = [0 0 0]x12 + [0 0 0]x55 + [0 0 0]x63 + [1] >= [0] = ParseSuccess(Nil()) [0 0 0] [0 0 0] [0 0 0] [0] [0] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 0] [1] bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [1] >= [0 0 0]x1 + [1] = bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) [0 0 0] [0 0 0] [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1 0 0] [1 0 0] [1] [1 0 0] [1] bind'_0[6](eos(),x31,x27,x76,Cons(x60,x44),S(x28)) = [0 0 0]x27 + [0 0 0]x28 + [0 0 0]x31 + [0 0 0]x44 + [0 0 0]x60 + [0 0 0]x76 + [1] >= [0 0 0]x28 + [1] = ParseFail(S(x28)) [0 0 0] [0 0 0] [0 0 0] [1 0 1] [1 0 1] [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 0] [1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4, x3,x2,Nil(),S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [1] >= [0 0 0]x1 + [1] = ParseFail(S(x1)) [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 0] [1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5, x4,x3,Cons(A(),x2),S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 0]x5 + [1] >= [0 0 0]x1 + [1] = ParseFail(S(S(x1))) [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1 0 0] [1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5, x4,x3,Cons(B(),x2),S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 0]x5 + [1] >= [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [1] = bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [1] [0 0 0] [1 0 1] [0 0 0] [0] [1 0 0] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 0] [1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5, x4,x3,Cons(C(),x2),S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 0]x5 + [1] >= [0 0 0]x1 + [1] = ParseFail(S(S(x1))) [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 0] bind'_0[6](return_x(),x11,x9,runParser_0(),x4,S(x2)) = [0 0 0]x11 + [0 0 0]x2 + [0 0 0]x4 + [0 0 0]x9 + [1] >= [0 0 0]x4 = ParseSuccess(x4) [0 0 0] [0 0 0] [1 0 1] [0 0 0] [0] [0 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 0] [1 0 0] [1] bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) = [0 0 0]x11 + [0 0 0]x2 + [0 0 0]x4 + [0 0 0]x9 + [1] >= [0 0 0]x2 + [0 0 0]x4 + [1] = bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) [0 0 0] [0 0 0] [1 0 1] [0 0 0] [0] [0 0 0] [1 0 1] [0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) = [0 0 0]x1 + [0 0 0]x2 + [0 1 0]x3 + [0 0 0]x4 + [1 0 1]x5 >= [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [1 0 1]x5 = bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [1 0 1] [0 0 0] [0 0 0] [0 0 0] [1 0 0] [1] [1] rec[string_0][6](x23,Nil()) = [0 0 0]x23 + [1] >= [0] = ParseFail(0()) [0 1 1] [0] [0] [1 0 1] [1 0 0] [1] [1 0 0] [1] rec[string_0][6](x23,Cons(A(),x2)) = [0 0 0]x2 + [0 0 0]x23 + [1] >= [0 0 0]x2 + [1] = bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) [1 0 1] [0 1 1] [0] [1 0 1] [0] [1 0 1] [1 0 0] [1] [1] rec[string_0][6](x23,Cons(B(),x2)) = [0 0 0]x2 + [0 0 0]x23 + [1] >= [1] = ParseFail(S(0())) [1 0 1] [0 1 1] [0] [0] [1 0 1] [1 0 0] [1] [1] rec[string_0][6](x23,Cons(C(),x2)) = [0 0 0]x2 + [0 0 0]x23 + [1] >= [1] = ParseFail(S(0())) [1 0 1] [0 1 1] [0] [0] [1 1 0] [1] [1 0 0] [1] main(x3) = [0 0 0]x3 + [1] >= [0 0 0]x3 + [1] = rec[string_0][6](bot[1](),x3) [1 0 1] [1] [1 0 0] [0] [1 1 0] [1] [1 0 0] [1] main(x3) = [0 0 0]x3 + [1] >= [0 0 0]x3 + [1] = rec[string_0][6](bot[3](),x3) [1 0 1] [1] [1 0 0] [1] [1 1 0] [1] [1 0 0] [1] main(x3) = [0 0 0]x3 + [1] >= [0 0 0]x3 + [1] = rec[string_0][6](bot[5](),x3) [1 0 1] [1] [1 0 0] [1] problem: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](eos(),x31,x27,x76,Cons(x60,x44),S(x28)) -> ParseFail(S(x28)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5,x4,x3,Cons(A(),x2),S(x1)) -> ParseFail(S(S(x1))) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5,x4,x3,Cons(C(),x2),S(x1)) -> ParseFail(S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) main(x3) -> rec[string_0][6](bot[1](),x3) main(x3) -> rec[string_0][6](bot[3](),x3) main(x3) -> rec[string_0][6](bot[5](),x3) Matrix Interpretation Processor: dim=3 interpretation: [0] [bot[5]] = [0] [0], [0] [bot[3]] = [0] [1], [0] [bot[1]] = [0] [0], [1 0 1] [1] [main](x0) = [0 1 1]x0 + [0] [1 1 1] [1], [0] [0] = [0] [1], [1 0 0] [1 0 1] [rec[string_0][6]](x0, x1) = [0 0 0]x0 + [0 1 1]x1 [0 0 1] [0 1 1] , [0] [bot[6]] = [0] [0], [0] [C] = [1] [0], [0] [B] = [0] [1], [0] [A] = [1] [0], [0] [return_x] = [1] [1], [1 0 0] [1 0 0] [bind_p_f](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [0] [filter_0] = [0] [0], [0] [any] = [0] [0], [1 1 0] [ParseFail](x0) = [0 0 0]x0 [0 0 0] , [1 0 1] [1 0 1] [Cons](x0, x1) = [0 0 0]x0 + [1 1 0]x1 [0 1 0] [0 0 0] , [0] [Unit] = [0] [0], [0] [bind_1] = [0] [1], [0] [Nil] = [0] [0], [0] [runParser_0] = [0] [0], [1] [eos] = [0] [1], [0] [bot[4]] = [0] [0], [1 1 0] [1 0 0] [1 0 0] [1 0 0] [1 0 1] [1 0 1] [bind'_0[6]](x0, x1, x2, x3, x4, x5) = [0 0 1]x0 + [0 0 0]x1 + [0 0 0]x2 + [0 0 0]x3 + [1 0 0]x4 + [0 0 1]x5 [0 0 0] [0 0 0] [0 0 0] [0 0 1] [1 0 0] [0 0 0] , [0] [bot[2]] = [0] [0], [1 0 1] [1 0 0] [1 0 0] [1 0 1] [1 1 0] [bind_1[4]](x0, x1, x2, x3, x4) = [0 1 0]x0 + [0 0 0]x1 + [0 0 0]x2 + [1 0 0]x3 + [0 0 1]x4 [0 1 0] [0 0 1] [0 0 0] [1 0 0] [0 0 0] , [1 0 0] [S](x0) = [0 0 1]x0 [0 0 1] , [1 0 0] [bind'_0](x0) = [0 0 1]x0 [0 1 0] orientation: [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 1 0] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 1 0] bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) = [0 0 1]x1 + [1 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 1]x5 >= [0 0 1]x1 + [1 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 1]x5 = bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) [0 0 0] [1 0 0] [0 0 0] [0 0 1] [0 0 1] [0 0 0] [1 0 0] [0 0 0] [0 0 1] [0 0 0] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 1 0] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 1 0] bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) = [0 0 1]x1 + [1 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 1]x5 >= [0 0 1]x1 + [1 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 1]x5 = bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) [0 0 0] [1 0 0] [0 0 0] [0 0 1] [0 0 1] [0 0 0] [1 0 0] [0 0 0] [0 0 1] [0 0 0] [1 0 1] [1 0 0] [1 0 0] [1] [1 0 1] [1] bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) = [0 0 1]x1 + [0 0 0]x2 + [0 0 0]x3 + [1] >= [0 0 1]x1 + [1] = bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) [0 0 0] [0 0 0] [0 0 0] [1] [0 0 0] [1] [1 0 0] [1 0 1] [1 0 0] [1 0 1] [1 1 1] [1 0 0] [1] [1 0 1] bind'_0[6](eos(),x31,x27,x76,Cons(x60,x44),S(x28)) = [0 0 0]x27 + [0 0 1]x28 + [0 0 0]x31 + [1 0 1]x44 + [1 0 1]x60 + [0 0 0]x76 + [1] >= [0 0 0]x28 = ParseFail(S(x28)) [0 0 0] [0 0 0] [0 0 0] [1 0 1] [1 0 1] [0 0 1] [0] [0 0 0] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1 0 1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4, x3,x2,Nil(),S(x1)) = [0 0 1]x1 + [0 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 >= [0 0 0]x1 = ParseFail(S(x1)) [0 0 0] [0 0 1] [0 0 0] [0 0 0] [0 0 0] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5, x4,x3,Cons(A(),x2),S(x1)) = [0 0 1]x1 + [1 0 1]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 0]x5 + [0] >= [0 0 0]x1 = ParseFail(S(S(x1))) [0 0 0] [1 0 1] [0 0 1] [0 0 0] [0 0 0] [0] [0 0 0] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 1] [1 0 1] [1 0 0] [1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5, x4,x3,Cons(B(),x2),S(x1)) = [0 0 1]x1 + [1 0 1]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 0]x5 + [1] >= [0 0 1]x1 + [1 0 0]x2 + [0 0 0]x3 + [1] = bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) [0 0 0] [1 0 1] [0 0 1] [0 0 0] [0 0 0] [1] [0 0 0] [1 0 0] [0 0 1] [1] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 0 0] [1] [1 0 1] bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5, x4,x3,Cons(C(),x2),S(x1)) = [0 0 1]x1 + [1 0 1]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 0]x5 + [0] >= [0 0 0]x1 = ParseFail(S(S(x1))) [0 0 0] [1 0 1] [0 0 1] [0 0 0] [0 0 0] [0] [0 0 0] [1 0 0] [1 0 1] [1 0 1] [1 0 0] [1] [1 0 1] [1 0 1] [1] bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) = [0 0 0]x11 + [0 0 1]x2 + [1 0 0]x4 + [0 0 0]x9 + [1] >= [0 0 1]x2 + [1 0 0]x4 + [1] = bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) [0 0 0] [0 0 0] [1 0 0] [0 0 0] [1] [0 0 0] [1 0 0] [1] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 1 0] [1 0 1] [1 0 1] [1 0 0] [1 0 0] [1 1 0] bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) = [0 0 1]x1 + [1 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 1]x5 >= [0 0 1]x1 + [1 0 0]x2 + [0 0 0]x3 + [0 0 0]x4 + [0 0 1]x5 = bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) [0 0 0] [1 0 0] [0 0 0] [0 0 1] [0 0 1] [0 0 0] [1 0 0] [0 0 0] [0 0 1] [0 0 0] [1 0 0] [0] rec[string_0][6](x23,Nil()) = [0 0 0]x23 >= [0] = ParseFail(0()) [0 0 1] [0] [1 0 1] [1 0 0] [1] [1 0 1] [1] rec[string_0][6](x23,Cons(A(),x2)) = [1 1 0]x2 + [0 0 0]x23 + [1] >= [1 0 0]x2 + [1] = bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) [1 1 0] [0 0 1] [1] [1 0 0] [1] [1 0 1] [1 0 0] [1] [1] rec[string_0][6](x23,Cons(B(),x2)) = [1 1 0]x2 + [0 0 0]x23 + [0] >= [0] = ParseFail(S(0())) [1 1 0] [0 0 1] [0] [0] [1 0 1] [1 0 0] [1] [1] rec[string_0][6](x23,Cons(C(),x2)) = [1 1 0]x2 + [0 0 0]x23 + [1] >= [0] = ParseFail(S(0())) [1 1 0] [0 0 1] [1] [0] [1 0 1] [1] [1 0 1] main(x3) = [0 1 1]x3 + [0] >= [0 1 1]x3 = rec[string_0][6](bot[1](),x3) [1 1 1] [1] [0 1 1] [1 0 1] [1] [1 0 1] [0] main(x3) = [0 1 1]x3 + [0] >= [0 1 1]x3 + [0] = rec[string_0][6](bot[3](),x3) [1 1 1] [1] [0 1 1] [1] [1 0 1] [1] [1 0 1] main(x3) = [0 1 1]x3 + [0] >= [0 1 1]x3 = rec[string_0][6](bot[5](),x3) [1 1 1] [1] [0 1 1] problem: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) DP Processor: DPs: bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6]#(x23,Cons(A(),x2)) -> bind_1[4]#(bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) TRS: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) TDG Processor: DPs: bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6]#(x23,Cons(A(),x2)) -> bind_1[4]#(bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) TRS: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) graph: rec[string_0][6]#(x23,Cons(A(),x2)) -> bind_1[4]#(bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6]#(x23,Cons(A(),x2)) -> bind_1[4]#(bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) rec[string_0][6]#(x23,Cons(A(),x2)) -> bind_1[4]#(bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) -> bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) -> bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) -> bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) -> bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) -> bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) -> bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) -> bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) -> bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) -> bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) SCC Processor: #sccs: 1 #rules: 6 #arcs: 21/49 DPs: bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4]#(bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) TRS: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) Subterm Criterion Processor: simple projection: pi(bind_1[4]#) = 3 pi(bind'_0[6]#) = 4 problem: DPs: bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) TRS: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) EDG Processor: DPs: bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) TRS: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) graph: bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) -> bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) -> bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) -> bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) -> bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) -> bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) -> bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) CDG Processor: DPs: bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) TRS: bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[2](),x4,x2,S(x1)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6](eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())),x4,x3,x2,Nil(),S(x1)) -> ParseFail(S(x1)) bind'_0[6](bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x())), x5,x4,x3,Cons(B(),x2),S(x1)) -> bind_1[4](bind'_0(return_x()),x3,B(),x2,S(S(x1))) bind'_0[6](return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4](bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) bind_1[4](bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6](x5,x3,bot[6](),x4,x2,S(x1)) rec[string_0][6](x23,Nil()) -> ParseFail(0()) rec[string_0][6](x23,Cons(A(),x2)) -> bind_1[4](bind'_0(bind_p_f(bind_p_f(any(),filter_0()),bind'_0(return_x()))), bind_1(),A(),x2,S(0())) rec[string_0][6](x23,Cons(B(),x2)) -> ParseFail(S(0())) rec[string_0][6](x23,Cons(C(),x2)) -> ParseFail(S(0())) graph: bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(return_x(),x11,x9,bind_1(),x4,S(x2)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),x4,S(x2)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[6](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[4](),x4,x2,S(x1)) bind'_0[6]#(eos(),x3,x2,bind_1(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(eos()),runParser_0(),Unit(),Nil(),S(x1)) -> bind_1[4]#(bind'_0(x5),x4,x3,x2,S(x1)) -> bind'_0[6]#(x5,x3,bot[2](),x4,x2,S(x1)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 6/25