Runtime Complexity TRS:
The TRS R consists of the following rules:

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)
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
lookup(0, instrs) → instrs
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)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


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)
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'
lookup'(0', instrs) → instrs
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)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
turing'/1
turing'/3
turing[Ite][True][Ite][False][Ite]'/0
turing[Ite][True][Ite][False][Ite]'/1
turing[Ite][True][Ite][False][Ite]'/2
turing[Ite][True][Ite][False][Ite]'/3
turing[Ite][True][Ite][False][Ite]'/4
Cons'/0
Cons'/1

Runtime Complexity TRS:
The TRS R consists of the following rules:


turing'(I'(IfGoto'(igtNat1, igtNat2), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Goto'(gtNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Right', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Left', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Write'(wNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Halt', r), rtape) → rtape
turing'(Empty', rtape) → rtape
lookup'(S'(x), I'(l, r)) → lookup'(x, r)
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') → True'
notEmpty'(Nil') → False'
lookup'(0', instrs) → instrs
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, tapeinput)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
turing'(I'(IfGoto'(igtNat1, igtNat2), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Goto'(gtNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Right', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Left', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Write'(wNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Halt', r), rtape) → rtape
turing'(Empty', rtape) → rtape
lookup'(S'(x), I'(l, r)) → lookup'(x, r)
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') → True'
notEmpty'(Nil') → False'
lookup'(0', instrs) → instrs
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, tapeinput)

Types:
turing' :: I':Empty' → turing[Ite][True][Ite][False][Ite]' → turing[Ite][True][Ite][False][Ite]'
I' :: IfGoto':Goto':Right':Left':Write':Halt' → I':Empty' → I':Empty'
IfGoto' :: getGotoFirst' → getGotoSecond' → IfGoto':Goto':Right':Left':Write':Halt'
turing[Ite][True][Ite][False][Ite]' :: turing[Ite][True][Ite][False][Ite]'
Goto' :: getGoto' → IfGoto':Goto':Right':Left':Write':Halt'
Right' :: IfGoto':Goto':Right':Left':Write':Halt'
Left' :: IfGoto':Goto':Right':Left':Write':Halt'
Write' :: getWrite' → IfGoto':Goto':Right':Left':Write':Halt'
Halt' :: IfGoto':Goto':Right':Left':Write':Halt'
Empty' :: I':Empty'
lookup' :: S':0' → I':Empty' → I':Empty'
S' :: S':0' → S':0'
instrsConstrCheck' :: I':Empty' → I':Empty' → True':False'
True' :: True':False'
False' :: True':False'
instrConstrCheck' :: IfGoto':Goto':Right':Left':Write':Halt' → IfGoto':Goto':Right':Left':Write':Halt' → True':False'
notEmpty' :: Cons':Nil' → True':False'
Cons' :: Cons':Nil'
Nil' :: Cons':Nil'
0' :: S':0'
instrsSecond' :: I':Empty' → I':Empty'
instrsFirst' :: I':Empty' → IfGoto':Goto':Right':Left':Write':Halt'
getWrite' :: IfGoto':Goto':Right':Left':Write':Halt' → getWrite'
getGotoSecond' :: IfGoto':Goto':Right':Left':Write':Halt' → getGotoSecond'
getGotoFirst' :: IfGoto':Goto':Right':Left':Write':Halt' → getGotoFirst'
getGoto' :: IfGoto':Goto':Right':Left':Write':Halt' → getGoto'
run' :: I':Empty' → turing[Ite][True][Ite][False][Ite]' → turing[Ite][True][Ite][False][Ite]'
_hole_turing[Ite][True][Ite][False][Ite]'1 :: turing[Ite][True][Ite][False][Ite]'
_hole_I':Empty'2 :: I':Empty'
_hole_IfGoto':Goto':Right':Left':Write':Halt'3 :: IfGoto':Goto':Right':Left':Write':Halt'
_hole_getGotoFirst'4 :: getGotoFirst'
_hole_getGotoSecond'5 :: getGotoSecond'
_hole_getGoto'6 :: getGoto'
_hole_getWrite'7 :: getWrite'
_hole_S':0'8 :: S':0'
_hole_True':False'9 :: True':False'
_hole_Cons':Nil'10 :: Cons':Nil'
_gen_I':Empty'11 :: Nat → I':Empty'
_gen_S':0'12 :: Nat → S':0'

Heuristically decided to analyse the following defined symbols:
lookup'

Rules:
turing'(I'(IfGoto'(igtNat1, igtNat2), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Goto'(gtNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Right', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Left', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Write'(wNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Halt', r), rtape) → rtape
turing'(Empty', rtape) → rtape
lookup'(S'(x), I'(l, r)) → lookup'(x, r)
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') → True'
notEmpty'(Nil') → False'
lookup'(0', instrs) → instrs
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, tapeinput)

Types:
turing' :: I':Empty' → turing[Ite][True][Ite][False][Ite]' → turing[Ite][True][Ite][False][Ite]'
I' :: IfGoto':Goto':Right':Left':Write':Halt' → I':Empty' → I':Empty'
IfGoto' :: getGotoFirst' → getGotoSecond' → IfGoto':Goto':Right':Left':Write':Halt'
turing[Ite][True][Ite][False][Ite]' :: turing[Ite][True][Ite][False][Ite]'
Goto' :: getGoto' → IfGoto':Goto':Right':Left':Write':Halt'
Right' :: IfGoto':Goto':Right':Left':Write':Halt'
Left' :: IfGoto':Goto':Right':Left':Write':Halt'
Write' :: getWrite' → IfGoto':Goto':Right':Left':Write':Halt'
Halt' :: IfGoto':Goto':Right':Left':Write':Halt'
Empty' :: I':Empty'
lookup' :: S':0' → I':Empty' → I':Empty'
S' :: S':0' → S':0'
instrsConstrCheck' :: I':Empty' → I':Empty' → True':False'
True' :: True':False'
False' :: True':False'
instrConstrCheck' :: IfGoto':Goto':Right':Left':Write':Halt' → IfGoto':Goto':Right':Left':Write':Halt' → True':False'
notEmpty' :: Cons':Nil' → True':False'
Cons' :: Cons':Nil'
Nil' :: Cons':Nil'
0' :: S':0'
instrsSecond' :: I':Empty' → I':Empty'
instrsFirst' :: I':Empty' → IfGoto':Goto':Right':Left':Write':Halt'
getWrite' :: IfGoto':Goto':Right':Left':Write':Halt' → getWrite'
getGotoSecond' :: IfGoto':Goto':Right':Left':Write':Halt' → getGotoSecond'
getGotoFirst' :: IfGoto':Goto':Right':Left':Write':Halt' → getGotoFirst'
getGoto' :: IfGoto':Goto':Right':Left':Write':Halt' → getGoto'
run' :: I':Empty' → turing[Ite][True][Ite][False][Ite]' → turing[Ite][True][Ite][False][Ite]'
_hole_turing[Ite][True][Ite][False][Ite]'1 :: turing[Ite][True][Ite][False][Ite]'
_hole_I':Empty'2 :: I':Empty'
_hole_IfGoto':Goto':Right':Left':Write':Halt'3 :: IfGoto':Goto':Right':Left':Write':Halt'
_hole_getGotoFirst'4 :: getGotoFirst'
_hole_getGotoSecond'5 :: getGotoSecond'
_hole_getGoto'6 :: getGoto'
_hole_getWrite'7 :: getWrite'
_hole_S':0'8 :: S':0'
_hole_True':False'9 :: True':False'
_hole_Cons':Nil'10 :: Cons':Nil'
_gen_I':Empty'11 :: Nat → I':Empty'
_gen_S':0'12 :: Nat → S':0'

Generator Equations:
_gen_I':Empty'11(0) ⇔ Empty'
_gen_I':Empty'11(+(x, 1)) ⇔ I'(IfGoto'(_hole_getGotoFirst'4, _hole_getGotoSecond'5), _gen_I':Empty'11(x))
_gen_S':0'12(0) ⇔ 0'
_gen_S':0'12(+(x, 1)) ⇔ S'(_gen_S':0'12(x))

The following defined symbols remain to be analysed:
lookup'

Proved the following rewrite lemma:
lookup'(_gen_S':0'12(_n14), _gen_I':Empty'11(_n14)) → _gen_I':Empty'11(0), rt ∈ Ω(1 + n14)

Induction Base:
lookup'(_gen_S':0'12(0), _gen_I':Empty'11(0)) →RΩ(1)
_gen_I':Empty'11(0)

Induction Step:
lookup'(_gen_S':0'12(+(_$n15, 1)), _gen_I':Empty'11(+(_$n15, 1))) →RΩ(1)
lookup'(_gen_S':0'12(_$n15), _gen_I':Empty'11(_$n15)) →IH
_gen_I':Empty'11(0)

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
turing'(I'(IfGoto'(igtNat1, igtNat2), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Goto'(gtNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Right', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Left', r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Write'(wNat), r), rtape) → turing[Ite][True][Ite][False][Ite]'
turing'(I'(Halt', r), rtape) → rtape
turing'(Empty', rtape) → rtape
lookup'(S'(x), I'(l, r)) → lookup'(x, r)
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') → True'
notEmpty'(Nil') → False'
lookup'(0', instrs) → instrs
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, tapeinput)

Types:
turing' :: I':Empty' → turing[Ite][True][Ite][False][Ite]' → turing[Ite][True][Ite][False][Ite]'
I' :: IfGoto':Goto':Right':Left':Write':Halt' → I':Empty' → I':Empty'
IfGoto' :: getGotoFirst' → getGotoSecond' → IfGoto':Goto':Right':Left':Write':Halt'
turing[Ite][True][Ite][False][Ite]' :: turing[Ite][True][Ite][False][Ite]'
Goto' :: getGoto' → IfGoto':Goto':Right':Left':Write':Halt'
Right' :: IfGoto':Goto':Right':Left':Write':Halt'
Left' :: IfGoto':Goto':Right':Left':Write':Halt'
Write' :: getWrite' → IfGoto':Goto':Right':Left':Write':Halt'
Halt' :: IfGoto':Goto':Right':Left':Write':Halt'
Empty' :: I':Empty'
lookup' :: S':0' → I':Empty' → I':Empty'
S' :: S':0' → S':0'
instrsConstrCheck' :: I':Empty' → I':Empty' → True':False'
True' :: True':False'
False' :: True':False'
instrConstrCheck' :: IfGoto':Goto':Right':Left':Write':Halt' → IfGoto':Goto':Right':Left':Write':Halt' → True':False'
notEmpty' :: Cons':Nil' → True':False'
Cons' :: Cons':Nil'
Nil' :: Cons':Nil'
0' :: S':0'
instrsSecond' :: I':Empty' → I':Empty'
instrsFirst' :: I':Empty' → IfGoto':Goto':Right':Left':Write':Halt'
getWrite' :: IfGoto':Goto':Right':Left':Write':Halt' → getWrite'
getGotoSecond' :: IfGoto':Goto':Right':Left':Write':Halt' → getGotoSecond'
getGotoFirst' :: IfGoto':Goto':Right':Left':Write':Halt' → getGotoFirst'
getGoto' :: IfGoto':Goto':Right':Left':Write':Halt' → getGoto'
run' :: I':Empty' → turing[Ite][True][Ite][False][Ite]' → turing[Ite][True][Ite][False][Ite]'
_hole_turing[Ite][True][Ite][False][Ite]'1 :: turing[Ite][True][Ite][False][Ite]'
_hole_I':Empty'2 :: I':Empty'
_hole_IfGoto':Goto':Right':Left':Write':Halt'3 :: IfGoto':Goto':Right':Left':Write':Halt'
_hole_getGotoFirst'4 :: getGotoFirst'
_hole_getGotoSecond'5 :: getGotoSecond'
_hole_getGoto'6 :: getGoto'
_hole_getWrite'7 :: getWrite'
_hole_S':0'8 :: S':0'
_hole_True':False'9 :: True':False'
_hole_Cons':Nil'10 :: Cons':Nil'
_gen_I':Empty'11 :: Nat → I':Empty'
_gen_S':0'12 :: Nat → S':0'

Lemmas:
lookup'(_gen_S':0'12(_n14), _gen_I':Empty'11(_n14)) → _gen_I':Empty'11(0), rt ∈ Ω(1 + n14)

Generator Equations:
_gen_I':Empty'11(0) ⇔ Empty'
_gen_I':Empty'11(+(x, 1)) ⇔ I'(IfGoto'(_hole_getGotoFirst'4, _hole_getGotoSecond'5), _gen_I':Empty'11(x))
_gen_S':0'12(0) ⇔ 0'
_gen_S':0'12(+(x, 1)) ⇔ S'(_gen_S':0'12(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
lookup'(_gen_S':0'12(_n14), _gen_I':Empty'11(_n14)) → _gen_I':Empty'11(0), rt ∈ Ω(1 + n14)