(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) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:member12(T74, T75, .(T76, T77)) :- member12(T74, T75, T77).
member124(T122, X126, .(T123, T124)) :- member124(T122, X126, T124).
reach1(T41, T42, .(T43, T44)) :- member12(T41, T42, T44).
reach1(T94, T95, T96) :- member124(T94, X85, T96).
reach1(T94, T95, T96) :- ','(member1c24(T94, T101, T96), reach1(T101, T95, T96)).
Clauses:
memberc12(T63, T64, .(.(T63, .(T64, [])), T65)).
memberc12(T74, T75, .(T76, T77)) :- memberc12(T74, T75, T77).
reachc1(T22, T23, .(.(T22, .(T23, [])), T24)).
reachc1(T41, T42, .(T43, T44)) :- memberc12(T41, T42, T44).
reachc1(T94, T95, T96) :- ','(member1c24(T94, T101, T96), reachc1(T101, T95, T96)).
member1c24(T114, X112, .(.(T114, .(X112, [])), T115)).
member1c24(T122, X126, .(T123, T124)) :- member1c24(T122, X126, T124).
Afs:
reach1(x1, x2, x3) = reach1(x1, x2, x3)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:reach1_in: (b,b,b)
member12_in: (b,b,b)
member124_in: (b,f,b)
member1c24_in: (b,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
REACH1_IN_GGG(T41, T42, .(T43, T44)) → U3_GGG(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
REACH1_IN_GGG(T41, T42, .(T43, T44)) → MEMBER12_IN_GGG(T41, T42, T44)
MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → U1_GGG(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → MEMBER12_IN_GGG(T74, T75, T77)
REACH1_IN_GGG(T94, T95, T96) → U4_GGG(T94, T95, T96, member124_in_gag(T94, X85, T96))
REACH1_IN_GGG(T94, T95, T96) → MEMBER124_IN_GAG(T94, X85, T96)
MEMBER124_IN_GAG(T122, X126, .(T123, T124)) → U2_GAG(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
MEMBER124_IN_GAG(T122, X126, .(T123, T124)) → MEMBER124_IN_GAG(T122, X126, T124)
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member1c24_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → U6_GGG(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member1c24_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, X126, .(T123, T124)) → U12_gag(T122, X126, T123, T124, member1c24_in_gag(T122, X126, T124))
U12_gag(T122, X126, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member1c24_in_gag(x1, x2, x3) = member1c24_in_gag(x1, x3)
[] = []
member1c24_out_gag(x1, x2, x3) = member1c24_out_gag(x1, x2, x3)
U12_gag(x1, x2, x3, x4, x5) = U12_gag(x1, x3, x4, x5)
REACH1_IN_GGG(x1, x2, x3) = REACH1_IN_GGG(x1, x2, x3)
U3_GGG(x1, x2, x3, x4, x5) = U3_GGG(x1, x2, x3, x4, x5)
MEMBER12_IN_GGG(x1, x2, x3) = MEMBER12_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5) = U1_GGG(x1, x2, x3, x4, x5)
U4_GGG(x1, x2, x3, x4) = U4_GGG(x1, x2, x3, x4)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5) = U2_GAG(x1, x3, x4, x5)
U5_GGG(x1, x2, x3, x4) = U5_GGG(x1, x2, x3, x4)
U6_GGG(x1, x2, x3, x4) = U6_GGG(x1, x2, x3, x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(T41, T42, .(T43, T44)) → U3_GGG(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
REACH1_IN_GGG(T41, T42, .(T43, T44)) → MEMBER12_IN_GGG(T41, T42, T44)
MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → U1_GGG(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → MEMBER12_IN_GGG(T74, T75, T77)
REACH1_IN_GGG(T94, T95, T96) → U4_GGG(T94, T95, T96, member124_in_gag(T94, X85, T96))
REACH1_IN_GGG(T94, T95, T96) → MEMBER124_IN_GAG(T94, X85, T96)
MEMBER124_IN_GAG(T122, X126, .(T123, T124)) → U2_GAG(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
MEMBER124_IN_GAG(T122, X126, .(T123, T124)) → MEMBER124_IN_GAG(T122, X126, T124)
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member1c24_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → U6_GGG(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member1c24_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, X126, .(T123, T124)) → U12_gag(T122, X126, T123, T124, member1c24_in_gag(T122, X126, T124))
U12_gag(T122, X126, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member1c24_in_gag(x1, x2, x3) = member1c24_in_gag(x1, x3)
[] = []
member1c24_out_gag(x1, x2, x3) = member1c24_out_gag(x1, x2, x3)
U12_gag(x1, x2, x3, x4, x5) = U12_gag(x1, x3, x4, x5)
REACH1_IN_GGG(x1, x2, x3) = REACH1_IN_GGG(x1, x2, x3)
U3_GGG(x1, x2, x3, x4, x5) = U3_GGG(x1, x2, x3, x4, x5)
MEMBER12_IN_GGG(x1, x2, x3) = MEMBER12_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5) = U1_GGG(x1, x2, x3, x4, x5)
U4_GGG(x1, x2, x3, x4) = U4_GGG(x1, x2, x3, x4)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5) = U2_GAG(x1, x3, x4, x5)
U5_GGG(x1, x2, x3, x4) = U5_GGG(x1, x2, x3, x4)
U6_GGG(x1, x2, x3, x4) = U6_GGG(x1, x2, x3, 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 7 less nodes.(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:The TRS P consists of the following rules:
MEMBER124_IN_GAG(T122, X126, .(T123, T124)) → MEMBER124_IN_GAG(T122, X126, T124)
The TRS R consists of the following rules:
member1c24_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, X126, .(T123, T124)) → U12_gag(T122, X126, T123, T124, member1c24_in_gag(T122, X126, T124))
U12_gag(T122, X126, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
member1c24_in_gag(x1, x2, x3) = member1c24_in_gag(x1, x3)
[] = []
member1c24_out_gag(x1, x2, x3) = member1c24_out_gag(x1, x2, x3)
U12_gag(x1, x2, x3, x4, x5) = U12_gag(x1, x3, x4, x5)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
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:
MEMBER124_IN_GAG(T122, X126, .(T123, T124)) → MEMBER124_IN_GAG(T122, X126, T124)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
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:
MEMBER124_IN_GAG(T122, .(T123, T124)) → MEMBER124_IN_GAG(T122, T124)
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:
- MEMBER124_IN_GAG(T122, .(T123, T124)) → MEMBER124_IN_GAG(T122, T124)
The graph contains the following edges 1 >= 1, 2 > 2
(13) YES
(14) Obligation:
Pi DP problem:The TRS P consists of the following rules:
MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → MEMBER12_IN_GGG(T74, T75, T77)
The TRS R consists of the following rules:
member1c24_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, X126, .(T123, T124)) → U12_gag(T122, X126, T123, T124, member1c24_in_gag(T122, X126, T124))
U12_gag(T122, X126, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
member1c24_in_gag(x1, x2, x3) = member1c24_in_gag(x1, x3)
[] = []
member1c24_out_gag(x1, x2, x3) = member1c24_out_gag(x1, x2, x3)
U12_gag(x1, x2, x3, x4, x5) = U12_gag(x1, x3, x4, x5)
MEMBER12_IN_GGG(x1, x2, x3) = MEMBER12_IN_GGG(x1, x2, x3)
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:
MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → MEMBER12_IN_GGG(T74, T75, T77)
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:
MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → MEMBER12_IN_GGG(T74, T75, T77)
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:
- MEMBER12_IN_GGG(T74, T75, .(T76, T77)) → MEMBER12_IN_GGG(T74, T75, T77)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
(20) YES
(21) Obligation:
Pi DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member1c24_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member1c24_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, X126, .(T123, T124)) → U12_gag(T122, X126, T123, T124, member1c24_in_gag(T122, X126, T124))
U12_gag(T122, X126, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
member1c24_in_gag(x1, x2, x3) = member1c24_in_gag(x1, x3)
[] = []
member1c24_out_gag(x1, x2, x3) = member1c24_out_gag(x1, x2, x3)
U12_gag(x1, x2, x3, x4, x5) = U12_gag(x1, x3, x4, x5)
REACH1_IN_GGG(x1, x2, x3) = REACH1_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4) = U5_GGG(x1, x2, x3, x4)
We have to consider all (P,R,Pi)-chains
(22) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(23) Obligation:
Q DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member1c24_in_gag(T94, T96))
U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member1c24_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, .(T123, T124)) → U12_gag(T122, T123, T124, member1c24_in_gag(T122, T124))
U12_gag(T122, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The set Q consists of the following terms:
member1c24_in_gag(x0, x1)
U12_gag(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(24) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member1c24_in_gag(T94, T96)) at position [3] we obtained the following new rules [LPAR04]:
REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(x0, y1, .(.(x0, .(x1, [])), x2), member1c24_out_gag(x0, x1, .(.(x0, .(x1, [])), x2)))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(x0, y1, .(x1, x2), U12_gag(x0, x1, x2, member1c24_in_gag(x0, x2)))
(25) Obligation:
Q DP problem:The TRS P consists of the following rules:
U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(x0, y1, .(.(x0, .(x1, [])), x2), member1c24_out_gag(x0, x1, .(.(x0, .(x1, [])), x2)))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(x0, y1, .(x1, x2), U12_gag(x0, x1, x2, member1c24_in_gag(x0, x2)))
The TRS R consists of the following rules:
member1c24_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, .(T123, T124)) → U12_gag(T122, T123, T124, member1c24_in_gag(T122, T124))
U12_gag(T122, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The set Q consists of the following terms:
member1c24_in_gag(x0, x1)
U12_gag(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(26) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule U5_GGG(T94, T95, T96, member1c24_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96) we obtained the following new rules [LPAR04]:
U5_GGG(z0, z1, .(.(z0, .(z2, [])), z3), member1c24_out_gag(z0, z2, .(.(z0, .(z2, [])), z3))) → REACH1_IN_GGG(z2, z1, .(.(z0, .(z2, [])), z3))
U5_GGG(z0, z1, .(z2, z3), member1c24_out_gag(z0, x3, .(z2, z3))) → REACH1_IN_GGG(x3, z1, .(z2, z3))
(27) Obligation:
Q DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(x0, y1, .(.(x0, .(x1, [])), x2), member1c24_out_gag(x0, x1, .(.(x0, .(x1, [])), x2)))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(x0, y1, .(x1, x2), U12_gag(x0, x1, x2, member1c24_in_gag(x0, x2)))
U5_GGG(z0, z1, .(.(z0, .(z2, [])), z3), member1c24_out_gag(z0, z2, .(.(z0, .(z2, [])), z3))) → REACH1_IN_GGG(z2, z1, .(.(z0, .(z2, [])), z3))
U5_GGG(z0, z1, .(z2, z3), member1c24_out_gag(z0, x3, .(z2, z3))) → REACH1_IN_GGG(x3, z1, .(z2, z3))
The TRS R consists of the following rules:
member1c24_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member1c24_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member1c24_in_gag(T122, .(T123, T124)) → U12_gag(T122, T123, T124, member1c24_in_gag(T122, T124))
U12_gag(T122, T123, T124, member1c24_out_gag(T122, X126, T124)) → member1c24_out_gag(T122, X126, .(T123, T124))
The set Q consists of the following terms:
member1c24_in_gag(x0, x1)
U12_gag(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(28) 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 = U5_GGG(z2, z1, .(.(z2, .(z2, [])), z3), member1c24_out_gag(z2, z2, .(.(z2, .(z2, [])), z3))) evaluates to t =U5_GGG(z2, z1, .(.(z2, .(z2, [])), z3), member1c24_out_gag(z2, z2, .(.(z2, .(z2, [])), z3)))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
U5_GGG(z2, z1, .(.(z2, .(z2, [])), z3), member1c24_out_gag(z2, z2, .(.(z2, .(z2, [])), z3))) → REACH1_IN_GGG(z2, z1, .(.(z2, .(z2, [])), z3))
with rule U5_GGG(z0, z1', .(.(z0, .(z2', [])), z3'), member1c24_out_gag(z0, z2', .(.(z0, .(z2', [])), z3'))) → REACH1_IN_GGG(z2', z1', .(.(z0, .(z2', [])), z3')) at position [] and matcher [z0 / z2, z1' / z1, z2' / z2, z3' / z3]
REACH1_IN_GGG(z2, z1, .(.(z2, .(z2, [])), z3)) → U5_GGG(z2, z1, .(.(z2, .(z2, [])), z3), member1c24_out_gag(z2, z2, .(.(z2, .(z2, [])), z3)))
with rule REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(x0, y1, .(.(x0, .(x1, [])), x2), member1c24_out_gag(x0, x1, .(.(x0, .(x1, [])), x2)))
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.