interpretations
Execution Time (secs) | - |
Answer | YES(?,O(n^1)) |
Input | SK90 2.29 |
YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ prime(0()) -> false()
, prime(s(0())) -> false()
, prime(s(s(x))) -> prime1(s(s(x)), s(x))
, prime1(x, 0()) -> false()
, prime1(x, s(0())) -> true()
, prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y)))
, divp(x, y) -> =(rem(x, y), 0()) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The following argument positions are usable:
Uargs(prime) = {}, Uargs(s) = {}, Uargs(prime1) = {},
Uargs(and) = {1, 2}, Uargs(not) = {1}, Uargs(divp) = {},
Uargs(=) = {}, Uargs(rem) = {}
TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).
[prime](x1) = [2] x1 + [0]
[0] = [2]
[false] = [0]
[s](x1) = [1] x1 + [2]
[prime1](x1, x2) = [2] x2 + [0]
[true] = [0]
[and](x1, x2) = [1] x1 + [1] x2 + [0]
[not](x1) = [1] x1 + [1]
[divp](x1, x2) = [2]
[=](x1, x2) = [1] x1 + [0]
[rem](x1, x2) = [1]
This order satisfies following ordering constraints
[prime(0())] = [4]
> [0]
= [false()]
[prime(s(0()))] = [8]
> [0]
= [false()]
[prime(s(s(x)))] = [2] x + [8]
> [2] x + [4]
= [prime1(s(s(x)), s(x))]
[prime1(x, 0())] = [4]
> [0]
= [false()]
[prime1(x, s(0()))] = [8]
> [0]
= [true()]
[prime1(x, s(s(y)))] = [2] y + [8]
> [2] y + [7]
= [and(not(divp(s(s(y)), x)), prime1(x, s(y)))]
[divp(x, y)] = [2]
> [1]
= [=(rem(x, y), 0())]
Hurray, we answered YES(?,O(n^1))
lmpo
Execution Time (secs) | - |
Answer | YES(?,ELEMENTARY) |
Input | SK90 2.29 |
YES(?,ELEMENTARY)
We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).
Strict Trs:
{ prime(0()) -> false()
, prime(s(0())) -> false()
, prime(s(s(x))) -> prime1(s(s(x)), s(x))
, prime1(x, 0()) -> false()
, prime1(x, s(0())) -> true()
, prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y)))
, divp(x, y) -> =(rem(x, y), 0()) }
Obligation:
innermost runtime complexity
Answer:
YES(?,ELEMENTARY)
The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping
safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
safe(prime1) = {}, safe(true) = {}, safe(and) = {1, 2},
safe(not) = {1}, safe(divp) = {2}, safe(=) = {1, 2},
safe(rem) = {1, 2}
and precedence
prime > prime1, prime1 > divp .
Following symbols are considered recursive:
{prime, prime1}
The recursion depth is 2.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ prime(0();) -> false()
, prime(s(; 0());) -> false()
, prime(s(; s(; x));) -> prime1(s(; s(; x)), s(; x);)
, prime1(x, 0();) -> false()
, prime1(x, s(; 0());) -> true()
, prime1(x, s(; s(; y));) ->
and(; not(; divp(s(; s(; y)); x)), prime1(x, s(; y);))
, divp(x; y) -> =(; rem(; x, y), 0()) }
Weak Trs :
Hurray, we answered YES(?,ELEMENTARY)
mpo
Execution Time (secs) | - |
Answer | YES(?,PRIMREC) |
Input | SK90 2.29 |
YES(?,PRIMREC)
We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).
Strict Trs:
{ prime(0()) -> false()
, prime(s(0())) -> false()
, prime(s(s(x))) -> prime1(s(s(x)), s(x))
, prime1(x, 0()) -> false()
, prime1(x, s(0())) -> true()
, prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y)))
, divp(x, y) -> =(rem(x, y), 0()) }
Obligation:
innermost runtime complexity
Answer:
YES(?,PRIMREC)
The input was oriented with the instance of'multiset path orders'
as induced by the precedence
prime > false, prime > prime1, prime1 > false, prime1 > and,
prime1 > not, prime1 > divp, divp > =, divp > rem, 0 ~ divp,
s ~ true .
Hurray, we answered YES(?,PRIMREC)
popstar
Execution Time (secs) | 0.240 |
Answer | YES(?,POLY) |
Input | SK90 2.29 |
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ prime(0()) -> false()
, prime(s(0())) -> false()
, prime(s(s(x))) -> prime1(s(s(x)), s(x))
, prime1(x, 0()) -> false()
, prime1(x, s(0())) -> true()
, prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y)))
, divp(x, y) -> =(rem(x, y), 0()) }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order'
as induced by the safe mapping
safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
safe(prime1) = {1}, safe(true) = {}, safe(and) = {1, 2},
safe(not) = {1}, safe(divp) = {1, 2}, safe(=) = {1, 2},
safe(rem) = {1, 2}
and precedence
prime > prime1, prime1 > divp .
Following symbols are considered recursive:
{prime, prime1}
The recursion depth is 2.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ prime(0();) -> false()
, prime(s(; 0());) -> false()
, prime(s(; s(; x));) -> prime1(s(; x); s(; s(; x)))
, prime1(0(); x) -> false()
, prime1(s(; 0()); x) -> true()
, prime1(s(; s(; y)); x) ->
and(; not(; divp(; s(; s(; y)), x)), prime1(s(; y); x))
, divp(; x, y) -> =(; rem(; x, y), 0()) }
Weak Trs :
Hurray, we answered YES(?,POLY)
popstar-ps
Execution Time (secs) | 0.304 |
Answer | YES(?,POLY) |
Input | SK90 2.29 |
YES(?,POLY)
We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).
Strict Trs:
{ prime(0()) -> false()
, prime(s(0())) -> false()
, prime(s(s(x))) -> prime1(s(s(x)), s(x))
, prime1(x, 0()) -> false()
, prime1(x, s(0())) -> true()
, prime1(x, s(s(y))) -> and(not(divp(s(s(y)), x)), prime1(x, s(y)))
, divp(x, y) -> =(rem(x, y), 0()) }
Obligation:
innermost runtime complexity
Answer:
YES(?,POLY)
The input was oriented with the instance of 'Polynomial Path Order
(PS)' as induced by the safe mapping
safe(prime) = {}, safe(0) = {}, safe(false) = {}, safe(s) = {1},
safe(prime1) = {1}, safe(true) = {}, safe(and) = {1, 2},
safe(not) = {1}, safe(divp) = {1, 2}, safe(=) = {1, 2},
safe(rem) = {1, 2}
and precedence
prime > prime1, prime1 > divp .
Following symbols are considered recursive:
{prime, prime1}
The recursion depth is 2.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ prime(0();) -> false()
, prime(s(; 0());) -> false()
, prime(s(; s(; x));) -> prime1(s(; x); s(; s(; x)))
, prime1(0(); x) -> false()
, prime1(s(; 0()); x) -> true()
, prime1(s(; s(; y)); x) ->
and(; not(; divp(; s(; s(; y)), x)), prime1(s(; y); x))
, divp(; x, y) -> =(; rem(; x, y), 0()) }
Weak Trs :
Hurray, we answered YES(?,POLY)