interpretations
TIMEOUT
We are left with following problem, upon which TcT provides the
certificate TIMEOUT.
Strict Trs:
{ din(der(der(X))) -> u41(din(der(X)), X)
, din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
, din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
, u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
, u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
, u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
, u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
, u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
, u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
innermost runtime complexity
Answer:
TIMEOUT
Computation stopped due to timeout after 20.0 seconds.
Arrrr..
lmpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
, u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
, u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
, din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
, u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
, u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
, din(der(der(X))) -> u41(din(der(X)), X)
, u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
, u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
, u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
, u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
, din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
, u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
, u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
, din(der(der(X))) -> u41(din(der(X)), X)
, u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
, u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
, u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
, u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
, din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
, u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
, u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
, din(der(der(X))) -> u41(din(der(X)), X)
, u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
, u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
, u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
, u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
, din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
, u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
, u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
, din(der(der(X))) -> u41(din(der(X)), X)
, u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
, u42(dout(DDX), X, DX) -> dout(DDX) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..