(0) Obligation:
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
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
turing(I(IfGoto(z0, z1), z2), z3, z4, z5) → turing[Ite][True][Ite][False][Ite](False, I(IfGoto(z0, z1), z2), z3, z4, z5)
turing(I(Goto(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](False, I(Goto(z0), z1), z2, z3, z4)
turing(I(Right, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Right, z0), z1, z2, z3)
turing(I(Left, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Left, z0), z1, z2, z3)
turing(I(Write(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](True, I(Write(z0), z1), z2, z3, z4)
turing(I(Halt, z0), z1, z2, z3) → z2
turing(Empty, z0, z1, z2) → z1
lookup(S(z0), I(z1, z2)) → lookup(z0, z2)
lookup(0, z0) → z0
instrsConstrCheck(I(z0, z1), I(z2, z3)) → True
instrsConstrCheck(I(z0, z1), Empty) → False
instrsConstrCheck(Empty, I(z0, z1)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(z0, z1), IfGoto(z2, z3)) → True
instrConstrCheck(IfGoto(z0, z1), Goto(z2)) → False
instrConstrCheck(IfGoto(z0, z1), Right) → False
instrConstrCheck(IfGoto(z0, z1), Left) → False
instrConstrCheck(IfGoto(z0, z1), Write(z2)) → False
instrConstrCheck(IfGoto(z0, z1), Halt) → False
instrConstrCheck(Goto(z0), IfGoto(z1, z2)) → False
instrConstrCheck(Goto(z0), Goto(z1)) → True
instrConstrCheck(Goto(z0), Right) → False
instrConstrCheck(Goto(z0), Left) → False
instrConstrCheck(Goto(z0), Write(z1)) → False
instrConstrCheck(Goto(z0), Halt) → False
instrConstrCheck(Right, IfGoto(z0, z1)) → False
instrConstrCheck(Right, Goto(z0)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(z0)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(z0, z1)) → False
instrConstrCheck(Left, Goto(z0)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(z0)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(z0), IfGoto(z1, z2)) → False
instrConstrCheck(Write(z0), Goto(z1)) → False
instrConstrCheck(Write(z0), Right) → False
instrConstrCheck(Write(z0), Left) → False
instrConstrCheck(Write(z0), Write(z1)) → True
instrConstrCheck(Write(z0), Halt) → False
instrConstrCheck(Halt, IfGoto(z0, z1)) → False
instrConstrCheck(Halt, Goto(z0)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(z0)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
instrsSecond(I(z0, z1)) → z1
instrsFirst(I(z0, z1)) → z0
getWrite(Write(z0)) → z0
getGotoSecond(IfGoto(z0, z1)) → z1
getGotoFirst(IfGoto(z0, z1)) → z0
getGoto(Goto(z0)) → z0
run(z0, z1) → turing(z0, Nil, z1, z0)
Tuples:
TURING(I(IfGoto(z0, z1), z2), z3, z4, z5) → c
TURING(I(Goto(z0), z1), z2, z3, z4) → c1
TURING(I(Right, z0), z1, z2, z3) → c2
TURING(I(Left, z0), z1, z2, z3) → c3
TURING(I(Write(z0), z1), z2, z3, z4) → c4
TURING(I(Halt, z0), z1, z2, z3) → c5
TURING(Empty, z0, z1, z2) → c6
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
LOOKUP(0, z0) → c8
INSTRSCONSTRCHECK(I(z0, z1), I(z2, z3)) → c9
INSTRSCONSTRCHECK(I(z0, z1), Empty) → c10
INSTRSCONSTRCHECK(Empty, I(z0, z1)) → c11
INSTRSCONSTRCHECK(Empty, Empty) → c12
INSTRCONSTRCHECK(IfGoto(z0, z1), IfGoto(z2, z3)) → c13
INSTRCONSTRCHECK(IfGoto(z0, z1), Goto(z2)) → c14
INSTRCONSTRCHECK(IfGoto(z0, z1), Right) → c15
INSTRCONSTRCHECK(IfGoto(z0, z1), Left) → c16
INSTRCONSTRCHECK(IfGoto(z0, z1), Write(z2)) → c17
INSTRCONSTRCHECK(IfGoto(z0, z1), Halt) → c18
INSTRCONSTRCHECK(Goto(z0), IfGoto(z1, z2)) → c19
INSTRCONSTRCHECK(Goto(z0), Goto(z1)) → c20
INSTRCONSTRCHECK(Goto(z0), Right) → c21
INSTRCONSTRCHECK(Goto(z0), Left) → c22
INSTRCONSTRCHECK(Goto(z0), Write(z1)) → c23
INSTRCONSTRCHECK(Goto(z0), Halt) → c24
INSTRCONSTRCHECK(Right, IfGoto(z0, z1)) → c25
INSTRCONSTRCHECK(Right, Goto(z0)) → c26
INSTRCONSTRCHECK(Right, Right) → c27
INSTRCONSTRCHECK(Right, Left) → c28
INSTRCONSTRCHECK(Right, Write(z0)) → c29
INSTRCONSTRCHECK(Right, Halt) → c30
INSTRCONSTRCHECK(Left, IfGoto(z0, z1)) → c31
INSTRCONSTRCHECK(Left, Goto(z0)) → c32
INSTRCONSTRCHECK(Left, Right) → c33
INSTRCONSTRCHECK(Left, Left) → c34
INSTRCONSTRCHECK(Left, Write(z0)) → c35
INSTRCONSTRCHECK(Left, Halt) → c36
INSTRCONSTRCHECK(Write(z0), IfGoto(z1, z2)) → c37
INSTRCONSTRCHECK(Write(z0), Goto(z1)) → c38
INSTRCONSTRCHECK(Write(z0), Right) → c39
INSTRCONSTRCHECK(Write(z0), Left) → c40
INSTRCONSTRCHECK(Write(z0), Write(z1)) → c41
INSTRCONSTRCHECK(Write(z0), Halt) → c42
INSTRCONSTRCHECK(Halt, IfGoto(z0, z1)) → c43
INSTRCONSTRCHECK(Halt, Goto(z0)) → c44
INSTRCONSTRCHECK(Halt, Right) → c45
INSTRCONSTRCHECK(Halt, Left) → c46
INSTRCONSTRCHECK(Halt, Write(z0)) → c47
INSTRCONSTRCHECK(Halt, Halt) → c48
NOTEMPTY(Cons(z0, z1)) → c49
NOTEMPTY(Nil) → c50
INSTRSSECOND(I(z0, z1)) → c51
INSTRSFIRST(I(z0, z1)) → c52
GETWRITE(Write(z0)) → c53
GETGOTOSECOND(IfGoto(z0, z1)) → c54
GETGOTOFIRST(IfGoto(z0, z1)) → c55
GETGOTO(Goto(z0)) → c56
RUN(z0, z1) → c57(TURING(z0, Nil, z1, z0))
S tuples:
TURING(I(IfGoto(z0, z1), z2), z3, z4, z5) → c
TURING(I(Goto(z0), z1), z2, z3, z4) → c1
TURING(I(Right, z0), z1, z2, z3) → c2
TURING(I(Left, z0), z1, z2, z3) → c3
TURING(I(Write(z0), z1), z2, z3, z4) → c4
TURING(I(Halt, z0), z1, z2, z3) → c5
TURING(Empty, z0, z1, z2) → c6
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
LOOKUP(0, z0) → c8
INSTRSCONSTRCHECK(I(z0, z1), I(z2, z3)) → c9
INSTRSCONSTRCHECK(I(z0, z1), Empty) → c10
INSTRSCONSTRCHECK(Empty, I(z0, z1)) → c11
INSTRSCONSTRCHECK(Empty, Empty) → c12
INSTRCONSTRCHECK(IfGoto(z0, z1), IfGoto(z2, z3)) → c13
INSTRCONSTRCHECK(IfGoto(z0, z1), Goto(z2)) → c14
INSTRCONSTRCHECK(IfGoto(z0, z1), Right) → c15
INSTRCONSTRCHECK(IfGoto(z0, z1), Left) → c16
INSTRCONSTRCHECK(IfGoto(z0, z1), Write(z2)) → c17
INSTRCONSTRCHECK(IfGoto(z0, z1), Halt) → c18
INSTRCONSTRCHECK(Goto(z0), IfGoto(z1, z2)) → c19
INSTRCONSTRCHECK(Goto(z0), Goto(z1)) → c20
INSTRCONSTRCHECK(Goto(z0), Right) → c21
INSTRCONSTRCHECK(Goto(z0), Left) → c22
INSTRCONSTRCHECK(Goto(z0), Write(z1)) → c23
INSTRCONSTRCHECK(Goto(z0), Halt) → c24
INSTRCONSTRCHECK(Right, IfGoto(z0, z1)) → c25
INSTRCONSTRCHECK(Right, Goto(z0)) → c26
INSTRCONSTRCHECK(Right, Right) → c27
INSTRCONSTRCHECK(Right, Left) → c28
INSTRCONSTRCHECK(Right, Write(z0)) → c29
INSTRCONSTRCHECK(Right, Halt) → c30
INSTRCONSTRCHECK(Left, IfGoto(z0, z1)) → c31
INSTRCONSTRCHECK(Left, Goto(z0)) → c32
INSTRCONSTRCHECK(Left, Right) → c33
INSTRCONSTRCHECK(Left, Left) → c34
INSTRCONSTRCHECK(Left, Write(z0)) → c35
INSTRCONSTRCHECK(Left, Halt) → c36
INSTRCONSTRCHECK(Write(z0), IfGoto(z1, z2)) → c37
INSTRCONSTRCHECK(Write(z0), Goto(z1)) → c38
INSTRCONSTRCHECK(Write(z0), Right) → c39
INSTRCONSTRCHECK(Write(z0), Left) → c40
INSTRCONSTRCHECK(Write(z0), Write(z1)) → c41
INSTRCONSTRCHECK(Write(z0), Halt) → c42
INSTRCONSTRCHECK(Halt, IfGoto(z0, z1)) → c43
INSTRCONSTRCHECK(Halt, Goto(z0)) → c44
INSTRCONSTRCHECK(Halt, Right) → c45
INSTRCONSTRCHECK(Halt, Left) → c46
INSTRCONSTRCHECK(Halt, Write(z0)) → c47
INSTRCONSTRCHECK(Halt, Halt) → c48
NOTEMPTY(Cons(z0, z1)) → c49
NOTEMPTY(Nil) → c50
INSTRSSECOND(I(z0, z1)) → c51
INSTRSFIRST(I(z0, z1)) → c52
GETWRITE(Write(z0)) → c53
GETGOTOSECOND(IfGoto(z0, z1)) → c54
GETGOTOFIRST(IfGoto(z0, z1)) → c55
GETGOTO(Goto(z0)) → c56
RUN(z0, z1) → c57(TURING(z0, Nil, z1, z0))
K tuples:none
Defined Rule Symbols:
turing, lookup, instrsConstrCheck, instrConstrCheck, notEmpty, instrsSecond, instrsFirst, getWrite, getGotoSecond, getGotoFirst, getGoto, run
Defined Pair Symbols:
TURING, LOOKUP, INSTRSCONSTRCHECK, INSTRCONSTRCHECK, NOTEMPTY, INSTRSSECOND, INSTRSFIRST, GETWRITE, GETGOTOSECOND, GETGOTOFIRST, GETGOTO, RUN
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 57 trailing nodes:
INSTRCONSTRCHECK(Left, Halt) → c36
INSTRCONSTRCHECK(IfGoto(z0, z1), Write(z2)) → c17
INSTRCONSTRCHECK(Left, Left) → c34
INSTRCONSTRCHECK(Halt, Write(z0)) → c47
GETGOTOSECOND(IfGoto(z0, z1)) → c54
INSTRCONSTRCHECK(IfGoto(z0, z1), Goto(z2)) → c14
INSTRCONSTRCHECK(IfGoto(z0, z1), IfGoto(z2, z3)) → c13
NOTEMPTY(Cons(z0, z1)) → c49
INSTRCONSTRCHECK(IfGoto(z0, z1), Halt) → c18
TURING(I(Goto(z0), z1), z2, z3, z4) → c1
INSTRSCONSTRCHECK(I(z0, z1), I(z2, z3)) → c9
INSTRCONSTRCHECK(Write(z0), Write(z1)) → c41
INSTRCONSTRCHECK(Goto(z0), Write(z1)) → c23
INSTRSCONSTRCHECK(I(z0, z1), Empty) → c10
INSTRSCONSTRCHECK(Empty, Empty) → c12
INSTRCONSTRCHECK(IfGoto(z0, z1), Right) → c15
INSTRCONSTRCHECK(Left, IfGoto(z0, z1)) → c31
GETGOTO(Goto(z0)) → c56
INSTRCONSTRCHECK(Right, Goto(z0)) → c26
LOOKUP(0, z0) → c8
INSTRCONSTRCHECK(Halt, Goto(z0)) → c44
INSTRCONSTRCHECK(Right, Write(z0)) → c29
RUN(z0, z1) → c57(TURING(z0, Nil, z1, z0))
INSTRCONSTRCHECK(Left, Right) → c33
TURING(I(Right, z0), z1, z2, z3) → c2
INSTRSCONSTRCHECK(Empty, I(z0, z1)) → c11
INSTRCONSTRCHECK(Write(z0), Halt) → c42
INSTRCONSTRCHECK(Halt, Right) → c45
INSTRCONSTRCHECK(Write(z0), Right) → c39
INSTRCONSTRCHECK(Halt, Halt) → c48
TURING(I(Left, z0), z1, z2, z3) → c3
INSTRCONSTRCHECK(Goto(z0), Halt) → c24
INSTRCONSTRCHECK(Right, Left) → c28
INSTRCONSTRCHECK(Left, Goto(z0)) → c32
INSTRCONSTRCHECK(Write(z0), Goto(z1)) → c38
INSTRCONSTRCHECK(Right, IfGoto(z0, z1)) → c25
TURING(I(Halt, z0), z1, z2, z3) → c5
TURING(I(Write(z0), z1), z2, z3, z4) → c4
INSTRCONSTRCHECK(Goto(z0), IfGoto(z1, z2)) → c19
TURING(Empty, z0, z1, z2) → c6
INSTRCONSTRCHECK(IfGoto(z0, z1), Left) → c16
INSTRCONSTRCHECK(Write(z0), Left) → c40
INSTRCONSTRCHECK(Goto(z0), Left) → c22
INSTRCONSTRCHECK(Left, Write(z0)) → c35
INSTRCONSTRCHECK(Right, Halt) → c30
INSTRCONSTRCHECK(Halt, IfGoto(z0, z1)) → c43
GETGOTOFIRST(IfGoto(z0, z1)) → c55
INSTRCONSTRCHECK(Goto(z0), Goto(z1)) → c20
INSTRCONSTRCHECK(Write(z0), IfGoto(z1, z2)) → c37
INSTRSSECOND(I(z0, z1)) → c51
NOTEMPTY(Nil) → c50
GETWRITE(Write(z0)) → c53
TURING(I(IfGoto(z0, z1), z2), z3, z4, z5) → c
INSTRCONSTRCHECK(Goto(z0), Right) → c21
INSTRSFIRST(I(z0, z1)) → c52
INSTRCONSTRCHECK(Halt, Left) → c46
INSTRCONSTRCHECK(Right, Right) → c27
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
turing(I(IfGoto(z0, z1), z2), z3, z4, z5) → turing[Ite][True][Ite][False][Ite](False, I(IfGoto(z0, z1), z2), z3, z4, z5)
turing(I(Goto(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](False, I(Goto(z0), z1), z2, z3, z4)
turing(I(Right, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Right, z0), z1, z2, z3)
turing(I(Left, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Left, z0), z1, z2, z3)
turing(I(Write(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](True, I(Write(z0), z1), z2, z3, z4)
turing(I(Halt, z0), z1, z2, z3) → z2
turing(Empty, z0, z1, z2) → z1
lookup(S(z0), I(z1, z2)) → lookup(z0, z2)
lookup(0, z0) → z0
instrsConstrCheck(I(z0, z1), I(z2, z3)) → True
instrsConstrCheck(I(z0, z1), Empty) → False
instrsConstrCheck(Empty, I(z0, z1)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(z0, z1), IfGoto(z2, z3)) → True
instrConstrCheck(IfGoto(z0, z1), Goto(z2)) → False
instrConstrCheck(IfGoto(z0, z1), Right) → False
instrConstrCheck(IfGoto(z0, z1), Left) → False
instrConstrCheck(IfGoto(z0, z1), Write(z2)) → False
instrConstrCheck(IfGoto(z0, z1), Halt) → False
instrConstrCheck(Goto(z0), IfGoto(z1, z2)) → False
instrConstrCheck(Goto(z0), Goto(z1)) → True
instrConstrCheck(Goto(z0), Right) → False
instrConstrCheck(Goto(z0), Left) → False
instrConstrCheck(Goto(z0), Write(z1)) → False
instrConstrCheck(Goto(z0), Halt) → False
instrConstrCheck(Right, IfGoto(z0, z1)) → False
instrConstrCheck(Right, Goto(z0)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(z0)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(z0, z1)) → False
instrConstrCheck(Left, Goto(z0)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(z0)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(z0), IfGoto(z1, z2)) → False
instrConstrCheck(Write(z0), Goto(z1)) → False
instrConstrCheck(Write(z0), Right) → False
instrConstrCheck(Write(z0), Left) → False
instrConstrCheck(Write(z0), Write(z1)) → True
instrConstrCheck(Write(z0), Halt) → False
instrConstrCheck(Halt, IfGoto(z0, z1)) → False
instrConstrCheck(Halt, Goto(z0)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(z0)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
instrsSecond(I(z0, z1)) → z1
instrsFirst(I(z0, z1)) → z0
getWrite(Write(z0)) → z0
getGotoSecond(IfGoto(z0, z1)) → z1
getGotoFirst(IfGoto(z0, z1)) → z0
getGoto(Goto(z0)) → z0
run(z0, z1) → turing(z0, Nil, z1, z0)
Tuples:
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
S tuples:
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
K tuples:none
Defined Rule Symbols:
turing, lookup, instrsConstrCheck, instrConstrCheck, notEmpty, instrsSecond, instrsFirst, getWrite, getGotoSecond, getGotoFirst, getGoto, run
Defined Pair Symbols:
LOOKUP
Compound Symbols:
c7
(5) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
turing(I(IfGoto(z0, z1), z2), z3, z4, z5) → turing[Ite][True][Ite][False][Ite](False, I(IfGoto(z0, z1), z2), z3, z4, z5)
turing(I(Goto(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](False, I(Goto(z0), z1), z2, z3, z4)
turing(I(Right, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Right, z0), z1, z2, z3)
turing(I(Left, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Left, z0), z1, z2, z3)
turing(I(Write(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](True, I(Write(z0), z1), z2, z3, z4)
turing(I(Halt, z0), z1, z2, z3) → z2
turing(Empty, z0, z1, z2) → z1
lookup(S(z0), I(z1, z2)) → lookup(z0, z2)
lookup(0, z0) → z0
instrsConstrCheck(I(z0, z1), I(z2, z3)) → True
instrsConstrCheck(I(z0, z1), Empty) → False
instrsConstrCheck(Empty, I(z0, z1)) → False
instrsConstrCheck(Empty, Empty) → True
instrConstrCheck(IfGoto(z0, z1), IfGoto(z2, z3)) → True
instrConstrCheck(IfGoto(z0, z1), Goto(z2)) → False
instrConstrCheck(IfGoto(z0, z1), Right) → False
instrConstrCheck(IfGoto(z0, z1), Left) → False
instrConstrCheck(IfGoto(z0, z1), Write(z2)) → False
instrConstrCheck(IfGoto(z0, z1), Halt) → False
instrConstrCheck(Goto(z0), IfGoto(z1, z2)) → False
instrConstrCheck(Goto(z0), Goto(z1)) → True
instrConstrCheck(Goto(z0), Right) → False
instrConstrCheck(Goto(z0), Left) → False
instrConstrCheck(Goto(z0), Write(z1)) → False
instrConstrCheck(Goto(z0), Halt) → False
instrConstrCheck(Right, IfGoto(z0, z1)) → False
instrConstrCheck(Right, Goto(z0)) → False
instrConstrCheck(Right, Right) → True
instrConstrCheck(Right, Left) → False
instrConstrCheck(Right, Write(z0)) → False
instrConstrCheck(Right, Halt) → False
instrConstrCheck(Left, IfGoto(z0, z1)) → False
instrConstrCheck(Left, Goto(z0)) → False
instrConstrCheck(Left, Right) → False
instrConstrCheck(Left, Left) → True
instrConstrCheck(Left, Write(z0)) → False
instrConstrCheck(Left, Halt) → False
instrConstrCheck(Write(z0), IfGoto(z1, z2)) → False
instrConstrCheck(Write(z0), Goto(z1)) → False
instrConstrCheck(Write(z0), Right) → False
instrConstrCheck(Write(z0), Left) → False
instrConstrCheck(Write(z0), Write(z1)) → True
instrConstrCheck(Write(z0), Halt) → False
instrConstrCheck(Halt, IfGoto(z0, z1)) → False
instrConstrCheck(Halt, Goto(z0)) → False
instrConstrCheck(Halt, Right) → False
instrConstrCheck(Halt, Left) → False
instrConstrCheck(Halt, Write(z0)) → False
instrConstrCheck(Halt, Halt) → True
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
instrsSecond(I(z0, z1)) → z1
instrsFirst(I(z0, z1)) → z0
getWrite(Write(z0)) → z0
getGotoSecond(IfGoto(z0, z1)) → z1
getGotoFirst(IfGoto(z0, z1)) → z0
getGoto(Goto(z0)) → z0
run(z0, z1) → turing(z0, Nil, z1, z0)
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
S tuples:
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:
LOOKUP
Compound Symbols:
c7
(7) CdtRuleRemovalProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
We considered the (Usable) Rules:none
And the Tuples:
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(I(x1, x2)) = x2
POL(LOOKUP(x1, x2)) = x1 + [4]x2
POL(S(x1)) = [2] + x1
POL(c7(x1)) = x1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
S tuples:none
K tuples:
LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2))
Defined Rule Symbols:none
Defined Pair Symbols:
LOOKUP
Compound Symbols:
c7
(9) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(10) BOUNDS(O(1), O(1))