MAYBE
* Step 1: Failure MAYBE
  + 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:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE