(0) Obligation:
Clauses:
reach(X, Y, Edges) :- member(.(X, .(Y, [])), Edges).
reach(X, Z, Edges) :- ','(member1(.(X, .(Y, [])), Edges), reach(Y, Z, Edges)).
member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
member1(H, .(H, L)).
member1(X, .(H, L)) :- member1(X, L).
Queries:
reach(g,g,g).
(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:
reach_in: (b,b,b)
member_in: (b,b)
member1_in: (f,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x4)
(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:
REACH_IN_GGG(X, Y, Edges) → U1_GGG(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Y, Edges) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U4_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Z, Edges) → MEMBER1_IN_AG(.(X, .(Y, [])), Edges)
MEMBER1_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_GGG(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U1_GGG(
x1,
x2,
x3,
x4) =
U1_GGG(
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x4)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x2,
x3,
x4)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
x2)
U5_AG(
x1,
x2,
x3,
x4) =
U5_AG(
x4)
U3_GGG(
x1,
x2,
x3,
x4) =
U3_GGG(
x4)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(X, Y, Edges) → U1_GGG(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Y, Edges) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U4_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Z, Edges) → MEMBER1_IN_AG(.(X, .(Y, [])), Edges)
MEMBER1_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_GGG(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U1_GGG(
x1,
x2,
x3,
x4) =
U1_GGG(
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x4)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x2,
x3,
x4)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
x2)
U5_AG(
x1,
x2,
x3,
x4) =
U5_AG(
x4)
U3_GGG(
x1,
x2,
x3,
x4) =
U3_GGG(
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 6 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x4)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
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:
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
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:
MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)
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:
- MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)
The graph contains the following edges 1 > 1
(13) TRUE
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
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:
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (EQUIVALENT 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:
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
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:
- MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
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:
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x2,
x3,
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:
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
[] =
[]
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x2,
x3,
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:
REACH_IN_GGG(X, Z, Edges) → U2_GGG(Z, Edges, member1_in_ag(Edges))
U2_GGG(Z, Edges, member1_out_ag(.(X, .(Y, [])))) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H)
member1_in_ag(.(H, L)) → U5_ag(member1_in_ag(L))
U5_ag(member1_out_ag(X)) → member1_out_ag(X)
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0)
We have to consider all (P,Q,R)-chains.
(26) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
REACH_IN_GGG(
X,
Z,
Edges) →
U2_GGG(
Z,
Edges,
member1_in_ag(
Edges)) at position [2] we obtained the following new rules [LPAR04]:
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y1, .(x0, x1), member1_out_ag(x0))
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y1, .(x0, x1), U5_ag(member1_in_ag(x1)))
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGG(Z, Edges, member1_out_ag(.(X, .(Y, [])))) → REACH_IN_GGG(Y, Z, Edges)
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y1, .(x0, x1), member1_out_ag(x0))
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y1, .(x0, x1), U5_ag(member1_in_ag(x1)))
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H)
member1_in_ag(.(H, L)) → U5_ag(member1_in_ag(L))
U5_ag(member1_out_ag(X)) → member1_out_ag(X)
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0)
We have to consider all (P,Q,R)-chains.
(28) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U2_GGG(
Z,
Edges,
member1_out_ag(
.(
X,
.(
Y,
[])))) →
REACH_IN_GGG(
Y,
Z,
Edges) we obtained the following new rules [LPAR04]:
U2_GGG(z1, .(.(x2, .(x3, [])), z3), member1_out_ag(.(x2, .(x3, [])))) → REACH_IN_GGG(x3, z1, .(.(x2, .(x3, [])), z3))
U2_GGG(z1, .(z2, z3), member1_out_ag(.(x2, .(x3, [])))) → REACH_IN_GGG(x3, z1, .(z2, z3))
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y1, .(x0, x1), member1_out_ag(x0))
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y1, .(x0, x1), U5_ag(member1_in_ag(x1)))
U2_GGG(z1, .(.(x2, .(x3, [])), z3), member1_out_ag(.(x2, .(x3, [])))) → REACH_IN_GGG(x3, z1, .(.(x2, .(x3, [])), z3))
U2_GGG(z1, .(z2, z3), member1_out_ag(.(x2, .(x3, [])))) → REACH_IN_GGG(x3, z1, .(z2, z3))
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H)
member1_in_ag(.(H, L)) → U5_ag(member1_in_ag(L))
U5_ag(member1_out_ag(X)) → member1_out_ag(X)
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0)
We have to consider all (P,Q,R)-chains.
(30) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
REACH_IN_GGG(
y0,
y1,
.(
x0,
x1)) →
U2_GGG(
y1,
.(
x0,
x1),
member1_out_ag(
x0)) we obtained the following new rules [LPAR04]:
REACH_IN_GGG(x0, x1, .(.(y_1, .(y_2, [])), x3)) → U2_GGG(x1, .(.(y_1, .(y_2, [])), x3), member1_out_ag(.(y_1, .(y_2, []))))
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y1, .(x0, x1), U5_ag(member1_in_ag(x1)))
U2_GGG(z1, .(.(x2, .(x3, [])), z3), member1_out_ag(.(x2, .(x3, [])))) → REACH_IN_GGG(x3, z1, .(.(x2, .(x3, [])), z3))
U2_GGG(z1, .(z2, z3), member1_out_ag(.(x2, .(x3, [])))) → REACH_IN_GGG(x3, z1, .(z2, z3))
REACH_IN_GGG(x0, x1, .(.(y_1, .(y_2, [])), x3)) → U2_GGG(x1, .(.(y_1, .(y_2, [])), x3), member1_out_ag(.(y_1, .(y_2, []))))
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H)
member1_in_ag(.(H, L)) → U5_ag(member1_in_ag(L))
U5_ag(member1_out_ag(X)) → member1_out_ag(X)
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0)
We have to consider all (P,Q,R)-chains.
(32) 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 =
REACH_IN_GGG(
x0,
x1,
.(
.(
y_1,
.(
y_2,
[])),
x3')) evaluates to t =
REACH_IN_GGG(
y_2,
x1,
.(
.(
y_1,
.(
y_2,
[])),
x3'))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [x0 / y_2]
Rewriting sequenceREACH_IN_GGG(x0, x1, .(.(y_1, .(y_2, [])), x3')) →
U2_GGG(
x1,
.(
.(
y_1,
.(
y_2,
[])),
x3'),
member1_out_ag(
.(
y_1,
.(
y_2,
[]))))
with rule
REACH_IN_GGG(
x0',
x1',
.(
.(
y_1',
.(
y_2',
[])),
x3'')) →
U2_GGG(
x1',
.(
.(
y_1',
.(
y_2',
[])),
x3''),
member1_out_ag(
.(
y_1',
.(
y_2',
[])))) at position [] and matcher [
x0' /
x0,
x1' /
x1,
y_1' /
y_1,
y_2' /
y_2,
x3'' /
x3']
U2_GGG(x1, .(.(y_1, .(y_2, [])), x3'), member1_out_ag(.(y_1, .(y_2, [])))) →
REACH_IN_GGG(
y_2,
x1,
.(
.(
y_1,
.(
y_2,
[])),
x3'))
with rule
U2_GGG(
z1,
.(
.(
x2,
.(
x3,
[])),
z3),
member1_out_ag(
.(
x2,
.(
x3,
[])))) →
REACH_IN_GGG(
x3,
z1,
.(
.(
x2,
.(
x3,
[])),
z3))
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.
(33) FALSE
(34) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
reach_in: (b,b,b)
member_in: (b,b)
member1_in: (f,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x1,
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x1,
x2,
x3,
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg(
x1,
x2,
x3)
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x1,
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x1,
x2,
x3,
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(35) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x1,
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x1,
x2,
x3,
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg(
x1,
x2,
x3)
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x1,
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x1,
x2,
x3,
x4)
(36) 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:
REACH_IN_GGG(X, Y, Edges) → U1_GGG(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Y, Edges) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U4_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Z, Edges) → MEMBER1_IN_AG(.(X, .(Y, [])), Edges)
MEMBER1_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_GGG(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x1,
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x1,
x2,
x3,
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg(
x1,
x2,
x3)
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x1,
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x1,
x2,
x3,
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U1_GGG(
x1,
x2,
x3,
x4) =
U1_GGG(
x1,
x2,
x3,
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x1,
x2,
x3,
x4)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
x2)
U5_AG(
x1,
x2,
x3,
x4) =
U5_AG(
x2,
x3,
x4)
U3_GGG(
x1,
x2,
x3,
x4) =
U3_GGG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(37) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(X, Y, Edges) → U1_GGG(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Y, Edges) → MEMBER_IN_GG(.(X, .(Y, [])), Edges)
MEMBER_IN_GG(X, .(H, L)) → U4_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
REACH_IN_GGG(X, Z, Edges) → MEMBER1_IN_AG(.(X, .(Y, [])), Edges)
MEMBER1_IN_AG(X, .(H, L)) → U5_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_GGG(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x1,
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x1,
x2,
x3,
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg(
x1,
x2,
x3)
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x1,
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x1,
x2,
x3,
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U1_GGG(
x1,
x2,
x3,
x4) =
U1_GGG(
x1,
x2,
x3,
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
U4_GG(
x1,
x2,
x3,
x4) =
U4_GG(
x1,
x2,
x3,
x4)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x1,
x2,
x3,
x4)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
x2)
U5_AG(
x1,
x2,
x3,
x4) =
U5_AG(
x2,
x3,
x4)
U3_GGG(
x1,
x2,
x3,
x4) =
U3_GGG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(38) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 6 less nodes.
(39) Complex Obligation (AND)
(40) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x1,
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x1,
x2,
x3,
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg(
x1,
x2,
x3)
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x1,
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x1,
x2,
x3,
x4)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
x2)
We have to consider all (P,R,Pi)-chains
(41) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(42) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
MEMBER1_IN_AG(
x1,
x2) =
MEMBER1_IN_AG(
x2)
We have to consider all (P,R,Pi)-chains
(43) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(45) 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:
- MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)
The graph contains the following edges 1 > 1
(46) TRUE
(47) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x1,
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x1,
x2,
x3,
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg(
x1,
x2,
x3)
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x1,
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x1,
x2,
x3,
x4)
MEMBER_IN_GG(
x1,
x2) =
MEMBER_IN_GG(
x1,
x2)
We have to consider all (P,R,Pi)-chains
(48) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(49) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
(50) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(52) 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:
- MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
The graph contains the following edges 1 >= 1, 2 > 2
(53) TRUE
(54) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
reach_in_ggg(X, Y, Edges) → U1_ggg(X, Y, Edges, member_in_gg(.(X, .(Y, [])), Edges))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U4_gg(X, H, L, member_in_gg(X, L))
U4_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_ggg(X, Y, Edges, member_out_gg(.(X, .(Y, [])), Edges)) → reach_out_ggg(X, Y, Edges)
reach_in_ggg(X, Z, Edges) → U2_ggg(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_ggg(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → U3_ggg(X, Z, Edges, reach_in_ggg(Y, Z, Edges))
U3_ggg(X, Z, Edges, reach_out_ggg(Y, Z, Edges)) → reach_out_ggg(X, Z, Edges)
The argument filtering Pi contains the following mapping:
reach_in_ggg(
x1,
x2,
x3) =
reach_in_ggg(
x1,
x2,
x3)
U1_ggg(
x1,
x2,
x3,
x4) =
U1_ggg(
x1,
x2,
x3,
x4)
member_in_gg(
x1,
x2) =
member_in_gg(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
member_out_gg(
x1,
x2) =
member_out_gg(
x1,
x2)
U4_gg(
x1,
x2,
x3,
x4) =
U4_gg(
x1,
x2,
x3,
x4)
[] =
[]
reach_out_ggg(
x1,
x2,
x3) =
reach_out_ggg(
x1,
x2,
x3)
U2_ggg(
x1,
x2,
x3,
x4) =
U2_ggg(
x1,
x2,
x3,
x4)
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
U3_ggg(
x1,
x2,
x3,
x4) =
U3_ggg(
x1,
x2,
x3,
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(55) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(56) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(.(X, .(Y, [])), Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U5_ag(X, H, L, member1_in_ag(X, L))
U5_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
[] =
[]
member1_in_ag(
x1,
x2) =
member1_in_ag(
x2)
member1_out_ag(
x1,
x2) =
member1_out_ag(
x1,
x2)
U5_ag(
x1,
x2,
x3,
x4) =
U5_ag(
x2,
x3,
x4)
REACH_IN_GGG(
x1,
x2,
x3) =
REACH_IN_GGG(
x1,
x2,
x3)
U2_GGG(
x1,
x2,
x3,
x4) =
U2_GGG(
x1,
x2,
x3,
x4)
We have to consider all (P,R,Pi)-chains
(57) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(X, Z, Edges) → U2_GGG(X, Z, Edges, member1_in_ag(Edges))
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(.(H, L)) → U5_ag(H, L, member1_in_ag(L))
U5_ag(H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(59) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
REACH_IN_GGG(
X,
Z,
Edges) →
U2_GGG(
X,
Z,
Edges,
member1_in_ag(
Edges)) at position [3] we obtained the following new rules [LPAR04]:
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y0, y1, .(x0, x1), member1_out_ag(x0, .(x0, x1)))
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y0, y1, .(x0, x1), U5_ag(x0, x1, member1_in_ag(x1)))
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U2_GGG(X, Z, Edges, member1_out_ag(.(X, .(Y, [])), Edges)) → REACH_IN_GGG(Y, Z, Edges)
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y0, y1, .(x0, x1), member1_out_ag(x0, .(x0, x1)))
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y0, y1, .(x0, x1), U5_ag(x0, x1, member1_in_ag(x1)))
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(.(H, L)) → U5_ag(H, L, member1_in_ag(L))
U5_ag(H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(61) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U2_GGG(
X,
Z,
Edges,
member1_out_ag(
.(
X,
.(
Y,
[])),
Edges)) →
REACH_IN_GGG(
Y,
Z,
Edges) we obtained the following new rules [LPAR04]:
U2_GGG(z0, z1, .(.(z0, .(x3, [])), z3), member1_out_ag(.(z0, .(x3, [])), .(.(z0, .(x3, [])), z3))) → REACH_IN_GGG(x3, z1, .(.(z0, .(x3, [])), z3))
U2_GGG(z0, z1, .(z2, z3), member1_out_ag(.(z0, .(x3, [])), .(z2, z3))) → REACH_IN_GGG(x3, z1, .(z2, z3))
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y0, y1, .(x0, x1), member1_out_ag(x0, .(x0, x1)))
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y0, y1, .(x0, x1), U5_ag(x0, x1, member1_in_ag(x1)))
U2_GGG(z0, z1, .(.(z0, .(x3, [])), z3), member1_out_ag(.(z0, .(x3, [])), .(.(z0, .(x3, [])), z3))) → REACH_IN_GGG(x3, z1, .(.(z0, .(x3, [])), z3))
U2_GGG(z0, z1, .(z2, z3), member1_out_ag(.(z0, .(x3, [])), .(z2, z3))) → REACH_IN_GGG(x3, z1, .(z2, z3))
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(.(H, L)) → U5_ag(H, L, member1_in_ag(L))
U5_ag(H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(63) ForwardInstantiation (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
REACH_IN_GGG(
y0,
y1,
.(
x0,
x1)) →
U2_GGG(
y0,
y1,
.(
x0,
x1),
member1_out_ag(
x0,
.(
x0,
x1))) we obtained the following new rules [LPAR04]:
REACH_IN_GGG(x0, x1, .(.(y_2, .(y_3, [])), x3)) → U2_GGG(x0, x1, .(.(y_2, .(y_3, [])), x3), member1_out_ag(.(y_2, .(y_3, [])), .(.(y_2, .(y_3, [])), x3)))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REACH_IN_GGG(y0, y1, .(x0, x1)) → U2_GGG(y0, y1, .(x0, x1), U5_ag(x0, x1, member1_in_ag(x1)))
U2_GGG(z0, z1, .(.(z0, .(x3, [])), z3), member1_out_ag(.(z0, .(x3, [])), .(.(z0, .(x3, [])), z3))) → REACH_IN_GGG(x3, z1, .(.(z0, .(x3, [])), z3))
U2_GGG(z0, z1, .(z2, z3), member1_out_ag(.(z0, .(x3, [])), .(z2, z3))) → REACH_IN_GGG(x3, z1, .(z2, z3))
REACH_IN_GGG(x0, x1, .(.(y_2, .(y_3, [])), x3)) → U2_GGG(x0, x1, .(.(y_2, .(y_3, [])), x3), member1_out_ag(.(y_2, .(y_3, [])), .(.(y_2, .(y_3, [])), x3)))
The TRS R consists of the following rules:
member1_in_ag(.(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(.(H, L)) → U5_ag(H, L, member1_in_ag(L))
U5_ag(H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
The set Q consists of the following terms:
member1_in_ag(x0)
U5_ag(x0, x1, x2)
We have to consider all (P,Q,R)-chains.
(65) 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 =
REACH_IN_GGG(
x0,
x1,
.(
.(
x0,
.(
y_3,
[])),
x3')) evaluates to t =
REACH_IN_GGG(
y_3,
x1,
.(
.(
x0,
.(
y_3,
[])),
x3'))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [y_3 / x0]
Rewriting sequenceREACH_IN_GGG(x0, x1, .(.(x0, .(x0, [])), x3')) →
U2_GGG(
x0,
x1,
.(
.(
x0,
.(
x0,
[])),
x3'),
member1_out_ag(
.(
x0,
.(
x0,
[])),
.(
.(
x0,
.(
x0,
[])),
x3')))
with rule
REACH_IN_GGG(
x0',
x1',
.(
.(
y_2,
.(
y_3,
[])),
x3'')) →
U2_GGG(
x0',
x1',
.(
.(
y_2,
.(
y_3,
[])),
x3''),
member1_out_ag(
.(
y_2,
.(
y_3,
[])),
.(
.(
y_2,
.(
y_3,
[])),
x3''))) at position [] and matcher [
x0' /
x0,
x1' /
x1,
y_2 /
x0,
y_3 /
x0,
x3'' /
x3']
U2_GGG(x0, x1, .(.(x0, .(x0, [])), x3'), member1_out_ag(.(x0, .(x0, [])), .(.(x0, .(x0, [])), x3'))) →
REACH_IN_GGG(
x0,
x1,
.(
.(
x0,
.(
x0,
[])),
x3'))
with rule
U2_GGG(
z0,
z1,
.(
.(
z0,
.(
x3,
[])),
z3),
member1_out_ag(
.(
z0,
.(
x3,
[])),
.(
.(
z0,
.(
x3,
[])),
z3))) →
REACH_IN_GGG(
x3,
z1,
.(
.(
z0,
.(
x3,
[])),
z3))
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.
(66) FALSE