MAYBE
Time: 0.226913
TRS:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
DP:
DP:
{min#(s x, s y) -> min#(x, y),
max#(s x, s y) -> max#(x, y),
+#(s x, y) -> +#(x, y),
-#(s x, s y) -> -#(x, y),
*#(x, s y) -> +#(x, *(x, y)),
*#(x, s y) -> *#(x, y),
f#(s x, s y) -> min#(s x, s y),
f#(s x, s y) -> max#(s x, s y),
f#(s x, s y) -> -#(min(s x, s y), max(s x, s y)),
f#(s x, s y) -> *#(s x, s y),
f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
TRS:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
UR:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
a(z, w) -> z,
a(z, w) -> w}
EDG:
{(f#(s x, s y) -> max#(s x, s y), max#(s x, s y) -> max#(x, y))
(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y))
(f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y)), f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y)))
(f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y)), f#(s x, s y) -> *#(s x, s y))
(f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y)), f#(s x, s y) -> -#(min(s x, s y), max(s x, s y)))
(f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y)), f#(s x, s y) -> max#(s x, s y))
(f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y)), f#(s x, s y) -> min#(s x, s y))
(max#(s x, s y) -> max#(x, y), max#(s x, s y) -> max#(x, y))
(-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
(*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(x, *(x, y)))
(*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y))
(+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
(min#(s x, s y) -> min#(x, y), min#(s x, s y) -> min#(x, y))
(f#(s x, s y) -> -#(min(s x, s y), max(s x, s y)), -#(s x, s y) -> -#(x, y))
(f#(s x, s y) -> *#(s x, s y), *#(x, s y) -> +#(x, *(x, y)))
(f#(s x, s y) -> *#(s x, s y), *#(x, s y) -> *#(x, y))
(f#(s x, s y) -> min#(s x, s y), min#(s x, s y) -> min#(x, y))}
STATUS:
arrows: 0.859504
SCCS (6):
Scc:
{f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
Scc:
{-#(s x, s y) -> -#(x, y)}
Scc:
{*#(x, s y) -> *#(x, y)}
Scc:
{+#(s x, y) -> +#(x, y)}
Scc:
{max#(s x, s y) -> max#(x, y)}
Scc:
{min#(s x, s y) -> min#(x, y)}
SCC (1):
Strict:
{f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
Weak:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
Fail
SCC (1):
Strict:
{-#(s x, s y) -> -#(x, y)}
Weak:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[min](x0, x1) = x0 + x1 + 1,
[max](x0, x1) = x0 + x1 + 1,
[+](x0, x1) = x0 + 1,
[-](x0, x1) = x0 + 1,
[*](x0, x1) = x0 + 1,
[f](x0, x1) = x0,
[s](x0) = x0 + 1,
[p](x0) = x0 + 1,
[0] = 1,
[-#](x0, x1) = x0 + 1
Strict:
-#(s x, s y) -> -#(x, y)
2 + 0y + 1x >= 1 + 0y + 1x
Weak:
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))
1 + 0y + 1x >= 4 + 1y + 1x
p s x -> x
2 + 1x >= 1x
*(x, s y) -> +(x, *(x, y))
2 + 1y + 0x >= 1 + 0y + 1x
*(x, 0()) -> 0()
2 + 0x >= 1
-(s x, s y) -> -(x, y)
2 + 1y + 0x >= 1 + 1y + 0x
-(x, 0()) -> x
2 + 0x >= 1x
+(s x, y) -> s +(x, y)
2 + 0y + 1x >= 2 + 0y + 1x
+(0(), y) -> y
2 + 0y >= 1y
max(s x, s y) -> s max(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
max(0(), y) -> y
2 + 1y >= 1y
max(x, 0()) -> x
2 + 1x >= 1x
min(s x, s y) -> s min(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
min(0(), y) -> 0()
2 + 1y >= 1
min(x, 0()) -> 0()
2 + 1x >= 1
Qed
SCC (1):
Strict:
{*#(x, s y) -> *#(x, y)}
Weak:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[min](x0, x1) = x0 + x1 + 1,
[max](x0, x1) = x0 + x1 + 1,
[+](x0, x1) = x0 + 1,
[-](x0, x1) = x0 + 1,
[*](x0, x1) = x0 + x1 + 1,
[f](x0, x1) = x0 + 1,
[s](x0) = x0 + 1,
[p](x0) = x0 + 1,
[0] = 1,
[*#](x0, x1) = x0 + 1
Strict:
*#(x, s y) -> *#(x, y)
2 + 1y + 0x >= 1 + 1y + 0x
Weak:
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))
2 + 0y + 1x >= 5 + 1y + 1x
p s x -> x
2 + 1x >= 1x
*(x, s y) -> +(x, *(x, y))
2 + 1y + 1x >= 1 + 0y + 1x
*(x, 0()) -> 0()
2 + 1x >= 1
-(s x, s y) -> -(x, y)
2 + 1y + 0x >= 1 + 1y + 0x
-(x, 0()) -> x
2 + 0x >= 1x
+(s x, y) -> s +(x, y)
2 + 0y + 1x >= 2 + 0y + 1x
+(0(), y) -> y
2 + 0y >= 1y
max(s x, s y) -> s max(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
max(0(), y) -> y
2 + 1y >= 1y
max(x, 0()) -> x
2 + 1x >= 1x
min(s x, s y) -> s min(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
min(0(), y) -> 0()
2 + 1y >= 1
min(x, 0()) -> 0()
2 + 1x >= 1
Qed
SCC (1):
Strict:
{+#(s x, y) -> +#(x, y)}
Weak:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[min](x0, x1) = x0 + x1 + 1,
[max](x0, x1) = x0 + x1 + 1,
[+](x0, x1) = x0 + 1,
[-](x0, x1) = x0 + 1,
[*](x0, x1) = x0 + x1 + 1,
[f](x0, x1) = x0 + 1,
[s](x0) = x0 + 1,
[p](x0) = x0 + 1,
[0] = 1,
[+#](x0, x1) = x0 + 1
Strict:
+#(s x, y) -> +#(x, y)
2 + 0y + 1x >= 1 + 0y + 1x
Weak:
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))
2 + 0y + 1x >= 5 + 1y + 1x
p s x -> x
2 + 1x >= 1x
*(x, s y) -> +(x, *(x, y))
2 + 1y + 1x >= 1 + 0y + 1x
*(x, 0()) -> 0()
2 + 1x >= 1
-(s x, s y) -> -(x, y)
2 + 1y + 0x >= 1 + 1y + 0x
-(x, 0()) -> x
2 + 0x >= 1x
+(s x, y) -> s +(x, y)
2 + 0y + 1x >= 2 + 0y + 1x
+(0(), y) -> y
2 + 0y >= 1y
max(s x, s y) -> s max(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
max(0(), y) -> y
2 + 1y >= 1y
max(x, 0()) -> x
2 + 1x >= 1x
min(s x, s y) -> s min(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
min(0(), y) -> 0()
2 + 1y >= 1
min(x, 0()) -> 0()
2 + 1x >= 1
Qed
SCC (1):
Strict:
{max#(s x, s y) -> max#(x, y)}
Weak:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[min](x0, x1) = x0 + x1 + 1,
[max](x0, x1) = x0 + x1 + 1,
[+](x0, x1) = x0 + 1,
[-](x0, x1) = x0 + 1,
[*](x0, x1) = x0 + 1,
[f](x0, x1) = x0,
[s](x0) = x0 + 1,
[p](x0) = x0 + 1,
[0] = 1,
[max#](x0, x1) = x0 + 1
Strict:
max#(s x, s y) -> max#(x, y)
2 + 0y + 1x >= 1 + 0y + 1x
Weak:
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))
1 + 0y + 1x >= 4 + 1y + 1x
p s x -> x
2 + 1x >= 1x
*(x, s y) -> +(x, *(x, y))
2 + 1y + 0x >= 1 + 0y + 1x
*(x, 0()) -> 0()
2 + 0x >= 1
-(s x, s y) -> -(x, y)
2 + 1y + 0x >= 1 + 1y + 0x
-(x, 0()) -> x
2 + 0x >= 1x
+(s x, y) -> s +(x, y)
2 + 0y + 1x >= 2 + 0y + 1x
+(0(), y) -> y
2 + 0y >= 1y
max(s x, s y) -> s max(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
max(0(), y) -> y
2 + 1y >= 1y
max(x, 0()) -> x
2 + 1x >= 1x
min(s x, s y) -> s min(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
min(0(), y) -> 0()
2 + 1y >= 1
min(x, 0()) -> 0()
2 + 1x >= 1
Qed
SCC (1):
Strict:
{min#(s x, s y) -> min#(x, y)}
Weak:
{ min(x, 0()) -> 0(),
min(0(), y) -> 0(),
min(s x, s y) -> s min(x, y),
max(x, 0()) -> x,
max(0(), y) -> y,
max(s x, s y) -> s max(x, y),
+(0(), y) -> y,
+(s x, y) -> s +(x, y),
-(x, 0()) -> x,
-(s x, s y) -> -(x, y),
*(x, 0()) -> 0(),
*(x, s y) -> +(x, *(x, y)),
p s x -> x,
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[min](x0, x1) = x0 + x1 + 1,
[max](x0, x1) = x0 + x1 + 1,
[+](x0, x1) = x0 + 1,
[-](x0, x1) = x0 + 1,
[*](x0, x1) = x0 + 1,
[f](x0, x1) = x0,
[s](x0) = x0 + 1,
[p](x0) = x0 + 1,
[0] = 1,
[min#](x0, x1) = x0 + 1
Strict:
min#(s x, s y) -> min#(x, y)
2 + 0y + 1x >= 1 + 0y + 1x
Weak:
f(s x, s y) -> f(-(min(s x, s y), max(s x, s y)), *(s x, s y))
1 + 0y + 1x >= 4 + 1y + 1x
p s x -> x
2 + 1x >= 1x
*(x, s y) -> +(x, *(x, y))
2 + 1y + 0x >= 1 + 0y + 1x
*(x, 0()) -> 0()
2 + 0x >= 1
-(s x, s y) -> -(x, y)
2 + 1y + 0x >= 1 + 1y + 0x
-(x, 0()) -> x
2 + 0x >= 1x
+(s x, y) -> s +(x, y)
2 + 0y + 1x >= 2 + 0y + 1x
+(0(), y) -> y
2 + 0y >= 1y
max(s x, s y) -> s max(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
max(0(), y) -> y
2 + 1y >= 1y
max(x, 0()) -> x
2 + 1x >= 1x
min(s x, s y) -> s min(x, y)
3 + 1y + 1x >= 2 + 1y + 1x
min(0(), y) -> 0()
2 + 1y >= 1
min(x, 0()) -> 0()
2 + 1x >= 1
Qed