* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            getGoto(Goto(int)) -> int
            getGotoFirst(IfGoto(i1,i2)) -> i1
            getGotoSecond(IfGoto(i1,i2)) -> i2
            getWrite(Write(int)) -> int
            instrConstrCheck(Goto(gtNat),Goto(gtNat2)) -> True()
            instrConstrCheck(Goto(gtNat),Halt()) -> False()
            instrConstrCheck(Goto(gtNat),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Goto(gtNat),Left()) -> False()
            instrConstrCheck(Goto(gtNat),Right()) -> False()
            instrConstrCheck(Goto(gtNat),Write(wNat2)) -> False()
            instrConstrCheck(Halt(),Goto(gtNat2)) -> False()
            instrConstrCheck(Halt(),Halt()) -> True()
            instrConstrCheck(Halt(),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Halt(),Left()) -> False()
            instrConstrCheck(Halt(),Right()) -> False()
            instrConstrCheck(Halt(),Write(wNat2)) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Goto(gtNat2)) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Halt()) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),IfGoto(igtNat12,igtNat22)) -> True()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Left()) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Right()) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Write(wNat2)) -> False()
            instrConstrCheck(Left(),Goto(gtNat2)) -> False()
            instrConstrCheck(Left(),Halt()) -> False()
            instrConstrCheck(Left(),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Left(),Left()) -> True()
            instrConstrCheck(Left(),Right()) -> False()
            instrConstrCheck(Left(),Write(wNat2)) -> False()
            instrConstrCheck(Right(),Goto(gtNat2)) -> False()
            instrConstrCheck(Right(),Halt()) -> False()
            instrConstrCheck(Right(),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Right(),Left()) -> False()
            instrConstrCheck(Right(),Right()) -> True()
            instrConstrCheck(Right(),Write(wNat2)) -> False()
            instrConstrCheck(Write(wNat),Goto(gtNat2)) -> False()
            instrConstrCheck(Write(wNat),Halt()) -> False()
            instrConstrCheck(Write(wNat),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Write(wNat),Left()) -> False()
            instrConstrCheck(Write(wNat),Right()) -> False()
            instrConstrCheck(Write(wNat),Write(wNat2)) -> True()
            instrsConstrCheck(Empty(),Empty()) -> True()
            instrsConstrCheck(Empty(),I(x,y)) -> False()
            instrsConstrCheck(I(l1,r1),Empty()) -> False()
            instrsConstrCheck(I(l1,r1),I(x,y)) -> True()
            instrsFirst(I(l,r)) -> l
            instrsSecond(I(l,r)) -> r
            lookup(0(),instrs) -> instrs
            lookup(S(x),I(l,r)) -> lookup(x,r)
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            run(prog,tapeinput) -> turing(prog,Nil(),tapeinput,prog)
            turing(Empty(),revltape,rtape,prog) -> rtape
            turing(I(Goto(int),r),revltape,rtape,prog) -> turing(lookup(int,prog),revltape,rtape,prog)
            turing(I(Halt(),r),revltape,rtape,prog) -> rtape
            turing(I(IfGoto(i1,i2),r),revltape,Cons(x,xs),prog) -> turing[Ite](!EQ(x,i1)
                                                                              ,I(IfGoto(i1,i2),r)
                                                                              ,revltape
                                                                              ,Cons(x,xs)
                                                                              ,prog)
            turing(I(Left(),r),Cons(x,xs),rtape,prog) -> turing(r,xs,Cons(x,rtape),prog)
            turing(I(Left(),r),Nil(),rtape,prog) -> turing(r,Nil(),Cons(0(),rtape),prog)
            turing(I(Right(),r),revltape,Cons(x,xs),prog) -> turing(r,Cons(x,revltape),xs,prog)
            turing(I(Right(),r),revltape,Nil(),prog) -> turing(r,Cons(0(),revltape),Nil(),prog)
            turing(I(Write(int),r),revltape,Cons(x,xs),prog) -> turing(r,revltape,Cons(int,xs),prog)
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            turing[Ite](False(),I(l,r),revltape,rtape,prog) -> turing(r,revltape,rtape,prog)
            turing[Ite](True(),I(IfGoto(i1,i2),r),revltape,rtape,prog) -> turing(lookup(i2,prog),revltape,rtape,prog)
        - Signature:
            {!EQ/2,getGoto/1,getGotoFirst/1,getGotoSecond/1,getWrite/1,instrConstrCheck/2,instrsConstrCheck/2
            ,instrsFirst/1,instrsSecond/1,lookup/2,notEmpty/1,run/2,turing/4,turing[Ite]/5} / {0/0,Cons/2,Empty/0
            ,False/0,Goto/1,Halt/0,I/2,IfGoto/2,Left/0,Nil/0,Right/0,S/1,True/0,Write/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,getGoto,getGotoFirst,getGotoSecond,getWrite
            ,instrConstrCheck,instrsConstrCheck,instrsFirst,instrsSecond,lookup,notEmpty,run,turing
            ,turing[Ite]} and constructors {0,Cons,Empty,False,Goto,Halt,I,IfGoto,Left,Nil,Right,S,True,Write}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            getGoto(Goto(int)) -> int
            getGotoFirst(IfGoto(i1,i2)) -> i1
            getGotoSecond(IfGoto(i1,i2)) -> i2
            getWrite(Write(int)) -> int
            instrConstrCheck(Goto(gtNat),Goto(gtNat2)) -> True()
            instrConstrCheck(Goto(gtNat),Halt()) -> False()
            instrConstrCheck(Goto(gtNat),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Goto(gtNat),Left()) -> False()
            instrConstrCheck(Goto(gtNat),Right()) -> False()
            instrConstrCheck(Goto(gtNat),Write(wNat2)) -> False()
            instrConstrCheck(Halt(),Goto(gtNat2)) -> False()
            instrConstrCheck(Halt(),Halt()) -> True()
            instrConstrCheck(Halt(),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Halt(),Left()) -> False()
            instrConstrCheck(Halt(),Right()) -> False()
            instrConstrCheck(Halt(),Write(wNat2)) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Goto(gtNat2)) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Halt()) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),IfGoto(igtNat12,igtNat22)) -> True()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Left()) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Right()) -> False()
            instrConstrCheck(IfGoto(igtNat1,igtNat2),Write(wNat2)) -> False()
            instrConstrCheck(Left(),Goto(gtNat2)) -> False()
            instrConstrCheck(Left(),Halt()) -> False()
            instrConstrCheck(Left(),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Left(),Left()) -> True()
            instrConstrCheck(Left(),Right()) -> False()
            instrConstrCheck(Left(),Write(wNat2)) -> False()
            instrConstrCheck(Right(),Goto(gtNat2)) -> False()
            instrConstrCheck(Right(),Halt()) -> False()
            instrConstrCheck(Right(),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Right(),Left()) -> False()
            instrConstrCheck(Right(),Right()) -> True()
            instrConstrCheck(Right(),Write(wNat2)) -> False()
            instrConstrCheck(Write(wNat),Goto(gtNat2)) -> False()
            instrConstrCheck(Write(wNat),Halt()) -> False()
            instrConstrCheck(Write(wNat),IfGoto(igtNat12,igtNat22)) -> False()
            instrConstrCheck(Write(wNat),Left()) -> False()
            instrConstrCheck(Write(wNat),Right()) -> False()
            instrConstrCheck(Write(wNat),Write(wNat2)) -> True()
            instrsConstrCheck(Empty(),Empty()) -> True()
            instrsConstrCheck(Empty(),I(x,y)) -> False()
            instrsConstrCheck(I(l1,r1),Empty()) -> False()
            instrsConstrCheck(I(l1,r1),I(x,y)) -> True()
            instrsFirst(I(l,r)) -> l
            instrsSecond(I(l,r)) -> r
            lookup(0(),instrs) -> instrs
            lookup(S(x),I(l,r)) -> lookup(x,r)
            notEmpty(Cons(x,xs)) -> True()
            notEmpty(Nil()) -> False()
            run(prog,tapeinput) -> turing(prog,Nil(),tapeinput,prog)
            turing(Empty(),revltape,rtape,prog) -> rtape
            turing(I(Goto(int),r),revltape,rtape,prog) -> turing(lookup(int,prog),revltape,rtape,prog)
            turing(I(Halt(),r),revltape,rtape,prog) -> rtape
            turing(I(IfGoto(i1,i2),r),revltape,Cons(x,xs),prog) -> turing[Ite](!EQ(x,i1)
                                                                              ,I(IfGoto(i1,i2),r)
                                                                              ,revltape
                                                                              ,Cons(x,xs)
                                                                              ,prog)
            turing(I(Left(),r),Cons(x,xs),rtape,prog) -> turing(r,xs,Cons(x,rtape),prog)
            turing(I(Left(),r),Nil(),rtape,prog) -> turing(r,Nil(),Cons(0(),rtape),prog)
            turing(I(Right(),r),revltape,Cons(x,xs),prog) -> turing(r,Cons(x,revltape),xs,prog)
            turing(I(Right(),r),revltape,Nil(),prog) -> turing(r,Cons(0(),revltape),Nil(),prog)
            turing(I(Write(int),r),revltape,Cons(x,xs),prog) -> turing(r,revltape,Cons(int,xs),prog)
        - Weak TRS:
            !EQ(0(),0()) -> True()
            !EQ(0(),S(y)) -> False()
            !EQ(S(x),0()) -> False()
            !EQ(S(x),S(y)) -> !EQ(x,y)
            turing[Ite](False(),I(l,r),revltape,rtape,prog) -> turing(r,revltape,rtape,prog)
            turing[Ite](True(),I(IfGoto(i1,i2),r),revltape,rtape,prog) -> turing(lookup(i2,prog),revltape,rtape,prog)
        - Signature:
            {!EQ/2,getGoto/1,getGotoFirst/1,getGotoSecond/1,getWrite/1,instrConstrCheck/2,instrsConstrCheck/2
            ,instrsFirst/1,instrsSecond/1,lookup/2,notEmpty/1,run/2,turing/4,turing[Ite]/5} / {0/0,Cons/2,Empty/0
            ,False/0,Goto/1,Halt/0,I/2,IfGoto/2,Left/0,Nil/0,Right/0,S/1,True/0,Write/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {!EQ,getGoto,getGotoFirst,getGotoSecond,getWrite
            ,instrConstrCheck,instrsConstrCheck,instrsFirst,instrsSecond,lookup,notEmpty,run,turing
            ,turing[Ite]} and constructors {0,Cons,Empty,False,Goto,Halt,I,IfGoto,Left,Nil,Right,S,True,Write}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          lookup(x,z){x -> S(x),z -> I(y,z)} =
            lookup(S(x),I(y,z)) ->^+ lookup(x,z)
              = C[lookup(x,z) = lookup(x,z){}]

WORST_CASE(Omega(n^1),?)