(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) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph.
(2) Obligation:
Clauses:member12(T63, T64, .(.(T63, .(T64, [])), T65)).
member12(T74, T75, .(T76, T77)) :- member12(T74, T75, T77).
member124(T114, X112, .(.(T114, .(X112, [])), T115)).
member124(T122, X126, .(T123, T124)) :- member124(T122, X126, T124).
reach1(T22, T23, .(.(T22, .(T23, [])), T24)).
reach1(T41, T42, .(T43, T44)) :- member12(T41, T42, T44).
reach1(T94, T95, T96) :- member124(T94, X85, T96).
reach1(T94, T95, T96) :- ','(member124(T94, T101, T96), reach1(T101, T95, T96)).
Queries:
reach1(g,g,g).
(3) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:reach1_in: (b,b,b)
member12_in: (b,b,b)
member124_in: (b,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_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)
member12_out_ggg(x1, x2, x3) = member12_out_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)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, 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)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_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)
member12_out_ggg(x1, x2, x3) = member12_out_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)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, 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)
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:Pi DP problem:
The TRS P consists of the following rules:
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, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_GGG(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_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)
member12_out_ggg(x1, x2, x3) = member12_out_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)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, 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)
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
(6) 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, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_GGG(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_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)
member12_out_ggg(x1, x2, x3) = member12_out_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)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, 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)
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
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 7 less nodes.(8) Complex Obligation (AND)
(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)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_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)
member12_out_ggg(x1, x2, x3) = member12_out_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)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, 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)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(11) 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
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(13) 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.
(14) 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
(15) YES
(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)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_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)
member12_out_ggg(x1, x2, x3) = member12_out_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)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, 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)
MEMBER12_IN_GGG(x1, x2, x3) = MEMBER12_IN_GGG(x1, x2, x3)
We have to consider all (P,R,Pi)-chains
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(18) 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
(19) PiDPToQDPProof (EQUIVALENT transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(20) 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.
(21) 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
(22) YES
(23) Obligation:
Pi DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_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)
member12_out_ggg(x1, x2, x3) = member12_out_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)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, 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)
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
(24) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(25) Obligation:
Pi DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5) = U2_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
(26) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(27) Obligation:
Q DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member124_in_gag(T94, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member124_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, .(T123, T124)) → U2_gag(T122, T123, T124, member124_in_gag(T122, T124))
U2_gag(T122, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
The set Q consists of the following terms:
member124_in_gag(x0, x1)
U2_gag(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(28) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member124_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), member124_out_gag(x0, x1, .(.(x0, .(x1, [])), x2)))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(x0, y1, .(x1, x2), U2_gag(x0, x1, x2, member124_in_gag(x0, x2)))
(29) Obligation:
Q DP problem:The TRS P consists of the following rules:
U5_GGG(T94, T95, T96, member124_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), member124_out_gag(x0, x1, .(.(x0, .(x1, [])), x2)))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(x0, y1, .(x1, x2), U2_gag(x0, x1, x2, member124_in_gag(x0, x2)))
The TRS R consists of the following rules:
member124_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, .(T123, T124)) → U2_gag(T122, T123, T124, member124_in_gag(T122, T124))
U2_gag(T122, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
The set Q consists of the following terms:
member124_in_gag(x0, x1)
U2_gag(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(30) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule U5_GGG(T94, T95, T96, member124_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), member124_out_gag(z0, z2, .(.(z0, .(z2, [])), z3))) → REACH1_IN_GGG(z2, z1, .(.(z0, .(z2, [])), z3))
U5_GGG(z0, z1, .(z2, z3), member124_out_gag(z0, x3, .(z2, z3))) → REACH1_IN_GGG(x3, z1, .(z2, z3))
(31) 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), member124_out_gag(x0, x1, .(.(x0, .(x1, [])), x2)))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(x0, y1, .(x1, x2), U2_gag(x0, x1, x2, member124_in_gag(x0, x2)))
U5_GGG(z0, z1, .(.(z0, .(z2, [])), z3), member124_out_gag(z0, z2, .(.(z0, .(z2, [])), z3))) → REACH1_IN_GGG(z2, z1, .(.(z0, .(z2, [])), z3))
U5_GGG(z0, z1, .(z2, z3), member124_out_gag(z0, x3, .(z2, z3))) → REACH1_IN_GGG(x3, z1, .(z2, z3))
The TRS R consists of the following rules:
member124_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, .(T123, T124)) → U2_gag(T122, T123, T124, member124_in_gag(T122, T124))
U2_gag(T122, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
The set Q consists of the following terms:
member124_in_gag(x0, x1)
U2_gag(x0, x1, x2, x3)
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 = U5_GGG(z2, z1, .(.(z2, .(z2, [])), z3), member124_out_gag(z2, z2, .(.(z2, .(z2, [])), z3))) evaluates to t =U5_GGG(z2, z1, .(.(z2, .(z2, [])), z3), member124_out_gag(z2, z2, .(.(z2, .(z2, [])), z3)))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequence
U5_GGG(z2, z1, .(.(z2, .(z2, [])), z3), member124_out_gag(z2, z2, .(.(z2, .(z2, [])), z3))) → REACH1_IN_GGG(z2, z1, .(.(z2, .(z2, [])), z3))
with rule U5_GGG(z0, z1', .(.(z0, .(z2', [])), z3'), member124_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), member124_out_gag(z2, z2, .(.(z2, .(z2, [])), z3)))
with rule REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(x0, y1, .(.(x0, .(x1, [])), x2), member124_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.
(33) NO
(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:reach1_in: (b,b,b)
member12_in: (b,b,b)
member124_in: (b,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_ggg
U3_ggg(x1, x2, x3, x4, x5) = U3_ggg(x5)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3) = member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5) = U1_ggg(x5)
U4_ggg(x1, x2, x3, x4) = U4_ggg(x4)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
U5_ggg(x1, x2, x3, x4) = U5_ggg(x2, x3, x4)
U6_ggg(x1, x2, x3, x4) = U6_ggg(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:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_ggg
U3_ggg(x1, x2, x3, x4, x5) = U3_ggg(x5)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3) = member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5) = U1_ggg(x5)
U4_ggg(x1, x2, x3, x4) = U4_ggg(x4)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
U5_ggg(x1, x2, x3, x4) = U5_ggg(x2, x3, x4)
U6_ggg(x1, x2, x3, x4) = U6_ggg(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:
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, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_GGG(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_ggg
U3_ggg(x1, x2, x3, x4, x5) = U3_ggg(x5)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3) = member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5) = U1_ggg(x5)
U4_ggg(x1, x2, x3, x4) = U4_ggg(x4)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
U5_ggg(x1, x2, x3, x4) = U5_ggg(x2, x3, x4)
U6_ggg(x1, x2, x3, x4) = U6_ggg(x4)
REACH1_IN_GGG(x1, x2, x3) = REACH1_IN_GGG(x1, x2, x3)
U3_GGG(x1, x2, x3, x4, x5) = U3_GGG(x5)
MEMBER12_IN_GGG(x1, x2, x3) = MEMBER12_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5) = U1_GGG(x5)
U4_GGG(x1, x2, x3, x4) = U4_GGG(x4)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5) = U2_GAG(x5)
U5_GGG(x1, x2, x3, x4) = U5_GGG(x2, x3, x4)
U6_GGG(x1, x2, x3, x4) = U6_GGG(x4)
We have to consider all (P,R,Pi)-chains
(37) 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, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_GGG(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_ggg
U3_ggg(x1, x2, x3, x4, x5) = U3_ggg(x5)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3) = member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5) = U1_ggg(x5)
U4_ggg(x1, x2, x3, x4) = U4_ggg(x4)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
U5_ggg(x1, x2, x3, x4) = U5_ggg(x2, x3, x4)
U6_ggg(x1, x2, x3, x4) = U6_ggg(x4)
REACH1_IN_GGG(x1, x2, x3) = REACH1_IN_GGG(x1, x2, x3)
U3_GGG(x1, x2, x3, x4, x5) = U3_GGG(x5)
MEMBER12_IN_GGG(x1, x2, x3) = MEMBER12_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5) = U1_GGG(x5)
U4_GGG(x1, x2, x3, x4) = U4_GGG(x4)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5) = U2_GAG(x5)
U5_GGG(x1, x2, x3, x4) = U5_GGG(x2, x3, x4)
U6_GGG(x1, x2, x3, x4) = U6_GGG(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 7 less nodes.(39) Complex Obligation (AND)
(40) 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:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_ggg
U3_ggg(x1, x2, x3, x4, x5) = U3_ggg(x5)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3) = member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5) = U1_ggg(x5)
U4_ggg(x1, x2, x3, x4) = U4_ggg(x4)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
U5_ggg(x1, x2, x3, x4) = U5_ggg(x2, x3, x4)
U6_ggg(x1, x2, x3, x4) = U6_ggg(x4)
MEMBER124_IN_GAG(x1, x2, x3) = MEMBER124_IN_GAG(x1, x3)
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:
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
(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:
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.
(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:
- MEMBER124_IN_GAG(T122, .(T123, T124)) → MEMBER124_IN_GAG(T122, T124)
The graph contains the following edges 1 >= 1, 2 > 2
(46) YES
(47) 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:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_ggg
U3_ggg(x1, x2, x3, x4, x5) = U3_ggg(x5)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3) = member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5) = U1_ggg(x5)
U4_ggg(x1, x2, x3, x4) = U4_ggg(x4)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
U5_ggg(x1, x2, x3, x4) = U5_ggg(x2, x3, x4)
U6_ggg(x1, x2, x3, x4) = U6_ggg(x4)
MEMBER12_IN_GGG(x1, x2, x3) = MEMBER12_IN_GGG(x1, x2, x3)
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:
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
(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:
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.
(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:
- 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
(53) YES
(54) Obligation:
Pi DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
reach1_in_ggg(T22, T23, .(.(T22, .(T23, [])), T24)) → reach1_out_ggg(T22, T23, .(.(T22, .(T23, [])), T24))
reach1_in_ggg(T41, T42, .(T43, T44)) → U3_ggg(T41, T42, T43, T44, member12_in_ggg(T41, T42, T44))
member12_in_ggg(T63, T64, .(.(T63, .(T64, [])), T65)) → member12_out_ggg(T63, T64, .(.(T63, .(T64, [])), T65))
member12_in_ggg(T74, T75, .(T76, T77)) → U1_ggg(T74, T75, T76, T77, member12_in_ggg(T74, T75, T77))
U1_ggg(T74, T75, T76, T77, member12_out_ggg(T74, T75, T77)) → member12_out_ggg(T74, T75, .(T76, T77))
U3_ggg(T41, T42, T43, T44, member12_out_ggg(T41, T42, T44)) → reach1_out_ggg(T41, T42, .(T43, T44))
reach1_in_ggg(T94, T95, T96) → U4_ggg(T94, T95, T96, member124_in_gag(T94, X85, T96))
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
U4_ggg(T94, T95, T96, member124_out_gag(T94, X85, T96)) → reach1_out_ggg(T94, T95, T96)
reach1_in_ggg(T94, T95, T96) → U5_ggg(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_ggg(T94, T95, T96, member124_out_gag(T94, T101, T96)) → U6_ggg(T94, T95, T96, reach1_in_ggg(T101, T95, T96))
U6_ggg(T94, T95, T96, reach1_out_ggg(T101, T95, T96)) → reach1_out_ggg(T94, T95, T96)
The argument filtering Pi contains the following mapping:
reach1_in_ggg(x1, x2, x3) = reach1_in_ggg(x1, x2, x3)
.(x1, x2) = .(x1, x2)
[] = []
reach1_out_ggg(x1, x2, x3) = reach1_out_ggg
U3_ggg(x1, x2, x3, x4, x5) = U3_ggg(x5)
member12_in_ggg(x1, x2, x3) = member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3) = member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5) = U1_ggg(x5)
U4_ggg(x1, x2, x3, x4) = U4_ggg(x4)
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
U5_ggg(x1, x2, x3, x4) = U5_ggg(x2, x3, x4)
U6_ggg(x1, x2, x3, x4) = U6_ggg(x4)
REACH1_IN_GGG(x1, x2, x3) = REACH1_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4) = U5_GGG(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:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T94, T95, T96, member124_in_gag(T94, T101, T96))
U5_GGG(T94, T95, T96, member124_out_gag(T94, T101, T96)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member124_in_gag(T114, X112, .(.(T114, .(X112, [])), T115)) → member124_out_gag(T114, X112, .(.(T114, .(X112, [])), T115))
member124_in_gag(T122, X126, .(T123, T124)) → U2_gag(T122, X126, T123, T124, member124_in_gag(T122, X126, T124))
U2_gag(T122, X126, T123, T124, member124_out_gag(T122, X126, T124)) → member124_out_gag(T122, X126, .(T123, T124))
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
[] = []
member124_in_gag(x1, x2, x3) = member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3) = member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x5)
REACH1_IN_GGG(x1, x2, x3) = REACH1_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4) = U5_GGG(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:
REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T95, T96, member124_in_gag(T94, T96))
U5_GGG(T95, T96, member124_out_gag(T101)) → REACH1_IN_GGG(T101, T95, T96)
The TRS R consists of the following rules:
member124_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member124_out_gag(X112)
member124_in_gag(T122, .(T123, T124)) → U2_gag(member124_in_gag(T122, T124))
U2_gag(member124_out_gag(X126)) → member124_out_gag(X126)
The set Q consists of the following terms:
member124_in_gag(x0, x1)
U2_gag(x0)
We have to consider all (P,Q,R)-chains.
(59) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule REACH1_IN_GGG(T94, T95, T96) → U5_GGG(T95, T96, member124_in_gag(T94, T96)) at position [2] we obtained the following new rules [LPAR04]:
REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(y1, .(.(x0, .(x1, [])), x2), member124_out_gag(x1))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(y1, .(x1, x2), U2_gag(member124_in_gag(x0, x2)))
(60) Obligation:
Q DP problem:The TRS P consists of the following rules:
U5_GGG(T95, T96, member124_out_gag(T101)) → REACH1_IN_GGG(T101, T95, T96)
REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(y1, .(.(x0, .(x1, [])), x2), member124_out_gag(x1))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(y1, .(x1, x2), U2_gag(member124_in_gag(x0, x2)))
The TRS R consists of the following rules:
member124_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member124_out_gag(X112)
member124_in_gag(T122, .(T123, T124)) → U2_gag(member124_in_gag(T122, T124))
U2_gag(member124_out_gag(X126)) → member124_out_gag(X126)
The set Q consists of the following terms:
member124_in_gag(x0, x1)
U2_gag(x0)
We have to consider all (P,Q,R)-chains.
(61) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule U5_GGG(T95, T96, member124_out_gag(T101)) → REACH1_IN_GGG(T101, T95, T96) we obtained the following new rules [LPAR04]:
U5_GGG(z1, .(.(z0, .(z2, [])), z3), member124_out_gag(z2)) → REACH1_IN_GGG(z2, z1, .(.(z0, .(z2, [])), z3))
U5_GGG(z1, .(z2, z3), member124_out_gag(x2)) → REACH1_IN_GGG(x2, z1, .(z2, z3))
(62) Obligation:
Q DP problem:The TRS P consists of the following rules:
REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(y1, .(.(x0, .(x1, [])), x2), member124_out_gag(x1))
REACH1_IN_GGG(x0, y1, .(x1, x2)) → U5_GGG(y1, .(x1, x2), U2_gag(member124_in_gag(x0, x2)))
U5_GGG(z1, .(.(z0, .(z2, [])), z3), member124_out_gag(z2)) → REACH1_IN_GGG(z2, z1, .(.(z0, .(z2, [])), z3))
U5_GGG(z1, .(z2, z3), member124_out_gag(x2)) → REACH1_IN_GGG(x2, z1, .(z2, z3))
The TRS R consists of the following rules:
member124_in_gag(T114, .(.(T114, .(X112, [])), T115)) → member124_out_gag(X112)
member124_in_gag(T122, .(T123, T124)) → U2_gag(member124_in_gag(T122, T124))
U2_gag(member124_out_gag(X126)) → member124_out_gag(X126)
The set Q consists of the following terms:
member124_in_gag(x0, x1)
U2_gag(x0)
We have to consider all (P,Q,R)-chains.
(63) 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(z1, .(.(z2, .(z2, [])), z3), member124_out_gag(z2)) evaluates to t =U5_GGG(z1, .(.(z2, .(z2, [])), z3), member124_out_gag(z2))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [ ]
Rewriting sequence
U5_GGG(z1, .(.(z2, .(z2, [])), z3), member124_out_gag(z2)) → REACH1_IN_GGG(z2, z1, .(.(z2, .(z2, [])), z3))
with rule U5_GGG(z1', .(.(z0, .(z2', [])), z3'), member124_out_gag(z2')) → REACH1_IN_GGG(z2', z1', .(.(z0, .(z2', [])), z3')) at position [] and matcher [z1' / z1, z0 / z2, z2' / z2, z3' / z3]
REACH1_IN_GGG(z2, z1, .(.(z2, .(z2, [])), z3)) → U5_GGG(z1, .(.(z2, .(z2, [])), z3), member124_out_gag(z2))
with rule REACH1_IN_GGG(x0, y1, .(.(x0, .(x1, [])), x2)) → U5_GGG(y1, .(.(x0, .(x1, [])), x2), member124_out_gag(x1))
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.