Tool CaT
stdout:
YES(?,O(n^2))
Problem:
top(sent(x)) -> top(check(rest(x)))
rest(nil()) -> sent(nil())
rest(cons(x,y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
check(cons(x,y)) -> cons(x,y)
Proof:
Complexity Transformation Processor:
strict:
top(sent(x)) -> top(check(rest(x)))
rest(nil()) -> sent(nil())
rest(cons(x,y)) -> sent(y)
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
check(cons(x,y)) -> cons(x,y)
weak:
Matrix Interpretation Processor:
dimension: 3
max_matrix:
[1 2 2]
[0 0 0]
[0 0 0]
interpretation:
[1 0 2] [1 2 0] [1]
[cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
[0 0 0] [0 0 0] [0],
[0]
[nil] = [0]
[0],
[1 0 0]
[check](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0]
[rest](x0) = [0 0 0]x0
[0 0 0] ,
[1 0 0] [0]
[top](x0) = [0 0 0]x0 + [2]
[0 0 0] [0],
[1 2 0]
[sent](x0) = [0 0 0]x0
[0 0 0]
orientation:
[1 2 0] [0] [1 0 0] [0]
top(sent(x)) = [0 0 0]x + [2] >= [0 0 0]x + [2] = top(check(rest(x)))
[0 0 0] [0] [0 0 0] [0]
[0] [0]
rest(nil()) = [0] >= [0] = sent(nil())
[0] [0]
[1 0 2] [1 2 0] [1] [1 2 0]
rest(cons(x,y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]y = sent(y)
[0 0 0] [0 0 0] [0] [0 0 0]
[1 2 0] [1 0 0]
check(sent(x)) = [0 0 0]x >= [0 0 0]x = sent(check(x))
[0 0 0] [0 0 0]
[1 0 0] [1 0 0]
check(rest(x)) = [0 0 0]x >= [0 0 0]x = rest(check(x))
[0 0 0] [0 0 0]
[1 0 2] [1 2 0] [1] [1 0 0] [1 2 0] [1]
check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = cons(check(x),y)
[0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0]
[1 0 2] [1 2 0] [1] [1 0 2] [1 0 0] [1]
check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = cons(x,check(y))
[0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0]
[1 0 2] [1 2 0] [1] [1 0 2] [1 2 0] [1]
check(cons(x,y)) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = cons(x,y)
[0 0 0] [0 0 0] [0] [0 0 0] [0 0 0] [0]
problem:
strict:
top(sent(x)) -> top(check(rest(x)))
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
check(cons(x,y)) -> cons(x,y)
weak:
rest(cons(x,y)) -> sent(y)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[cons](x0, x1) = x0 + x1 + 18,
[nil] = 105,
[check](x0) = x0 + 37,
[rest](x0) = x0 + 63,
[top](x0) = x0 + 5,
[sent](x0) = x0 + 81
orientation:
top(sent(x)) = x + 86 >= x + 105 = top(check(rest(x)))
rest(nil()) = 168 >= 186 = sent(nil())
check(sent(x)) = x + 118 >= x + 118 = sent(check(x))
check(rest(x)) = x + 100 >= x + 100 = rest(check(x))
check(cons(x,y)) = x + y + 55 >= x + y + 55 = cons(check(x),y)
check(cons(x,y)) = x + y + 55 >= x + y + 55 = cons(x,check(y))
check(cons(x,y)) = x + y + 55 >= x + y + 18 = cons(x,y)
rest(cons(x,y)) = x + y + 81 >= y + 81 = sent(y)
problem:
strict:
top(sent(x)) -> top(check(rest(x)))
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
weak:
check(cons(x,y)) -> cons(x,y)
rest(cons(x,y)) -> sent(y)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[cons](x0, x1) = x0 + x1 + 8,
[nil] = 66,
[check](x0) = x0,
[rest](x0) = x0 + 5,
[top](x0) = x0 + 229,
[sent](x0) = x0 + 10
orientation:
top(sent(x)) = x + 239 >= x + 234 = top(check(rest(x)))
rest(nil()) = 71 >= 76 = sent(nil())
check(sent(x)) = x + 10 >= x + 10 = sent(check(x))
check(rest(x)) = x + 5 >= x + 5 = rest(check(x))
check(cons(x,y)) = x + y + 8 >= x + y + 8 = cons(check(x),y)
check(cons(x,y)) = x + y + 8 >= x + y + 8 = cons(x,check(y))
check(cons(x,y)) = x + y + 8 >= x + y + 8 = cons(x,y)
rest(cons(x,y)) = x + y + 13 >= y + 10 = sent(y)
problem:
strict:
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
weak:
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
rest(cons(x,y)) -> sent(y)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 0 0 1]
[0 0 0 1]
[0 0 0 0]
[0 0 0 1]
interpretation:
[1 0 0 0] [1 0 0 1] [0]
[0 0 0 0] [0 0 0 0] [0]
[cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0]
[0 0 0 1] [0 0 0 1] [1],
[0]
[0]
[nil] = [0]
[0],
[1 0 0 1]
[0 0 0 0]
[check](x0) = [0 0 0 0]x0
[0 0 0 1] ,
[1 0 0 0]
[0 0 0 0]
[rest](x0) = [0 0 0 0]x0
[0 0 0 1] ,
[1 0 0 0] [0]
[0 0 0 1] [0]
[top](x0) = [0 0 0 0]x0 + [0]
[0 0 0 1] [1],
[1 0 0 1]
[0 0 0 0]
[sent](x0) = [0 0 0 0]x0
[0 0 0 1]
orientation:
[0] [0]
[0] [0]
rest(nil()) = [0] >= [0] = sent(nil())
[0] [0]
[1 0 0 2] [1 0 0 2]
[0 0 0 0] [0 0 0 0]
check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x))
[0 0 0 1] [0 0 0 1]
[1 0 0 1] [1 0 0 1]
[0 0 0 0] [0 0 0 0]
check(rest(x)) = [0 0 0 0]x >= [0 0 0 0]x = rest(check(x))
[0 0 0 1] [0 0 0 1]
[1 0 0 1] [1 0 0 2] [1] [1 0 0 1] [1 0 0 1] [0]
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(check(x),y)
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1]
[1 0 0 1] [1 0 0 2] [1] [1 0 0 0] [1 0 0 2] [0]
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,check(y))
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1]
[1 0 0 1] [0] [1 0 0 1] [0]
[0 0 0 1] [0] [0 0 0 1] [0]
top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x)))
[0 0 0 1] [1] [0 0 0 1] [1]
[1 0 0 1] [1 0 0 2] [1] [1 0 0 0] [1 0 0 1] [0]
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]x + [0 0 0 0]y + [0] = cons(x,y)
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1] [0 0 0 1] [1]
[1 0 0 0] [1 0 0 1] [0] [1 0 0 1]
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0]
rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 0]y + [0] >= [0 0 0 0]y = sent(y)
[0 0 0 1] [0 0 0 1] [1] [0 0 0 1]
problem:
strict:
rest(nil()) -> sent(nil())
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
weak:
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
rest(cons(x,y)) -> sent(y)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 0 1 1]
[0 0 1 1]
[0 0 0 0]
interpretation:
[1 0 0 0] [1 0 1 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[cons](x0, x1) = [0 0 0 0]x0 + [0 0 0 1]x1 + [1]
[0 0 0 0] [0 0 0 0] [0],
[0]
[0]
[nil] = [0]
[1],
[1 0 0 0]
[0 0 1 0]
[check](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 0 0 1]
[0 0 1 1]
[rest](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 1 0 0]
[0 0 0 0]
[top](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 1 0]
[0 0 0 1]
[sent](x0) = [0 0 0 0]x0
[0 0 0 0]
orientation:
[1] [0]
[1] [1]
rest(nil()) = [0] >= [0] = sent(nil())
[0] [0]
[1 0 1 0] [1 0 1 0]
[0 0 0 0] [0 0 0 0]
check(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = sent(check(x))
[0 0 0 0] [0 0 0 0]
[1 0 0 1] [1 0 0 0]
[0 0 1 0] [0 0 1 0]
check(rest(x)) = [0 0 1 0]x >= [0 0 1 0]x = rest(check(x))
[0 0 0 0] [0 0 0 0]
[1 0 0 0] [1 0 1 0] [0] [1 0 0 0] [1 0 1 0] [0]
[0 0 0 0] [0 0 0 1] [1] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [1] >= [0 0 0 0]x + [0 0 0 1]y + [1] = cons(check(x),y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [1 0 1 0] [0] [1 0 0 0] [1 0 1 0] [0]
[0 0 0 0] [0 0 0 1] [1] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [1] >= [0 0 0 0]x + [0 0 0 0]y + [1] = cons(x,check(y))
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 1 1] [1 0 1 1]
[0 0 0 0] [0 0 0 0]
top(sent(x)) = [0 0 0 0]x >= [0 0 0 0]x = top(check(rest(x)))
[0 0 0 0] [0 0 0 0]
[1 0 0 0] [1 0 1 0] [0] [1 0 0 0] [1 0 1 0] [0]
[0 0 0 0] [0 0 0 1] [1] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [1] >= [0 0 0 0]x + [0 0 0 1]y + [1] = cons(x,y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 0 0] [1 0 1 0] [0] [1 0 1 0]
[0 0 0 0] [0 0 0 1] [1] [0 0 0 1]
rest(cons(x,y)) = [0 0 0 0]x + [0 0 0 1]y + [1] >= [0 0 0 0]y = sent(y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0]
problem:
strict:
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
weak:
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
rest(cons(x,y)) -> sent(y)
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 1]
[0 0 1 1]
[0 0 1 1]
[0 0 0 0]
interpretation:
[1 0 1 1] [1 0 1 0] [1]
[0 0 0 0] [0 0 0 0] [0]
[cons](x0, x1) = [0 0 1 0]x0 + [0 0 1 1]x1 + [0]
[0 0 0 0] [0 0 0 0] [0],
[0]
[0]
[nil] = [0]
[1],
[1 0 1 0]
[0 0 1 0]
[check](x0) = [0 0 1 0]x0
[0 0 0 0] ,
[1 0 0 1] [0]
[0 0 1 1] [1]
[rest](x0) = [0 0 1 0]x0 + [1]
[0 0 0 0] [0],
[1 1 0 0]
[0 0 0 0]
[top](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 1 0] [1]
[0 0 1 1] [1]
[sent](x0) = [0 0 1 0]x0 + [1]
[0 0 0 0] [0]
orientation:
[1 0 2 0] [2] [1 0 2 0] [1]
[0 0 1 0] [1] [0 0 1 0] [1]
check(sent(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = sent(check(x))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 1 1] [1] [1 0 1 0] [0]
[0 0 1 0] [1] [0 0 1 0] [1]
check(rest(x)) = [0 0 1 0]x + [1] >= [0 0 1 0]x + [1] = rest(check(x))
[0 0 0 0] [0] [0 0 0 0] [0]
[1] [1]
[2] [2]
rest(nil()) = [1] >= [1] = sent(nil())
[0] [0]
[1 0 2 1] [1 0 2 1] [1] [1 0 2 0] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(check(x),y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 2 1] [1 0 2 1] [1] [1 0 1 1] [1 0 2 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 0]y + [0] = cons(x,check(y))
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 2 1] [2] [1 0 2 1] [2]
[0 0 0 0] [0] [0 0 0 0] [0]
top(sent(x)) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = top(check(rest(x)))
[0 0 0 0] [0] [0 0 0 0] [0]
[1 0 2 1] [1 0 2 1] [1] [1 0 1 1] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [0] [0 0 0 0] [0 0 0 0] [0]
check(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [0] >= [0 0 1 0]x + [0 0 1 1]y + [0] = cons(x,y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0]
[1 0 1 1] [1 0 1 0] [1] [1 0 1 0] [1]
[0 0 1 0] [0 0 1 1] [1] [0 0 1 1] [1]
rest(cons(x,y)) = [0 0 1 0]x + [0 0 1 1]y + [1] >= [0 0 1 0]y + [1] = sent(y)
[0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0]
problem:
strict:
weak:
check(sent(x)) -> sent(check(x))
check(rest(x)) -> rest(check(x))
rest(nil()) -> sent(nil())
check(cons(x,y)) -> cons(check(x),y)
check(cons(x,y)) -> cons(x,check(y))
top(sent(x)) -> top(check(rest(x)))
check(cons(x,y)) -> cons(x,y)
rest(cons(x,y)) -> sent(y)
Qed
Tool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ top(sent(x)) -> top(check(rest(x)))
, rest(nil()) -> sent(nil())
, rest(cons(x, y)) -> sent(y)
, check(sent(x)) -> sent(check(x))
, check(rest(x)) -> rest(check(x))
, check(cons(x, y)) -> cons(check(x), y)
, check(cons(x, y)) -> cons(x, check(y))
, check(cons(x, y)) -> cons(x, y)}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
stdout:
MAYBE
Tool RC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ top(sent(x)) -> top(check(rest(x)))
, rest(nil()) -> sent(nil())
, rest(cons(x, y)) -> sent(y)
, check(sent(x)) -> sent(check(x))
, check(rest(x)) -> rest(check(x))
, check(cons(x, y)) -> cons(check(x), y)
, check(cons(x, y)) -> cons(x, check(y))
, check(cons(x, y)) -> cons(x, y)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds