0.00/0.86 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

0.00/0.86

0.00/0.86
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS

0.00/0.86

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

0.00/0.86

↳2 CdtProblem

0.00/0.86

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

0.00/0.86

↳4 CdtProblem

0.00/0.86

↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

0.00/0.86

↳6 CdtProblem

0.00/0.86

↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

0.00/0.86

↳8 CdtProblem

0.00/0.86

↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))

0.00/0.86

↳10 BOUNDS(O(1), O(1))

0.00/0.86

0.00/0.86 0.00/0.86

0.00/0.86

(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) 0.00/0.86
turing(I(Goto(gtNat), r), revltape, rtape, prog) → turing[Ite][True][Ite][False][Ite](False, I(Goto(gtNat), r), revltape, rtape, prog) 0.00/0.86
turing(I(Right, r), revltape, rtape, prog) → turing[Ite][True][Ite][False][Ite](False, I(Right, r), revltape, rtape, prog) 0.00/0.86
turing(I(Left, r), revltape, rtape, prog) → turing[Ite][True][Ite][False][Ite](False, I(Left, r), revltape, rtape, prog) 0.00/0.86
turing(I(Write(wNat), r), revltape, rtape, prog) → turing[Ite][True][Ite][False][Ite](True, I(Write(wNat), r), revltape, rtape, prog) 0.00/0.86
turing(I(Halt, r), revltape, rtape, prog) → rtape 0.00/0.86
turing(Empty, revltape, rtape, prog) → rtape 0.00/0.86
lookup(S(x), I(l, r)) → lookup(x, r) 0.00/0.86
instrsConstrCheck(I(l1, r1), I(x, y)) → True 0.00/0.86
instrsConstrCheck(I(l1, r1), Empty) → False 0.00/0.86
instrsConstrCheck(Empty, I(x, y)) → False 0.00/0.86
instrsConstrCheck(Empty, Empty) → True 0.00/0.86
instrConstrCheck(IfGoto(igtNat1, igtNat2), IfGoto(igtNat12, igtNat22)) → True 0.00/0.86
instrConstrCheck(IfGoto(igtNat1, igtNat2), Goto(gtNat2)) → False 0.00/0.88
instrConstrCheck(IfGoto(igtNat1, igtNat2), Right) → False 0.00/0.88
instrConstrCheck(IfGoto(igtNat1, igtNat2), Left) → False 0.00/0.88
instrConstrCheck(IfGoto(igtNat1, igtNat2), Write(wNat2)) → False 0.00/0.88
instrConstrCheck(IfGoto(igtNat1, igtNat2), Halt) → False 0.00/0.88
instrConstrCheck(Goto(gtNat), IfGoto(igtNat12, igtNat22)) → False 0.00/0.88
instrConstrCheck(Goto(gtNat), Goto(gtNat2)) → True 0.00/0.88
instrConstrCheck(Goto(gtNat), Right) → False 0.00/0.88
instrConstrCheck(Goto(gtNat), Left) → False 0.00/0.88
instrConstrCheck(Goto(gtNat), Write(wNat2)) → False 0.00/0.88
instrConstrCheck(Goto(gtNat), Halt) → False 0.00/0.88
instrConstrCheck(Right, IfGoto(igtNat12, igtNat22)) → False 0.00/0.88
instrConstrCheck(Right, Goto(gtNat2)) → False 0.00/0.88
instrConstrCheck(Right, Right) → True 0.00/0.88
instrConstrCheck(Right, Left) → False 0.00/0.88
instrConstrCheck(Right, Write(wNat2)) → False 0.00/0.88
instrConstrCheck(Right, Halt) → False 0.00/0.88
instrConstrCheck(Left, IfGoto(igtNat12, igtNat22)) → False 0.00/0.88
instrConstrCheck(Left, Goto(gtNat2)) → False 0.00/0.88
instrConstrCheck(Left, Right) → False 0.00/0.88
instrConstrCheck(Left, Left) → True 0.00/0.88
instrConstrCheck(Left, Write(wNat2)) → False 0.00/0.88
instrConstrCheck(Left, Halt) → False 0.00/0.88
instrConstrCheck(Write(wNat), IfGoto(igtNat12, igtNat22)) → False 0.00/0.88
instrConstrCheck(Write(wNat), Goto(gtNat2)) → False 0.00/0.88
instrConstrCheck(Write(wNat), Right) → False 0.00/0.88
instrConstrCheck(Write(wNat), Left) → False 0.00/0.88
instrConstrCheck(Write(wNat), Write(wNat2)) → True 0.00/0.88
instrConstrCheck(Write(wNat), Halt) → False 0.00/0.88
instrConstrCheck(Halt, IfGoto(igtNat12, igtNat22)) → False 0.00/0.88
instrConstrCheck(Halt, Goto(gtNat2)) → False 0.00/0.88
instrConstrCheck(Halt, Right) → False 0.00/0.88
instrConstrCheck(Halt, Left) → False 0.00/0.88
instrConstrCheck(Halt, Write(wNat2)) → False 0.00/0.88
instrConstrCheck(Halt, Halt) → True 0.00/0.88
notEmpty(Cons(x, xs)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
lookup(0, instrs) → instrs 0.00/0.88
instrsSecond(I(l, r)) → r 0.00/0.88
instrsFirst(I(l, r)) → l 0.00/0.88
getWrite(Write(int)) → int 0.00/0.88
getGotoSecond(IfGoto(i1, i2)) → i2 0.00/0.88
getGotoFirst(IfGoto(i1, i2)) → i1 0.00/0.88
getGoto(Goto(int)) → int 0.00/0.88
run(prog, tapeinput) → turing(prog, Nil, tapeinput, prog)

Rewrite Strategy: INNERMOST

0.00/0.88

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

0.00/0.88

(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) 0.00/0.88
turing(I(Goto(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](False, I(Goto(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Right, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Right, z0), z1, z2, z3) 0.00/0.88
turing(I(Left, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Left, z0), z1, z2, z3) 0.00/0.88
turing(I(Write(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](True, I(Write(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Halt, z0), z1, z2, z3) → z2 0.00/0.88
turing(Empty, z0, z1, z2) → z1 0.00/0.88
lookup(S(z0), I(z1, z2)) → lookup(z0, z2) 0.00/0.88
lookup(0, z0) → z0 0.00/0.88
instrsConstrCheck(I(z0, z1), I(z2, z3)) → True 0.00/0.88
instrsConstrCheck(I(z0, z1), Empty) → False 0.00/0.88
instrsConstrCheck(Empty, I(z0, z1)) → False 0.00/0.88
instrsConstrCheck(Empty, Empty) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), IfGoto(z2, z3)) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Goto(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Right) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Left) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Write(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Halt) → False 0.00/0.88
instrConstrCheck(Goto(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Goto(z1)) → True 0.00/0.88
instrConstrCheck(Goto(z0), Right) → False 0.00/0.88
instrConstrCheck(Goto(z0), Left) → False 0.00/0.88
instrConstrCheck(Goto(z0), Write(z1)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Halt) → False 0.00/0.88
instrConstrCheck(Right, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Right, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Right, Right) → True 0.00/0.88
instrConstrCheck(Right, Left) → False 0.00/0.88
instrConstrCheck(Right, Write(z0)) → False 0.00/0.88
instrConstrCheck(Right, Halt) → False 0.00/0.88
instrConstrCheck(Left, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Left, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Left, Right) → False 0.00/0.88
instrConstrCheck(Left, Left) → True 0.00/0.88
instrConstrCheck(Left, Write(z0)) → False 0.00/0.88
instrConstrCheck(Left, Halt) → False 0.00/0.88
instrConstrCheck(Write(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Write(z0), Goto(z1)) → False 0.00/0.88
instrConstrCheck(Write(z0), Right) → False 0.00/0.88
instrConstrCheck(Write(z0), Left) → False 0.00/0.88
instrConstrCheck(Write(z0), Write(z1)) → True 0.00/0.88
instrConstrCheck(Write(z0), Halt) → False 0.00/0.88
instrConstrCheck(Halt, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Halt, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Right) → False 0.00/0.88
instrConstrCheck(Halt, Left) → False 0.00/0.88
instrConstrCheck(Halt, Write(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Halt) → True 0.00/0.88
notEmpty(Cons(z0, z1)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
instrsSecond(I(z0, z1)) → z1 0.00/0.88
instrsFirst(I(z0, z1)) → z0 0.00/0.88
getWrite(Write(z0)) → z0 0.00/0.88
getGotoSecond(IfGoto(z0, z1)) → z1 0.00/0.88
getGotoFirst(IfGoto(z0, z1)) → z0 0.00/0.88
getGoto(Goto(z0)) → z0 0.00/0.88
run(z0, z1) → turing(z0, Nil, z1, z0)

Tuples:

LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2)) 0.00/0.88
RUN(z0, z1) → c57(TURING(z0, Nil, z1, z0))

S tuples:

LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2)) 0.00/0.88
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:

LOOKUP, RUN

Compound Symbols:

c7, c57

0.00/0.88

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

0.00/0.88

(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) 0.00/0.88
turing(I(Goto(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](False, I(Goto(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Right, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Right, z0), z1, z2, z3) 0.00/0.88
turing(I(Left, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Left, z0), z1, z2, z3) 0.00/0.88
turing(I(Write(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](True, I(Write(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Halt, z0), z1, z2, z3) → z2 0.00/0.88
turing(Empty, z0, z1, z2) → z1 0.00/0.88
lookup(S(z0), I(z1, z2)) → lookup(z0, z2) 0.00/0.88
lookup(0, z0) → z0 0.00/0.88
instrsConstrCheck(I(z0, z1), I(z2, z3)) → True 0.00/0.88
instrsConstrCheck(I(z0, z1), Empty) → False 0.00/0.88
instrsConstrCheck(Empty, I(z0, z1)) → False 0.00/0.88
instrsConstrCheck(Empty, Empty) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), IfGoto(z2, z3)) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Goto(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Right) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Left) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Write(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Halt) → False 0.00/0.88
instrConstrCheck(Goto(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Goto(z1)) → True 0.00/0.88
instrConstrCheck(Goto(z0), Right) → False 0.00/0.88
instrConstrCheck(Goto(z0), Left) → False 0.00/0.88
instrConstrCheck(Goto(z0), Write(z1)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Halt) → False 0.00/0.88
instrConstrCheck(Right, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Right, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Right, Right) → True 0.00/0.88
instrConstrCheck(Right, Left) → False 0.00/0.88
instrConstrCheck(Right, Write(z0)) → False 0.00/0.88
instrConstrCheck(Right, Halt) → False 0.00/0.88
instrConstrCheck(Left, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Left, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Left, Right) → False 0.00/0.88
instrConstrCheck(Left, Left) → True 0.00/0.88
instrConstrCheck(Left, Write(z0)) → False 0.00/0.88
instrConstrCheck(Left, Halt) → False 0.00/0.88
instrConstrCheck(Write(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Write(z0), Goto(z1)) → False 0.00/0.88
instrConstrCheck(Write(z0), Right) → False 0.00/0.88
instrConstrCheck(Write(z0), Left) → False 0.00/0.88
instrConstrCheck(Write(z0), Write(z1)) → True 0.00/0.88
instrConstrCheck(Write(z0), Halt) → False 0.00/0.88
instrConstrCheck(Halt, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Halt, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Right) → False 0.00/0.88
instrConstrCheck(Halt, Left) → False 0.00/0.88
instrConstrCheck(Halt, Write(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Halt) → True 0.00/0.88
notEmpty(Cons(z0, z1)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
instrsSecond(I(z0, z1)) → z1 0.00/0.88
instrsFirst(I(z0, z1)) → z0 0.00/0.88
getWrite(Write(z0)) → z0 0.00/0.88
getGotoSecond(IfGoto(z0, z1)) → z1 0.00/0.88
getGotoFirst(IfGoto(z0, z1)) → z0 0.00/0.88
getGoto(Goto(z0)) → z0 0.00/0.88
run(z0, z1) → turing(z0, Nil, z1, z0)

Tuples:

LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2)) 0.00/0.88
RUN(z0, z1) → c57

S tuples:

LOOKUP(S(z0), I(z1, z2)) → c7(LOOKUP(z0, z2)) 0.00/0.88
RUN(z0, z1) → c57

K tuples:none
Defined Rule Symbols:

turing, lookup, instrsConstrCheck, instrConstrCheck, notEmpty, instrsSecond, instrsFirst, getWrite, getGotoSecond, getGotoFirst, getGoto, run

Defined Pair Symbols:

LOOKUP, RUN

Compound Symbols:

c7, c57

0.00/0.88

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

RUN(z0, z1) → c57

0.00/0.88

(6) 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) 0.00/0.88
turing(I(Goto(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](False, I(Goto(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Right, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Right, z0), z1, z2, z3) 0.00/0.88
turing(I(Left, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Left, z0), z1, z2, z3) 0.00/0.88
turing(I(Write(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](True, I(Write(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Halt, z0), z1, z2, z3) → z2 0.00/0.88
turing(Empty, z0, z1, z2) → z1 0.00/0.88
lookup(S(z0), I(z1, z2)) → lookup(z0, z2) 0.00/0.88
lookup(0, z0) → z0 0.00/0.88
instrsConstrCheck(I(z0, z1), I(z2, z3)) → True 0.00/0.88
instrsConstrCheck(I(z0, z1), Empty) → False 0.00/0.88
instrsConstrCheck(Empty, I(z0, z1)) → False 0.00/0.88
instrsConstrCheck(Empty, Empty) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), IfGoto(z2, z3)) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Goto(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Right) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Left) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Write(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Halt) → False 0.00/0.88
instrConstrCheck(Goto(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Goto(z1)) → True 0.00/0.88
instrConstrCheck(Goto(z0), Right) → False 0.00/0.88
instrConstrCheck(Goto(z0), Left) → False 0.00/0.88
instrConstrCheck(Goto(z0), Write(z1)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Halt) → False 0.00/0.88
instrConstrCheck(Right, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Right, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Right, Right) → True 0.00/0.88
instrConstrCheck(Right, Left) → False 0.00/0.88
instrConstrCheck(Right, Write(z0)) → False 0.00/0.88
instrConstrCheck(Right, Halt) → False 0.00/0.88
instrConstrCheck(Left, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Left, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Left, Right) → False 0.00/0.88
instrConstrCheck(Left, Left) → True 0.00/0.88
instrConstrCheck(Left, Write(z0)) → False 0.00/0.88
instrConstrCheck(Left, Halt) → False 0.00/0.88
instrConstrCheck(Write(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Write(z0), Goto(z1)) → False 0.00/0.88
instrConstrCheck(Write(z0), Right) → False 0.00/0.88
instrConstrCheck(Write(z0), Left) → False 0.00/0.88
instrConstrCheck(Write(z0), Write(z1)) → True 0.00/0.88
instrConstrCheck(Write(z0), Halt) → False 0.00/0.88
instrConstrCheck(Halt, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Halt, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Right) → False 0.00/0.88
instrConstrCheck(Halt, Left) → False 0.00/0.88
instrConstrCheck(Halt, Write(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Halt) → True 0.00/0.88
notEmpty(Cons(z0, z1)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
instrsSecond(I(z0, z1)) → z1 0.00/0.88
instrsFirst(I(z0, z1)) → z0 0.00/0.88
getWrite(Write(z0)) → z0 0.00/0.88
getGotoSecond(IfGoto(z0, z1)) → z1 0.00/0.88
getGotoFirst(IfGoto(z0, z1)) → z0 0.00/0.88
getGoto(Goto(z0)) → z0 0.00/0.88
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

0.00/0.88

(7) CdtPolyRedPairProof (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 : 0.00/0.88

POL(I(x₁, x₂)) = [1] + x₂ 0.00/0.88
POL(LOOKUP(x₁, x₂)) = x₂ 0.00/0.88
POL(S(x₁)) = 0 0.00/0.88
POL(c7(x₁)) = x₁

0.00/0.88

(8) 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) 0.00/0.88
turing(I(Goto(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](False, I(Goto(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Right, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Right, z0), z1, z2, z3) 0.00/0.88
turing(I(Left, z0), z1, z2, z3) → turing[Ite][True][Ite][False][Ite](False, I(Left, z0), z1, z2, z3) 0.00/0.88
turing(I(Write(z0), z1), z2, z3, z4) → turing[Ite][True][Ite][False][Ite](True, I(Write(z0), z1), z2, z3, z4) 0.00/0.88
turing(I(Halt, z0), z1, z2, z3) → z2 0.00/0.88
turing(Empty, z0, z1, z2) → z1 0.00/0.88
lookup(S(z0), I(z1, z2)) → lookup(z0, z2) 0.00/0.88
lookup(0, z0) → z0 0.00/0.88
instrsConstrCheck(I(z0, z1), I(z2, z3)) → True 0.00/0.88
instrsConstrCheck(I(z0, z1), Empty) → False 0.00/0.88
instrsConstrCheck(Empty, I(z0, z1)) → False 0.00/0.88
instrsConstrCheck(Empty, Empty) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), IfGoto(z2, z3)) → True 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Goto(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Right) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Left) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Write(z2)) → False 0.00/0.88
instrConstrCheck(IfGoto(z0, z1), Halt) → False 0.00/0.88
instrConstrCheck(Goto(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Goto(z1)) → True 0.00/0.88
instrConstrCheck(Goto(z0), Right) → False 0.00/0.88
instrConstrCheck(Goto(z0), Left) → False 0.00/0.88
instrConstrCheck(Goto(z0), Write(z1)) → False 0.00/0.88
instrConstrCheck(Goto(z0), Halt) → False 0.00/0.88
instrConstrCheck(Right, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Right, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Right, Right) → True 0.00/0.88
instrConstrCheck(Right, Left) → False 0.00/0.88
instrConstrCheck(Right, Write(z0)) → False 0.00/0.88
instrConstrCheck(Right, Halt) → False 0.00/0.88
instrConstrCheck(Left, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Left, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Left, Right) → False 0.00/0.88
instrConstrCheck(Left, Left) → True 0.00/0.88
instrConstrCheck(Left, Write(z0)) → False 0.00/0.88
instrConstrCheck(Left, Halt) → False 0.00/0.88
instrConstrCheck(Write(z0), IfGoto(z1, z2)) → False 0.00/0.88
instrConstrCheck(Write(z0), Goto(z1)) → False 0.00/0.88
instrConstrCheck(Write(z0), Right) → False 0.00/0.88
instrConstrCheck(Write(z0), Left) → False 0.00/0.88
instrConstrCheck(Write(z0), Write(z1)) → True 0.00/0.88
instrConstrCheck(Write(z0), Halt) → False 0.00/0.88
instrConstrCheck(Halt, IfGoto(z0, z1)) → False 0.00/0.88
instrConstrCheck(Halt, Goto(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Right) → False 0.00/0.88
instrConstrCheck(Halt, Left) → False 0.00/0.88
instrConstrCheck(Halt, Write(z0)) → False 0.00/0.88
instrConstrCheck(Halt, Halt) → True 0.00/0.88
notEmpty(Cons(z0, z1)) → True 0.00/0.88
notEmpty(Nil) → False 0.00/0.88
instrsSecond(I(z0, z1)) → z1 0.00/0.88
instrsFirst(I(z0, z1)) → z0 0.00/0.88
getWrite(Write(z0)) → z0 0.00/0.88
getGotoSecond(IfGoto(z0, z1)) → z1 0.00/0.88
getGotoFirst(IfGoto(z0, z1)) → z0 0.00/0.88
getGoto(Goto(z0)) → z0 0.00/0.88
run(z0, z1) → turing(z0, Nil, z1, z0)

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:

turing, lookup, instrsConstrCheck, instrConstrCheck, notEmpty, instrsSecond, instrsFirst, getWrite, getGotoSecond, getGotoFirst, getGoto, run

Defined Pair Symbols:

LOOKUP

Compound Symbols:

c7

0.00/0.88

(9) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

0.00/0.88

(10) BOUNDS(O(1), O(1))

0.00/0.88