(0) Obligation:
Clauses:
rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
notZero(s(X)).
geq(s(X), s(Y)) :- geq(X, Y).
geq(X, 0).
Queries:
rem(g,g,a).
(1) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
rem_in: (b,b,f)
sub_in: (b,b,f)
geq_in: (b,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x3)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x3)
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
NOTZERO_IN_G(
x1) =
NOTZERO_IN_G(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x2,
x4)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x4)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x4)
U4_GGA(
x1,
x2,
x3) =
U4_GGA(
x1,
x2,
x3)
U5_GGA(
x1,
x2,
x3) =
U5_GGA(
x1,
x3)
GEQ_IN_GG(
x1,
x2) =
GEQ_IN_GG(
x1,
x2)
U7_GG(
x1,
x2,
x3) =
U7_GG(
x3)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
NOTZERO_IN_G(
x1) =
NOTZERO_IN_G(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x2,
x4)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x4)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x4)
U4_GGA(
x1,
x2,
x3) =
U4_GGA(
x1,
x2,
x3)
U5_GGA(
x1,
x2,
x3) =
U5_GGA(
x1,
x3)
GEQ_IN_GG(
x1,
x2) =
GEQ_IN_GG(
x1,
x2)
U7_GG(
x1,
x2,
x3) =
U7_GG(
x3)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 9 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x3)
GEQ_IN_GG(
x1,
x2) =
GEQ_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
(13) TRUE
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x3)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
(20) TRUE
(21) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x2,
x4)
We have to consider all (P,R,Pi)-chains
(22) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
The argument filtering Pi contains the following mapping:
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x2,
x4)
We have to consider all (P,R,Pi)-chains
(24) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U1_GGA(X, Y, notZero_out_g) → U2_GGA(Y, sub_in_gga(X, Y))
U2_GGA(Y, sub_out_gga(Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(X, Y) → U1_GGA(X, Y, notZero_in_g(Y))
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X)
notZero_in_g(s(X)) → notZero_out_g
U6_gga(sub_out_gga(Z)) → sub_out_gga(Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
notZero_in_g(x0)
U6_gga(x0)
We have to consider all (P,Q,R)-chains.
(26) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
rem_in: (b,b,f)
sub_in: (b,b,f)
geq_in: (b,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x2,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x1,
x2,
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg(
x1,
x2)
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x1,
x2,
x3)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(27) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x2,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x1,
x2,
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg(
x1,
x2)
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x1,
x2,
x3)
(28) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x2,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x1,
x2,
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg(
x1,
x2)
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x1,
x2,
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
NOTZERO_IN_G(
x1) =
NOTZERO_IN_G(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3) =
U4_GGA(
x1,
x2,
x3)
U5_GGA(
x1,
x2,
x3) =
U5_GGA(
x1,
x2,
x3)
GEQ_IN_GG(
x1,
x2) =
GEQ_IN_GG(
x1,
x2)
U7_GG(
x1,
x2,
x3) =
U7_GG(
x1,
x2,
x3)
We have to consider all (P,R,Pi)-chains
(29) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
REM_IN_GGA(X, Y, R) → NOTZERO_IN_G(Y)
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U1_GGA(X, Y, R, notZero_out_g(Y)) → SUB_IN_GGA(X, Y, Z)
SUB_IN_GGA(s(X), s(Y), Z) → U6_GGA(X, Y, Z, sub_in_gga(X, Y, Z))
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → U3_GGA(X, Y, R, rem_in_gga(Z, Y, R))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, X) → U4_GGA(X, Y, notZero_in_g(Y))
REM_IN_GGA(X, Y, X) → NOTZERO_IN_G(Y)
U4_GGA(X, Y, notZero_out_g(Y)) → U5_GGA(X, Y, geq_in_gg(X, Y))
U4_GGA(X, Y, notZero_out_g(Y)) → GEQ_IN_GG(X, Y)
GEQ_IN_GG(s(X), s(Y)) → U7_GG(X, Y, geq_in_gg(X, Y))
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x2,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x1,
x2,
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg(
x1,
x2)
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x1,
x2,
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
NOTZERO_IN_G(
x1) =
NOTZERO_IN_G(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
U6_GGA(
x1,
x2,
x3,
x4) =
U6_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4) =
U3_GGA(
x1,
x2,
x4)
U4_GGA(
x1,
x2,
x3) =
U4_GGA(
x1,
x2,
x3)
U5_GGA(
x1,
x2,
x3) =
U5_GGA(
x1,
x2,
x3)
GEQ_IN_GG(
x1,
x2) =
GEQ_IN_GG(
x1,
x2)
U7_GG(
x1,
x2,
x3) =
U7_GG(
x1,
x2,
x3)
We have to consider all (P,R,Pi)-chains
(30) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 9 less nodes.
(31) Complex Obligation (AND)
(32) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x2,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x1,
x2,
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg(
x1,
x2)
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x1,
x2,
x3)
GEQ_IN_GG(
x1,
x2) =
GEQ_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(33) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(34) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(35) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(37) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- GEQ_IN_GG(s(X), s(Y)) → GEQ_IN_GG(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
(38) TRUE
(39) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x2,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x1,
x2,
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg(
x1,
x2)
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x1,
x2,
x3)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(40) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(41) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y), Z) → SUB_IN_GGA(X, Y, Z)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
SUB_IN_GGA(
x1,
x2,
x3) =
SUB_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(42) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(43) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(44) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- SUB_IN_GGA(s(X), s(Y)) → SUB_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
(45) TRUE
(46) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
The TRS R consists of the following rules:
rem_in_gga(X, Y, R) → U1_gga(X, Y, R, notZero_in_g(Y))
notZero_in_g(s(X)) → notZero_out_g(s(X))
U1_gga(X, Y, R, notZero_out_g(Y)) → U2_gga(X, Y, R, sub_in_gga(X, Y, Z))
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
U2_gga(X, Y, R, sub_out_gga(X, Y, Z)) → U3_gga(X, Y, R, rem_in_gga(Z, Y, R))
rem_in_gga(X, Y, X) → U4_gga(X, Y, notZero_in_g(Y))
U4_gga(X, Y, notZero_out_g(Y)) → U5_gga(X, Y, geq_in_gg(X, Y))
geq_in_gg(s(X), s(Y)) → U7_gg(X, Y, geq_in_gg(X, Y))
geq_in_gg(X, 0) → geq_out_gg(X, 0)
U7_gg(X, Y, geq_out_gg(X, Y)) → geq_out_gg(s(X), s(Y))
U5_gga(X, Y, geq_out_gg(X, Y)) → rem_out_gga(X, Y, X)
U3_gga(X, Y, R, rem_out_gga(Z, Y, R)) → rem_out_gga(X, Y, R)
The argument filtering Pi contains the following mapping:
rem_in_gga(
x1,
x2,
x3) =
rem_in_gga(
x1,
x2)
U1_gga(
x1,
x2,
x3,
x4) =
U1_gga(
x1,
x2,
x4)
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
U3_gga(
x1,
x2,
x3,
x4) =
U3_gga(
x1,
x2,
x4)
U4_gga(
x1,
x2,
x3) =
U4_gga(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3) =
U5_gga(
x1,
x2,
x3)
geq_in_gg(
x1,
x2) =
geq_in_gg(
x1,
x2)
U7_gg(
x1,
x2,
x3) =
U7_gg(
x1,
x2,
x3)
geq_out_gg(
x1,
x2) =
geq_out_gg(
x1,
x2)
rem_out_gga(
x1,
x2,
x3) =
rem_out_gga(
x1,
x2,
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(47) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(48) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U1_GGA(X, Y, R, notZero_out_g(Y)) → U2_GGA(X, Y, R, sub_in_gga(X, Y, Z))
U2_GGA(X, Y, R, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y, R)
REM_IN_GGA(X, Y, R) → U1_GGA(X, Y, R, notZero_in_g(Y))
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y), Z) → U6_gga(X, Y, Z, sub_in_gga(X, Y, Z))
sub_in_gga(X, 0, X) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, Z, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
The argument filtering Pi contains the following mapping:
notZero_in_g(
x1) =
notZero_in_g(
x1)
s(
x1) =
s(
x1)
notZero_out_g(
x1) =
notZero_out_g(
x1)
sub_in_gga(
x1,
x2,
x3) =
sub_in_gga(
x1,
x2)
U6_gga(
x1,
x2,
x3,
x4) =
U6_gga(
x1,
x2,
x4)
0 =
0
sub_out_gga(
x1,
x2,
x3) =
sub_out_gga(
x1,
x2,
x3)
REM_IN_GGA(
x1,
x2,
x3) =
REM_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3,
x4) =
U1_GGA(
x1,
x2,
x4)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(49) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U1_GGA(X, Y, notZero_out_g(Y)) → U2_GGA(X, Y, sub_in_gga(X, Y))
U2_GGA(X, Y, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(X, Y) → U1_GGA(X, Y, notZero_in_g(Y))
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
notZero_in_g(x0)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(51) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U1_GGA(X, Y, notZero_out_g(Y)) → U2_GGA(X, Y, sub_in_gga(X, Y))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(REM_IN_GGA(x1, x2)) = x1 + x2
POL(U1_GGA(x1, x2, x3)) = x1 + x3
POL(U2_GGA(x1, x2, x3)) = x3
POL(U6_gga(x1, x2, x3)) = 1 + x3
POL(notZero_in_g(x1)) = x1
POL(notZero_out_g(x1)) = 1
POL(s(x1)) = 1 + x1
POL(sub_in_gga(x1, x2)) = x1
POL(sub_out_gga(x1, x2, x3)) = x2 + x3
The following usable rules [FROCOS05] were oriented:
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(X, Y, sub_out_gga(X, Y, Z)) → REM_IN_GGA(Z, Y)
REM_IN_GGA(X, Y) → U1_GGA(X, Y, notZero_in_g(Y))
The TRS R consists of the following rules:
sub_in_gga(s(X), s(Y)) → U6_gga(X, Y, sub_in_gga(X, Y))
sub_in_gga(X, 0) → sub_out_gga(X, 0, X)
notZero_in_g(s(X)) → notZero_out_g(s(X))
U6_gga(X, Y, sub_out_gga(X, Y, Z)) → sub_out_gga(s(X), s(Y), Z)
The set Q consists of the following terms:
sub_in_gga(x0, x1)
notZero_in_g(x0)
U6_gga(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(53) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(54) TRUE