(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.



(29) NO