YES(O(1),O(n^1)) 9.05/2.48 YES(O(1),O(n^1)) 9.05/2.48 9.05/2.48 We are left with following problem, upon which TcT provides the 9.05/2.48 certificate YES(O(1),O(n^1)). 9.05/2.48 9.05/2.48 Strict Trs: 9.05/2.48 { turing(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) -> 9.05/2.48 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.48 I(IfGoto(igtNat1, igtNat2), r), 9.05/2.48 revltape, 9.05/2.48 rtape, 9.05/2.48 prog) 9.05/2.48 , turing(I(Goto(gtNat), r), revltape, rtape, prog) -> 9.05/2.48 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.48 I(Goto(gtNat), r), 9.05/2.48 revltape, 9.05/2.48 rtape, 9.05/2.48 prog) 9.05/2.48 , turing(I(Right(), r), revltape, rtape, prog) -> 9.05/2.48 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.48 I(Right(), r), 9.05/2.48 revltape, 9.05/2.48 rtape, 9.05/2.48 prog) 9.05/2.48 , turing(I(Left(), r), revltape, rtape, prog) -> 9.05/2.48 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.48 I(Left(), r), 9.05/2.48 revltape, 9.05/2.48 rtape, 9.05/2.48 prog) 9.05/2.48 , turing(I(Write(wNat), r), revltape, rtape, prog) -> 9.05/2.48 turing[Ite][True][Ite][False][Ite](True(), 9.05/2.48 I(Write(wNat), r), 9.05/2.48 revltape, 9.05/2.48 rtape, 9.05/2.48 prog) 9.05/2.48 , turing(I(Halt(), r), revltape, rtape, prog) -> rtape 9.05/2.48 , turing(Empty(), revltape, rtape, prog) -> rtape 9.05/2.48 , lookup(S(x), I(l, r)) -> lookup(x, r) 9.05/2.48 , lookup(0(), instrs) -> instrs 9.05/2.48 , instrsConstrCheck(I(l1, r1), I(x, y)) -> True() 9.05/2.48 , instrsConstrCheck(I(l1, r1), Empty()) -> False() 9.05/2.48 , instrsConstrCheck(Empty(), I(x, y)) -> False() 9.05/2.48 , instrsConstrCheck(Empty(), Empty()) -> True() 9.05/2.48 , instrConstrCheck(IfGoto(igtNat1, igtNat2), 9.05/2.48 IfGoto(igtNat12, igtNat22)) 9.05/2.48 -> True() 9.05/2.48 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.05/2.48 False() 9.05/2.48 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Right()) -> False() 9.05/2.48 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Left()) -> False() 9.05/2.48 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.05/2.48 False() 9.05/2.48 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt()) -> False() 9.05/2.48 , instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.48 False() 9.05/2.48 , instrConstrCheck(Goto(gtNat), Goto(gtNat2)) -> True() 9.05/2.48 , instrConstrCheck(Goto(gtNat), Right()) -> False() 9.05/2.48 , instrConstrCheck(Goto(gtNat), Left()) -> False() 9.05/2.48 , instrConstrCheck(Goto(gtNat), Write(wNat2)) -> False() 9.05/2.48 , instrConstrCheck(Goto(gtNat), Halt()) -> False() 9.05/2.48 , instrConstrCheck(Right(), IfGoto(igtNat12, igtNat22)) -> False() 9.05/2.48 , instrConstrCheck(Right(), Goto(gtNat2)) -> False() 9.05/2.48 , instrConstrCheck(Right(), Right()) -> True() 9.05/2.48 , instrConstrCheck(Right(), Left()) -> False() 9.05/2.48 , instrConstrCheck(Right(), Write(wNat2)) -> False() 9.05/2.48 , instrConstrCheck(Right(), Halt()) -> False() 9.05/2.48 , instrConstrCheck(Left(), IfGoto(igtNat12, igtNat22)) -> False() 9.05/2.48 , instrConstrCheck(Left(), Goto(gtNat2)) -> False() 9.05/2.48 , instrConstrCheck(Left(), Right()) -> False() 9.05/2.48 , instrConstrCheck(Left(), Left()) -> True() 9.05/2.48 , instrConstrCheck(Left(), Write(wNat2)) -> False() 9.05/2.48 , instrConstrCheck(Left(), Halt()) -> False() 9.05/2.48 , instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.48 False() 9.05/2.48 , instrConstrCheck(Write(wNat), Goto(gtNat2)) -> False() 9.05/2.48 , instrConstrCheck(Write(wNat), Right()) -> False() 9.05/2.48 , instrConstrCheck(Write(wNat), Left()) -> False() 9.05/2.48 , instrConstrCheck(Write(wNat), Write(wNat2)) -> True() 9.05/2.48 , instrConstrCheck(Write(wNat), Halt()) -> False() 9.05/2.48 , instrConstrCheck(Halt(), IfGoto(igtNat12, igtNat22)) -> False() 9.05/2.48 , instrConstrCheck(Halt(), Goto(gtNat2)) -> False() 9.05/2.48 , instrConstrCheck(Halt(), Right()) -> False() 9.05/2.48 , instrConstrCheck(Halt(), Left()) -> False() 9.05/2.48 , instrConstrCheck(Halt(), Write(wNat2)) -> False() 9.05/2.48 , instrConstrCheck(Halt(), Halt()) -> True() 9.05/2.48 , notEmpty(Cons(x, xs)) -> True() 9.05/2.48 , notEmpty(Nil()) -> False() 9.05/2.48 , instrsSecond(I(l, r)) -> r 9.05/2.48 , instrsFirst(I(l, r)) -> l 9.05/2.48 , getWrite(Write(int)) -> int 9.05/2.48 , getGotoSecond(IfGoto(i1, i2)) -> i2 9.05/2.48 , getGotoFirst(IfGoto(i1, i2)) -> i1 9.05/2.48 , getGoto(Goto(int)) -> int 9.05/2.48 , run(prog, tapeinput) -> turing(prog, Nil(), tapeinput, prog) } 9.05/2.48 Obligation: 9.05/2.48 innermost runtime complexity 9.05/2.48 Answer: 9.05/2.48 YES(O(1),O(n^1)) 9.05/2.48 9.05/2.48 We add the following weak dependency pairs: 9.05/2.48 9.05/2.48 Strict DPs: 9.05/2.48 { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) 9.05/2.48 -> c_1() 9.05/2.48 , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.05/2.48 , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.05/2.48 , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.05/2.48 , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.05/2.48 , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.05/2.48 , turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.05/2.48 , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) 9.05/2.48 , lookup^#(0(), instrs) -> c_9() 9.05/2.48 , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.05/2.48 , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.05/2.48 , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.05/2.48 , instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.05/2.48 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.05/2.48 IfGoto(igtNat12, igtNat22)) 9.05/2.48 -> c_14() 9.05/2.48 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.05/2.48 c_15() 9.05/2.48 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16() 9.05/2.48 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17() 9.05/2.48 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.05/2.48 c_18() 9.05/2.48 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19() 9.05/2.48 , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.48 c_20() 9.05/2.48 , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.05/2.48 , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.05/2.48 , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.05/2.48 , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.05/2.48 , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.05/2.48 , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26() 9.05/2.48 , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.05/2.48 , instrConstrCheck^#(Right(), Right()) -> c_28() 9.05/2.48 , instrConstrCheck^#(Right(), Left()) -> c_29() 9.05/2.48 , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.05/2.48 , instrConstrCheck^#(Right(), Halt()) -> c_31() 9.05/2.48 , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32() 9.05/2.48 , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.05/2.48 , instrConstrCheck^#(Left(), Right()) -> c_34() 9.05/2.48 , instrConstrCheck^#(Left(), Left()) -> c_35() 9.05/2.48 , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.05/2.48 , instrConstrCheck^#(Left(), Halt()) -> c_37() 9.05/2.48 , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.48 c_38() 9.05/2.48 , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.05/2.48 , instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.05/2.48 , instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.05/2.48 , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.05/2.48 , instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.05/2.48 , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44() 9.05/2.48 , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.05/2.48 , instrConstrCheck^#(Halt(), Right()) -> c_46() 9.05/2.48 , instrConstrCheck^#(Halt(), Left()) -> c_47() 9.05/2.48 , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.05/2.48 , instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.05/2.48 , notEmpty^#(Cons(x, xs)) -> c_50() 9.05/2.48 , notEmpty^#(Nil()) -> c_51() 9.05/2.48 , instrsSecond^#(I(l, r)) -> c_52() 9.05/2.48 , instrsFirst^#(I(l, r)) -> c_53() 9.05/2.48 , getWrite^#(Write(int)) -> c_54() 9.05/2.48 , getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.05/2.48 , getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.05/2.48 , getGoto^#(Goto(int)) -> c_57() 9.05/2.48 , run^#(prog, tapeinput) -> 9.05/2.48 c_58(turing^#(prog, Nil(), tapeinput, prog)) } 9.05/2.48 9.05/2.48 and mark the set of starting terms. 9.05/2.48 9.05/2.48 We are left with following problem, upon which TcT provides the 9.05/2.48 certificate YES(O(1),O(n^1)). 9.05/2.48 9.05/2.48 Strict DPs: 9.05/2.48 { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) 9.05/2.49 -> c_1() 9.05/2.49 , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.05/2.49 , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.05/2.49 , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.05/2.49 , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.05/2.49 , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.05/2.49 , turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.05/2.49 , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) 9.05/2.49 , lookup^#(0(), instrs) -> c_9() 9.05/2.49 , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.05/2.49 , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.05/2.49 , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.05/2.49 , instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.05/2.49 IfGoto(igtNat12, igtNat22)) 9.05/2.49 -> c_14() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.05/2.49 c_15() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.05/2.49 c_18() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.49 c_20() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.05/2.49 , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26() 9.05/2.49 , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.05/2.49 , instrConstrCheck^#(Right(), Right()) -> c_28() 9.05/2.49 , instrConstrCheck^#(Right(), Left()) -> c_29() 9.05/2.49 , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.05/2.49 , instrConstrCheck^#(Right(), Halt()) -> c_31() 9.05/2.49 , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32() 9.05/2.49 , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.05/2.49 , instrConstrCheck^#(Left(), Right()) -> c_34() 9.05/2.49 , instrConstrCheck^#(Left(), Left()) -> c_35() 9.05/2.49 , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.05/2.49 , instrConstrCheck^#(Left(), Halt()) -> c_37() 9.05/2.49 , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.49 c_38() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.05/2.49 , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44() 9.05/2.49 , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.05/2.49 , instrConstrCheck^#(Halt(), Right()) -> c_46() 9.05/2.49 , instrConstrCheck^#(Halt(), Left()) -> c_47() 9.05/2.49 , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.05/2.49 , instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.05/2.49 , notEmpty^#(Cons(x, xs)) -> c_50() 9.05/2.49 , notEmpty^#(Nil()) -> c_51() 9.05/2.49 , instrsSecond^#(I(l, r)) -> c_52() 9.05/2.49 , instrsFirst^#(I(l, r)) -> c_53() 9.05/2.49 , getWrite^#(Write(int)) -> c_54() 9.05/2.49 , getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.05/2.49 , getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.05/2.49 , getGoto^#(Goto(int)) -> c_57() 9.05/2.49 , run^#(prog, tapeinput) -> 9.05/2.49 c_58(turing^#(prog, Nil(), tapeinput, prog)) } 9.05/2.49 Strict Trs: 9.05/2.49 { turing(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) -> 9.05/2.49 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.49 I(IfGoto(igtNat1, igtNat2), r), 9.05/2.49 revltape, 9.05/2.49 rtape, 9.05/2.49 prog) 9.05/2.49 , turing(I(Goto(gtNat), r), revltape, rtape, prog) -> 9.05/2.49 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.49 I(Goto(gtNat), r), 9.05/2.49 revltape, 9.05/2.49 rtape, 9.05/2.49 prog) 9.05/2.49 , turing(I(Right(), r), revltape, rtape, prog) -> 9.05/2.49 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.49 I(Right(), r), 9.05/2.49 revltape, 9.05/2.49 rtape, 9.05/2.49 prog) 9.05/2.49 , turing(I(Left(), r), revltape, rtape, prog) -> 9.05/2.49 turing[Ite][True][Ite][False][Ite](False(), 9.05/2.49 I(Left(), r), 9.05/2.49 revltape, 9.05/2.49 rtape, 9.05/2.49 prog) 9.05/2.49 , turing(I(Write(wNat), r), revltape, rtape, prog) -> 9.05/2.49 turing[Ite][True][Ite][False][Ite](True(), 9.05/2.49 I(Write(wNat), r), 9.05/2.49 revltape, 9.05/2.49 rtape, 9.05/2.49 prog) 9.05/2.49 , turing(I(Halt(), r), revltape, rtape, prog) -> rtape 9.05/2.49 , turing(Empty(), revltape, rtape, prog) -> rtape 9.05/2.49 , lookup(S(x), I(l, r)) -> lookup(x, r) 9.05/2.49 , lookup(0(), instrs) -> instrs 9.05/2.49 , instrsConstrCheck(I(l1, r1), I(x, y)) -> True() 9.05/2.49 , instrsConstrCheck(I(l1, r1), Empty()) -> False() 9.05/2.49 , instrsConstrCheck(Empty(), I(x, y)) -> False() 9.05/2.49 , instrsConstrCheck(Empty(), Empty()) -> True() 9.05/2.49 , instrConstrCheck(IfGoto(igtNat1, igtNat2), 9.05/2.49 IfGoto(igtNat12, igtNat22)) 9.05/2.49 -> True() 9.05/2.49 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.05/2.49 False() 9.05/2.49 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Right()) -> False() 9.05/2.49 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Left()) -> False() 9.05/2.49 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.05/2.49 False() 9.05/2.49 , instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt()) -> False() 9.05/2.49 , instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.49 False() 9.05/2.49 , instrConstrCheck(Goto(gtNat), Goto(gtNat2)) -> True() 9.05/2.49 , instrConstrCheck(Goto(gtNat), Right()) -> False() 9.05/2.49 , instrConstrCheck(Goto(gtNat), Left()) -> False() 9.05/2.49 , instrConstrCheck(Goto(gtNat), Write(wNat2)) -> False() 9.05/2.49 , instrConstrCheck(Goto(gtNat), Halt()) -> False() 9.05/2.49 , instrConstrCheck(Right(), IfGoto(igtNat12, igtNat22)) -> False() 9.05/2.49 , instrConstrCheck(Right(), Goto(gtNat2)) -> False() 9.05/2.49 , instrConstrCheck(Right(), Right()) -> True() 9.05/2.49 , instrConstrCheck(Right(), Left()) -> False() 9.05/2.49 , instrConstrCheck(Right(), Write(wNat2)) -> False() 9.05/2.49 , instrConstrCheck(Right(), Halt()) -> False() 9.05/2.49 , instrConstrCheck(Left(), IfGoto(igtNat12, igtNat22)) -> False() 9.05/2.49 , instrConstrCheck(Left(), Goto(gtNat2)) -> False() 9.05/2.49 , instrConstrCheck(Left(), Right()) -> False() 9.05/2.49 , instrConstrCheck(Left(), Left()) -> True() 9.05/2.49 , instrConstrCheck(Left(), Write(wNat2)) -> False() 9.05/2.49 , instrConstrCheck(Left(), Halt()) -> False() 9.05/2.49 , instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.49 False() 9.05/2.49 , instrConstrCheck(Write(wNat), Goto(gtNat2)) -> False() 9.05/2.49 , instrConstrCheck(Write(wNat), Right()) -> False() 9.05/2.49 , instrConstrCheck(Write(wNat), Left()) -> False() 9.05/2.49 , instrConstrCheck(Write(wNat), Write(wNat2)) -> True() 9.05/2.49 , instrConstrCheck(Write(wNat), Halt()) -> False() 9.05/2.49 , instrConstrCheck(Halt(), IfGoto(igtNat12, igtNat22)) -> False() 9.05/2.49 , instrConstrCheck(Halt(), Goto(gtNat2)) -> False() 9.05/2.49 , instrConstrCheck(Halt(), Right()) -> False() 9.05/2.49 , instrConstrCheck(Halt(), Left()) -> False() 9.05/2.49 , instrConstrCheck(Halt(), Write(wNat2)) -> False() 9.05/2.49 , instrConstrCheck(Halt(), Halt()) -> True() 9.05/2.49 , notEmpty(Cons(x, xs)) -> True() 9.05/2.49 , notEmpty(Nil()) -> False() 9.05/2.49 , instrsSecond(I(l, r)) -> r 9.05/2.49 , instrsFirst(I(l, r)) -> l 9.05/2.49 , getWrite(Write(int)) -> int 9.05/2.49 , getGotoSecond(IfGoto(i1, i2)) -> i2 9.05/2.49 , getGotoFirst(IfGoto(i1, i2)) -> i1 9.05/2.49 , getGoto(Goto(int)) -> int 9.05/2.49 , run(prog, tapeinput) -> turing(prog, Nil(), tapeinput, prog) } 9.05/2.49 Obligation: 9.05/2.49 innermost runtime complexity 9.05/2.49 Answer: 9.05/2.49 YES(O(1),O(n^1)) 9.05/2.49 9.05/2.49 No rule is usable, rules are removed from the input problem. 9.05/2.49 9.05/2.49 We are left with following problem, upon which TcT provides the 9.05/2.49 certificate YES(O(1),O(n^1)). 9.05/2.49 9.05/2.49 Strict DPs: 9.05/2.49 { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) 9.05/2.49 -> c_1() 9.05/2.49 , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.05/2.49 , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.05/2.49 , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.05/2.49 , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.05/2.49 , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.05/2.49 , turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.05/2.49 , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) 9.05/2.49 , lookup^#(0(), instrs) -> c_9() 9.05/2.49 , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.05/2.49 , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.05/2.49 , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.05/2.49 , instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.05/2.49 IfGoto(igtNat12, igtNat22)) 9.05/2.49 -> c_14() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.05/2.49 c_15() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.05/2.49 c_18() 9.05/2.49 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.49 c_20() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.05/2.49 , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.05/2.49 , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26() 9.05/2.49 , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.05/2.49 , instrConstrCheck^#(Right(), Right()) -> c_28() 9.05/2.49 , instrConstrCheck^#(Right(), Left()) -> c_29() 9.05/2.49 , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.05/2.49 , instrConstrCheck^#(Right(), Halt()) -> c_31() 9.05/2.49 , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32() 9.05/2.49 , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.05/2.49 , instrConstrCheck^#(Left(), Right()) -> c_34() 9.05/2.49 , instrConstrCheck^#(Left(), Left()) -> c_35() 9.05/2.49 , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.05/2.49 , instrConstrCheck^#(Left(), Halt()) -> c_37() 9.05/2.49 , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.05/2.49 c_38() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.05/2.49 , instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.05/2.49 , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44() 9.05/2.49 , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.05/2.49 , instrConstrCheck^#(Halt(), Right()) -> c_46() 9.05/2.49 , instrConstrCheck^#(Halt(), Left()) -> c_47() 9.05/2.49 , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.05/2.49 , instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.05/2.49 , notEmpty^#(Cons(x, xs)) -> c_50() 9.05/2.49 , notEmpty^#(Nil()) -> c_51() 9.05/2.49 , instrsSecond^#(I(l, r)) -> c_52() 9.05/2.49 , instrsFirst^#(I(l, r)) -> c_53() 9.05/2.49 , getWrite^#(Write(int)) -> c_54() 9.05/2.49 , getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.05/2.49 , getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.05/2.49 , getGoto^#(Goto(int)) -> c_57() 9.05/2.49 , run^#(prog, tapeinput) -> 9.05/2.49 c_58(turing^#(prog, Nil(), tapeinput, prog)) } 9.05/2.49 Obligation: 9.05/2.49 innermost runtime complexity 9.05/2.49 Answer: 9.05/2.49 YES(O(1),O(n^1)) 9.05/2.49 9.05/2.49 The weightgap principle applies (using the following constant 9.05/2.49 growth matrix-interpretation) 9.05/2.49 9.05/2.49 The following argument positions are usable: 9.05/2.49 Uargs(c_8) = {1}, Uargs(c_58) = {1} 9.05/2.49 9.05/2.49 TcT has computed the following constructor-restricted matrix 9.05/2.49 interpretation. 9.05/2.49 9.05/2.49 [I](x1, x2) = [1 0] x2 + [0] 9.05/2.49 [0 0] [0] 9.05/2.49 9.05/2.49 [IfGoto](x1, x2) = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [Goto](x1) = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [Right] = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [Left] = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [Write](x1) = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [Halt] = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [Empty] = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [S](x1) = [1 0] x1 + [0] 9.05/2.49 [0 0] [0] 9.05/2.49 9.05/2.49 [Cons](x1, x2) = [1] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [Nil] = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [0] = [1] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [turing^#](x1, x2, x3, x4) = [2 1] x2 + [1 1] x3 + [1 9.05/2.49 1] x4 + [0] 9.05/2.49 [2 2] [1 1] [2 9.05/2.49 2] [0] 9.05/2.49 9.05/2.49 [c_1] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_2] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_3] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_4] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_5] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_6] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_7] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [lookup^#](x1, x2) = [0] 9.05/2.49 [2] 9.05/2.49 9.05/2.49 [c_8](x1) = [1 0] x1 + [2] 9.05/2.49 [0 1] [0] 9.05/2.49 9.05/2.49 [c_9] = [1] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [instrsConstrCheck^#](x1, x2) = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_10] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_11] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_12] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_13] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [instrConstrCheck^#](x1, x2) = [0] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_14] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_15] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_16] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_17] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_18] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_19] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_20] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_21] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_22] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_23] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_24] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_25] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_26] = [2] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_27] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_28] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_29] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_30] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_31] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_32] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_33] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_34] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_35] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_36] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_37] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_38] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_39] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_40] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_41] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_42] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_43] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_44] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_45] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_46] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_47] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_48] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_49] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [notEmpty^#](x1) = [0 0] x1 + [0] 9.05/2.49 [1 1] [2] 9.05/2.49 9.05/2.49 [c_50] = [1] 9.05/2.49 [0] 9.05/2.49 9.05/2.49 [c_51] = [1] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [instrsSecond^#](x1) = [1 1] x1 + [0] 9.05/2.49 [1 2] [2] 9.05/2.49 9.05/2.49 [c_52] = [1] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [instrsFirst^#](x1) = [2 1] x1 + [0] 9.05/2.49 [2 2] [2] 9.05/2.49 9.05/2.49 [c_53] = [1] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [getWrite^#](x1) = [1 2] x1 + [1] 9.05/2.49 [2 1] [2] 9.05/2.49 9.05/2.49 [c_54] = [0] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [getGotoSecond^#](x1) = [2 2] x1 + [1] 9.05/2.49 [1 1] [2] 9.05/2.49 9.05/2.49 [c_55] = [0] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [getGotoFirst^#](x1) = [1 1] x1 + [1] 9.05/2.49 [1 1] [2] 9.05/2.49 9.05/2.49 [c_56] = [0] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [getGoto^#](x1) = [1 1] x1 + [1] 9.05/2.49 [1 2] [2] 9.05/2.49 9.05/2.49 [c_57] = [0] 9.05/2.49 [1] 9.05/2.49 9.05/2.49 [run^#](x1, x2) = [2 2] x1 + [1 2] x2 + [1] 9.05/2.49 [2 2] [2 2] [2] 9.05/2.49 9.05/2.49 [c_58](x1) = [1 0] x1 + [2] 9.05/2.49 [0 1] [2] 9.05/2.49 9.05/2.49 The order satisfies the following ordering constraints: 9.05/2.49 9.05/2.49 [turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0] 9.05/2.49 [2 2] [1 1] [2 2] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_1()] 9.05/2.49 9.05/2.49 [turing^#(I(Goto(gtNat), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0] 9.05/2.49 [2 2] [1 1] [2 2] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_2()] 9.05/2.49 9.05/2.49 [turing^#(I(Right(), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0] 9.05/2.49 [2 2] [1 1] [2 2] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_3()] 9.05/2.49 9.05/2.49 [turing^#(I(Left(), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0] 9.05/2.49 [2 2] [1 1] [2 2] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_4()] 9.05/2.49 9.05/2.49 [turing^#(I(Write(wNat), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0] 9.05/2.49 [2 2] [1 1] [2 2] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_5()] 9.05/2.49 9.05/2.49 [turing^#(I(Halt(), r), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0] 9.05/2.49 [2 2] [1 1] [2 2] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_6()] 9.05/2.49 9.05/2.49 [turing^#(Empty(), revltape, rtape, prog)] = [2 1] revltape + [1 1] rtape + [1 1] prog + [0] 9.05/2.49 [2 2] [1 1] [2 2] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_7()] 9.05/2.49 9.05/2.49 [lookup^#(S(x), I(l, r))] = [0] 9.05/2.49 [2] 9.05/2.49 ? [2] 9.05/2.49 [2] 9.05/2.49 = [c_8(lookup^#(x, r))] 9.05/2.49 9.05/2.49 [lookup^#(0(), instrs)] = [0] 9.05/2.49 [2] 9.05/2.49 ? [1] 9.05/2.49 [1] 9.05/2.49 = [c_9()] 9.05/2.49 9.05/2.49 [instrsConstrCheck^#(I(l1, r1), I(x, y))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_10()] 9.05/2.49 9.05/2.49 [instrsConstrCheck^#(I(l1, r1), Empty())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_11()] 9.05/2.49 9.05/2.49 [instrsConstrCheck^#(Empty(), I(x, y))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_12()] 9.05/2.49 9.05/2.49 [instrsConstrCheck^#(Empty(), Empty())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_13()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), = [0] 9.05/2.49 IfGoto(igtNat12, igtNat22))] [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_14()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_15()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_16()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_17()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_18()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_19()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_20()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Goto(gtNat), Goto(gtNat2))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_21()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Goto(gtNat), Right())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_22()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Goto(gtNat), Left())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_23()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Goto(gtNat), Write(wNat2))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_24()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Goto(gtNat), Halt())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_25()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [2] 9.05/2.49 [0] 9.05/2.49 = [c_26()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Right(), Goto(gtNat2))] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_27()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Right(), Right())] = [0] 9.05/2.49 [0] 9.05/2.49 ? [1] 9.05/2.49 [0] 9.05/2.49 = [c_28()] 9.05/2.49 9.05/2.49 [instrConstrCheck^#(Right(), Left())] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_29()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Right(), Write(wNat2))] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_30()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Right(), Halt())] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_31()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22))] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_32()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Left(), Goto(gtNat2))] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_33()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Left(), Right())] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_34()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Left(), Left())] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_35()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Left(), Write(wNat2))] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_36()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Left(), Halt())] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_37()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22))] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_38()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Write(wNat), Goto(gtNat2))] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.05/2.50 = [c_39()] 9.05/2.50 9.05/2.50 [instrConstrCheck^#(Write(wNat), Right())] = [0] 9.05/2.50 [0] 9.05/2.50 ? [1] 9.05/2.50 [0] 9.41/2.50 = [c_40()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Write(wNat), Left())] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_41()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Write(wNat), Write(wNat2))] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_42()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Write(wNat), Halt())] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_43()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22))] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_44()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Halt(), Goto(gtNat2))] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_45()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Halt(), Right())] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_46()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Halt(), Left())] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_47()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Halt(), Write(wNat2))] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_48()] 9.41/2.50 9.41/2.50 [instrConstrCheck^#(Halt(), Halt())] = [0] 9.41/2.50 [0] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_49()] 9.41/2.50 9.41/2.50 [notEmpty^#(Cons(x, xs))] = [0] 9.41/2.50 [4] 9.41/2.50 ? [1] 9.41/2.50 [0] 9.41/2.50 = [c_50()] 9.41/2.50 9.41/2.50 [notEmpty^#(Nil())] = [0] 9.41/2.50 [2] 9.41/2.50 ? [1] 9.41/2.50 [1] 9.41/2.50 = [c_51()] 9.41/2.50 9.41/2.50 [instrsSecond^#(I(l, r))] = [1 0] r + [0] 9.41/2.50 [1 0] [2] 9.41/2.50 ? [1] 9.41/2.50 [1] 9.41/2.50 = [c_52()] 9.41/2.50 9.41/2.50 [instrsFirst^#(I(l, r))] = [2 0] r + [0] 9.41/2.50 [2 0] [2] 9.41/2.50 ? [1] 9.41/2.50 [1] 9.41/2.50 = [c_53()] 9.41/2.50 9.41/2.50 [getWrite^#(Write(int))] = [1] 9.41/2.50 [2] 9.41/2.50 > [0] 9.41/2.50 [1] 9.41/2.50 = [c_54()] 9.41/2.50 9.41/2.50 [getGotoSecond^#(IfGoto(i1, i2))] = [1] 9.41/2.50 [2] 9.41/2.50 > [0] 9.41/2.50 [1] 9.41/2.50 = [c_55()] 9.41/2.50 9.41/2.50 [getGotoFirst^#(IfGoto(i1, i2))] = [1] 9.41/2.50 [2] 9.41/2.50 > [0] 9.41/2.50 [1] 9.41/2.50 = [c_56()] 9.41/2.50 9.41/2.50 [getGoto^#(Goto(int))] = [1] 9.41/2.50 [2] 9.41/2.50 > [0] 9.41/2.50 [1] 9.41/2.50 = [c_57()] 9.41/2.50 9.41/2.50 [run^#(prog, tapeinput)] = [2 2] prog + [1 2] tapeinput + [1] 9.41/2.50 [2 2] [2 2] [2] 9.41/2.50 ? [1 1] prog + [1 1] tapeinput + [2] 9.41/2.50 [2 2] [1 1] [2] 9.41/2.50 = [c_58(turing^#(prog, Nil(), tapeinput, prog))] 9.41/2.50 9.41/2.50 9.41/2.50 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 9.41/2.50 9.41/2.50 We are left with following problem, upon which TcT provides the 9.41/2.50 certificate YES(O(1),O(n^1)). 9.41/2.50 9.41/2.50 Strict DPs: 9.41/2.50 { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) 9.41/2.50 -> c_1() 9.41/2.50 , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.41/2.50 , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.41/2.50 , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.41/2.50 , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.41/2.50 , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.41/2.50 , turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.41/2.50 , lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) 9.41/2.50 , lookup^#(0(), instrs) -> c_9() 9.41/2.50 , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.41/2.50 , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.41/2.50 , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.41/2.50 , instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.41/2.50 IfGoto(igtNat12, igtNat22)) 9.41/2.50 -> c_14() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.41/2.50 c_15() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.41/2.50 c_18() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.50 c_20() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.41/2.50 , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26() 9.41/2.50 , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.41/2.50 , instrConstrCheck^#(Right(), Right()) -> c_28() 9.41/2.50 , instrConstrCheck^#(Right(), Left()) -> c_29() 9.41/2.50 , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.41/2.50 , instrConstrCheck^#(Right(), Halt()) -> c_31() 9.41/2.50 , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32() 9.41/2.50 , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.41/2.50 , instrConstrCheck^#(Left(), Right()) -> c_34() 9.41/2.50 , instrConstrCheck^#(Left(), Left()) -> c_35() 9.41/2.50 , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.41/2.50 , instrConstrCheck^#(Left(), Halt()) -> c_37() 9.41/2.50 , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.50 c_38() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.41/2.50 , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44() 9.41/2.50 , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.41/2.50 , instrConstrCheck^#(Halt(), Right()) -> c_46() 9.41/2.50 , instrConstrCheck^#(Halt(), Left()) -> c_47() 9.41/2.50 , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.41/2.50 , instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.41/2.50 , notEmpty^#(Cons(x, xs)) -> c_50() 9.41/2.50 , notEmpty^#(Nil()) -> c_51() 9.41/2.50 , instrsSecond^#(I(l, r)) -> c_52() 9.41/2.50 , instrsFirst^#(I(l, r)) -> c_53() 9.41/2.50 , run^#(prog, tapeinput) -> 9.41/2.50 c_58(turing^#(prog, Nil(), tapeinput, prog)) } 9.41/2.50 Weak DPs: 9.41/2.50 { getWrite^#(Write(int)) -> c_54() 9.41/2.50 , getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.41/2.50 , getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.41/2.50 , getGoto^#(Goto(int)) -> c_57() } 9.41/2.50 Obligation: 9.41/2.50 innermost runtime complexity 9.41/2.50 Answer: 9.41/2.50 YES(O(1),O(n^1)) 9.41/2.50 9.41/2.50 We estimate the number of application of 9.41/2.50 {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} 9.41/2.50 by applications of 9.41/2.50 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}) 9.41/2.50 = {8,54}. Here rules are labeled as follows: 9.41/2.50 9.41/2.50 DPs: 9.41/2.50 { 1: turing^#(I(IfGoto(igtNat1, igtNat2), r), 9.41/2.50 revltape, 9.41/2.50 rtape, 9.41/2.50 prog) 9.41/2.50 -> c_1() 9.41/2.50 , 2: turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.41/2.50 , 3: turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.41/2.50 , 4: turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.41/2.50 , 5: turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.41/2.50 , 6: turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.41/2.50 , 7: turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.41/2.50 , 8: lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) 9.41/2.50 , 9: lookup^#(0(), instrs) -> c_9() 9.41/2.50 , 10: instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.41/2.50 , 11: instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.41/2.50 , 12: instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.41/2.50 , 13: instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.41/2.50 , 14: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.41/2.50 IfGoto(igtNat12, igtNat22)) 9.41/2.50 -> c_14() 9.41/2.50 , 15: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.41/2.50 c_15() 9.41/2.50 , 16: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> 9.41/2.50 c_16() 9.41/2.50 , 17: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> 9.41/2.50 c_17() 9.41/2.50 , 18: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.41/2.50 c_18() 9.41/2.50 , 19: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> 9.41/2.50 c_19() 9.41/2.50 , 20: instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) 9.41/2.50 -> c_20() 9.41/2.50 , 21: instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.41/2.50 , 22: instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.41/2.50 , 23: instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.41/2.50 , 24: instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.41/2.50 , 25: instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.41/2.50 , 26: instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> 9.41/2.50 c_26() 9.41/2.50 , 27: instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.41/2.50 , 28: instrConstrCheck^#(Right(), Right()) -> c_28() 9.41/2.50 , 29: instrConstrCheck^#(Right(), Left()) -> c_29() 9.41/2.50 , 30: instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.41/2.50 , 31: instrConstrCheck^#(Right(), Halt()) -> c_31() 9.41/2.50 , 32: instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> 9.41/2.50 c_32() 9.41/2.50 , 33: instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.41/2.50 , 34: instrConstrCheck^#(Left(), Right()) -> c_34() 9.41/2.50 , 35: instrConstrCheck^#(Left(), Left()) -> c_35() 9.41/2.50 , 36: instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.41/2.50 , 37: instrConstrCheck^#(Left(), Halt()) -> c_37() 9.41/2.50 , 38: instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) 9.41/2.50 -> c_38() 9.41/2.50 , 39: instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.41/2.50 , 40: instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.41/2.50 , 41: instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.41/2.50 , 42: instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.41/2.50 , 43: instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.41/2.50 , 44: instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> 9.41/2.50 c_44() 9.41/2.50 , 45: instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.41/2.50 , 46: instrConstrCheck^#(Halt(), Right()) -> c_46() 9.41/2.50 , 47: instrConstrCheck^#(Halt(), Left()) -> c_47() 9.41/2.50 , 48: instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.41/2.50 , 49: instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.41/2.50 , 50: notEmpty^#(Cons(x, xs)) -> c_50() 9.41/2.50 , 51: notEmpty^#(Nil()) -> c_51() 9.41/2.50 , 52: instrsSecond^#(I(l, r)) -> c_52() 9.41/2.50 , 53: instrsFirst^#(I(l, r)) -> c_53() 9.41/2.50 , 54: run^#(prog, tapeinput) -> 9.41/2.50 c_58(turing^#(prog, Nil(), tapeinput, prog)) 9.41/2.50 , 55: getWrite^#(Write(int)) -> c_54() 9.41/2.50 , 56: getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.41/2.50 , 57: getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.41/2.50 , 58: getGoto^#(Goto(int)) -> c_57() } 9.41/2.50 9.41/2.50 We are left with following problem, upon which TcT provides the 9.41/2.50 certificate YES(O(1),O(n^1)). 9.41/2.50 9.41/2.50 Strict DPs: 9.41/2.50 { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) 9.41/2.50 , run^#(prog, tapeinput) -> 9.41/2.50 c_58(turing^#(prog, Nil(), tapeinput, prog)) } 9.41/2.50 Weak DPs: 9.41/2.50 { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) 9.41/2.50 -> c_1() 9.41/2.50 , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.41/2.50 , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.41/2.50 , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.41/2.50 , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.41/2.50 , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.41/2.50 , turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.41/2.50 , lookup^#(0(), instrs) -> c_9() 9.41/2.50 , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.41/2.50 , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.41/2.50 , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.41/2.50 , instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.41/2.50 IfGoto(igtNat12, igtNat22)) 9.41/2.50 -> c_14() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.41/2.50 c_15() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.41/2.50 c_18() 9.41/2.50 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.50 c_20() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.41/2.50 , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.41/2.50 , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26() 9.41/2.50 , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.41/2.50 , instrConstrCheck^#(Right(), Right()) -> c_28() 9.41/2.50 , instrConstrCheck^#(Right(), Left()) -> c_29() 9.41/2.50 , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.41/2.50 , instrConstrCheck^#(Right(), Halt()) -> c_31() 9.41/2.50 , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32() 9.41/2.50 , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.41/2.50 , instrConstrCheck^#(Left(), Right()) -> c_34() 9.41/2.50 , instrConstrCheck^#(Left(), Left()) -> c_35() 9.41/2.50 , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.41/2.50 , instrConstrCheck^#(Left(), Halt()) -> c_37() 9.41/2.50 , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.50 c_38() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.41/2.50 , instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.41/2.50 , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44() 9.41/2.50 , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.41/2.50 , instrConstrCheck^#(Halt(), Right()) -> c_46() 9.41/2.50 , instrConstrCheck^#(Halt(), Left()) -> c_47() 9.41/2.50 , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.41/2.50 , instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.41/2.50 , notEmpty^#(Cons(x, xs)) -> c_50() 9.41/2.50 , notEmpty^#(Nil()) -> c_51() 9.41/2.50 , instrsSecond^#(I(l, r)) -> c_52() 9.41/2.50 , instrsFirst^#(I(l, r)) -> c_53() 9.41/2.50 , getWrite^#(Write(int)) -> c_54() 9.41/2.50 , getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.41/2.50 , getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.41/2.50 , getGoto^#(Goto(int)) -> c_57() } 9.41/2.51 Obligation: 9.41/2.51 innermost runtime complexity 9.41/2.51 Answer: 9.41/2.51 YES(O(1),O(n^1)) 9.41/2.51 9.41/2.51 We estimate the number of application of {2} by applications of 9.41/2.51 Pre({2}) = {}. Here rules are labeled as follows: 9.41/2.51 9.41/2.51 DPs: 9.41/2.51 { 1: lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) 9.41/2.51 , 2: run^#(prog, tapeinput) -> 9.41/2.51 c_58(turing^#(prog, Nil(), tapeinput, prog)) 9.41/2.51 , 3: turing^#(I(IfGoto(igtNat1, igtNat2), r), 9.41/2.51 revltape, 9.41/2.51 rtape, 9.41/2.51 prog) 9.41/2.51 -> c_1() 9.41/2.51 , 4: turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.41/2.51 , 5: turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.41/2.51 , 6: turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.41/2.51 , 7: turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.41/2.51 , 8: turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.41/2.51 , 9: turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.41/2.51 , 10: lookup^#(0(), instrs) -> c_9() 9.41/2.51 , 11: instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.41/2.51 , 12: instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.41/2.51 , 13: instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.41/2.51 , 14: instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.41/2.51 , 15: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.41/2.51 IfGoto(igtNat12, igtNat22)) 9.41/2.51 -> c_14() 9.41/2.51 , 16: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.41/2.51 c_15() 9.41/2.51 , 17: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> 9.41/2.51 c_16() 9.41/2.51 , 18: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> 9.41/2.51 c_17() 9.41/2.51 , 19: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.41/2.51 c_18() 9.41/2.51 , 20: instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> 9.41/2.51 c_19() 9.41/2.51 , 21: instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) 9.41/2.51 -> c_20() 9.41/2.51 , 22: instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.41/2.51 , 23: instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.41/2.51 , 24: instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.41/2.51 , 25: instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.41/2.51 , 26: instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.41/2.51 , 27: instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> 9.41/2.51 c_26() 9.41/2.51 , 28: instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.41/2.51 , 29: instrConstrCheck^#(Right(), Right()) -> c_28() 9.41/2.51 , 30: instrConstrCheck^#(Right(), Left()) -> c_29() 9.41/2.51 , 31: instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.41/2.51 , 32: instrConstrCheck^#(Right(), Halt()) -> c_31() 9.41/2.51 , 33: instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> 9.41/2.51 c_32() 9.41/2.51 , 34: instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.41/2.51 , 35: instrConstrCheck^#(Left(), Right()) -> c_34() 9.41/2.51 , 36: instrConstrCheck^#(Left(), Left()) -> c_35() 9.41/2.51 , 37: instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.41/2.51 , 38: instrConstrCheck^#(Left(), Halt()) -> c_37() 9.41/2.51 , 39: instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) 9.41/2.51 -> c_38() 9.41/2.51 , 40: instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.41/2.51 , 41: instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.41/2.51 , 42: instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.41/2.51 , 43: instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.41/2.51 , 44: instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.41/2.51 , 45: instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> 9.41/2.51 c_44() 9.41/2.51 , 46: instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.41/2.51 , 47: instrConstrCheck^#(Halt(), Right()) -> c_46() 9.41/2.51 , 48: instrConstrCheck^#(Halt(), Left()) -> c_47() 9.41/2.51 , 49: instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.41/2.51 , 50: instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.41/2.51 , 51: notEmpty^#(Cons(x, xs)) -> c_50() 9.41/2.51 , 52: notEmpty^#(Nil()) -> c_51() 9.41/2.51 , 53: instrsSecond^#(I(l, r)) -> c_52() 9.41/2.51 , 54: instrsFirst^#(I(l, r)) -> c_53() 9.41/2.51 , 55: getWrite^#(Write(int)) -> c_54() 9.41/2.51 , 56: getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.41/2.51 , 57: getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.41/2.51 , 58: getGoto^#(Goto(int)) -> c_57() } 9.41/2.51 9.41/2.51 We are left with following problem, upon which TcT provides the 9.41/2.51 certificate YES(O(1),O(n^1)). 9.41/2.51 9.41/2.51 Strict DPs: { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) } 9.41/2.51 Weak DPs: 9.41/2.51 { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) 9.41/2.51 -> c_1() 9.41/2.51 , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.41/2.51 , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.41/2.51 , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.41/2.51 , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.41/2.51 , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.41/2.51 , turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.41/2.51 , lookup^#(0(), instrs) -> c_9() 9.41/2.51 , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.41/2.51 , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.41/2.51 , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.41/2.51 , instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.41/2.51 IfGoto(igtNat12, igtNat22)) 9.41/2.51 -> c_14() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.41/2.51 c_15() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.41/2.51 c_18() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.51 c_20() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.41/2.51 , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26() 9.41/2.51 , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.41/2.51 , instrConstrCheck^#(Right(), Right()) -> c_28() 9.41/2.51 , instrConstrCheck^#(Right(), Left()) -> c_29() 9.41/2.51 , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.41/2.51 , instrConstrCheck^#(Right(), Halt()) -> c_31() 9.41/2.51 , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32() 9.41/2.51 , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.41/2.51 , instrConstrCheck^#(Left(), Right()) -> c_34() 9.41/2.51 , instrConstrCheck^#(Left(), Left()) -> c_35() 9.41/2.51 , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.41/2.51 , instrConstrCheck^#(Left(), Halt()) -> c_37() 9.41/2.51 , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.51 c_38() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.41/2.51 , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44() 9.41/2.51 , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.41/2.51 , instrConstrCheck^#(Halt(), Right()) -> c_46() 9.41/2.51 , instrConstrCheck^#(Halt(), Left()) -> c_47() 9.41/2.51 , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.41/2.51 , instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.41/2.51 , notEmpty^#(Cons(x, xs)) -> c_50() 9.41/2.51 , notEmpty^#(Nil()) -> c_51() 9.41/2.51 , instrsSecond^#(I(l, r)) -> c_52() 9.41/2.51 , instrsFirst^#(I(l, r)) -> c_53() 9.41/2.51 , getWrite^#(Write(int)) -> c_54() 9.41/2.51 , getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.41/2.51 , getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.41/2.51 , getGoto^#(Goto(int)) -> c_57() 9.41/2.51 , run^#(prog, tapeinput) -> 9.41/2.51 c_58(turing^#(prog, Nil(), tapeinput, prog)) } 9.41/2.51 Obligation: 9.41/2.51 innermost runtime complexity 9.41/2.51 Answer: 9.41/2.51 YES(O(1),O(n^1)) 9.41/2.51 9.41/2.51 The following weak DPs constitute a sub-graph of the DG that is 9.41/2.51 closed under successors. The DPs are removed. 9.41/2.51 9.41/2.51 { turing^#(I(IfGoto(igtNat1, igtNat2), r), revltape, rtape, prog) 9.41/2.51 -> c_1() 9.41/2.51 , turing^#(I(Goto(gtNat), r), revltape, rtape, prog) -> c_2() 9.41/2.51 , turing^#(I(Right(), r), revltape, rtape, prog) -> c_3() 9.41/2.51 , turing^#(I(Left(), r), revltape, rtape, prog) -> c_4() 9.41/2.51 , turing^#(I(Write(wNat), r), revltape, rtape, prog) -> c_5() 9.41/2.51 , turing^#(I(Halt(), r), revltape, rtape, prog) -> c_6() 9.41/2.51 , turing^#(Empty(), revltape, rtape, prog) -> c_7() 9.41/2.51 , lookup^#(0(), instrs) -> c_9() 9.41/2.51 , instrsConstrCheck^#(I(l1, r1), I(x, y)) -> c_10() 9.41/2.51 , instrsConstrCheck^#(I(l1, r1), Empty()) -> c_11() 9.41/2.51 , instrsConstrCheck^#(Empty(), I(x, y)) -> c_12() 9.41/2.51 , instrsConstrCheck^#(Empty(), Empty()) -> c_13() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), 9.41/2.51 IfGoto(igtNat12, igtNat22)) 9.41/2.51 -> c_14() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) -> 9.41/2.51 c_15() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Right()) -> c_16() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Left()) -> c_17() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Write(wNat2)) -> 9.41/2.51 c_18() 9.41/2.51 , instrConstrCheck^#(IfGoto(igtNat1, igtNat2), Halt()) -> c_19() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.51 c_20() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Goto(gtNat2)) -> c_21() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Right()) -> c_22() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Left()) -> c_23() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Write(wNat2)) -> c_24() 9.41/2.51 , instrConstrCheck^#(Goto(gtNat), Halt()) -> c_25() 9.41/2.51 , instrConstrCheck^#(Right(), IfGoto(igtNat12, igtNat22)) -> c_26() 9.41/2.51 , instrConstrCheck^#(Right(), Goto(gtNat2)) -> c_27() 9.41/2.51 , instrConstrCheck^#(Right(), Right()) -> c_28() 9.41/2.51 , instrConstrCheck^#(Right(), Left()) -> c_29() 9.41/2.51 , instrConstrCheck^#(Right(), Write(wNat2)) -> c_30() 9.41/2.51 , instrConstrCheck^#(Right(), Halt()) -> c_31() 9.41/2.51 , instrConstrCheck^#(Left(), IfGoto(igtNat12, igtNat22)) -> c_32() 9.41/2.51 , instrConstrCheck^#(Left(), Goto(gtNat2)) -> c_33() 9.41/2.51 , instrConstrCheck^#(Left(), Right()) -> c_34() 9.41/2.51 , instrConstrCheck^#(Left(), Left()) -> c_35() 9.41/2.51 , instrConstrCheck^#(Left(), Write(wNat2)) -> c_36() 9.41/2.51 , instrConstrCheck^#(Left(), Halt()) -> c_37() 9.41/2.51 , instrConstrCheck^#(Write(wNat), IfGoto(igtNat12, igtNat22)) -> 9.41/2.51 c_38() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Goto(gtNat2)) -> c_39() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Right()) -> c_40() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Left()) -> c_41() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Write(wNat2)) -> c_42() 9.41/2.51 , instrConstrCheck^#(Write(wNat), Halt()) -> c_43() 9.41/2.51 , instrConstrCheck^#(Halt(), IfGoto(igtNat12, igtNat22)) -> c_44() 9.41/2.51 , instrConstrCheck^#(Halt(), Goto(gtNat2)) -> c_45() 9.41/2.51 , instrConstrCheck^#(Halt(), Right()) -> c_46() 9.41/2.51 , instrConstrCheck^#(Halt(), Left()) -> c_47() 9.41/2.51 , instrConstrCheck^#(Halt(), Write(wNat2)) -> c_48() 9.41/2.51 , instrConstrCheck^#(Halt(), Halt()) -> c_49() 9.41/2.51 , notEmpty^#(Cons(x, xs)) -> c_50() 9.41/2.51 , notEmpty^#(Nil()) -> c_51() 9.41/2.51 , instrsSecond^#(I(l, r)) -> c_52() 9.41/2.51 , instrsFirst^#(I(l, r)) -> c_53() 9.41/2.51 , getWrite^#(Write(int)) -> c_54() 9.41/2.51 , getGotoSecond^#(IfGoto(i1, i2)) -> c_55() 9.41/2.51 , getGotoFirst^#(IfGoto(i1, i2)) -> c_56() 9.41/2.51 , getGoto^#(Goto(int)) -> c_57() 9.41/2.51 , run^#(prog, tapeinput) -> 9.41/2.51 c_58(turing^#(prog, Nil(), tapeinput, prog)) } 9.41/2.51 9.41/2.51 We are left with following problem, upon which TcT provides the 9.41/2.51 certificate YES(O(1),O(n^1)). 9.41/2.51 9.41/2.51 Strict DPs: { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) } 9.41/2.51 Obligation: 9.41/2.51 innermost runtime complexity 9.41/2.51 Answer: 9.41/2.51 YES(O(1),O(n^1)) 9.41/2.51 9.41/2.51 We use the processor 'Small Polynomial Path Order (PS,1-bounded)' 9.41/2.51 to orient following rules strictly. 9.41/2.51 9.41/2.51 DPs: 9.41/2.51 { 1: lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) } 9.41/2.51 9.41/2.51 Sub-proof: 9.41/2.51 ---------- 9.41/2.51 The input was oriented with the instance of 'Small Polynomial Path 9.41/2.51 Order (PS,1-bounded)' as induced by the safe mapping 9.41/2.51 9.41/2.51 safe(I) = {1, 2}, safe(S) = {1}, safe(lookup^#) = {1}, 9.41/2.51 safe(c_8) = {} 9.41/2.51 9.41/2.51 and precedence 9.41/2.51 9.41/2.51 empty . 9.41/2.51 9.41/2.51 Following symbols are considered recursive: 9.41/2.51 9.41/2.51 {lookup^#} 9.41/2.51 9.41/2.51 The recursion depth is 1. 9.41/2.51 9.41/2.51 Further, following argument filtering is employed: 9.41/2.51 9.41/2.51 pi(I) = [2], pi(S) = [], pi(lookup^#) = [2], pi(c_8) = [1] 9.41/2.51 9.41/2.51 Usable defined function symbols are a subset of: 9.41/2.51 9.41/2.51 {lookup^#} 9.41/2.51 9.41/2.51 For your convenience, here are the satisfied ordering constraints: 9.41/2.51 9.41/2.51 pi(lookup^#(S(x), I(l, r))) = lookup^#(I(; r);) 9.41/2.51 > c_8(lookup^#(r;);) 9.41/2.51 = pi(c_8(lookup^#(x, r))) 9.41/2.51 9.41/2.51 9.41/2.51 The strictly oriented rules are moved into the weak component. 9.41/2.51 9.41/2.51 We are left with following problem, upon which TcT provides the 9.41/2.51 certificate YES(O(1),O(1)). 9.41/2.51 9.41/2.51 Weak DPs: { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) } 9.41/2.51 Obligation: 9.41/2.51 innermost runtime complexity 9.41/2.51 Answer: 9.41/2.51 YES(O(1),O(1)) 9.41/2.51 9.41/2.51 The following weak DPs constitute a sub-graph of the DG that is 9.41/2.51 closed under successors. The DPs are removed. 9.41/2.51 9.41/2.51 { lookup^#(S(x), I(l, r)) -> c_8(lookup^#(x, r)) } 9.41/2.51 9.41/2.51 We are left with following problem, upon which TcT provides the 9.41/2.51 certificate YES(O(1),O(1)). 9.41/2.51 9.41/2.51 Rules: Empty 9.41/2.51 Obligation: 9.41/2.51 innermost runtime complexity 9.41/2.51 Answer: 9.41/2.51 YES(O(1),O(1)) 9.41/2.51 9.41/2.51 Empty rules are trivially bounded 9.41/2.51 9.41/2.51 Hurray, we answered YES(O(1),O(n^1)) 9.41/2.51 EOF