(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(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(Goto(int),r),revltape,rtape,prog) -> turing(lookup(int,prog),revltape,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(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(Write(int),r),revltape,Cons(x,xs),prog) -> turing(r,revltape,Cons(int,xs),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)
        !EQ(S(x),S(y)) ->= !EQ(x,y)
        !EQ(0,S(y)) ->= False
        !EQ(S(x),0) ->= False
        !EQ(0,0) ->= True
        turing[Ite](True,I(IfGoto(i1,i2),r),revltape,rtape,prog) ->= turing(lookup(i2,prog),revltape,rtape,prog)
        turing[Ite](False,I(l,r),revltape,rtape,prog) ->= turing(r,revltape,rtape,prog)
)