Tool CaT
stdout:
MAYBE
Problem:
p(s(N)) -> N
+(N,0()) -> N
+(s(N),s(M)) -> s(s(+(N,M)))
*(N,0()) -> 0()
*(s(N),s(M)) -> s(+(N,+(M,*(N,M))))
gt(0(),M) -> False()
gt(NzN,0()) -> u_4(is_NzNat(NzN))
u_4(True()) -> True()
is_NzNat(0()) -> False()
is_NzNat(s(N)) -> True()
gt(s(N),s(M)) -> gt(N,M)
lt(N,M) -> gt(M,N)
d(0(),N) -> N
d(s(N),s(M)) -> d(N,M)
quot(N,NzM) -> u_11(is_NzNat(NzM),N,NzM)
u_11(True(),N,NzM) -> u_1(gt(N,NzM),N,NzM)
u_1(True(),N,NzM) -> s(quot(d(N,NzM),NzM))
quot(NzM,NzM) -> u_01(is_NzNat(NzM))
u_01(True()) -> s(0())
quot(N,NzM) -> u_21(is_NzNat(NzM),NzM,N)
u_21(True(),NzM,N) -> u_2(gt(NzM,N))
u_2(True()) -> 0()
gcd(0(),N) -> 0()
gcd(NzM,NzM) -> u_02(is_NzNat(NzM),NzM)
u_02(True(),NzM) -> NzM
gcd(NzN,NzM) -> u_31(is_NzNat(NzN),is_NzNat(NzM),NzN,NzM)
u_31(True(),True(),NzN,NzM) -> u_3(gt(NzN,NzM),NzN,NzM)
u_3(True(),NzN,NzM) -> gcd(d(NzN,NzM),NzM)
Proof:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ p(s(N)) -> N
, +(N, 0()) -> N
, +(s(N), s(M)) -> s(s(+(N, M)))
, *(N, 0()) -> 0()
, *(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
, gt(0(), M) -> False()
, gt(NzN, 0()) -> u_4(is_NzNat(NzN))
, u_4(True()) -> True()
, is_NzNat(0()) -> False()
, is_NzNat(s(N)) -> True()
, gt(s(N), s(M)) -> gt(N, M)
, lt(N, M) -> gt(M, N)
, d(0(), N) -> N
, d(s(N), s(M)) -> d(N, M)
, quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM)
, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM)
, u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM))
, quot(NzM, NzM) -> u_01(is_NzNat(NzM))
, u_01(True()) -> s(0())
, quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N)
, u_21(True(), NzM, N) -> u_2(gt(NzM, N))
, u_2(True()) -> 0()
, gcd(0(), N) -> 0()
, gcd(NzM, NzM) -> u_02(is_NzNat(NzM), NzM)
, u_02(True(), NzM) -> NzM
, gcd(NzN, NzM) -> u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM)
, u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)}
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:
{ p(s(N)) -> N
, +(N, 0()) -> N
, +(s(N), s(M)) -> s(s(+(N, M)))
, *(N, 0()) -> 0()
, *(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
, gt(0(), M) -> False()
, gt(NzN, 0()) -> u_4(is_NzNat(NzN))
, u_4(True()) -> True()
, is_NzNat(0()) -> False()
, is_NzNat(s(N)) -> True()
, gt(s(N), s(M)) -> gt(N, M)
, lt(N, M) -> gt(M, N)
, d(0(), N) -> N
, d(s(N), s(M)) -> d(N, M)
, quot(N, NzM) -> u_11(is_NzNat(NzM), N, NzM)
, u_11(True(), N, NzM) -> u_1(gt(N, NzM), N, NzM)
, u_1(True(), N, NzM) -> s(quot(d(N, NzM), NzM))
, quot(NzM, NzM) -> u_01(is_NzNat(NzM))
, u_01(True()) -> s(0())
, quot(N, NzM) -> u_21(is_NzNat(NzM), NzM, N)
, u_21(True(), NzM, N) -> u_2(gt(NzM, N))
, u_2(True()) -> 0()
, gcd(0(), N) -> 0()
, gcd(NzM, NzM) -> u_02(is_NzNat(NzM), NzM)
, u_02(True(), NzM) -> NzM
, gcd(NzN, NzM) -> u_31(is_NzNat(NzN), is_NzNat(NzM), NzN, NzM)
, u_31(True(), True(), NzN, NzM) -> u_3(gt(NzN, NzM), NzN, NzM)
, u_3(True(), NzN, NzM) -> gcd(d(NzN, NzM), NzM)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds