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))