(0) Obligation:
Clauses:
fold(X, [], Z) :- ','(!, eq(X, Z)).
fold(X, Y, Z) :- ','(head(Y, H), ','(tail(Y, T), ','(myop(X, H, V), fold(V, T, Z)))).
myop(a, b, a).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
eq(X, X).
Queries:
fold(g,g,a).
(1) CutEliminatorProof (SOUND transformation)
Eliminated all cuts by simply ignoring them[PROLOG].
(2) Obligation:
Clauses:
fold(X, [], Z) :- eq(X, Z).
fold(X, Y, Z) :- ','(head(Y, H), ','(tail(Y, T), ','(myop(X, H, V), fold(V, T, Z)))).
myop(a, b, a).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
eq(X, X).
Queries:
fold(g,g,a).
(3) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
fold_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x1,
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x1,
x2,
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x1,
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x1,
x2,
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
(5) 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:
FOLD_IN_GGA(X, [], Z) → U1_GGA(X, Z, eq_in_ga(X, Z))
FOLD_IN_GGA(X, [], Z) → EQ_IN_GA(X, Z)
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
FOLD_IN_GGA(X, Y, Z) → HEAD_IN_GA(Y, H)
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → TAIL_IN_GA(Y, T)
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → MYOP_IN_GAA(X, H, V)
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_GGA(X, Y, Z, fold_in_gga(V, T, Z))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x1,
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x1,
x2,
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x1,
x3)
EQ_IN_GA(
x1,
x2) =
EQ_IN_GA(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
HEAD_IN_GA(
x1,
x2) =
HEAD_IN_GA(
x1)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x2,
x5)
TAIL_IN_GA(
x1,
x2) =
TAIL_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x1,
x2,
x5,
x6)
MYOP_IN_GAA(
x1,
x2,
x3) =
MYOP_IN_GAA(
x1)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, [], Z) → U1_GGA(X, Z, eq_in_ga(X, Z))
FOLD_IN_GGA(X, [], Z) → EQ_IN_GA(X, Z)
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
FOLD_IN_GGA(X, Y, Z) → HEAD_IN_GA(Y, H)
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → TAIL_IN_GA(Y, T)
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → MYOP_IN_GAA(X, H, V)
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_GGA(X, Y, Z, fold_in_gga(V, T, Z))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x1,
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x1,
x2,
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x1,
x3)
EQ_IN_GA(
x1,
x2) =
EQ_IN_GA(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
HEAD_IN_GA(
x1,
x2) =
HEAD_IN_GA(
x1)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x2,
x5)
TAIL_IN_GA(
x1,
x2) =
TAIL_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x1,
x2,
x5,
x6)
MYOP_IN_GAA(
x1,
x2,
x3) =
MYOP_IN_GAA(
x1)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x1,
x2,
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 6 less nodes.
(8) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x1,
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x1,
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x1,
x2,
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x2,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x1,
x2,
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x1,
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x1,
x2,
x4)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x2,
x5)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x1,
x2,
x5,
x6)
We have to consider all (P,R,Pi)-chains
(9) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(10) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
The argument filtering Pi contains the following mapping:
[] =
[]
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga(
x1)
.(
x1,
x2) =
.(
x1,
x2)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x1,
x2)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x1,
x2,
x3)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x2,
x5)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x1,
x2,
x5,
x6)
We have to consider all (P,R,Pi)-chains
(11) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, Y) → U2_GGA(X, Y, head_in_ga(Y))
U2_GGA(X, Y, head_out_ga(Y)) → U3_GGA(X, Y, tail_in_ga(Y))
U3_GGA(X, Y, tail_out_ga(Y, T)) → U4_GGA(X, Y, T, myop_in_gaa(X))
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
The TRS R consists of the following rules:
head_in_ga([]) → head_out_ga([])
head_in_ga(.(H, X2)) → head_out_ga(.(H, X2))
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X3, T)) → tail_out_ga(.(X3, T), T)
myop_in_gaa(a) → myop_out_gaa(a, b, a)
The set Q consists of the following terms:
head_in_ga(x0)
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(13) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
FOLD_IN_GGA(
X,
Y) →
U2_GGA(
X,
Y,
head_in_ga(
Y)) at position [2] we obtained the following new rules [LPAR04]:
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(X, Y, head_out_ga(Y)) → U3_GGA(X, Y, tail_in_ga(Y))
U3_GGA(X, Y, tail_out_ga(Y, T)) → U4_GGA(X, Y, T, myop_in_gaa(X))
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
The TRS R consists of the following rules:
head_in_ga([]) → head_out_ga([])
head_in_ga(.(H, X2)) → head_out_ga(.(H, X2))
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X3, T)) → tail_out_ga(.(X3, T), T)
myop_in_gaa(a) → myop_out_gaa(a, b, a)
The set Q consists of the following terms:
head_in_ga(x0)
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(15) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(X, Y, head_out_ga(Y)) → U3_GGA(X, Y, tail_in_ga(Y))
U3_GGA(X, Y, tail_out_ga(Y, T)) → U4_GGA(X, Y, T, myop_in_gaa(X))
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(a, b, a)
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X3, T)) → tail_out_ga(.(X3, T), T)
The set Q consists of the following terms:
head_in_ga(x0)
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(17) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
head_in_ga(x0)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(X, Y, head_out_ga(Y)) → U3_GGA(X, Y, tail_in_ga(Y))
U3_GGA(X, Y, tail_out_ga(Y, T)) → U4_GGA(X, Y, T, myop_in_gaa(X))
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(a, b, a)
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X3, T)) → tail_out_ga(.(X3, T), T)
The set Q consists of the following terms:
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(19) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U2_GGA(
X,
Y,
head_out_ga(
Y)) →
U3_GGA(
X,
Y,
tail_in_ga(
Y)) at position [2] we obtained the following new rules [LPAR04]:
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(X, Y, tail_out_ga(Y, T)) → U4_GGA(X, Y, T, myop_in_gaa(X))
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(a, b, a)
tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X3, T)) → tail_out_ga(.(X3, T), T)
The set Q consists of the following terms:
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(21) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(X, Y, tail_out_ga(Y, T)) → U4_GGA(X, Y, T, myop_in_gaa(X))
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(a, b, a)
The set Q consists of the following terms:
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(23) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
tail_in_ga(x0)
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(X, Y, tail_out_ga(Y, T)) → U4_GGA(X, Y, T, myop_in_gaa(X))
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(a, b, a)
The set Q consists of the following terms:
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(25) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U3_GGA(
X,
Y,
tail_out_ga(
Y,
T)) →
U4_GGA(
X,
Y,
T,
myop_in_gaa(
X)) at position [3] we obtained the following new rules [LPAR04]:
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(a, b, a)
The set Q consists of the following terms:
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(27) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
R is empty.
The set Q consists of the following terms:
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(29) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
myop_in_gaa(x0)
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(X, Y, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(31) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
X,
Y,
T,
myop_out_gaa(
X,
H,
V)) →
FOLD_IN_GGA(
V,
T) we obtained the following new rules [LPAR04]:
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga([]))
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(33) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
FOLD_IN_GGA(
y0,
[]) →
U2_GGA(
y0,
[],
head_out_ga(
[])) we obtained the following new rules [LPAR04]:
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(y0, .(x0, x1)) → U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1)))
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(35) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
FOLD_IN_GGA(
y0,
.(
x0,
x1)) →
U2_GGA(
y0,
.(
x0,
x1),
head_out_ga(
.(
x0,
x1))) we obtained the following new rules [LPAR04]:
FOLD_IN_GGA(a, .(x1, x2)) → U2_GGA(a, .(x1, x2), head_out_ga(.(x1, x2)))
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(y0, [], head_out_ga([])) → U3_GGA(y0, [], tail_out_ga([], []))
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
FOLD_IN_GGA(a, .(x1, x2)) → U2_GGA(a, .(x1, x2), head_out_ga(.(x1, x2)))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(37) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U2_GGA(
y0,
[],
head_out_ga(
[])) →
U3_GGA(
y0,
[],
tail_out_ga(
[],
[])) we obtained the following new rules [LPAR04]:
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(y0, .(x0, x1), head_out_ga(.(x0, x1))) → U3_GGA(y0, .(x0, x1), tail_out_ga(.(x0, x1), x1))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
FOLD_IN_GGA(a, .(x1, x2)) → U2_GGA(a, .(x1, x2), head_out_ga(.(x1, x2)))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(39) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U2_GGA(
y0,
.(
x0,
x1),
head_out_ga(
.(
x0,
x1))) →
U3_GGA(
y0,
.(
x0,
x1),
tail_out_ga(
.(
x0,
x1),
x1)) we obtained the following new rules [LPAR04]:
U2_GGA(a, .(z0, z1), head_out_ga(.(z0, z1))) → U3_GGA(a, .(z0, z1), tail_out_ga(.(z0, z1), z1))
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
FOLD_IN_GGA(a, .(x1, x2)) → U2_GGA(a, .(x1, x2), head_out_ga(.(x1, x2)))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
U2_GGA(a, .(z0, z1), head_out_ga(.(z0, z1))) → U3_GGA(a, .(z0, z1), tail_out_ga(.(z0, z1), z1))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(41) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
FOLD_IN_GGA(a, .(x1, x2)) → U2_GGA(a, .(x1, x2), head_out_ga(.(x1, x2)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
| POL(U3_GGA(x1, x2, x3)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| POL(tail_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(U4_GGA(x1, x2, x3, x4)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
| POL(myop_out_gaa(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| POL(FOLD_IN_GGA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
| POL(U2_GGA(x1, x2, x3)) = | 0 | + | | · | x1 | + | | · | x2 | + | | · | x3 |
| POL(head_out_ga(x1)) = | | + | | · | x1 |
| POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
none
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
U2_GGA(a, .(z0, z1), head_out_ga(.(z0, z1))) → U3_GGA(a, .(z0, z1), tail_out_ga(.(z0, z1), z1))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(43) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(45) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
a,
y1,
tail_out_ga(
y1,
y2)) →
U4_GGA(
a,
y1,
y2,
myop_out_gaa(
a,
b,
a)) we obtained the following new rules [LPAR04]:
U3_GGA(a, [], tail_out_ga([], [])) → U4_GGA(a, [], [], myop_out_gaa(a, b, a))
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
U3_GGA(a, [], tail_out_ga([], [])) → U4_GGA(a, [], [], myop_out_gaa(a, b, a))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(47) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
a,
y1,
tail_out_ga(
y1,
y2)) →
U4_GGA(
a,
y1,
y2,
myop_out_gaa(
a,
b,
a)) we obtained the following new rules [LPAR04]:
U3_GGA(a, [], tail_out_ga([], [])) → U4_GGA(a, [], [], myop_out_gaa(a, b, a))
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
U3_GGA(a, [], tail_out_ga([], [])) → U4_GGA(a, [], [], myop_out_gaa(a, b, a))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(49) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
a,
z0,
z1,
myop_out_gaa(
a,
b,
a)) →
FOLD_IN_GGA(
a,
z1) we obtained the following new rules [LPAR04]:
U4_GGA(a, [], [], myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, [])
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
U3_GGA(a, [], tail_out_ga([], [])) → U4_GGA(a, [], [], myop_out_gaa(a, b, a))
U4_GGA(a, [], [], myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, [])
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(51) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
U2_GGA(
a,
[],
head_out_ga(
[])) evaluates to t =
U2_GGA(
a,
[],
head_out_ga(
[]))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequenceU2_GGA(a, [], head_out_ga([])) →
U3_GGA(
a,
[],
tail_out_ga(
[],
[]))
with rule
U2_GGA(
a,
[],
head_out_ga(
[])) →
U3_GGA(
a,
[],
tail_out_ga(
[],
[])) at position [] and matcher [ ]
U3_GGA(a, [], tail_out_ga([], [])) →
U4_GGA(
a,
[],
[],
myop_out_gaa(
a,
b,
a))
with rule
U3_GGA(
a,
[],
tail_out_ga(
[],
[])) →
U4_GGA(
a,
[],
[],
myop_out_gaa(
a,
b,
a)) at position [] and matcher [ ]
U4_GGA(a, [], [], myop_out_gaa(a, b, a)) →
FOLD_IN_GGA(
a,
[])
with rule
U4_GGA(
a,
[],
[],
myop_out_gaa(
a,
b,
a)) →
FOLD_IN_GGA(
a,
[]) at position [] and matcher [ ]
FOLD_IN_GGA(a, []) →
U2_GGA(
a,
[],
head_out_ga(
[]))
with rule
FOLD_IN_GGA(
a,
[]) →
U2_GGA(
a,
[],
head_out_ga(
[]))
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(52) FALSE
(53) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U2_GGA(a, .(z0, z1), head_out_ga(.(z0, z1))) → U3_GGA(a, .(z0, z1), tail_out_ga(.(z0, z1), z1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(.(x1, x2)) = 1 + x2
POL(FOLD_IN_GGA(x1, x2)) = x2
POL(U2_GGA(x1, x2, x3)) = x2
POL(U3_GGA(x1, x2, x3)) = x3
POL(U4_GGA(x1, x2, x3, x4)) = x3
POL([]) = 0
POL(a) = 0
POL(b) = 0
POL(head_out_ga(x1)) = 0
POL(myop_out_gaa(x1, x2, x3)) = 0
POL(tail_out_ga(x1, x2)) = x2
The following usable rules [FROCOS05] were oriented:
none
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(a, y1, tail_out_ga(y1, y2)) → U4_GGA(a, y1, y2, myop_out_gaa(a, b, a))
U4_GGA(a, z0, z1, myop_out_gaa(a, b, a)) → FOLD_IN_GGA(a, z1)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga([]))
FOLD_IN_GGA(a, .(x1, x2)) → U2_GGA(a, .(x1, x2), head_out_ga(.(x1, x2)))
U2_GGA(a, [], head_out_ga([])) → U3_GGA(a, [], tail_out_ga([], []))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(55) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
fold_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(56) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
(57) 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:
FOLD_IN_GGA(X, [], Z) → U1_GGA(X, Z, eq_in_ga(X, Z))
FOLD_IN_GGA(X, [], Z) → EQ_IN_GA(X, Z)
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
FOLD_IN_GGA(X, Y, Z) → HEAD_IN_GA(Y, H)
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → TAIL_IN_GA(Y, T)
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → MYOP_IN_GAA(X, H, V)
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_GGA(X, Y, Z, fold_in_gga(V, T, Z))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x3)
EQ_IN_GA(
x1,
x2) =
EQ_IN_GA(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
HEAD_IN_GA(
x1,
x2) =
HEAD_IN_GA(
x1)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x5)
TAIL_IN_GA(
x1,
x2) =
TAIL_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x5,
x6)
MYOP_IN_GAA(
x1,
x2,
x3) =
MYOP_IN_GAA(
x1)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x4)
We have to consider all (P,R,Pi)-chains
(58) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, [], Z) → U1_GGA(X, Z, eq_in_ga(X, Z))
FOLD_IN_GGA(X, [], Z) → EQ_IN_GA(X, Z)
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
FOLD_IN_GGA(X, Y, Z) → HEAD_IN_GA(Y, H)
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → TAIL_IN_GA(Y, T)
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → MYOP_IN_GAA(X, H, V)
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_GGA(X, Y, Z, fold_in_gga(V, T, Z))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U1_GGA(
x1,
x2,
x3) =
U1_GGA(
x3)
EQ_IN_GA(
x1,
x2) =
EQ_IN_GA(
x1)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
HEAD_IN_GA(
x1,
x2) =
HEAD_IN_GA(
x1)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x5)
TAIL_IN_GA(
x1,
x2) =
TAIL_IN_GA(
x1)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x5,
x6)
MYOP_IN_GAA(
x1,
x2,
x3) =
MYOP_IN_GAA(
x1)
U5_GGA(
x1,
x2,
x3,
x4) =
U5_GGA(
x4)
We have to consider all (P,R,Pi)-chains
(59) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 6 less nodes.
(60) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
fold_in_gga(X, [], Z) → U1_gga(X, Z, eq_in_ga(X, Z))
eq_in_ga(X, X) → eq_out_ga(X, X)
U1_gga(X, Z, eq_out_ga(X, Z)) → fold_out_gga(X, [], Z)
fold_in_gga(X, Y, Z) → U2_gga(X, Y, Z, head_in_ga(Y, H))
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
U2_gga(X, Y, Z, head_out_ga(Y, H)) → U3_gga(X, Y, Z, H, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
U3_gga(X, Y, Z, H, tail_out_ga(Y, T)) → U4_gga(X, Y, Z, H, T, myop_in_gaa(X, H, V))
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
U4_gga(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → U5_gga(X, Y, Z, fold_in_gga(V, T, Z))
U5_gga(X, Y, Z, fold_out_gga(V, T, Z)) → fold_out_gga(X, Y, Z)
The argument filtering Pi contains the following mapping:
fold_in_gga(
x1,
x2,
x3) =
fold_in_gga(
x1,
x2)
[] =
[]
U1_gga(
x1,
x2,
x3) =
U1_gga(
x3)
eq_in_ga(
x1,
x2) =
eq_in_ga(
x1)
eq_out_ga(
x1,
x2) =
eq_out_ga(
x2)
fold_out_gga(
x1,
x2,
x3) =
fold_out_gga(
x3)
U2_gga(
x1,
x2,
x3,
x4) =
U2_gga(
x1,
x2,
x4)
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U3_gga(
x1,
x2,
x3,
x4,
x5) =
U3_gga(
x1,
x5)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_gga(
x5,
x6)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x2,
x3)
U5_gga(
x1,
x2,
x3,
x4) =
U5_gga(
x4)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x5)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x5,
x6)
We have to consider all (P,R,Pi)-chains
(61) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(62) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, Y, Z) → U2_GGA(X, Y, Z, head_in_ga(Y, H))
U2_GGA(X, Y, Z, head_out_ga(Y, H)) → U3_GGA(X, Y, Z, H, tail_in_ga(Y, T))
U3_GGA(X, Y, Z, H, tail_out_ga(Y, T)) → U4_GGA(X, Y, Z, H, T, myop_in_gaa(X, H, V))
U4_GGA(X, Y, Z, H, T, myop_out_gaa(X, H, V)) → FOLD_IN_GGA(V, T, Z)
The TRS R consists of the following rules:
head_in_ga([], X1) → head_out_ga([], X1)
head_in_ga(.(H, X2), H) → head_out_ga(.(H, X2), H)
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X3, T), T) → tail_out_ga(.(X3, T), T)
myop_in_gaa(a, b, a) → myop_out_gaa(a, b, a)
The argument filtering Pi contains the following mapping:
[] =
[]
head_in_ga(
x1,
x2) =
head_in_ga(
x1)
head_out_ga(
x1,
x2) =
head_out_ga
.(
x1,
x2) =
.(
x1,
x2)
tail_in_ga(
x1,
x2) =
tail_in_ga(
x1)
tail_out_ga(
x1,
x2) =
tail_out_ga(
x2)
myop_in_gaa(
x1,
x2,
x3) =
myop_in_gaa(
x1)
a =
a
myop_out_gaa(
x1,
x2,
x3) =
myop_out_gaa(
x2,
x3)
FOLD_IN_GGA(
x1,
x2,
x3) =
FOLD_IN_GGA(
x1,
x2)
U2_GGA(
x1,
x2,
x3,
x4) =
U2_GGA(
x1,
x2,
x4)
U3_GGA(
x1,
x2,
x3,
x4,
x5) =
U3_GGA(
x1,
x5)
U4_GGA(
x1,
x2,
x3,
x4,
x5,
x6) =
U4_GGA(
x5,
x6)
We have to consider all (P,R,Pi)-chains
(63) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, Y) → U2_GGA(X, Y, head_in_ga(Y))
U2_GGA(X, Y, head_out_ga) → U3_GGA(X, tail_in_ga(Y))
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
The TRS R consists of the following rules:
head_in_ga([]) → head_out_ga
head_in_ga(.(H, X2)) → head_out_ga
tail_in_ga([]) → tail_out_ga([])
tail_in_ga(.(X3, T)) → tail_out_ga(T)
myop_in_gaa(a) → myop_out_gaa(b, a)
The set Q consists of the following terms:
head_in_ga(x0)
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(65) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
No dependency pairs are removed.
The following rules are removed from R:
tail_in_ga(.(X3, T)) → tail_out_ga(T)
head_in_ga(.(H, X2)) → head_out_ga
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(.(x1, x2)) = x1 + 2·x2
POL(FOLD_IN_GGA(x1, x2)) = 2·x1 + 2·x2
POL(U2_GGA(x1, x2, x3)) = 2·x1 + x2 + x3
POL(U3_GGA(x1, x2)) = 2·x1 + x2
POL(U4_GGA(x1, x2)) = 2·x1 + x2
POL([]) = 0
POL(a) = 0
POL(b) = 0
POL(head_in_ga(x1)) = x1
POL(head_out_ga) = 0
POL(myop_in_gaa(x1)) = 2·x1
POL(myop_out_gaa(x1, x2)) = 2·x1 + 2·x2
POL(tail_in_ga(x1)) = x1
POL(tail_out_ga(x1)) = 2·x1
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(X, Y) → U2_GGA(X, Y, head_in_ga(Y))
U2_GGA(X, Y, head_out_ga) → U3_GGA(X, tail_in_ga(Y))
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
tail_in_ga([]) → tail_out_ga([])
head_in_ga([]) → head_out_ga
The set Q consists of the following terms:
head_in_ga(x0)
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(67) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
FOLD_IN_GGA(
X,
Y) →
U2_GGA(
X,
Y,
head_in_ga(
Y)) at position [2] we obtained the following new rules [LPAR04]:
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(X, Y, head_out_ga) → U3_GGA(X, tail_in_ga(Y))
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
tail_in_ga([]) → tail_out_ga([])
head_in_ga([]) → head_out_ga
The set Q consists of the following terms:
head_in_ga(x0)
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(69) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(X, Y, head_out_ga) → U3_GGA(X, tail_in_ga(Y))
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
tail_in_ga([]) → tail_out_ga([])
The set Q consists of the following terms:
head_in_ga(x0)
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(71) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
head_in_ga(x0)
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(X, Y, head_out_ga) → U3_GGA(X, tail_in_ga(Y))
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
tail_in_ga([]) → tail_out_ga([])
The set Q consists of the following terms:
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(73) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U2_GGA(
X,
Y,
head_out_ga) →
U3_GGA(
X,
tail_in_ga(
Y)) at position [1] we obtained the following new rules [LPAR04]:
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
tail_in_ga([]) → tail_out_ga([])
The set Q consists of the following terms:
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(75) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
The set Q consists of the following terms:
tail_in_ga(x0)
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(77) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
tail_in_ga(x0)
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(X, tail_out_ga(T)) → U4_GGA(T, myop_in_gaa(X))
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
The set Q consists of the following terms:
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(79) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
U3_GGA(
X,
tail_out_ga(
T)) →
U4_GGA(
T,
myop_in_gaa(
X)) at position [1] we obtained the following new rules [LPAR04]:
U3_GGA(a, tail_out_ga(y1)) → U4_GGA(y1, myop_out_gaa(b, a))
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
U3_GGA(a, tail_out_ga(y1)) → U4_GGA(y1, myop_out_gaa(b, a))
The TRS R consists of the following rules:
myop_in_gaa(a) → myop_out_gaa(b, a)
The set Q consists of the following terms:
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(81) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
U3_GGA(a, tail_out_ga(y1)) → U4_GGA(y1, myop_out_gaa(b, a))
R is empty.
The set Q consists of the following terms:
myop_in_gaa(x0)
We have to consider all (P,Q,R)-chains.
(83) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
myop_in_gaa(x0)
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(T, myop_out_gaa(H, V)) → FOLD_IN_GGA(V, T)
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
U3_GGA(a, tail_out_ga(y1)) → U4_GGA(y1, myop_out_gaa(b, a))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(85) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
T,
myop_out_gaa(
H,
V)) →
FOLD_IN_GGA(
V,
T) we obtained the following new rules [LPAR04]:
U4_GGA(z0, myop_out_gaa(b, a)) → FOLD_IN_GGA(a, z0)
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(y0, []) → U2_GGA(y0, [], head_out_ga)
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
U3_GGA(a, tail_out_ga(y1)) → U4_GGA(y1, myop_out_gaa(b, a))
U4_GGA(z0, myop_out_gaa(b, a)) → FOLD_IN_GGA(a, z0)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(87) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
FOLD_IN_GGA(
y0,
[]) →
U2_GGA(
y0,
[],
head_out_ga) we obtained the following new rules [LPAR04]:
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga)
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGA(y0, [], head_out_ga) → U3_GGA(y0, tail_out_ga([]))
U3_GGA(a, tail_out_ga(y1)) → U4_GGA(y1, myop_out_gaa(b, a))
U4_GGA(z0, myop_out_gaa(b, a)) → FOLD_IN_GGA(a, z0)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(89) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U2_GGA(
y0,
[],
head_out_ga) →
U3_GGA(
y0,
tail_out_ga(
[])) we obtained the following new rules [LPAR04]:
U2_GGA(a, [], head_out_ga) → U3_GGA(a, tail_out_ga([]))
(90) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GGA(a, tail_out_ga(y1)) → U4_GGA(y1, myop_out_gaa(b, a))
U4_GGA(z0, myop_out_gaa(b, a)) → FOLD_IN_GGA(a, z0)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga)
U2_GGA(a, [], head_out_ga) → U3_GGA(a, tail_out_ga([]))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(91) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U3_GGA(
a,
tail_out_ga(
y1)) →
U4_GGA(
y1,
myop_out_gaa(
b,
a)) we obtained the following new rules [LPAR04]:
U3_GGA(a, tail_out_ga([])) → U4_GGA([], myop_out_gaa(b, a))
(92) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U4_GGA(z0, myop_out_gaa(b, a)) → FOLD_IN_GGA(a, z0)
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga)
U2_GGA(a, [], head_out_ga) → U3_GGA(a, tail_out_ga([]))
U3_GGA(a, tail_out_ga([])) → U4_GGA([], myop_out_gaa(b, a))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(93) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U4_GGA(
z0,
myop_out_gaa(
b,
a)) →
FOLD_IN_GGA(
a,
z0) we obtained the following new rules [LPAR04]:
U4_GGA([], myop_out_gaa(b, a)) → FOLD_IN_GGA(a, [])
(94) Obligation:
Q DP problem:
The TRS P consists of the following rules:
FOLD_IN_GGA(a, []) → U2_GGA(a, [], head_out_ga)
U2_GGA(a, [], head_out_ga) → U3_GGA(a, tail_out_ga([]))
U3_GGA(a, tail_out_ga([])) → U4_GGA([], myop_out_gaa(b, a))
U4_GGA([], myop_out_gaa(b, a)) → FOLD_IN_GGA(a, [])
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(95) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
U2_GGA(
a,
[],
head_out_ga) evaluates to t =
U2_GGA(
a,
[],
head_out_ga)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceU2_GGA(a, [], head_out_ga) →
U3_GGA(
a,
tail_out_ga(
[]))
with rule
U2_GGA(
a,
[],
head_out_ga) →
U3_GGA(
a,
tail_out_ga(
[])) at position [] and matcher [ ]
U3_GGA(a, tail_out_ga([])) →
U4_GGA(
[],
myop_out_gaa(
b,
a))
with rule
U3_GGA(
a,
tail_out_ga(
[])) →
U4_GGA(
[],
myop_out_gaa(
b,
a)) at position [] and matcher [ ]
U4_GGA([], myop_out_gaa(b, a)) →
FOLD_IN_GGA(
a,
[])
with rule
U4_GGA(
[],
myop_out_gaa(
b,
a)) →
FOLD_IN_GGA(
a,
[]) at position [] and matcher [ ]
FOLD_IN_GGA(a, []) →
U2_GGA(
a,
[],
head_out_ga)
with rule
FOLD_IN_GGA(
a,
[]) →
U2_GGA(
a,
[],
head_out_ga)
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.
(96) FALSE