Problem:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Proof:
Complexity Transformation Processor:
strict:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[top](x0) = x0 + 14,
[ok](x0) = x0 + 3,
[proper](x0) = x0 + 8,
[mark](x0) = x0 + 8,
[b] = 3,
[active](x0) = x0 + 2,
[f](x0, x1, x2) = x0 + x1 + x2 + 4,
[a] = 9
orientation:
active(f(a(),X,X)) = 2X + 15 >= X + 18 = mark(f(X,b(),b()))
active(b()) = 5 >= 17 = mark(a())
active(f(X1,X2,X3)) = X1 + X2 + X3 + 6 >= X1 + X2 + X3 + 6 = f(X1,active(X2),X3)
f(X1,mark(X2),X3) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 12 = mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 28 = f(proper(X1),proper(X2),proper(X3))
proper(a()) = 17 >= 12 = ok(a())
proper(b()) = 11 >= 6 = ok(b())
f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 13 >= X1 + X2 + X3 + 7 = ok(f(X1,X2,X3))
top(mark(X)) = X + 22 >= X + 22 = top(proper(X))
top(ok(X)) = X + 17 >= X + 16 = top(active(X))
problem:
strict:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
top(mark(X)) -> top(proper(X))
weak:
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[top](x0) = x0 + 4,
[ok](x0) = x0,
[proper](x0) = x0,
[mark](x0) = x0 + 1,
[b] = 13,
[active](x0) = x0,
[f](x0, x1, x2) = x0 + x1 + x2 + 4,
[a] = 12
orientation:
active(f(a(),X,X)) = 2X + 16 >= X + 31 = mark(f(X,b(),b()))
active(b()) = 13 >= 13 = mark(a())
active(f(X1,X2,X3)) = X1 + X2 + X3 + 4 >= X1 + X2 + X3 + 4 = f(X1,active(X2),X3)
f(X1,mark(X2),X3) = X1 + X2 + X3 + 5 >= X1 + X2 + X3 + 5 = mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) = X1 + X2 + X3 + 4 >= X1 + X2 + X3 + 4 = f(proper(X1),proper(X2),proper(X3))
top(mark(X)) = X + 5 >= X + 4 = top(proper(X))
proper(a()) = 12 >= 12 = ok(a())
proper(b()) = 13 >= 13 = ok(b())
f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 4 >= X1 + X2 + X3 + 4 = ok(f(X1,X2,X3))
top(ok(X)) = X + 4 >= X + 4 = top(active(X))
problem:
strict:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
weak:
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[top](x0) = x0 + 2,
[ok](x0) = x0 + 2,
[proper](x0) = x0 + 2,
[mark](x0) = x0 + 2,
[b] = 2,
[active](x0) = x0 + 2,
[f](x0, x1, x2) = x0 + x1 + x2 + 10,
[a] = 0
orientation:
active(f(a(),X,X)) = 2X + 12 >= X + 16 = mark(f(X,b(),b()))
active(b()) = 4 >= 2 = mark(a())
active(f(X1,X2,X3)) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 12 = f(X1,active(X2),X3)
f(X1,mark(X2),X3) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 12 = mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) = X1 + X2 + X3 + 12 >= X1 + X2 + X3 + 16 = f(proper(X1),proper(X2),proper(X3))
top(mark(X)) = X + 4 >= X + 4 = top(proper(X))
proper(a()) = 2 >= 2 = ok(a())
proper(b()) = 4 >= 4 = ok(b())
f(ok(X1),ok(X2),ok(X3)) = X1 + X2 + X3 + 16 >= X1 + X2 + X3 + 12 = ok(f(X1,X2,X3))
top(ok(X)) = X + 4 >= X + 4 = top(active(X))
problem:
strict:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
weak:
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
Splitting Processor:
strict:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
weak:
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
Splitting Processor:
strict:
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
weak:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {11,9,8,7,6,5}
transitions:
active0(2) -> 5*
active0(9) -> 5*
active0(4) -> 5*
active0(11) -> 5*
active0(1) -> 5*
active0(3) -> 5*
f0(3,4,2) -> 7*
f0(3,2,11) -> 7*
f0(3,4,11) -> 7*
f0(11,1,4) -> 7*
f0(1,1,4) -> 7*
f0(11,3,4) -> 7*
f0(1,3,4) -> 7*
f0(11,2,9) -> 7*
f0(1,2,9) -> 7*
f0(11,4,9) -> 7*
f0(11,9,4) -> 7*
f0(1,4,9) -> 7*
f0(1,9,4) -> 7*
f0(11,11,4) -> 7*
f0(11,1,1) -> 7*
f0(9,1,2) -> 7*
f0(4,1,2) -> 7*
f0(1,11,4) -> 7*
f0(1,1,1) -> 7*
f0(11,3,1) -> 7*
f0(9,3,2) -> 7*
f0(4,3,2) -> 7*
f0(1,3,1) -> 7*
f0(9,1,11) -> 7*
f0(4,1,11) -> 7*
f0(9,3,11) -> 7*
f0(4,3,11) -> 7*
f0(11,9,1) -> 7*
f0(9,9,2) -> 7*
f0(4,9,2) -> 7*
f0(1,9,1) -> 7*
f0(11,11,1) -> 7*
f0(9,11,2) -> 7*
f0(4,11,2) -> 7*
f0(1,11,1) -> 7*
f0(2,2,4) -> 7*
f0(9,9,11) -> 7*
f0(4,9,11) -> 7*
f0(2,4,4) -> 7*
f0(9,11,11) -> 7*
f0(11,2,3) -> 7*
f0(4,11,11) -> 7*
f0(2,1,9) -> 7*
f0(1,2,3) -> 7*
f0(11,4,3) -> 7*
f0(2,3,9) -> 7*
f0(1,4,3) -> 7*
f0(2,2,1) -> 7*
f0(2,9,9) -> 7*
f0(2,4,1) -> 7*
f0(2,11,9) -> 7*
f0(3,1,4) -> 7*
f0(3,3,4) -> 7*
f0(2,1,3) -> 7*
f0(3,2,9) -> 7*
f0(2,3,3) -> 7*
f0(3,4,9) -> 7*
f0(3,9,4) -> 7*
f0(11,1,2) -> 7*
f0(3,11,4) -> 7*
f0(3,1,1) -> 7*
f0(1,1,2) -> 7*
f0(11,3,2) -> 7*
f0(3,3,1) -> 7*
f0(1,3,2) -> 7*
f0(11,1,11) -> 7*
f0(2,9,3) -> 7*
f0(11,3,11) -> 7*
f0(1,1,11) -> 7*
f0(2,11,3) -> 7*
f0(11,9,2) -> 7*
f0(1,3,11) -> 7*
f0(3,9,1) -> 7*
f0(1,9,2) -> 7*
f0(11,11,2) -> 7*
f0(9,2,4) -> 7*
f0(3,11,1) -> 7*
f0(1,11,2) -> 7*
f0(4,2,4) -> 7*
f0(11,9,11) -> 7*
f0(9,4,4) -> 7*
f0(4,4,4) -> 7*
f0(11,11,11) -> 7*
f0(1,9,11) -> 7*
f0(9,1,9) -> 7*
f0(4,1,9) -> 7*
f0(1,11,11) -> 7*
f0(9,3,9) -> 7*
f0(3,2,3) -> 7*
f0(4,3,9) -> 7*
f0(3,4,3) -> 7*
f0(9,2,1) -> 7*
f0(4,2,1) -> 7*
f0(2,2,2) -> 7*
f0(9,9,9) -> 7*
f0(9,4,1) -> 7*
f0(4,9,9) -> 7*
f0(4,4,1) -> 7*
f0(2,4,2) -> 7*
f0(9,11,9) -> 7*
f0(4,11,9) -> 7*
f0(2,2,11) -> 7*
f0(2,4,11) -> 7*
f0(9,1,3) -> 7*
f0(4,1,3) -> 7*
f0(9,3,3) -> 7*
f0(4,3,3) -> 7*
f0(3,1,2) -> 7*
f0(9,9,3) -> 7*
f0(3,3,2) -> 7*
f0(4,9,3) -> 7*
f0(9,11,3) -> 7*
f0(3,1,11) -> 7*
f0(4,11,3) -> 7*
f0(3,3,11) -> 7*
f0(3,9,2) -> 7*
f0(11,2,4) -> 7*
f0(3,11,2) -> 7*
f0(1,2,4) -> 7*
f0(11,4,4) -> 7*
f0(3,9,11) -> 7*
f0(11,1,9) -> 7*
f0(1,4,4) -> 7*
f0(3,11,11) -> 7*
f0(1,1,9) -> 7*
f0(11,3,9) -> 7*
f0(1,3,9) -> 7*
f0(11,2,1) -> 7*
f0(9,2,2) -> 7*
f0(4,2,2) -> 7*
f0(11,9,9) -> 7*
f0(1,2,1) -> 7*
f0(11,4,1) -> 7*
f0(9,4,2) -> 7*
f0(4,4,2) -> 7*
f0(1,9,9) -> 7*
f0(11,11,9) -> 7*
f0(1,4,1) -> 7*
f0(9,2,11) -> 7*
f0(1,11,9) -> 7*
f0(4,2,11) -> 7*
f0(9,4,11) -> 7*
f0(4,4,11) -> 7*
f0(2,1,4) -> 7*
f0(2,3,4) -> 7*
f0(11,1,3) -> 7*
f0(1,1,3) -> 7*
f0(11,3,3) -> 7*
f0(2,2,9) -> 7*
f0(1,3,3) -> 7*
f0(2,4,9) -> 7*
f0(2,9,4) -> 7*
f0(2,11,4) -> 7*
f0(2,1,1) -> 7*
f0(11,9,3) -> 7*
f0(2,3,1) -> 7*
f0(1,9,3) -> 7*
f0(11,11,3) -> 7*
f0(1,11,3) -> 7*
f0(2,9,1) -> 7*
f0(2,11,1) -> 7*
f0(3,2,4) -> 7*
f0(3,4,4) -> 7*
f0(3,1,9) -> 7*
f0(2,2,3) -> 7*
f0(3,3,9) -> 7*
f0(2,4,3) -> 7*
f0(11,2,2) -> 7*
f0(3,2,1) -> 7*
f0(1,2,2) -> 7*
f0(11,4,2) -> 7*
f0(3,9,9) -> 7*
f0(3,4,1) -> 7*
f0(1,4,2) -> 7*
f0(11,2,11) -> 7*
f0(3,11,9) -> 7*
f0(1,2,11) -> 7*
f0(11,4,11) -> 7*
f0(1,4,11) -> 7*
f0(9,1,4) -> 7*
f0(4,1,4) -> 7*
f0(9,3,4) -> 7*
f0(4,3,4) -> 7*
f0(9,2,9) -> 7*
f0(3,1,3) -> 7*
f0(4,2,9) -> 7*
f0(9,4,9) -> 7*
f0(9,9,4) -> 7*
f0(3,3,3) -> 7*
f0(4,4,9) -> 7*
f0(4,9,4) -> 7*
f0(9,11,4) -> 7*
f0(9,1,1) -> 7*
f0(4,11,4) -> 7*
f0(4,1,1) -> 7*
f0(2,1,2) -> 7*
f0(9,3,1) -> 7*
f0(4,3,1) -> 7*
f0(2,3,2) -> 7*
f0(3,9,3) -> 7*
f0(2,1,11) -> 7*
f0(3,11,3) -> 7*
f0(2,3,11) -> 7*
f0(9,9,1) -> 7*
f0(4,9,1) -> 7*
f0(2,9,2) -> 7*
f0(9,11,1) -> 7*
f0(4,11,1) -> 7*
f0(2,11,2) -> 7*
f0(2,9,11) -> 7*
f0(9,2,3) -> 7*
f0(2,11,11) -> 7*
f0(4,2,3) -> 7*
f0(9,4,3) -> 7*
f0(4,4,3) -> 7*
f0(3,2,2) -> 7*
proper0(2) -> 6*
proper0(9) -> 6*
proper0(4) -> 6*
proper0(11) -> 6*
proper0(1) -> 6*
proper0(3) -> 6*
mark0(7) -> 7*
mark0(2) -> 9*,5,1
mark0(9) -> 1*
mark0(4) -> 1*
mark0(11) -> 1*
mark0(1) -> 1*
mark0(3) -> 1*
a0() -> 2*
b0() -> 3*
top0(5) -> 8*
top0(2) -> 8*
top0(9) -> 8*
top0(4) -> 8*
top0(11) -> 8*
top0(6) -> 8*
top0(1) -> 8*
top0(3) -> 8*
ok0(7) -> 7*
ok0(2) -> 11*,6,4
ok0(9) -> 4*
ok0(4) -> 4*
ok0(11) -> 4*
ok0(1) -> 4*
ok0(3) -> 11*,6,4
problem:
strict:
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
weak:
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
Bounds Processor:
bound: 0
enrichment: match
automaton:
final states: {11,9,8,7,6,5}
transitions:
active0(2) -> 6*
active0(9) -> 6*
active0(4) -> 6*
active0(11) -> 6*
active0(1) -> 6*
active0(3) -> 6*
f0(3,4,2) -> 7*
f0(3,2,11) -> 7*
f0(3,4,11) -> 7*
f0(11,1,4) -> 7*
f0(1,1,4) -> 7*
f0(11,3,4) -> 7*
f0(1,3,4) -> 7*
f0(11,2,9) -> 7*
f0(1,2,9) -> 7*
f0(11,4,9) -> 7*
f0(11,9,4) -> 7*
f0(1,4,9) -> 7*
f0(1,9,4) -> 7*
f0(11,11,4) -> 7*
f0(11,1,1) -> 7*
f0(9,1,2) -> 7*
f0(4,1,2) -> 7*
f0(1,11,4) -> 7*
f0(1,1,1) -> 7*
f0(11,3,1) -> 7*
f0(9,3,2) -> 7*
f0(4,3,2) -> 7*
f0(1,3,1) -> 7*
f0(9,1,11) -> 7*
f0(4,1,11) -> 7*
f0(9,3,11) -> 7*
f0(4,3,11) -> 7*
f0(11,9,1) -> 7*
f0(9,9,2) -> 7*
f0(4,9,2) -> 7*
f0(1,9,1) -> 7*
f0(11,11,1) -> 7*
f0(9,11,2) -> 7*
f0(4,11,2) -> 7*
f0(1,11,1) -> 7*
f0(2,2,4) -> 7*
f0(9,9,11) -> 7*
f0(4,9,11) -> 7*
f0(2,4,4) -> 7*
f0(9,11,11) -> 7*
f0(11,2,3) -> 7*
f0(4,11,11) -> 7*
f0(2,1,9) -> 7*
f0(1,2,3) -> 7*
f0(11,4,3) -> 7*
f0(2,3,9) -> 7*
f0(1,4,3) -> 7*
f0(2,2,1) -> 7*
f0(2,9,9) -> 7*
f0(2,4,1) -> 7*
f0(2,11,9) -> 7*
f0(3,1,4) -> 7*
f0(3,3,4) -> 7*
f0(2,1,3) -> 7*
f0(3,2,9) -> 7*
f0(2,3,3) -> 7*
f0(3,4,9) -> 7*
f0(3,9,4) -> 7*
f0(11,1,2) -> 7*
f0(3,11,4) -> 7*
f0(3,1,1) -> 7*
f0(1,1,2) -> 7*
f0(11,3,2) -> 7*
f0(3,3,1) -> 7*
f0(1,3,2) -> 7*
f0(11,1,11) -> 7*
f0(2,9,3) -> 7*
f0(11,3,11) -> 7*
f0(1,1,11) -> 7*
f0(2,11,3) -> 7*
f0(11,9,2) -> 7*
f0(1,3,11) -> 7*
f0(3,9,1) -> 7*
f0(1,9,2) -> 7*
f0(11,11,2) -> 7*
f0(9,2,4) -> 7*
f0(3,11,1) -> 7*
f0(1,11,2) -> 7*
f0(4,2,4) -> 7*
f0(11,9,11) -> 7*
f0(9,4,4) -> 7*
f0(4,4,4) -> 7*
f0(11,11,11) -> 7*
f0(1,9,11) -> 7*
f0(9,1,9) -> 7*
f0(4,1,9) -> 7*
f0(1,11,11) -> 7*
f0(9,3,9) -> 7*
f0(3,2,3) -> 7*
f0(4,3,9) -> 7*
f0(3,4,3) -> 7*
f0(9,2,1) -> 7*
f0(4,2,1) -> 7*
f0(2,2,2) -> 7*
f0(9,9,9) -> 7*
f0(9,4,1) -> 7*
f0(4,9,9) -> 7*
f0(4,4,1) -> 7*
f0(2,4,2) -> 7*
f0(9,11,9) -> 7*
f0(4,11,9) -> 7*
f0(2,2,11) -> 7*
f0(2,4,11) -> 7*
f0(9,1,3) -> 7*
f0(4,1,3) -> 7*
f0(9,3,3) -> 7*
f0(4,3,3) -> 7*
f0(3,1,2) -> 7*
f0(9,9,3) -> 7*
f0(3,3,2) -> 7*
f0(4,9,3) -> 7*
f0(9,11,3) -> 7*
f0(3,1,11) -> 7*
f0(4,11,3) -> 7*
f0(3,3,11) -> 7*
f0(3,9,2) -> 7*
f0(11,2,4) -> 7*
f0(3,11,2) -> 7*
f0(1,2,4) -> 7*
f0(11,4,4) -> 7*
f0(3,9,11) -> 7*
f0(11,1,9) -> 7*
f0(1,4,4) -> 7*
f0(3,11,11) -> 7*
f0(1,1,9) -> 7*
f0(11,3,9) -> 7*
f0(1,3,9) -> 7*
f0(11,2,1) -> 7*
f0(9,2,2) -> 7*
f0(4,2,2) -> 7*
f0(11,9,9) -> 7*
f0(1,2,1) -> 7*
f0(11,4,1) -> 7*
f0(9,4,2) -> 7*
f0(4,4,2) -> 7*
f0(1,9,9) -> 7*
f0(11,11,9) -> 7*
f0(1,4,1) -> 7*
f0(9,2,11) -> 7*
f0(1,11,9) -> 7*
f0(4,2,11) -> 7*
f0(9,4,11) -> 7*
f0(4,4,11) -> 7*
f0(2,1,4) -> 7*
f0(2,3,4) -> 7*
f0(11,1,3) -> 7*
f0(1,1,3) -> 7*
f0(11,3,3) -> 7*
f0(2,2,9) -> 7*
f0(1,3,3) -> 7*
f0(2,4,9) -> 7*
f0(2,9,4) -> 7*
f0(2,11,4) -> 7*
f0(2,1,1) -> 7*
f0(11,9,3) -> 7*
f0(2,3,1) -> 7*
f0(1,9,3) -> 7*
f0(11,11,3) -> 7*
f0(1,11,3) -> 7*
f0(2,9,1) -> 7*
f0(2,11,1) -> 7*
f0(3,2,4) -> 7*
f0(3,4,4) -> 7*
f0(3,1,9) -> 7*
f0(2,2,3) -> 7*
f0(3,3,9) -> 7*
f0(2,4,3) -> 7*
f0(11,2,2) -> 7*
f0(3,2,1) -> 7*
f0(1,2,2) -> 7*
f0(11,4,2) -> 7*
f0(3,9,9) -> 7*
f0(3,4,1) -> 7*
f0(1,4,2) -> 7*
f0(11,2,11) -> 7*
f0(3,11,9) -> 7*
f0(1,2,11) -> 7*
f0(11,4,11) -> 7*
f0(1,4,11) -> 7*
f0(9,1,4) -> 7*
f0(4,1,4) -> 7*
f0(9,3,4) -> 7*
f0(4,3,4) -> 7*
f0(9,2,9) -> 7*
f0(3,1,3) -> 7*
f0(4,2,9) -> 7*
f0(9,4,9) -> 7*
f0(9,9,4) -> 7*
f0(3,3,3) -> 7*
f0(4,4,9) -> 7*
f0(4,9,4) -> 7*
f0(9,11,4) -> 7*
f0(9,1,1) -> 7*
f0(4,11,4) -> 7*
f0(4,1,1) -> 7*
f0(2,1,2) -> 7*
f0(9,3,1) -> 7*
f0(4,3,1) -> 7*
f0(2,3,2) -> 7*
f0(3,9,3) -> 7*
f0(2,1,11) -> 7*
f0(3,11,3) -> 7*
f0(2,3,11) -> 7*
f0(9,9,1) -> 7*
f0(4,9,1) -> 7*
f0(2,9,2) -> 7*
f0(9,11,1) -> 7*
f0(4,11,1) -> 7*
f0(2,11,2) -> 7*
f0(2,9,11) -> 7*
f0(9,2,3) -> 7*
f0(2,11,11) -> 7*
f0(4,2,3) -> 7*
f0(9,4,3) -> 7*
f0(4,4,3) -> 7*
f0(3,2,2) -> 7*
proper0(2) -> 5*
proper0(9) -> 5*
proper0(4) -> 5*
proper0(11) -> 5*
proper0(1) -> 5*
proper0(3) -> 5*
mark0(7) -> 7*
mark0(2) -> 9*,6,1
mark0(9) -> 1*
mark0(4) -> 1*
mark0(11) -> 1*
mark0(1) -> 1*
mark0(3) -> 1*
a0() -> 2*
b0() -> 3*
top0(5) -> 8*
top0(2) -> 8*
top0(9) -> 8*
top0(4) -> 8*
top0(11) -> 8*
top0(6) -> 8*
top0(1) -> 8*
top0(3) -> 8*
ok0(7) -> 7*
ok0(2) -> 11*,5,4
ok0(9) -> 4*
ok0(4) -> 4*
ok0(11) -> 4*
ok0(1) -> 4*
ok0(3) -> 11*,5,4
problem:
strict:
weak:
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
Qed
strict:
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
weak:
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {16,14,12,8,7,6,5}
transitions:
active0(2) -> 6*
active0(14) -> 6*
active0(4) -> 6*
active0(16) -> 6*
active0(1) -> 6*
active0(3) -> 6*
f0(3,4,2) -> 5*
f0(16,3,16) -> 5*
f0(14,14,3) -> 5*
f0(1,3,16) -> 5*
f0(16,1,4) -> 5*
f0(3,14,14) -> 5*
f0(14,16,3) -> 5*
f0(4,14,3) -> 5*
f0(3,1,16) -> 5*
f0(16,3,4) -> 5*
f0(3,16,14) -> 5*
f0(4,16,3) -> 5*
f0(1,1,4) -> 5*
f0(14,1,14) -> 5*
f0(1,3,4) -> 5*
f0(3,14,2) -> 5*
f0(14,3,14) -> 5*
f0(4,1,14) -> 5*
f0(3,16,2) -> 5*
f0(4,3,14) -> 5*
f0(16,1,1) -> 5*
f0(14,1,2) -> 5*
f0(16,3,1) -> 5*
f0(14,3,2) -> 5*
f0(4,1,2) -> 5*
f0(1,1,1) -> 5*
f0(4,3,2) -> 5*
f0(1,3,1) -> 5*
f0(2,2,16) -> 5*
f0(2,4,16) -> 5*
f0(2,2,4) -> 5*
f0(2,4,4) -> 5*
f0(16,2,3) -> 5*
f0(16,4,3) -> 5*
f0(1,2,3) -> 5*
f0(2,14,16) -> 5*
f0(1,4,3) -> 5*
f0(2,16,16) -> 5*
f0(2,2,1) -> 5*
f0(2,14,4) -> 5*
f0(2,4,1) -> 5*
f0(2,16,4) -> 5*
f0(16,14,3) -> 5*
f0(3,3,16) -> 5*
f0(16,16,3) -> 5*
f0(1,14,3) -> 5*
f0(3,1,4) -> 5*
f0(1,16,3) -> 5*
f0(16,1,14) -> 5*
f0(3,3,4) -> 5*
f0(2,14,1) -> 5*
f0(16,3,14) -> 5*
f0(1,1,14) -> 5*
f0(2,1,3) -> 5*
f0(2,16,1) -> 5*
f0(1,3,14) -> 5*
f0(2,3,3) -> 5*
f0(16,1,2) -> 5*
f0(16,3,2) -> 5*
f0(3,1,1) -> 5*
f0(1,1,2) -> 5*
f0(3,3,1) -> 5*
f0(1,3,2) -> 5*
f0(14,2,16) -> 5*
f0(4,2,16) -> 5*
f0(14,4,16) -> 5*
f0(4,4,16) -> 5*
f0(14,2,4) -> 5*
f0(14,4,4) -> 5*
f0(4,2,4) -> 5*
f0(4,4,4) -> 5*
f0(14,14,16) -> 5*
f0(2,2,14) -> 5*
f0(3,2,3) -> 5*
f0(14,16,16) -> 5*
f0(4,14,16) -> 5*
f0(2,4,14) -> 5*
f0(3,4,3) -> 5*
f0(14,2,1) -> 5*
f0(4,16,16) -> 5*
f0(14,14,4) -> 5*
f0(14,4,1) -> 5*
f0(4,2,1) -> 5*
f0(2,2,2) -> 5*
f0(14,16,4) -> 5*
f0(4,14,4) -> 5*
f0(4,4,1) -> 5*
f0(2,4,2) -> 5*
f0(4,16,4) -> 5*
f0(2,14,14) -> 5*
f0(3,14,3) -> 5*
f0(2,1,16) -> 5*
f0(2,16,14) -> 5*
f0(3,16,3) -> 5*
f0(14,14,1) -> 5*
f0(14,1,3) -> 5*
f0(14,16,1) -> 5*
f0(4,14,1) -> 5*
f0(2,14,2) -> 5*
f0(3,1,14) -> 5*
f0(14,3,3) -> 5*
f0(4,1,3) -> 5*
f0(4,16,1) -> 5*
f0(2,16,2) -> 5*
f0(3,3,14) -> 5*
f0(4,3,3) -> 5*
f0(3,1,2) -> 5*
f0(3,3,2) -> 5*
f0(16,2,16) -> 5*
f0(16,4,16) -> 5*
f0(1,2,16) -> 5*
f0(1,4,16) -> 5*
f0(16,2,4) -> 5*
f0(16,4,4) -> 5*
f0(1,2,4) -> 5*
f0(14,2,14) -> 5*
f0(1,4,4) -> 5*
f0(16,14,16) -> 5*
f0(4,2,14) -> 5*
f0(14,4,14) -> 5*
f0(16,16,16) -> 5*
f0(4,4,14) -> 5*
f0(1,14,16) -> 5*
f0(16,2,1) -> 5*
f0(14,2,2) -> 5*
f0(1,16,16) -> 5*
f0(16,14,4) -> 5*
f0(16,4,1) -> 5*
f0(14,4,2) -> 5*
f0(4,2,2) -> 5*
f0(1,2,1) -> 5*
f0(16,16,4) -> 5*
f0(4,4,2) -> 5*
f0(1,14,4) -> 5*
f0(1,4,1) -> 5*
f0(14,14,14) -> 5*
f0(1,16,4) -> 5*
f0(2,3,16) -> 5*
f0(14,16,14) -> 5*
f0(4,14,14) -> 5*
f0(4,16,14) -> 5*
f0(2,1,4) -> 5*
f0(16,14,1) -> 5*
f0(14,14,2) -> 5*
f0(2,3,4) -> 5*
f0(16,1,3) -> 5*
f0(16,16,1) -> 5*
f0(14,16,2) -> 5*
f0(4,14,2) -> 5*
f0(1,14,1) -> 5*
f0(16,3,3) -> 5*
f0(4,16,2) -> 5*
f0(1,1,3) -> 5*
f0(1,16,1) -> 5*
f0(1,3,3) -> 5*
f0(2,1,1) -> 5*
f0(2,3,1) -> 5*
f0(3,2,16) -> 5*
f0(3,4,16) -> 5*
f0(3,2,4) -> 5*
f0(16,2,14) -> 5*
f0(3,4,4) -> 5*
f0(16,4,14) -> 5*
f0(1,2,14) -> 5*
f0(2,2,3) -> 5*
f0(3,14,16) -> 5*
f0(1,4,14) -> 5*
f0(2,4,3) -> 5*
f0(16,2,2) -> 5*
f0(3,16,16) -> 5*
f0(16,4,2) -> 5*
f0(3,2,1) -> 5*
f0(1,2,2) -> 5*
f0(14,1,16) -> 5*
f0(3,14,4) -> 5*
f0(3,4,1) -> 5*
f0(1,4,2) -> 5*
f0(14,3,16) -> 5*
f0(4,1,16) -> 5*
f0(16,14,14) -> 5*
f0(3,16,4) -> 5*
f0(4,3,16) -> 5*
f0(16,16,14) -> 5*
f0(14,1,4) -> 5*
f0(1,14,14) -> 5*
f0(2,14,3) -> 5*
f0(1,1,16) -> 5*
f0(1,16,14) -> 5*
f0(14,3,4) -> 5*
f0(4,1,4) -> 5*
f0(2,16,3) -> 5*
f0(16,14,2) -> 5*
f0(4,3,4) -> 5*
f0(16,16,2) -> 5*
f0(3,14,1) -> 5*
f0(1,14,2) -> 5*
f0(2,1,14) -> 5*
f0(3,1,3) -> 5*
f0(3,16,1) -> 5*
f0(1,16,2) -> 5*
f0(2,3,14) -> 5*
f0(3,3,3) -> 5*
f0(14,1,1) -> 5*
f0(14,3,1) -> 5*
f0(4,1,1) -> 5*
f0(2,1,2) -> 5*
f0(4,3,1) -> 5*
f0(2,3,2) -> 5*
f0(14,2,3) -> 5*
f0(3,2,14) -> 5*
f0(14,4,3) -> 5*
f0(4,2,3) -> 5*
f0(3,4,14) -> 5*
f0(4,4,3) -> 5*
f0(3,2,2) -> 5*
f0(16,1,16) -> 5*
proper0(2) -> 8*
proper0(14) -> 8*
proper0(4) -> 8*
proper0(16) -> 8*
proper0(1) -> 8*
proper0(3) -> 8*
mark0(2) -> 14*,6,1
mark0(14) -> 1*
mark0(4) -> 1*
mark0(16) -> 1*
mark0(1) -> 1*
mark0(3) -> 1*
a0() -> 2*
b0() -> 3*
top0(2) -> 7*
top0(14) -> 7*
top0(4) -> 7*
top0(16) -> 7*
top0(6) -> 7*
top0(1) -> 7*
top0(8) -> 7*
top0(3) -> 7*
ok0(5) -> 5*
ok0(12) -> 5*
ok0(2) -> 16*,8,4
ok0(14) -> 4*
ok0(4) -> 4*
ok0(16) -> 4*
ok0(1) -> 4*
ok0(3) -> 16*,8,4
mark1(10) -> 5*
mark1(5) -> 12*
mark1(12) -> 12*,5
f1(3,2,2) -> 12*,5,10
f1(16,1,16) -> 5,12*
f1(3,4,2) -> 12*,5,10
f1(16,3,16) -> 5,12*
f1(14,14,3) -> 5,12*
f1(1,3,16) -> 5,12*
f1(16,1,4) -> 5,12*
f1(3,14,14) -> 5,12*
f1(14,16,3) -> 5,12*
f1(4,14,3) -> 5,12*
f1(3,1,16) -> 5,12*
f1(16,3,4) -> 5,12*
f1(3,16,14) -> 5,12*
f1(4,16,3) -> 5,12*
f1(1,1,4) -> 12*,5,10
f1(14,1,14) -> 5,12*
f1(1,3,4) -> 12*,5,10
f1(3,14,2) -> 5,12*
f1(14,3,14) -> 5,12*
f1(4,1,14) -> 5,12*
f1(3,16,2) -> 5,12*
f1(4,3,14) -> 5,12*
f1(16,1,1) -> 5,12*
f1(14,1,2) -> 5,12*
f1(16,3,1) -> 5,12*
f1(14,3,2) -> 5,12*
f1(4,1,2) -> 12*,5,10
f1(1,1,1) -> 12*,5,10
f1(4,3,2) -> 12*,5,10
f1(1,3,1) -> 12*,5,10
f1(2,2,16) -> 5,12*
f1(2,4,16) -> 5,12*
f1(2,2,4) -> 12*,5,10
f1(2,4,4) -> 12*,5,10
f1(16,2,3) -> 5,12*
f1(16,4,3) -> 5,12*
f1(1,2,3) -> 12*,5,10
f1(2,14,16) -> 5,12*
f1(1,4,3) -> 12*,5,10
f1(2,16,16) -> 5,12*
f1(2,2,1) -> 12*,5,10
f1(2,14,4) -> 5,12*
f1(2,4,1) -> 12*,5,10
f1(2,16,4) -> 5,12*
f1(16,14,3) -> 5,12*
f1(3,3,16) -> 5,12*
f1(16,16,3) -> 5,12*
f1(1,14,3) -> 5,12*
f1(3,1,4) -> 12*,5,10
f1(1,16,3) -> 5,12*
f1(16,1,14) -> 5,12*
f1(3,3,4) -> 12*,5,10
f1(2,14,1) -> 5,12*
f1(16,3,14) -> 5,12*
f1(1,1,14) -> 5,12*
f1(2,1,3) -> 12*,5,10
f1(2,16,1) -> 5,12*
f1(1,3,14) -> 5,12*
f1(2,3,3) -> 12*,5,10
f1(16,1,2) -> 5,12*
f1(16,3,2) -> 5,12*
f1(3,1,1) -> 12*,5,10
f1(1,1,2) -> 12*,5,10
f1(3,3,1) -> 12*,5,10
f1(1,3,2) -> 12*,5,10
f1(14,2,16) -> 5,12*
f1(4,2,16) -> 5,12*
f1(14,4,16) -> 5,12*
f1(4,4,16) -> 5,12*
f1(14,2,4) -> 5,12*
f1(14,4,4) -> 5,12*
f1(4,2,4) -> 12*,5,10
f1(4,4,4) -> 12*,5,10
f1(14,14,16) -> 5,12*
f1(2,2,14) -> 5,12*
f1(3,2,3) -> 12*,5,10
f1(14,16,16) -> 5,12*
f1(4,14,16) -> 5,12*
f1(2,4,14) -> 5,12*
f1(3,4,3) -> 12*,5,10
f1(14,2,1) -> 5,12*
f1(4,16,16) -> 5,12*
f1(14,14,4) -> 5,12*
f1(14,4,1) -> 5,12*
f1(4,2,1) -> 12*,5,10
f1(2,2,2) -> 12*,5,10
f1(14,16,4) -> 5,12*
f1(4,14,4) -> 5,12*
f1(4,4,1) -> 12*,5,10
f1(2,4,2) -> 12*,5,10
f1(4,16,4) -> 5,12*
f1(2,14,14) -> 5,12*
f1(3,14,3) -> 5,12*
f1(2,1,16) -> 5,12*
f1(2,16,14) -> 5,12*
f1(3,16,3) -> 5,12*
f1(14,14,1) -> 5,12*
f1(14,1,3) -> 5,12*
f1(14,16,1) -> 5,12*
f1(4,14,1) -> 5,12*
f1(2,14,2) -> 5,12*
f1(3,1,14) -> 5,12*
f1(14,3,3) -> 5,12*
f1(4,1,3) -> 12*,5,10
f1(4,16,1) -> 5,12*
f1(2,16,2) -> 5,12*
f1(3,3,14) -> 5,12*
f1(4,3,3) -> 12*,5,10
f1(3,1,2) -> 12*,5,10
f1(3,3,2) -> 12*,5,10
f1(16,2,16) -> 5,12*
f1(16,4,16) -> 5,12*
f1(1,2,16) -> 5,12*
f1(1,4,16) -> 5,12*
f1(16,2,4) -> 5,12*
f1(16,4,4) -> 5,12*
f1(1,2,4) -> 12*,5,10
f1(14,2,14) -> 5,12*
f1(1,4,4) -> 12*,5,10
f1(16,14,16) -> 5,12*
f1(4,2,14) -> 5,12*
f1(14,4,14) -> 5,12*
f1(16,16,16) -> 5,12*
f1(4,4,14) -> 5,12*
f1(1,14,16) -> 5,12*
f1(16,2,1) -> 5,12*
f1(14,2,2) -> 5,12*
f1(1,16,16) -> 5,12*
f1(16,14,4) -> 5,12*
f1(16,4,1) -> 5,12*
f1(14,4,2) -> 5,12*
f1(4,2,2) -> 12*,5,10
f1(1,2,1) -> 12*,5,10
f1(16,16,4) -> 5,12*
f1(4,4,2) -> 12*,5,10
f1(1,14,4) -> 5,12*
f1(1,4,1) -> 12*,5,10
f1(14,14,14) -> 5,12*
f1(1,16,4) -> 5,12*
f1(2,3,16) -> 5,12*
f1(14,16,14) -> 5,12*
f1(4,14,14) -> 5,12*
f1(4,16,14) -> 5,12*
f1(2,1,4) -> 12*,5,10
f1(16,14,1) -> 5,12*
f1(14,14,2) -> 5,12*
f1(2,3,4) -> 12*,5,10
f1(16,1,3) -> 5,12*
f1(16,16,1) -> 5,12*
f1(14,16,2) -> 5,12*
f1(4,14,2) -> 5,12*
f1(1,14,1) -> 5,12*
f1(16,3,3) -> 5,12*
f1(4,16,2) -> 5,12*
f1(1,1,3) -> 12*,5,10
f1(1,16,1) -> 5,12*
f1(1,3,3) -> 12*,5,10
f1(2,1,1) -> 12*,5,10
f1(2,3,1) -> 12*,5,10
f1(3,2,16) -> 5,12*
f1(3,4,16) -> 5,12*
f1(3,2,4) -> 12*,5,10
f1(16,2,14) -> 5,12*
f1(3,4,4) -> 12*,5,10
f1(16,4,14) -> 5,12*
f1(1,2,14) -> 5,12*
f1(2,2,3) -> 12*,5,10
f1(3,14,16) -> 5,12*
f1(1,4,14) -> 5,12*
f1(2,4,3) -> 12*,5,10
f1(16,2,2) -> 5,12*
f1(3,16,16) -> 5,12*
f1(16,4,2) -> 5,12*
f1(3,2,1) -> 12*,5,10
f1(1,2,2) -> 12*,5,10
f1(14,1,16) -> 5,12*
f1(3,14,4) -> 5,12*
f1(3,4,1) -> 12*,5,10
f1(1,4,2) -> 12*,5,10
f1(14,3,16) -> 5,12*
f1(4,1,16) -> 5,12*
f1(16,14,14) -> 5,12*
f1(3,16,4) -> 5,12*
f1(4,3,16) -> 5,12*
f1(16,16,14) -> 5,12*
f1(14,1,4) -> 5,12*
f1(1,14,14) -> 5,12*
f1(2,14,3) -> 5,12*
f1(1,1,16) -> 5,12*
f1(1,16,14) -> 5,12*
f1(14,3,4) -> 5,12*
f1(4,1,4) -> 12*,5,10
f1(2,16,3) -> 5,12*
f1(16,14,2) -> 5,12*
f1(4,3,4) -> 12*,5,10
f1(16,16,2) -> 5,12*
f1(3,14,1) -> 5,12*
f1(1,14,2) -> 5,12*
f1(2,1,14) -> 5,12*
f1(3,1,3) -> 12*,5,10
f1(3,16,1) -> 5,12*
f1(1,16,2) -> 5,12*
f1(2,3,14) -> 5,12*
f1(3,3,3) -> 12*,5,10
f1(14,1,1) -> 5,12*
f1(14,3,1) -> 5,12*
f1(4,1,1) -> 12*,5,10
f1(2,1,2) -> 12*,5,10
f1(4,3,1) -> 12*,5,10
f1(2,3,2) -> 12*,5,10
f1(14,2,3) -> 5,12*
f1(3,2,14) -> 5,12*
f1(14,4,3) -> 5,12*
f1(4,2,3) -> 12*,5,10
f1(3,4,14) -> 5,12*
f1(4,4,3) -> 12*,5,10
ok1(5) -> 5,12*
ok1(12) -> 5,12*
problem:
strict:
weak:
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
Qed
strict:
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
weak:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
Matrix Interpretation Processor:
dimension: 4
max_matrix:
[1 1 1 0]
[0 0 1 0]
[0 0 0 1]
[0 0 0 0]
interpretation:
[1 0 0 0]
[0 0 1 0]
[top](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 1 0 0]
[0 0 1 0]
[ok](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 0 0]
[0 0 1 0]
[proper](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 0 0 0]
[0 0 0 0]
[mark](x0) = [0 0 0 1]x0
[0 0 0 0] ,
[0]
[0]
[b] = [0]
[0],
[1 0 0 0]
[0 0 0 0]
[active](x0) = [0 0 0 0]x0
[0 0 0 0] ,
[1 1 1 0] [1 0 0 0] [1 1 1 0]
[0 0 0 0] [0 0 0 0] [0 0 0 0]
[f](x0, x1, x2) = [0 0 0 0]x0 + [0 0 0 0]x1 + [0 0 0 0]x2
[0 0 0 0] [0 0 0 0] [0 0 0 0] ,
[0]
[0]
[a] = [1]
[0]
orientation:
[2 1 1 0] [1] [1 1 1 0]
[0 0 0 0] [0] [0 0 0 0]
active(f(a(),X,X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X = mark(f(X,b(),b()))
[0 0 0 0] [0] [0 0 0 0]
[0] [0]
[0] [0]
active(b()) = [0] >= [0] = mark(a())
[0] [0]
[1 0 0 0] [1 0 0 0]
[0 0 0 1] [0 0 0 0]
top(mark(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(proper(X))
[0 0 0 0] [0 0 0 0]
[0] [0]
[1] [1]
proper(a()) = [0] >= [0] = ok(a())
[0] [0]
[0] [0]
[0] [0]
proper(b()) = [0] >= [0] = ok(b())
[0] [0]
[1 1 1 0] [1 1 0 0] [1 1 1 0] [1 1 1 0] [1 0 0 0] [1 1 1 0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
f(ok(X1),ok(X2),ok(X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = ok(f(X1,X2,X3))
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
[1 1 0 0] [1 0 0 0]
[0 0 0 0] [0 0 0 0]
top(ok(X)) = [0 0 0 0]X >= [0 0 0 0]X = top(active(X))
[0 0 0 0] [0 0 0 0]
[1 1 1 0] [1 0 0 0] [1 1 1 0] [1 1 1 0] [1 0 0 0] [1 1 1 0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
active(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = f(X1,active(X2),X3)
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
[1 1 1 0] [1 0 0 0] [1 1 1 0] [1 1 1 0] [1 0 0 0] [1 1 1 0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
f(X1,mark(X2),X3) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = mark(f(X1,X2,X3))
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
[1 1 1 0] [1 0 0 0] [1 1 1 0] [1 0 1 0] [1 0 0 0] [1 0 1 0]
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
proper(f(X1,X2,X3)) = [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 >= [0 0 0 0]X1 + [0 0 0 0]X2 + [0 0 0 0]X3 = f(proper(X1),proper(X2),proper(X3))
[0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0 0 0 0]
problem:
strict:
weak:
active(f(a(),X,X)) -> mark(f(X,b(),b()))
active(b()) -> mark(a())
top(mark(X)) -> top(proper(X))
proper(a()) -> ok(a())
proper(b()) -> ok(b())
f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3))
top(ok(X)) -> top(active(X))
active(f(X1,X2,X3)) -> f(X1,active(X2),X3)
f(X1,mark(X2),X3) -> mark(f(X1,X2,X3))
proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3))
Qed