(0) Obligation:
Clauses:
inorder(nil, []).
inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I))).
append([], X, X).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).
Queries:
inorder(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:
inorder_in: (b,f)
append_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x2,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x2,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x5)
(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:
INORDER_IN_GA(tree(L, V, R), I) → U1_GA(L, V, R, I, inorder_in_ga(L, LI))
INORDER_IN_GA(tree(L, V, R), I) → INORDER_IN_GA(L, LI)
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → U2_GA(L, V, R, I, LI, inorder_in_ga(R, RI))
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → INORDER_IN_GA(R, RI)
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_GA(L, V, R, I, append_in_gga(LI, .(V, RI), I))
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → APPEND_IN_GGA(LI, .(V, RI), I)
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → U4_GGA(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x2,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x5)
INORDER_IN_GA(
x1,
x2) =
INORDER_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x2,
x3,
x5)
U2_GA(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_GA(
x2,
x5,
x6)
U3_GA(
x1,
x2,
x3,
x4,
x5) =
U3_GA(
x5)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x5)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
INORDER_IN_GA(tree(L, V, R), I) → U1_GA(L, V, R, I, inorder_in_ga(L, LI))
INORDER_IN_GA(tree(L, V, R), I) → INORDER_IN_GA(L, LI)
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → U2_GA(L, V, R, I, LI, inorder_in_ga(R, RI))
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → INORDER_IN_GA(R, RI)
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_GA(L, V, R, I, append_in_gga(LI, .(V, RI), I))
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → APPEND_IN_GGA(LI, .(V, RI), I)
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → U4_GGA(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x2,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x5)
INORDER_IN_GA(
x1,
x2) =
INORDER_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x2,
x3,
x5)
U2_GA(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_GA(
x2,
x5,
x6)
U3_GA(
x1,
x2,
x3,
x4,
x5) =
U3_GA(
x5)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x2,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x5)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
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:
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND 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:
APPEND_IN_GGA(.(X, Xs), Ys) → APPEND_IN_GGA(Xs, Ys)
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:
- APPEND_IN_GGA(.(X, Xs), Ys) → APPEND_IN_GGA(Xs, Ys)
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:
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → INORDER_IN_GA(R, RI)
INORDER_IN_GA(tree(L, V, R), I) → U1_GA(L, V, R, I, inorder_in_ga(L, LI))
INORDER_IN_GA(tree(L, V, R), I) → INORDER_IN_GA(L, LI)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x2,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x5)
INORDER_IN_GA(
x1,
x2) =
INORDER_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U1_GA(V, R, inorder_out_ga(LI)) → INORDER_IN_GA(R)
INORDER_IN_GA(tree(L, V, R)) → U1_GA(V, R, inorder_in_ga(L))
INORDER_IN_GA(tree(L, V, R)) → INORDER_IN_GA(L)
The TRS R consists of the following rules:
inorder_in_ga(nil) → inorder_out_ga([])
inorder_in_ga(tree(L, V, R)) → U1_ga(V, R, inorder_in_ga(L))
U1_ga(V, R, inorder_out_ga(LI)) → U2_ga(V, LI, inorder_in_ga(R))
U2_ga(V, LI, inorder_out_ga(RI)) → U3_ga(append_in_gga(LI, .(V, RI)))
append_in_gga([], X) → append_out_gga(X)
append_in_gga(.(X, Xs), Ys) → U4_gga(X, append_in_gga(Xs, Ys))
U4_gga(X, append_out_gga(Zs)) → append_out_gga(.(X, Zs))
U3_ga(append_out_gga(I)) → inorder_out_ga(I)
The set Q consists of the following terms:
inorder_in_ga(x0)
U1_ga(x0, x1, x2)
U2_ga(x0, x1, x2)
append_in_gga(x0, x1)
U4_gga(x0, x1)
U3_ga(x0)
We have to consider all (P,Q,R)-chains.
(17) 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:
- INORDER_IN_GA(tree(L, V, R)) → U1_GA(V, R, inorder_in_ga(L))
The graph contains the following edges 1 > 1, 1 > 2
- INORDER_IN_GA(tree(L, V, R)) → INORDER_IN_GA(L)
The graph contains the following edges 1 > 1
- U1_GA(V, R, inorder_out_ga(LI)) → INORDER_IN_GA(R)
The graph contains the following edges 2 >= 1
(18) TRUE
(19) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
inorder_in: (b,f)
append_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x1,
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x1,
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x1,
x2,
x3,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x1,
x2,
x3,
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x3,
x5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(20) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x1,
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x1,
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x1,
x2,
x3,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x1,
x2,
x3,
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x3,
x5)
(21) 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:
INORDER_IN_GA(tree(L, V, R), I) → U1_GA(L, V, R, I, inorder_in_ga(L, LI))
INORDER_IN_GA(tree(L, V, R), I) → INORDER_IN_GA(L, LI)
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → U2_GA(L, V, R, I, LI, inorder_in_ga(R, RI))
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → INORDER_IN_GA(R, RI)
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_GA(L, V, R, I, append_in_gga(LI, .(V, RI), I))
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → APPEND_IN_GGA(LI, .(V, RI), I)
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → U4_GGA(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x1,
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x1,
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x1,
x2,
x3,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x1,
x2,
x3,
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x3,
x5)
INORDER_IN_GA(
x1,
x2) =
INORDER_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x1,
x2,
x3,
x5)
U2_GA(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_GA(
x1,
x2,
x3,
x5,
x6)
U3_GA(
x1,
x2,
x3,
x4,
x5) =
U3_GA(
x1,
x2,
x3,
x5)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(22) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
INORDER_IN_GA(tree(L, V, R), I) → U1_GA(L, V, R, I, inorder_in_ga(L, LI))
INORDER_IN_GA(tree(L, V, R), I) → INORDER_IN_GA(L, LI)
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → U2_GA(L, V, R, I, LI, inorder_in_ga(R, RI))
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → INORDER_IN_GA(R, RI)
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_GA(L, V, R, I, append_in_gga(LI, .(V, RI), I))
U2_GA(L, V, R, I, LI, inorder_out_ga(R, RI)) → APPEND_IN_GGA(LI, .(V, RI), I)
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → U4_GGA(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x1,
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x1,
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x1,
x2,
x3,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x1,
x2,
x3,
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x3,
x5)
INORDER_IN_GA(
x1,
x2) =
INORDER_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x1,
x2,
x3,
x5)
U2_GA(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_GA(
x1,
x2,
x3,
x5,
x6)
U3_GA(
x1,
x2,
x3,
x4,
x5) =
U3_GA(
x1,
x2,
x3,
x5)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
x1,
x2)
U4_GGA(
x1,
x2,
x3,
x4,
x5) =
U4_GGA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains
(23) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.
(24) Complex Obligation (AND)
(25) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x1,
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x1,
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x1,
x2,
x3,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x1,
x2,
x3,
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x3,
x5)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(26) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(27) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_GGA(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_GGA(Xs, Ys, Zs)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPEND_IN_GGA(
x1,
x2,
x3) =
APPEND_IN_GGA(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(28) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPEND_IN_GGA(.(X, Xs), Ys) → APPEND_IN_GGA(Xs, Ys)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(30) 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:
- APPEND_IN_GGA(.(X, Xs), Ys) → APPEND_IN_GGA(Xs, Ys)
The graph contains the following edges 1 > 1, 2 >= 2
(31) TRUE
(32) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
U1_GA(L, V, R, I, inorder_out_ga(L, LI)) → INORDER_IN_GA(R, RI)
INORDER_IN_GA(tree(L, V, R), I) → U1_GA(L, V, R, I, inorder_in_ga(L, LI))
INORDER_IN_GA(tree(L, V, R), I) → INORDER_IN_GA(L, LI)
The TRS R consists of the following rules:
inorder_in_ga(nil, []) → inorder_out_ga(nil, [])
inorder_in_ga(tree(L, V, R), I) → U1_ga(L, V, R, I, inorder_in_ga(L, LI))
U1_ga(L, V, R, I, inorder_out_ga(L, LI)) → U2_ga(L, V, R, I, LI, inorder_in_ga(R, RI))
U2_ga(L, V, R, I, LI, inorder_out_ga(R, RI)) → U3_ga(L, V, R, I, append_in_gga(LI, .(V, RI), I))
append_in_gga([], X, X) → append_out_gga([], X, X)
append_in_gga(.(X, Xs), Ys, .(X, Zs)) → U4_gga(X, Xs, Ys, Zs, append_in_gga(Xs, Ys, Zs))
U4_gga(X, Xs, Ys, Zs, append_out_gga(Xs, Ys, Zs)) → append_out_gga(.(X, Xs), Ys, .(X, Zs))
U3_ga(L, V, R, I, append_out_gga(LI, .(V, RI), I)) → inorder_out_ga(tree(L, V, R), I)
The argument filtering Pi contains the following mapping:
inorder_in_ga(
x1,
x2) =
inorder_in_ga(
x1)
nil =
nil
inorder_out_ga(
x1,
x2) =
inorder_out_ga(
x1,
x2)
tree(
x1,
x2,
x3) =
tree(
x1,
x2,
x3)
U1_ga(
x1,
x2,
x3,
x4,
x5) =
U1_ga(
x1,
x2,
x3,
x5)
U2_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U2_ga(
x1,
x2,
x3,
x5,
x6)
U3_ga(
x1,
x2,
x3,
x4,
x5) =
U3_ga(
x1,
x2,
x3,
x5)
append_in_gga(
x1,
x2,
x3) =
append_in_gga(
x1,
x2)
[] =
[]
append_out_gga(
x1,
x2,
x3) =
append_out_gga(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U4_gga(
x1,
x2,
x3,
x4,
x5) =
U4_gga(
x1,
x2,
x3,
x5)
INORDER_IN_GA(
x1,
x2) =
INORDER_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5) =
U1_GA(
x1,
x2,
x3,
x5)
We have to consider all (P,R,Pi)-chains