YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { turing(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(IfGoto(igtNat1, igtNat2), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Goto(gtNat), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(Goto(gtNat), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Right(), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(Right(), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Left(), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(Left(), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Write(wNat), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](True(),
                                       I(Write(wNat), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Halt(), r), revltape, rtape, prog) -> rtape
  , turing(Empty(), revltape, rtape, prog) -> rtape
  , lookup(S(x), I(l, r)) -> lookup(x, r)
  , lookup(0(), instrs) -> instrs
  , instrsConstrCheck(I(l1, r1), I(x, y)) -> True()
  , instrsConstrCheck(I(l1, r1), Empty()) -> False()
  , instrsConstrCheck(Empty(), I(x, y)) -> False()
  , instrsConstrCheck(Empty(), Empty()) -> True()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2),
                     IfGoto(igtNat12, igtNat22))
    -> True()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Right()) -> False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Left()) -> False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt()) -> False()
  , instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    False()
  , instrConstrCheck(Goto(gtNat), Goto(gtNat2)) -> True()
  , instrConstrCheck(Goto(gtNat), Right()) -> False()
  , instrConstrCheck(Goto(gtNat), Left()) -> False()
  , instrConstrCheck(Goto(gtNat), Write(wNat2)) -> False()
  , instrConstrCheck(Goto(gtNat), Halt()) -> False()
  , instrConstrCheck(Right(), IfGoto(igtNat12, igtNat22)) -> False()
  , instrConstrCheck(Right(), Goto(gtNat2)) -> False()
  , instrConstrCheck(Right(), Right()) -> True()
  , instrConstrCheck(Right(), Left()) -> False()
  , instrConstrCheck(Right(), Write(wNat2)) -> False()
  , instrConstrCheck(Right(), Halt()) -> False()
  , instrConstrCheck(Left(), IfGoto(igtNat12, igtNat22)) -> False()
  , instrConstrCheck(Left(), Goto(gtNat2)) -> False()
  , instrConstrCheck(Left(), Right()) -> False()
  , instrConstrCheck(Left(), Left()) -> True()
  , instrConstrCheck(Left(), Write(wNat2)) -> False()
  , instrConstrCheck(Left(), Halt()) -> False()
  , instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    False()
  , instrConstrCheck(Write(wNat), Goto(gtNat2)) -> False()
  , instrConstrCheck(Write(wNat), Right()) -> False()
  , instrConstrCheck(Write(wNat), Left()) -> False()
  , instrConstrCheck(Write(wNat), Write(wNat2)) -> True()
  , instrConstrCheck(Write(wNat), Halt()) -> False()
  , instrConstrCheck(Halt(), IfGoto(igtNat12, igtNat22)) -> False()
  , instrConstrCheck(Halt(), Goto(gtNat2)) -> False()
  , instrConstrCheck(Halt(), Right()) -> False()
  , instrConstrCheck(Halt(), Left()) -> False()
  , instrConstrCheck(Halt(), Write(wNat2)) -> False()
  , instrConstrCheck(Halt(), Halt()) -> True()
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , instrsSecond(I(l, r)) -> r
  , instrsFirst(I(l, r)) -> l
  , getWrite(Write(int)) -> int
  , getGotoSecond(IfGoto(i1, i2)) -> i2
  , getGotoFirst(IfGoto(i1, i2)) -> i1
  , getGoto(Goto(int)) -> int
  , run(prog, tapeinput) -> turing(prog, Nil(), tapeinput, prog) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We add the following innermost weak dependency pairs:

Strict DPs:
  { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)
    -> c_1()
  , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
  , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
  , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
  , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
  , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
  , turing^#(Empty(), revltape, rtape, prog) -> c_7()
  , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r))
  , lookup^#(0(), instrs) -> c_9()
  , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
  , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
  , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
  , instrsConstrCheck^#(Empty(), Empty()) -> c_13()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                       IfGoto(igtNat12, igtNat22))
    -> c_14()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    c_15()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    c_18()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19()
  , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    c_20()
  , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
  , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
  , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
  , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
  , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
  , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26()
  , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
  , instrConstrCheck^#(Right(), Right()) -> c_28()
  , instrConstrCheck^#(Right(), Left()) -> c_29()
  , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
  , instrConstrCheck^#(Right(), Halt()) -> c_31()
  , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32()
  , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
  , instrConstrCheck^#(Left(), Right()) -> c_34()
  , instrConstrCheck^#(Left(), Left()) -> c_35()
  , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
  , instrConstrCheck^#(Left(), Halt()) -> c_37()
  , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    c_38()
  , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
  , instrConstrCheck^#(Write(wNat), Right()) -> c_40()
  , instrConstrCheck^#(Write(wNat), Left()) -> c_41()
  , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
  , instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
  , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44()
  , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
  , instrConstrCheck^#(Halt(), Right()) -> c_46()
  , instrConstrCheck^#(Halt(), Left()) -> c_47()
  , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
  , instrConstrCheck^#(Halt(), Halt()) -> c_49()
  , notEmpty^#(Cons(x, xs)) -> c_50()
  , notEmpty^#(Nil()) -> c_51()
  , instrsSecond^#(I(l, r)) -> c_52()
  , instrsFirst^#(I(l, r)) -> c_53()
  , getWrite^#(Write(int)) -> c_54()
  , getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
  , getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
  , getGoto^#(Goto(int)) -> c_57()
  , run^#(prog, tapeinput) ->
    c_58(turing^#(prog, Nil(), tapeinput, prog)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)
    -> c_1()
  , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
  , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
  , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
  , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
  , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
  , turing^#(Empty(), revltape, rtape, prog) -> c_7()
  , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r))
  , lookup^#(0(), instrs) -> c_9()
  , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
  , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
  , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
  , instrsConstrCheck^#(Empty(), Empty()) -> c_13()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                       IfGoto(igtNat12, igtNat22))
    -> c_14()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    c_15()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    c_18()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19()
  , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    c_20()
  , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
  , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
  , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
  , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
  , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
  , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26()
  , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
  , instrConstrCheck^#(Right(), Right()) -> c_28()
  , instrConstrCheck^#(Right(), Left()) -> c_29()
  , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
  , instrConstrCheck^#(Right(), Halt()) -> c_31()
  , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32()
  , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
  , instrConstrCheck^#(Left(), Right()) -> c_34()
  , instrConstrCheck^#(Left(), Left()) -> c_35()
  , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
  , instrConstrCheck^#(Left(), Halt()) -> c_37()
  , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    c_38()
  , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
  , instrConstrCheck^#(Write(wNat), Right()) -> c_40()
  , instrConstrCheck^#(Write(wNat), Left()) -> c_41()
  , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
  , instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
  , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44()
  , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
  , instrConstrCheck^#(Halt(), Right()) -> c_46()
  , instrConstrCheck^#(Halt(), Left()) -> c_47()
  , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
  , instrConstrCheck^#(Halt(), Halt()) -> c_49()
  , notEmpty^#(Cons(x, xs)) -> c_50()
  , notEmpty^#(Nil()) -> c_51()
  , instrsSecond^#(I(l, r)) -> c_52()
  , instrsFirst^#(I(l, r)) -> c_53()
  , getWrite^#(Write(int)) -> c_54()
  , getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
  , getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
  , getGoto^#(Goto(int)) -> c_57()
  , run^#(prog, tapeinput) ->
    c_58(turing^#(prog, Nil(), tapeinput, prog)) }
Strict Trs:
  { turing(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(IfGoto(igtNat1, igtNat2), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Goto(gtNat), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(Goto(gtNat), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Right(), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(Right(), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Left(), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](False(),
                                       I(Left(), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Write(wNat), r), revltape, rtape, prog) ->
    turing[Ite][True][Ite][False][Ite](True(),
                                       I(Write(wNat), r),
                                       revltape,
                                       rtape,
                                       prog)
  , turing(I(Halt(), r), revltape, rtape, prog) -> rtape
  , turing(Empty(), revltape, rtape, prog) -> rtape
  , lookup(S(x), I(l, r)) -> lookup(x, r)
  , lookup(0(), instrs) -> instrs
  , instrsConstrCheck(I(l1, r1), I(x, y)) -> True()
  , instrsConstrCheck(I(l1, r1), Empty()) -> False()
  , instrsConstrCheck(Empty(), I(x, y)) -> False()
  , instrsConstrCheck(Empty(), Empty()) -> True()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2),
                     IfGoto(igtNat12, igtNat22))
    -> True()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Right()) -> False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Left()) -> False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    False()
  , instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt()) -> False()
  , instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    False()
  , instrConstrCheck(Goto(gtNat), Goto(gtNat2)) -> True()
  , instrConstrCheck(Goto(gtNat), Right()) -> False()
  , instrConstrCheck(Goto(gtNat), Left()) -> False()
  , instrConstrCheck(Goto(gtNat), Write(wNat2)) -> False()
  , instrConstrCheck(Goto(gtNat), Halt()) -> False()
  , instrConstrCheck(Right(), IfGoto(igtNat12, igtNat22)) -> False()
  , instrConstrCheck(Right(), Goto(gtNat2)) -> False()
  , instrConstrCheck(Right(), Right()) -> True()
  , instrConstrCheck(Right(), Left()) -> False()
  , instrConstrCheck(Right(), Write(wNat2)) -> False()
  , instrConstrCheck(Right(), Halt()) -> False()
  , instrConstrCheck(Left(), IfGoto(igtNat12, igtNat22)) -> False()
  , instrConstrCheck(Left(), Goto(gtNat2)) -> False()
  , instrConstrCheck(Left(), Right()) -> False()
  , instrConstrCheck(Left(), Left()) -> True()
  , instrConstrCheck(Left(), Write(wNat2)) -> False()
  , instrConstrCheck(Left(), Halt()) -> False()
  , instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    False()
  , instrConstrCheck(Write(wNat), Goto(gtNat2)) -> False()
  , instrConstrCheck(Write(wNat), Right()) -> False()
  , instrConstrCheck(Write(wNat), Left()) -> False()
  , instrConstrCheck(Write(wNat), Write(wNat2)) -> True()
  , instrConstrCheck(Write(wNat), Halt()) -> False()
  , instrConstrCheck(Halt(), IfGoto(igtNat12, igtNat22)) -> False()
  , instrConstrCheck(Halt(), Goto(gtNat2)) -> False()
  , instrConstrCheck(Halt(), Right()) -> False()
  , instrConstrCheck(Halt(), Left()) -> False()
  , instrConstrCheck(Halt(), Write(wNat2)) -> False()
  , instrConstrCheck(Halt(), Halt()) -> True()
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , instrsSecond(I(l, r)) -> r
  , instrsFirst(I(l, r)) -> l
  , getWrite(Write(int)) -> int
  , getGotoSecond(IfGoto(i1, i2)) -> i2
  , getGotoFirst(IfGoto(i1, i2)) -> i1
  , getGoto(Goto(int)) -> int
  , run(prog, tapeinput) -> turing(prog, Nil(), tapeinput, prog) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

No rule is usable, rules are removed from the input problem.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)
    -> c_1()
  , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
  , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
  , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
  , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
  , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
  , turing^#(Empty(), revltape, rtape, prog) -> c_7()
  , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r))
  , lookup^#(0(), instrs) -> c_9()
  , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
  , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
  , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
  , instrsConstrCheck^#(Empty(), Empty()) -> c_13()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                       IfGoto(igtNat12, igtNat22))
    -> c_14()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    c_15()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    c_18()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19()
  , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    c_20()
  , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
  , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
  , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
  , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
  , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
  , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26()
  , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
  , instrConstrCheck^#(Right(), Right()) -> c_28()
  , instrConstrCheck^#(Right(), Left()) -> c_29()
  , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
  , instrConstrCheck^#(Right(), Halt()) -> c_31()
  , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32()
  , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
  , instrConstrCheck^#(Left(), Right()) -> c_34()
  , instrConstrCheck^#(Left(), Left()) -> c_35()
  , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
  , instrConstrCheck^#(Left(), Halt()) -> c_37()
  , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    c_38()
  , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
  , instrConstrCheck^#(Write(wNat), Right()) -> c_40()
  , instrConstrCheck^#(Write(wNat), Left()) -> c_41()
  , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
  , instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
  , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44()
  , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
  , instrConstrCheck^#(Halt(), Right()) -> c_46()
  , instrConstrCheck^#(Halt(), Left()) -> c_47()
  , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
  , instrConstrCheck^#(Halt(), Halt()) -> c_49()
  , notEmpty^#(Cons(x, xs)) -> c_50()
  , notEmpty^#(Nil()) -> c_51()
  , instrsSecond^#(I(l, r)) -> c_52()
  , instrsFirst^#(I(l, r)) -> c_53()
  , getWrite^#(Write(int)) -> c_54()
  , getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
  , getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
  , getGoto^#(Goto(int)) -> c_57()
  , run^#(prog, tapeinput) ->
    c_58(turing^#(prog, Nil(), tapeinput, prog)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following constant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(c_8) = {1}, Uargs(c_58) = {1}

TcT has computed the following constructor-restricted matrix
interpretation.

                    [I](x1, x2) = [1 0] x2 + [0]                    
                                  [0 0]      [0]                    
                                                                    
               [IfGoto](x1, x2) = [0]                               
                                  [0]                               
                                                                    
                     [Goto](x1) = [0]                               
                                  [0]                               
                                                                    
                        [Right] = [0]                               
                                  [0]                               
                                                                    
                         [Left] = [0]                               
                                  [0]                               
                                                                    
                    [Write](x1) = [0]                               
                                  [0]                               
                                                                    
                         [Halt] = [0]                               
                                  [0]                               
                                                                    
                        [Empty] = [0]                               
                                  [0]                               
                                                                    
                        [S](x1) = [1 0] x1 + [0]                    
                                  [0 0]      [0]                    
                                                                    
                 [Cons](x1, x2) = [1]                               
                                  [1]                               
                                                                    
                          [Nil] = [0]                               
                                  [0]                               
                                                                    
                            [0] = [1]                               
                                  [1]                               
                                                                    
     [turing^#](x1, x2, x3, x4) = [2 1] x2 + [1 1] x3 + [1          
                                                         1] x4 + [0]
                                  [2 2]      [1 1]      [2          
                                                         2]      [0]
                                                                    
                          [c_1] = [1]                               
                                  [0]                               
                                                                    
                          [c_2] = [1]                               
                                  [0]                               
                                                                    
                          [c_3] = [1]                               
                                  [0]                               
                                                                    
                          [c_4] = [1]                               
                                  [0]                               
                                                                    
                          [c_5] = [1]                               
                                  [0]                               
                                                                    
                          [c_6] = [1]                               
                                  [0]                               
                                                                    
                          [c_7] = [1]                               
                                  [0]                               
                                                                    
             [lookup^#](x1, x2) = [0]                               
                                  [2]                               
                                                                    
                      [c_8](x1) = [1 0] x1 + [2]                    
                                  [0 1]      [0]                    
                                                                    
                          [c_9] = [1]                               
                                  [1]                               
                                                                    
  [instrsConstrCheck^#](x1, x2) = [0]                               
                                  [0]                               
                                                                    
                         [c_10] = [1]                               
                                  [0]                               
                                                                    
                         [c_11] = [1]                               
                                  [0]                               
                                                                    
                         [c_12] = [1]                               
                                  [0]                               
                                                                    
                         [c_13] = [1]                               
                                  [0]                               
                                                                    
   [instrConstrCheck^#](x1, x2) = [0]                               
                                  [0]                               
                                                                    
                         [c_14] = [1]                               
                                  [0]                               
                                                                    
                         [c_15] = [1]                               
                                  [0]                               
                                                                    
                         [c_16] = [1]                               
                                  [0]                               
                                                                    
                         [c_17] = [1]                               
                                  [0]                               
                                                                    
                         [c_18] = [1]                               
                                  [0]                               
                                                                    
                         [c_19] = [1]                               
                                  [0]                               
                                                                    
                         [c_20] = [1]                               
                                  [0]                               
                                                                    
                         [c_21] = [1]                               
                                  [0]                               
                                                                    
                         [c_22] = [1]                               
                                  [0]                               
                                                                    
                         [c_23] = [1]                               
                                  [0]                               
                                                                    
                         [c_24] = [1]                               
                                  [0]                               
                                                                    
                         [c_25] = [1]                               
                                  [0]                               
                                                                    
                         [c_26] = [2]                               
                                  [0]                               
                                                                    
                         [c_27] = [1]                               
                                  [0]                               
                                                                    
                         [c_28] = [1]                               
                                  [0]                               
                                                                    
                         [c_29] = [1]                               
                                  [0]                               
                                                                    
                         [c_30] = [1]                               
                                  [0]                               
                                                                    
                         [c_31] = [1]                               
                                  [0]                               
                                                                    
                         [c_32] = [1]                               
                                  [0]                               
                                                                    
                         [c_33] = [1]                               
                                  [0]                               
                                                                    
                         [c_34] = [1]                               
                                  [0]                               
                                                                    
                         [c_35] = [1]                               
                                  [0]                               
                                                                    
                         [c_36] = [1]                               
                                  [0]                               
                                                                    
                         [c_37] = [1]                               
                                  [0]                               
                                                                    
                         [c_38] = [1]                               
                                  [0]                               
                                                                    
                         [c_39] = [1]                               
                                  [0]                               
                                                                    
                         [c_40] = [1]                               
                                  [0]                               
                                                                    
                         [c_41] = [1]                               
                                  [0]                               
                                                                    
                         [c_42] = [1]                               
                                  [0]                               
                                                                    
                         [c_43] = [1]                               
                                  [0]                               
                                                                    
                         [c_44] = [1]                               
                                  [0]                               
                                                                    
                         [c_45] = [1]                               
                                  [0]                               
                                                                    
                         [c_46] = [1]                               
                                  [0]                               
                                                                    
                         [c_47] = [1]                               
                                  [0]                               
                                                                    
                         [c_48] = [1]                               
                                  [0]                               
                                                                    
                         [c_49] = [1]                               
                                  [0]                               
                                                                    
               [notEmpty^#](x1) = [0 0] x1 + [0]                    
                                  [1 1]      [2]                    
                                                                    
                         [c_50] = [1]                               
                                  [0]                               
                                                                    
                         [c_51] = [1]                               
                                  [1]                               
                                                                    
           [instrsSecond^#](x1) = [1 1] x1 + [0]                    
                                  [1 2]      [2]                    
                                                                    
                         [c_52] = [1]                               
                                  [1]                               
                                                                    
            [instrsFirst^#](x1) = [2 1] x1 + [0]                    
                                  [2 2]      [2]                    
                                                                    
                         [c_53] = [1]                               
                                  [1]                               
                                                                    
               [getWrite^#](x1) = [1 2] x1 + [1]                    
                                  [2 1]      [2]                    
                                                                    
                         [c_54] = [0]                               
                                  [1]                               
                                                                    
          [getGotoSecond^#](x1) = [2 2] x1 + [1]                    
                                  [1 1]      [2]                    
                                                                    
                         [c_55] = [0]                               
                                  [1]                               
                                                                    
           [getGotoFirst^#](x1) = [1 1] x1 + [1]                    
                                  [1 1]      [2]                    
                                                                    
                         [c_56] = [0]                               
                                  [1]                               
                                                                    
                [getGoto^#](x1) = [1 1] x1 + [1]                    
                                  [1 2]      [2]                    
                                                                    
                         [c_57] = [0]                               
                                  [1]                               
                                                                    
                [run^#](x1, x2) = [2 2] x1 + [1 2] x2 + [1]         
                                  [2 2]      [2 2]      [2]         
                                                                    
                     [c_58](x1) = [1 0] x1 + [2]                    
                                  [0 1]      [2]                    

The following symbols are considered usable

  {turing^#, lookup^#, instrsConstrCheck^#, instrConstrCheck^#,
   notEmpty^#, instrsSecond^#, instrsFirst^#, getWrite^#,
   getGotoSecond^#, getGotoFirst^#, getGoto^#, run^#}

The order satisfies the following ordering constraints:

  [turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0]
                                                                      [2 2]            [1 1]         [2 2]        [0]
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_1()]                                        
                                                                                                                     
               [turing^#(I(Goto(gtNat), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0]
                                                                      [2 2]            [1 1]         [2 2]        [0]
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_2()]                                        
                                                                                                                     
                   [turing^#(I(Right(), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0]
                                                                      [2 2]            [1 1]         [2 2]        [0]
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_3()]                                        
                                                                                                                     
                    [turing^#(I(Left(), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0]
                                                                      [2 2]            [1 1]         [2 2]        [0]
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_4()]                                        
                                                                                                                     
               [turing^#(I(Write(wNat), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0]
                                                                      [2 2]            [1 1]         [2 2]        [0]
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_5()]                                        
                                                                                                                     
                    [turing^#(I(Halt(), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0]
                                                                      [2 2]            [1 1]         [2 2]        [0]
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_6()]                                        
                                                                                                                     
                         [turing^#(Empty(), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0]
                                                                      [2 2]            [1 1]         [2 2]        [0]
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_7()]                                        
                                                                                                                     
                                          [lookup^#(S(x), I(l, r))] = [0]                                            
                                                                      [2]                                            
                                                                    ? [2]                                            
                                                                      [2]                                            
                                                                    = [c_8(lookup^#(x, r))]                          
                                                                                                                     
                                            [lookup^#(0(), instrs)] = [0]                                            
                                                                      [2]                                            
                                                                    ? [1]                                            
                                                                      [1]                                            
                                                                    = [c_9()]                                        
                                                                                                                     
                          [instrsConstrCheck^#(I(l1, r1), I(x, y))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_10()]                                       
                                                                                                                     
                          [instrsConstrCheck^#(I(l1, r1), Empty())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_11()]                                       
                                                                                                                     
                            [instrsConstrCheck^#(Empty(), I(x, y))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_12()]                                       
                                                                                                                     
                            [instrsConstrCheck^#(Empty(), Empty())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_13()]                                       
                                                                                                                     
                      [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), = [0]                                            
                                       IfGoto(igtNat12, igtNat22))]   [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_14()]                                       
                                                                                                                     
       [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_15()]                                       
                                                                                                                     
            [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_16()]                                       
                                                                                                                     
             [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_17()]                                       
                                                                                                                     
       [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_18()]                                       
                                                                                                                     
             [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_19()]                                       
                                                                                                                     
      [instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_20()]                                       
                                                                                                                     
                    [instrConstrCheck^#(Goto(gtNat), Goto(gtNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_21()]                                       
                                                                                                                     
                         [instrConstrCheck^#(Goto(gtNat), Right())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_22()]                                       
                                                                                                                     
                          [instrConstrCheck^#(Goto(gtNat), Left())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_23()]                                       
                                                                                                                     
                    [instrConstrCheck^#(Goto(gtNat), Write(wNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_24()]                                       
                                                                                                                     
                          [instrConstrCheck^#(Goto(gtNat), Halt())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_25()]                                       
                                                                                                                     
          [instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [2]                                            
                                                                      [0]                                            
                                                                    = [c_26()]                                       
                                                                                                                     
                        [instrConstrCheck^#(Right(), Goto(gtNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_27()]                                       
                                                                                                                     
                             [instrConstrCheck^#(Right(), Right())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_28()]                                       
                                                                                                                     
                              [instrConstrCheck^#(Right(), Left())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_29()]                                       
                                                                                                                     
                        [instrConstrCheck^#(Right(), Write(wNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_30()]                                       
                                                                                                                     
                              [instrConstrCheck^#(Right(), Halt())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_31()]                                       
                                                                                                                     
           [instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_32()]                                       
                                                                                                                     
                         [instrConstrCheck^#(Left(), Goto(gtNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_33()]                                       
                                                                                                                     
                              [instrConstrCheck^#(Left(), Right())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_34()]                                       
                                                                                                                     
                               [instrConstrCheck^#(Left(), Left())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_35()]                                       
                                                                                                                     
                         [instrConstrCheck^#(Left(), Write(wNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_36()]                                       
                                                                                                                     
                               [instrConstrCheck^#(Left(), Halt())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_37()]                                       
                                                                                                                     
      [instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_38()]                                       
                                                                                                                     
                    [instrConstrCheck^#(Write(wNat), Goto(gtNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_39()]                                       
                                                                                                                     
                         [instrConstrCheck^#(Write(wNat), Right())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_40()]                                       
                                                                                                                     
                          [instrConstrCheck^#(Write(wNat), Left())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_41()]                                       
                                                                                                                     
                    [instrConstrCheck^#(Write(wNat), Write(wNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_42()]                                       
                                                                                                                     
                          [instrConstrCheck^#(Write(wNat), Halt())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_43()]                                       
                                                                                                                     
           [instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_44()]                                       
                                                                                                                     
                         [instrConstrCheck^#(Halt(), Goto(gtNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_45()]                                       
                                                                                                                     
                              [instrConstrCheck^#(Halt(), Right())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_46()]                                       
                                                                                                                     
                               [instrConstrCheck^#(Halt(), Left())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_47()]                                       
                                                                                                                     
                         [instrConstrCheck^#(Halt(), Write(wNat2))] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_48()]                                       
                                                                                                                     
                               [instrConstrCheck^#(Halt(), Halt())] = [0]                                            
                                                                      [0]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_49()]                                       
                                                                                                                     
                                          [notEmpty^#(Cons(x, xs))] = [0]                                            
                                                                      [4]                                            
                                                                    ? [1]                                            
                                                                      [0]                                            
                                                                    = [c_50()]                                       
                                                                                                                     
                                                [notEmpty^#(Nil())] = [0]                                            
                                                                      [2]                                            
                                                                    ? [1]                                            
                                                                      [1]                                            
                                                                    = [c_51()]                                       
                                                                                                                     
                                          [instrsSecond^#(I(l, r))] = [1 0] r + [0]                                  
                                                                      [1 0]     [2]                                  
                                                                    ? [1]                                            
                                                                      [1]                                            
                                                                    = [c_52()]                                       
                                                                                                                     
                                           [instrsFirst^#(I(l, r))] = [2 0] r + [0]                                  
                                                                      [2 0]     [2]                                  
                                                                    ? [1]                                            
                                                                      [1]                                            
                                                                    = [c_53()]                                       
                                                                                                                     
                                           [getWrite^#(Write(int))] = [1]                                            
                                                                      [2]                                            
                                                                    > [0]                                            
                                                                      [1]                                            
                                                                    = [c_54()]                                       
                                                                                                                     
                                  [getGotoSecond^#(IfGoto(i1, i2))] = [1]                                            
                                                                      [2]                                            
                                                                    > [0]                                            
                                                                      [1]                                            
                                                                    = [c_55()]                                       
                                                                                                                     
                                   [getGotoFirst^#(IfGoto(i1, i2))] = [1]                                            
                                                                      [2]                                            
                                                                    > [0]                                            
                                                                      [1]                                            
                                                                    = [c_56()]                                       
                                                                                                                     
                                             [getGoto^#(Goto(int))] = [1]                                            
                                                                      [2]                                            
                                                                    > [0]                                            
                                                                      [1]                                            
                                                                    = [c_57()]                                       
                                                                                                                     
                                           [run^#(prog, tapeinput)] = [2 2] prog + [1 2] tapeinput + [1]             
                                                                      [2 2]        [2 2]             [2]             
                                                                    ? [1 1] prog + [1 1] tapeinput + [2]             
                                                                      [2 2]        [1 1]             [2]             
                                                                    = [c_58(turing^#(prog, Nil(), tapeinput, prog))] 
                                                                                                                     

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)
    -> c_1()
  , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
  , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
  , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
  , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
  , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
  , turing^#(Empty(), revltape, rtape, prog) -> c_7()
  , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r))
  , lookup^#(0(), instrs) -> c_9()
  , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
  , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
  , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
  , instrsConstrCheck^#(Empty(), Empty()) -> c_13()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                       IfGoto(igtNat12, igtNat22))
    -> c_14()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    c_15()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    c_18()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19()
  , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    c_20()
  , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
  , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
  , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
  , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
  , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
  , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26()
  , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
  , instrConstrCheck^#(Right(), Right()) -> c_28()
  , instrConstrCheck^#(Right(), Left()) -> c_29()
  , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
  , instrConstrCheck^#(Right(), Halt()) -> c_31()
  , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32()
  , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
  , instrConstrCheck^#(Left(), Right()) -> c_34()
  , instrConstrCheck^#(Left(), Left()) -> c_35()
  , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
  , instrConstrCheck^#(Left(), Halt()) -> c_37()
  , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    c_38()
  , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
  , instrConstrCheck^#(Write(wNat), Right()) -> c_40()
  , instrConstrCheck^#(Write(wNat), Left()) -> c_41()
  , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
  , instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
  , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44()
  , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
  , instrConstrCheck^#(Halt(), Right()) -> c_46()
  , instrConstrCheck^#(Halt(), Left()) -> c_47()
  , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
  , instrConstrCheck^#(Halt(), Halt()) -> c_49()
  , notEmpty^#(Cons(x, xs)) -> c_50()
  , notEmpty^#(Nil()) -> c_51()
  , instrsSecond^#(I(l, r)) -> c_52()
  , instrsFirst^#(I(l, r)) -> c_53()
  , run^#(prog, tapeinput) ->
    c_58(turing^#(prog, Nil(), tapeinput, prog)) }
Weak DPs:
  { getWrite^#(Write(int)) -> c_54()
  , getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
  , getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
  , getGoto^#(Goto(int)) -> c_57() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of
{1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53}
by applications of
Pre({1,2,3,4,5,6,7,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53})
= {8,54}. Here rules are labeled as follows:

  DPs:
    { 1: turing^#(I(IfGoto(igtNat1, igtNat2), r),
                  revltape,
                  rtape,
                  prog)
         -> c_1()
    , 2: turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
    , 3: turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
    , 4: turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
    , 5: turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
    , 6: turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
    , 7: turing^#(Empty(), revltape, rtape, prog) -> c_7()
    , 8: lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r))
    , 9: lookup^#(0(), instrs) -> c_9()
    , 10: instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
    , 11: instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
    , 12: instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
    , 13: instrsConstrCheck^#(Empty(), Empty()) -> c_13()
    , 14: instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                             IfGoto(igtNat12, igtNat22))
          -> c_14()
    , 15: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
          c_15()
    , 16: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) ->
          c_16()
    , 17: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) ->
          c_17()
    , 18: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
          c_18()
    , 19: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) ->
          c_19()
    , 20: instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22))
          -> c_20()
    , 21: instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
    , 22: instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
    , 23: instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
    , 24: instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
    , 25: instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
    , 26: instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) ->
          c_26()
    , 27: instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
    , 28: instrConstrCheck^#(Right(), Right()) -> c_28()
    , 29: instrConstrCheck^#(Right(), Left()) -> c_29()
    , 30: instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
    , 31: instrConstrCheck^#(Right(), Halt()) -> c_31()
    , 32: instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) ->
          c_32()
    , 33: instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
    , 34: instrConstrCheck^#(Left(), Right()) -> c_34()
    , 35: instrConstrCheck^#(Left(), Left()) -> c_35()
    , 36: instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
    , 37: instrConstrCheck^#(Left(), Halt()) -> c_37()
    , 38: instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22))
          -> c_38()
    , 39: instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
    , 40: instrConstrCheck^#(Write(wNat), Right()) -> c_40()
    , 41: instrConstrCheck^#(Write(wNat), Left()) -> c_41()
    , 42: instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
    , 43: instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
    , 44: instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) ->
          c_44()
    , 45: instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
    , 46: instrConstrCheck^#(Halt(), Right()) -> c_46()
    , 47: instrConstrCheck^#(Halt(), Left()) -> c_47()
    , 48: instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
    , 49: instrConstrCheck^#(Halt(), Halt()) -> c_49()
    , 50: notEmpty^#(Cons(x, xs)) -> c_50()
    , 51: notEmpty^#(Nil()) -> c_51()
    , 52: instrsSecond^#(I(l, r)) -> c_52()
    , 53: instrsFirst^#(I(l, r)) -> c_53()
    , 54: run^#(prog, tapeinput) ->
          c_58(turing^#(prog, Nil(), tapeinput, prog))
    , 55: getWrite^#(Write(int)) -> c_54()
    , 56: getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
    , 57: getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
    , 58: getGoto^#(Goto(int)) -> c_57() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs:
  { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r))
  , run^#(prog, tapeinput) ->
    c_58(turing^#(prog, Nil(), tapeinput, prog)) }
Weak DPs:
  { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)
    -> c_1()
  , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
  , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
  , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
  , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
  , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
  , turing^#(Empty(), revltape, rtape, prog) -> c_7()
  , lookup^#(0(), instrs) -> c_9()
  , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
  , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
  , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
  , instrsConstrCheck^#(Empty(), Empty()) -> c_13()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                       IfGoto(igtNat12, igtNat22))
    -> c_14()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    c_15()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    c_18()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19()
  , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    c_20()
  , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
  , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
  , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
  , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
  , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
  , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26()
  , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
  , instrConstrCheck^#(Right(), Right()) -> c_28()
  , instrConstrCheck^#(Right(), Left()) -> c_29()
  , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
  , instrConstrCheck^#(Right(), Halt()) -> c_31()
  , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32()
  , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
  , instrConstrCheck^#(Left(), Right()) -> c_34()
  , instrConstrCheck^#(Left(), Left()) -> c_35()
  , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
  , instrConstrCheck^#(Left(), Halt()) -> c_37()
  , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    c_38()
  , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
  , instrConstrCheck^#(Write(wNat), Right()) -> c_40()
  , instrConstrCheck^#(Write(wNat), Left()) -> c_41()
  , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
  , instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
  , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44()
  , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
  , instrConstrCheck^#(Halt(), Right()) -> c_46()
  , instrConstrCheck^#(Halt(), Left()) -> c_47()
  , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
  , instrConstrCheck^#(Halt(), Halt()) -> c_49()
  , notEmpty^#(Cons(x, xs)) -> c_50()
  , notEmpty^#(Nil()) -> c_51()
  , instrsSecond^#(I(l, r)) -> c_52()
  , instrsFirst^#(I(l, r)) -> c_53()
  , getWrite^#(Write(int)) -> c_54()
  , getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
  , getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
  , getGoto^#(Goto(int)) -> c_57() }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We estimate the number of application of {2} by applications of
Pre({2}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r))
    , 2: run^#(prog, tapeinput) ->
         c_58(turing^#(prog, Nil(), tapeinput, prog))
    , 3: turing^#(I(IfGoto(igtNat1, igtNat2), r),
                  revltape,
                  rtape,
                  prog)
         -> c_1()
    , 4: turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
    , 5: turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
    , 6: turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
    , 7: turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
    , 8: turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
    , 9: turing^#(Empty(), revltape, rtape, prog) -> c_7()
    , 10: lookup^#(0(), instrs) -> c_9()
    , 11: instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
    , 12: instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
    , 13: instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
    , 14: instrsConstrCheck^#(Empty(), Empty()) -> c_13()
    , 15: instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                             IfGoto(igtNat12, igtNat22))
          -> c_14()
    , 16: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
          c_15()
    , 17: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) ->
          c_16()
    , 18: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) ->
          c_17()
    , 19: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
          c_18()
    , 20: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) ->
          c_19()
    , 21: instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22))
          -> c_20()
    , 22: instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
    , 23: instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
    , 24: instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
    , 25: instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
    , 26: instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
    , 27: instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) ->
          c_26()
    , 28: instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
    , 29: instrConstrCheck^#(Right(), Right()) -> c_28()
    , 30: instrConstrCheck^#(Right(), Left()) -> c_29()
    , 31: instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
    , 32: instrConstrCheck^#(Right(), Halt()) -> c_31()
    , 33: instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) ->
          c_32()
    , 34: instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
    , 35: instrConstrCheck^#(Left(), Right()) -> c_34()
    , 36: instrConstrCheck^#(Left(), Left()) -> c_35()
    , 37: instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
    , 38: instrConstrCheck^#(Left(), Halt()) -> c_37()
    , 39: instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22))
          -> c_38()
    , 40: instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
    , 41: instrConstrCheck^#(Write(wNat), Right()) -> c_40()
    , 42: instrConstrCheck^#(Write(wNat), Left()) -> c_41()
    , 43: instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
    , 44: instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
    , 45: instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) ->
          c_44()
    , 46: instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
    , 47: instrConstrCheck^#(Halt(), Right()) -> c_46()
    , 48: instrConstrCheck^#(Halt(), Left()) -> c_47()
    , 49: instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
    , 50: instrConstrCheck^#(Halt(), Halt()) -> c_49()
    , 51: notEmpty^#(Cons(x, xs)) -> c_50()
    , 52: notEmpty^#(Nil()) -> c_51()
    , 53: instrsSecond^#(I(l, r)) -> c_52()
    , 54: instrsFirst^#(I(l, r)) -> c_53()
    , 55: getWrite^#(Write(int)) -> c_54()
    , 56: getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
    , 57: getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
    , 58: getGoto^#(Goto(int)) -> c_57() }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs: { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) }
Weak DPs:
  { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)
    -> c_1()
  , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
  , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
  , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
  , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
  , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
  , turing^#(Empty(), revltape, rtape, prog) -> c_7()
  , lookup^#(0(), instrs) -> c_9()
  , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
  , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
  , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
  , instrsConstrCheck^#(Empty(), Empty()) -> c_13()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                       IfGoto(igtNat12, igtNat22))
    -> c_14()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
    c_15()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
    c_18()
  , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19()
  , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
    c_20()
  , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
  , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
  , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
  , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
  , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
  , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26()
  , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
  , instrConstrCheck^#(Right(), Right()) -> c_28()
  , instrConstrCheck^#(Right(), Left()) -> c_29()
  , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
  , instrConstrCheck^#(Right(), Halt()) -> c_31()
  , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32()
  , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
  , instrConstrCheck^#(Left(), Right()) -> c_34()
  , instrConstrCheck^#(Left(), Left()) -> c_35()
  , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
  , instrConstrCheck^#(Left(), Halt()) -> c_37()
  , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
    c_38()
  , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
  , instrConstrCheck^#(Write(wNat), Right()) -> c_40()
  , instrConstrCheck^#(Write(wNat), Left()) -> c_41()
  , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
  , instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
  , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44()
  , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
  , instrConstrCheck^#(Halt(), Right()) -> c_46()
  , instrConstrCheck^#(Halt(), Left()) -> c_47()
  , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
  , instrConstrCheck^#(Halt(), Halt()) -> c_49()
  , notEmpty^#(Cons(x, xs)) -> c_50()
  , notEmpty^#(Nil()) -> c_51()
  , instrsSecond^#(I(l, r)) -> c_52()
  , instrsFirst^#(I(l, r)) -> c_53()
  , getWrite^#(Write(int)) -> c_54()
  , getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
  , getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
  , getGoto^#(Goto(int)) -> c_57()
  , run^#(prog, tapeinput) ->
    c_58(turing^#(prog, Nil(), tapeinput, prog)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)
  -> c_1()
, turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2()
, turing^#(I(Right(), r), revltape, rtape, prog) -> c_3()
, turing^#(I(Left(), r), revltape, rtape, prog) -> c_4()
, turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5()
, turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6()
, turing^#(Empty(), revltape, rtape, prog) -> c_7()
, lookup^#(0(), instrs) -> c_9()
, instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10()
, instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11()
, instrsConstrCheck^#(Empty(), I(x, y)) -> c_12()
, instrsConstrCheck^#(Empty(), Empty()) -> c_13()
, instrConstrCheck^#(IfGoto(igtNat1, igtNat2),
                     IfGoto(igtNat12, igtNat22))
  -> c_14()
, instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) ->
  c_15()
, instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16()
, instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17()
, instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) ->
  c_18()
, instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19()
, instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) ->
  c_20()
, instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21()
, instrConstrCheck^#(Goto(gtNat), Right()) -> c_22()
, instrConstrCheck^#(Goto(gtNat), Left()) -> c_23()
, instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24()
, instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25()
, instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26()
, instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27()
, instrConstrCheck^#(Right(), Right()) -> c_28()
, instrConstrCheck^#(Right(), Left()) -> c_29()
, instrConstrCheck^#(Right(), Write(wNat2)) -> c_30()
, instrConstrCheck^#(Right(), Halt()) -> c_31()
, instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32()
, instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33()
, instrConstrCheck^#(Left(), Right()) -> c_34()
, instrConstrCheck^#(Left(), Left()) -> c_35()
, instrConstrCheck^#(Left(), Write(wNat2)) -> c_36()
, instrConstrCheck^#(Left(), Halt()) -> c_37()
, instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) ->
  c_38()
, instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39()
, instrConstrCheck^#(Write(wNat), Right()) -> c_40()
, instrConstrCheck^#(Write(wNat), Left()) -> c_41()
, instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42()
, instrConstrCheck^#(Write(wNat), Halt()) -> c_43()
, instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44()
, instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45()
, instrConstrCheck^#(Halt(), Right()) -> c_46()
, instrConstrCheck^#(Halt(), Left()) -> c_47()
, instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48()
, instrConstrCheck^#(Halt(), Halt()) -> c_49()
, notEmpty^#(Cons(x, xs)) -> c_50()
, notEmpty^#(Nil()) -> c_51()
, instrsSecond^#(I(l, r)) -> c_52()
, instrsFirst^#(I(l, r)) -> c_53()
, getWrite^#(Write(int)) -> c_54()
, getGotoSecond^#(IfGoto(i1, i2)) -> c_55()
, getGotoFirst^#(IfGoto(i1, i2)) -> c_56()
, getGoto^#(Goto(int)) -> c_57()
, run^#(prog, tapeinput) ->
  c_58(turing^#(prog, Nil(), tapeinput, prog)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict DPs: { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.

DPs:
  { 1: lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) }

Sub-proof:
----------
  The input was oriented with the instance of 'Small Polynomial Path
  Order (PS,1-bounded)' as induced by the safe mapping
  
   safe(turing) = {}, safe(I) = {1, 2}, safe(IfGoto) = {1, 2},
   safe(turing[Ite][True][Ite][False][Ite]) = {1, 2, 3, 4, 5},
   safe(False) = {}, safe(Goto) = {1}, safe(Right) = {},
   safe(Left) = {}, safe(Write) = {1}, safe(True) = {},
   safe(Halt) = {}, safe(Empty) = {}, safe(lookup) = {},
   safe(S) = {1}, safe(instrsConstrCheck) = {},
   safe(instrConstrCheck) = {}, safe(notEmpty) = {},
   safe(Cons) = {1, 2}, safe(Nil) = {}, safe(0) = {},
   safe(instrsSecond) = {}, safe(instrsFirst) = {},
   safe(getWrite) = {}, safe(getGotoSecond) = {},
   safe(getGotoFirst) = {}, safe(getGoto) = {}, safe(run) = {},
   safe(turing^#) = {}, safe(c_1) = {}, safe(c_2) = {},
   safe(c_3) = {}, safe(c_4) = {}, safe(c_5) = {}, safe(c_6) = {},
   safe(c_7) = {}, safe(lookup^#) = {1}, safe(c_8) = {},
   safe(c_9) = {}, safe(instrsConstrCheck^#) = {}, safe(c_10) = {},
   safe(c_11) = {}, safe(c_12) = {}, safe(c_13) = {},
   safe(instrConstrCheck^#) = {}, safe(c_14) = {}, safe(c_15) = {},
   safe(c_16) = {}, safe(c_17) = {}, safe(c_18) = {}, safe(c_19) = {},
   safe(c_20) = {}, safe(c_21) = {}, safe(c_22) = {}, safe(c_23) = {},
   safe(c_24) = {}, safe(c_25) = {}, safe(c_26) = {}, safe(c_27) = {},
   safe(c_28) = {}, safe(c_29) = {}, safe(c_30) = {}, safe(c_31) = {},
   safe(c_32) = {}, safe(c_33) = {}, safe(c_34) = {}, safe(c_35) = {},
   safe(c_36) = {}, safe(c_37) = {}, safe(c_38) = {}, safe(c_39) = {},
   safe(c_40) = {}, safe(c_41) = {}, safe(c_42) = {}, safe(c_43) = {},
   safe(c_44) = {}, safe(c_45) = {}, safe(c_46) = {}, safe(c_47) = {},
   safe(c_48) = {}, safe(c_49) = {}, safe(notEmpty^#) = {},
   safe(c_50) = {}, safe(c_51) = {}, safe(instrsSecond^#) = {},
   safe(c_52) = {}, safe(instrsFirst^#) = {}, safe(c_53) = {},
   safe(getWrite^#) = {}, safe(c_54) = {}, safe(getGotoSecond^#) = {},
   safe(c_55) = {}, safe(getGotoFirst^#) = {}, safe(c_56) = {},
   safe(getGoto^#) = {}, safe(c_57) = {}, safe(run^#) = {},
   safe(c_58) = {}
  
  and precedence
  
   empty .
  
  Following symbols are considered recursive:
  
   {lookup^#}
  
  The recursion depth is 1.
  
  Further, following argument filtering is employed:
  
   pi(turing) = [], pi(I) = [2], pi(IfGoto) = [],
   pi(turing[Ite][True][Ite][False][Ite]) = [], pi(False) = [],
   pi(Goto) = [], pi(Right) = [], pi(Left) = [], pi(Write) = [],
   pi(True) = [], pi(Halt) = [], pi(Empty) = [], pi(lookup) = [],
   pi(S) = [], pi(instrsConstrCheck) = [], pi(instrConstrCheck) = [],
   pi(notEmpty) = [], pi(Cons) = [], pi(Nil) = [], pi(0) = [],
   pi(instrsSecond) = [], pi(instrsFirst) = [], pi(getWrite) = [],
   pi(getGotoSecond) = [], pi(getGotoFirst) = [], pi(getGoto) = [],
   pi(run) = [], pi(turing^#) = [], pi(c_1) = [], pi(c_2) = [],
   pi(c_3) = [], pi(c_4) = [], pi(c_5) = [], pi(c_6) = [],
   pi(c_7) = [], pi(lookup^#) = [2], pi(c_8) = [1], pi(c_9) = [],
   pi(instrsConstrCheck^#) = [], pi(c_10) = [], pi(c_11) = [],
   pi(c_12) = [], pi(c_13) = [], pi(instrConstrCheck^#) = [],
   pi(c_14) = [], pi(c_15) = [], pi(c_16) = [], pi(c_17) = [],
   pi(c_18) = [], pi(c_19) = [], pi(c_20) = [], pi(c_21) = [],
   pi(c_22) = [], pi(c_23) = [], pi(c_24) = [], pi(c_25) = [],
   pi(c_26) = [], pi(c_27) = [], pi(c_28) = [], pi(c_29) = [],
   pi(c_30) = [], pi(c_31) = [], pi(c_32) = [], pi(c_33) = [],
   pi(c_34) = [], pi(c_35) = [], pi(c_36) = [], pi(c_37) = [],
   pi(c_38) = [], pi(c_39) = [], pi(c_40) = [], pi(c_41) = [],
   pi(c_42) = [], pi(c_43) = [], pi(c_44) = [], pi(c_45) = [],
   pi(c_46) = [], pi(c_47) = [], pi(c_48) = [], pi(c_49) = [],
   pi(notEmpty^#) = [], pi(c_50) = [], pi(c_51) = [],
   pi(instrsSecond^#) = [], pi(c_52) = [], pi(instrsFirst^#) = [],
   pi(c_53) = [], pi(getWrite^#) = [], pi(c_54) = [],
   pi(getGotoSecond^#) = [], pi(c_55) = [], pi(getGotoFirst^#) = [],
   pi(c_56) = [], pi(getGoto^#) = [], pi(c_57) = [], pi(run^#) = [],
   pi(c_58) = []
  
  Usable defined function symbols are a subset of:
  
   {turing^#, lookup^#, instrsConstrCheck^#, instrConstrCheck^#,
    notEmpty^#, instrsSecond^#, instrsFirst^#, getWrite^#,
    getGotoSecond^#, getGotoFirst^#, getGoto^#, run^#}
  
  For your convenience, here are the satisfied ordering constraints:
  
    pi(lookup^#(S(x), I(l, r))) = lookup^#(I(; r);)      
                                > c_8(lookup^#(r;);)     
                                = pi(c_8(lookup^#(x, r)))
                                                         

The strictly oriented rules are moved into the weak component.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak DPs: { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) }

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Rules: Empty
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))