LMPO
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
MAYBE
We consider the following Problem:
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)}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..