(0) Obligation:

Clauses:

flat([], []).
flat(.([], T), R) :- flat(T, R).
flat(.(.(H, T), TT), .(H, R)) :- flat(.(T, TT), R).

Queries:

flat(a,g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

flat16([]).
flat16(.([], T17)) :- flat16(T17).
flat1([], []).
flat1(.([], []), []).
flat1(.([], .([], T11)), []) :- flat16(T11).
flat1(.([], []), []).
flat1(.([], .([], T45)), T44) :- flat1(T45, T44).
flat1(.([], .(.(T62, T66), T67)), .(T62, T65)) :- flat1(.(T66, T67), T65).
flat1(.(.(T78, T82), T83), .(T78, T81)) :- flat1(.(T82, T83), T81).
flat1(.(.(T90, []), T106), .(T90, T105)) :- flat1(T106, T105).
flat1(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) :- flat1(.(T119, T120), T118).

Queries:

flat1(a,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:
flat1_in: (f,b)
flat16_in: (f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x6)

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

FLAT1_IN_AG(.([], .([], T11)), []) → U2_AG(T11, flat16_in_a(T11))
FLAT1_IN_AG(.([], .([], T11)), []) → FLAT16_IN_A(T11)
FLAT16_IN_A(.([], T17)) → U1_A(T17, flat16_in_a(T17))
FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)
FLAT1_IN_AG(.([], .([], T45)), T44) → U3_AG(T45, T44, flat1_in_ag(T45, T44))
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_AG(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → U5_AG(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → U6_AG(T90, T106, T105, flat1_in_ag(T106, T105))
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_AG(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x6)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x2)
FLAT16_IN_A(x1)  =  FLAT16_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x3)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x1, x5)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x1, x5)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x1, x4)
U7_AG(x1, x2, x3, x4, x5, x6)  =  U7_AG(x1, x2, x6)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(.([], .([], T11)), []) → U2_AG(T11, flat16_in_a(T11))
FLAT1_IN_AG(.([], .([], T11)), []) → FLAT16_IN_A(T11)
FLAT16_IN_A(.([], T17)) → U1_A(T17, flat16_in_a(T17))
FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)
FLAT1_IN_AG(.([], .([], T45)), T44) → U3_AG(T45, T44, flat1_in_ag(T45, T44))
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_AG(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → U5_AG(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → U6_AG(T90, T106, T105, flat1_in_ag(T106, T105))
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_AG(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x6)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x2)
FLAT16_IN_A(x1)  =  FLAT16_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x3)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x1, x5)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x1, x5)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x1, x4)
U7_AG(x1, x2, x3, x4, x5, x6)  =  U7_AG(x1, x2, x6)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 8 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x6)
FLAT16_IN_A(x1)  =  FLAT16_IN_A

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:

FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)

R is empty.
The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
FLAT16_IN_A(x1)  =  FLAT16_IN_A

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:

FLAT16_IN_AFLAT16_IN_A

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = FLAT16_IN_A evaluates to t =FLAT16_IN_A

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from FLAT16_IN_A to FLAT16_IN_A.



(15) NO

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x6)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)

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:

FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

R is empty.
The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND 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:

FLAT1_IN_AG(.(T62, T65)) → FLAT1_IN_AG(T65)
FLAT1_IN_AG(T44) → FLAT1_IN_AG(T44)
FLAT1_IN_AG(.(T90, .(T115, T118))) → FLAT1_IN_AG(T118)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

FLAT1_IN_AG(.(T62, T65)) → FLAT1_IN_AG(T65)
FLAT1_IN_AG(.(T90, .(T115, T118))) → FLAT1_IN_AG(T118)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1 + 2·x2   
POL(FLAT1_IN_AG(x1)) = 2·x1   

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(T44) → FLAT1_IN_AG(T44)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(23) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = FLAT1_IN_AG(T44) evaluates to t =FLAT1_IN_AG(T44)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from FLAT1_IN_AG(T44) to FLAT1_IN_AG(T44).



(24) NO

(25) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
flat1_in: (f,b)
flat16_in: (f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x2, x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x4, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x4, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x3, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x5, x6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(26) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x2, x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x4, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x4, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x3, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x5, x6)

(27) 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:

FLAT1_IN_AG(.([], .([], T11)), []) → U2_AG(T11, flat16_in_a(T11))
FLAT1_IN_AG(.([], .([], T11)), []) → FLAT16_IN_A(T11)
FLAT16_IN_A(.([], T17)) → U1_A(T17, flat16_in_a(T17))
FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)
FLAT1_IN_AG(.([], .([], T45)), T44) → U3_AG(T45, T44, flat1_in_ag(T45, T44))
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_AG(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → U5_AG(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → U6_AG(T90, T106, T105, flat1_in_ag(T106, T105))
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_AG(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x2, x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x4, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x4, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x3, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x5, x6)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x2)
FLAT16_IN_A(x1)  =  FLAT16_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x1, x4, x5)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x1, x4, x5)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x1, x3, x4)
U7_AG(x1, x2, x3, x4, x5, x6)  =  U7_AG(x1, x2, x5, x6)

We have to consider all (P,R,Pi)-chains

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(.([], .([], T11)), []) → U2_AG(T11, flat16_in_a(T11))
FLAT1_IN_AG(.([], .([], T11)), []) → FLAT16_IN_A(T11)
FLAT16_IN_A(.([], T17)) → U1_A(T17, flat16_in_a(T17))
FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)
FLAT1_IN_AG(.([], .([], T45)), T44) → U3_AG(T45, T44, flat1_in_ag(T45, T44))
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_AG(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → U5_AG(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → U6_AG(T90, T106, T105, flat1_in_ag(T106, T105))
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_AG(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x2, x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x4, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x4, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x3, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x5, x6)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x2)
FLAT16_IN_A(x1)  =  FLAT16_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U3_AG(x1, x2, x3)  =  U3_AG(x2, x3)
U4_AG(x1, x2, x3, x4, x5)  =  U4_AG(x1, x4, x5)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x1, x4, x5)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x1, x3, x4)
U7_AG(x1, x2, x3, x4, x5, x6)  =  U7_AG(x1, x2, x5, x6)

We have to consider all (P,R,Pi)-chains

(29) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 8 less nodes.

(30) Complex Obligation (AND)

(31) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x2, x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x4, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x4, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x3, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x5, x6)
FLAT16_IN_A(x1)  =  FLAT16_IN_A

We have to consider all (P,R,Pi)-chains

(32) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(33) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT16_IN_A(.([], T17)) → FLAT16_IN_A(T17)

R is empty.
The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
FLAT16_IN_A(x1)  =  FLAT16_IN_A

We have to consider all (P,R,Pi)-chains

(34) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(35) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLAT16_IN_AFLAT16_IN_A

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(36) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = FLAT16_IN_A evaluates to t =FLAT16_IN_A

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from FLAT16_IN_A to FLAT16_IN_A.



(37) NO

(38) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

The TRS R consists of the following rules:

flat1_in_ag([], []) → flat1_out_ag([], [])
flat1_in_ag(.([], []), []) → flat1_out_ag(.([], []), [])
flat1_in_ag(.([], .([], T11)), []) → U2_ag(T11, flat16_in_a(T11))
flat16_in_a([]) → flat16_out_a([])
flat16_in_a(.([], T17)) → U1_a(T17, flat16_in_a(T17))
U1_a(T17, flat16_out_a(T17)) → flat16_out_a(.([], T17))
U2_ag(T11, flat16_out_a(T11)) → flat1_out_ag(.([], .([], T11)), [])
flat1_in_ag(.([], .([], T45)), T44) → U3_ag(T45, T44, flat1_in_ag(T45, T44))
flat1_in_ag(.([], .(.(T62, T66), T67)), .(T62, T65)) → U4_ag(T62, T66, T67, T65, flat1_in_ag(.(T66, T67), T65))
flat1_in_ag(.(.(T78, T82), T83), .(T78, T81)) → U5_ag(T78, T82, T83, T81, flat1_in_ag(.(T82, T83), T81))
flat1_in_ag(.(.(T90, []), T106), .(T90, T105)) → U6_ag(T90, T106, T105, flat1_in_ag(T106, T105))
flat1_in_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → U7_ag(T90, T115, T119, T120, T118, flat1_in_ag(.(T119, T120), T118))
U7_ag(T90, T115, T119, T120, T118, flat1_out_ag(.(T119, T120), T118)) → flat1_out_ag(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118)))
U6_ag(T90, T106, T105, flat1_out_ag(T106, T105)) → flat1_out_ag(.(.(T90, []), T106), .(T90, T105))
U5_ag(T78, T82, T83, T81, flat1_out_ag(.(T82, T83), T81)) → flat1_out_ag(.(.(T78, T82), T83), .(T78, T81))
U4_ag(T62, T66, T67, T65, flat1_out_ag(.(T66, T67), T65)) → flat1_out_ag(.([], .(.(T62, T66), T67)), .(T62, T65))
U3_ag(T45, T44, flat1_out_ag(T45, T44)) → flat1_out_ag(.([], .([], T45)), T44)

The argument filtering Pi contains the following mapping:
flat1_in_ag(x1, x2)  =  flat1_in_ag(x2)
[]  =  []
flat1_out_ag(x1, x2)  =  flat1_out_ag(x1, x2)
U2_ag(x1, x2)  =  U2_ag(x2)
flat16_in_a(x1)  =  flat16_in_a
flat16_out_a(x1)  =  flat16_out_a(x1)
U1_a(x1, x2)  =  U1_a(x2)
U3_ag(x1, x2, x3)  =  U3_ag(x2, x3)
.(x1, x2)  =  .(x1, x2)
U4_ag(x1, x2, x3, x4, x5)  =  U4_ag(x1, x4, x5)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x1, x4, x5)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x1, x3, x4)
U7_ag(x1, x2, x3, x4, x5, x6)  =  U7_ag(x1, x2, x5, x6)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(39) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(40) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(.([], .(.(T62, T66), T67)), .(T62, T65)) → FLAT1_IN_AG(.(T66, T67), T65)
FLAT1_IN_AG(.([], .([], T45)), T44) → FLAT1_IN_AG(T45, T44)
FLAT1_IN_AG(.(.(T78, T82), T83), .(T78, T81)) → FLAT1_IN_AG(.(T82, T83), T81)
FLAT1_IN_AG(.(.(T90, []), T106), .(T90, T105)) → FLAT1_IN_AG(T106, T105)
FLAT1_IN_AG(.(.(T90, .(T115, T119)), T120), .(T90, .(T115, T118))) → FLAT1_IN_AG(.(T119, T120), T118)

R is empty.
The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
FLAT1_IN_AG(x1, x2)  =  FLAT1_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(41) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(.(T62, T65)) → FLAT1_IN_AG(T65)
FLAT1_IN_AG(T44) → FLAT1_IN_AG(T44)
FLAT1_IN_AG(.(T90, .(T115, T118))) → FLAT1_IN_AG(T118)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(43) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

FLAT1_IN_AG(.(T62, T65)) → FLAT1_IN_AG(T65)
FLAT1_IN_AG(.(T90, .(T115, T118))) → FLAT1_IN_AG(T118)
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1 + 2·x2   
POL(FLAT1_IN_AG(x1)) = 2·x1   

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FLAT1_IN_AG(T44) → FLAT1_IN_AG(T44)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(45) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = FLAT1_IN_AG(T44) evaluates to t =FLAT1_IN_AG(T44)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from FLAT1_IN_AG(T44) to FLAT1_IN_AG(T44).



(46) NO