(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTORBASED)
(VAR gtNat gtNat2 i1 i2 igtNat1 igtNat12 igtNat2 igtNat22 instrs int l l1 prog r r1 revltape rtape tapeinput wNat wNat2 x xs y )
(STRATEGY INNERMOST)
(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)
        
)