We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, zero(0()) -> true()
, zero(s(x)) -> false()
, conv(x) -> conviter(x, cons(0(), nil()))
, conviter(x, l) -> if(zero(x), x, l)
, if(true(), x, l) -> l
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, zero(0()) -> true()
, zero(s(x)) -> false()
, conv(x) -> conviter(x, cons(0(), nil()))
, conviter(x, l) -> if(zero(x), x, l)
, if(true(), x, l) -> l
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(zero) = {}, Uargs(conv) = {}, Uargs(conviter) = {1, 2},
Uargs(cons) = {1}, Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [1]
[0 0] [1]
0() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
lastbit(x1) = [0 0] x1 + [1]
[0 0] [1]
zero(x1) = [0 0] x1 + [1]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
conv(x1) = [1 1] x1 + [0]
[0 0] [0]
conviter(x1, x2) = [1 1] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
nil() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [0 0] x3 + [0]
[0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ half(s(s(x))) -> s(half(x))
, lastbit(s(s(x))) -> lastbit(x)
, conv(x) -> conviter(x, cons(0(), nil()))
, conviter(x, l) -> if(zero(x), x, l)
, if(true(), x, l) -> l
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))}
Weak Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {conv(x) -> conviter(x, cons(0(), nil()))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(zero) = {}, Uargs(conv) = {}, Uargs(conviter) = {1, 2},
Uargs(cons) = {1}, Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [1]
[0 0] [1]
0() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
lastbit(x1) = [0 0] x1 + [1]
[0 0] [1]
zero(x1) = [0 0] x1 + [0]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
conv(x1) = [1 1] x1 + [2]
[0 0] [2]
conviter(x1, x2) = [1 1] x1 + [1 0] x2 + [1]
[0 0] [0 0] [1]
cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
nil() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [0 0] x3 + [1]
[0 0] [0 0] [0 0] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ half(s(s(x))) -> s(half(x))
, lastbit(s(s(x))) -> lastbit(x)
, conviter(x, l) -> if(zero(x), x, l)
, if(true(), x, l) -> l
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))}
Weak Trs:
{ conv(x) -> conviter(x, cons(0(), nil()))
, half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {if(true(), x, l) -> l}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(zero) = {}, Uargs(conv) = {}, Uargs(conviter) = {1, 2},
Uargs(cons) = {1}, Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [1]
[0 0] [1]
0() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [1]
lastbit(x1) = [0 0] x1 + [1]
[0 0] [1]
zero(x1) = [0 0] x1 + [0]
[0 0] [1]
true() = [0]
[0]
false() = [0]
[0]
conv(x1) = [1 1] x1 + [0]
[0 0] [2]
conviter(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 1] [0 0] [0]
nil() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 1] x2 + [1 0] x3 + [1]
[0 0] [0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ half(s(s(x))) -> s(half(x))
, lastbit(s(s(x))) -> lastbit(x)
, conviter(x, l) -> if(zero(x), x, l)
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))}
Weak Trs:
{ if(true(), x, l) -> l
, conv(x) -> conviter(x, cons(0(), nil()))
, half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(zero) = {}, Uargs(conv) = {}, Uargs(conviter) = {1, 2},
Uargs(cons) = {1}, Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [3]
[0 0] [0]
0() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
lastbit(x1) = [0 0] x1 + [0]
[0 0] [1]
zero(x1) = [0 0] x1 + [3]
[0 0] [1]
true() = [0]
[0]
false() = [3]
[0]
conv(x1) = [1 0] x1 + [2]
[0 1] [2]
conviter(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 0] [0 0] [1]
cons(x1, x2) = [1 0] x1 + [0 0] x2 + [2]
[0 0] [0 0] [0]
nil() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [3]
[0 0] [0 1] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ half(s(s(x))) -> s(half(x))
, lastbit(s(s(x))) -> lastbit(x)
, conviter(x, l) -> if(zero(x), x, l)}
Weak Trs:
{ if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))
, if(true(), x, l) -> l
, conv(x) -> conviter(x, cons(0(), nil()))
, half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {lastbit(s(s(x))) -> lastbit(x)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(zero) = {}, Uargs(conv) = {}, Uargs(conviter) = {1, 2},
Uargs(cons) = {1}, Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [1 0] x1 + [3]
[0 0] [2]
lastbit(x1) = [1 0] x1 + [1]
[0 0] [3]
zero(x1) = [0 1] x1 + [2]
[0 0] [3]
true() = [0]
[0]
false() = [2]
[3]
conv(x1) = [1 2] x1 + [3]
[0 0] [0]
conviter(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
[0 0] [0 1] [0]
cons(x1, x2) = [1 0] x1 + [0 0] x2 + [3]
[0 0] [0 0] [0]
nil() = [0]
[0]
if(x1, x2, x3) = [1 2] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 1] [0 1] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ half(s(s(x))) -> s(half(x))
, conviter(x, l) -> if(zero(x), x, l)}
Weak Trs:
{ lastbit(s(s(x))) -> lastbit(x)
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))
, if(true(), x, l) -> l
, conv(x) -> conviter(x, cons(0(), nil()))
, half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {conviter(x, l) -> if(zero(x), x, l)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(zero) = {}, Uargs(conv) = {}, Uargs(conviter) = {1, 2},
Uargs(cons) = {1}, Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [2]
lastbit(x1) = [0 0] x1 + [0]
[0 0] [3]
zero(x1) = [0 2] x1 + [0]
[0 1] [2]
true() = [0]
[0]
false() = [1]
[0]
conv(x1) = [1 2] x1 + [1]
[0 0] [2]
conviter(x1, x2) = [1 2] x1 + [1 0] x2 + [1]
[0 0] [0 1] [1]
cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
nil() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [0]
[0 0] [0 0] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs: {half(s(s(x))) -> s(half(x))}
Weak Trs:
{ conviter(x, l) -> if(zero(x), x, l)
, lastbit(s(s(x))) -> lastbit(x)
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))
, if(true(), x, l) -> l
, conv(x) -> conviter(x, cons(0(), nil()))
, half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {half(s(s(x))) -> s(half(x))}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(zero) = {}, Uargs(conv) = {}, Uargs(conviter) = {1, 2},
Uargs(cons) = {1}, Uargs(if) = {1}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
half(x1) = [1 0] x1 + [0]
[0 1] [0]
0() = [0]
[0]
s(x1) = [1 1] x1 + [0]
[0 0] [1]
lastbit(x1) = [0 0] x1 + [0]
[0 0] [1]
zero(x1) = [0 0] x1 + [0]
[0 0] [0]
true() = [0]
[0]
false() = [0]
[0]
conv(x1) = [1 0] x1 + [0]
[0 1] [1]
conviter(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
[0 1] [0 1] [1]
cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
[0 0] [0 0] [0]
nil() = [0]
[0]
if(x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 1] [0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Weak Trs:
{ half(s(s(x))) -> s(half(x))
, conviter(x, l) -> if(zero(x), x, l)
, lastbit(s(s(x))) -> lastbit(x)
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))
, if(true(), x, l) -> l
, conv(x) -> conviter(x, cons(0(), nil()))
, half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
We consider the following Problem:
Weak Trs:
{ half(s(s(x))) -> s(half(x))
, conviter(x, l) -> if(zero(x), x, l)
, lastbit(s(s(x))) -> lastbit(x)
, if(false(), x, l) -> conviter(half(x), cons(lastbit(x), l))
, if(true(), x, l) -> l
, conv(x) -> conviter(x, cons(0(), nil()))
, half(0()) -> 0()
, half(s(0())) -> 0()
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, zero(0()) -> true()
, zero(s(x)) -> false()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(O(1),O(1))
Proof:
Empty rules are trivially bounded
Hurray, we answered YES(?,O(n^1))