Left Termination of the query pattern ordered_in_1(g) w.r.t. the given Prolog program could not be shown:

(0) Obligation:

Clauses:

ordered([]) :- !.
ordered(.(X1, [])) :- !.
ordered(Xs) :- ','(head(Xs, X), ','(tail(Xs, Ys), ','(head(Ys, Y), ','(tail(Ys, Zs), ','(less(X, s(Y)), ordered(.(Y, Zs))))))).
head([], X2).
head(.(X, X3), X).
tail([], []).
tail(.(X4, Xs), Xs).
less(0, Y) :- ','(!, eq(Y, s(X5))).
less(X, Y) :- ','(p(X, Px), ','(p(Y, Py), less(Px, Py))).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

ordered(g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

ordered([]) :- true.
ordered(.(X1, [])) :- true.
ordered(Xs) :- ','(head(Xs, X), ','(tail(Xs, Ys), ','(head(Ys, Y), ','(tail(Ys, Zs), ','(less(X, s(Y)), ordered(.(Y, Zs))))))).
head([], X2).
head(.(X, X3), X).
tail([], []).
tail(.(X4, Xs), Xs).
less(0, Y) :- eq(Y, s(X5)).
less(X, Y) :- ','(p(X, Px), ','(p(Y, Py), less(Px, Py))).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

ordered(g).

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

ordered([]) :- true.
ordered(.(X1, [])) :- true.
ordered(Xs) :- ','(head(Xs, X), ','(tail(Xs, Ys), ','(head(Ys, Y), ','(tail(Ys, Zs), ','(less(X, s(Y)), ordered(.(Y, Zs))))))).
head([], X2).
head(.(X, X3), X).
tail([], []).
tail(.(X4, Xs), Xs).
less(0, Y) :- eq(Y, s(X5)).
less(X, Y) :- ','(p(X, Px), ','(p(Y, Py), less(Px, Py))).
p(0, 0).
p(s(X), X).
eq(X, X).
true.

Queries:

ordered(g).

(5) PrologToPiTRSProof (SOUND transformation)

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

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g(x1)
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x1, x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x1, x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x1, x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x1, x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

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

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g(x1)
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x1, x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x1, x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x1, x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x1, x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)

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

ORDERED_IN_G([]) → U1_G(true_in_)
ORDERED_IN_G([]) → TRUE_IN_
ORDERED_IN_G(.(X1, [])) → U2_G(X1, true_in_)
ORDERED_IN_G(.(X1, [])) → TRUE_IN_
ORDERED_IN_G(Xs) → U3_G(Xs, head_in_ga(Xs, X))
ORDERED_IN_G(Xs) → HEAD_IN_GA(Xs, X)
U3_G(Xs, head_out_ga(Xs, X)) → U4_G(Xs, X, tail_in_ga(Xs, Ys))
U3_G(Xs, head_out_ga(Xs, X)) → TAIL_IN_GA(Xs, Ys)
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → U5_G(Xs, X, Ys, head_in_ga(Ys, Y))
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → HEAD_IN_GA(Ys, Y)
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_G(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → TAIL_IN_GA(Ys, Zs)
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_G(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → LESS_IN_AA(X, s(Y))
LESS_IN_AA(0, Y) → U9_AA(Y, eq_in_aa(Y, s(X5)))
LESS_IN_AA(0, Y) → EQ_IN_AA(Y, s(X5))
LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
LESS_IN_AA(X, Y) → P_IN_AA(X, Px)
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U10_AA(X, Y, p_out_aa(X, Px)) → P_IN_AA(Y, Py)
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → U12_AA(X, Y, less_in_aa(Px, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_G(Xs, ordered_in_a(.(Y, Zs)))
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A([]) → U1_A(true_in_)
ORDERED_IN_A([]) → TRUE_IN_
ORDERED_IN_A(.(X1, [])) → U2_A(X1, true_in_)
ORDERED_IN_A(.(X1, [])) → TRUE_IN_
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
ORDERED_IN_A(Xs) → HEAD_IN_AA(Xs, X)
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U3_A(Xs, head_out_aa(Xs, X)) → TAIL_IN_AA(Xs, Ys)
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → HEAD_IN_AA(Ys, Y)
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → TAIL_IN_AA(Ys, Zs)
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → LESS_IN_AA(X, s(Y))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_A(Xs, ordered_in_a(.(Y, Zs)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g(x1)
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x1, x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x1, x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x1, x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x1, x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
ORDERED_IN_G(x1)  =  ORDERED_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
U3_G(x1, x2)  =  U3_G(x1, x2)
HEAD_IN_GA(x1, x2)  =  HEAD_IN_GA(x1)
U4_G(x1, x2, x3)  =  U4_G(x1, x3)
TAIL_IN_GA(x1, x2)  =  TAIL_IN_GA(x1)
U5_G(x1, x2, x3, x4)  =  U5_G(x1, x3, x4)
U6_G(x1, x2, x3, x4, x5)  =  U6_G(x1, x5)
U7_G(x1, x2, x3, x4, x5, x6)  =  U7_G(x1, x6)
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U9_AA(x1, x2)  =  U9_AA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)
U12_AA(x1, x2, x3)  =  U12_AA(x3)
U8_G(x1, x2)  =  U8_G(x1, x2)
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
HEAD_IN_AA(x1, x2)  =  HEAD_IN_AA
U4_A(x1, x2, x3)  =  U4_A(x3)
TAIL_IN_AA(x1, x2)  =  TAIL_IN_AA
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)
U8_A(x1, x2)  =  U8_A(x2)

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

(8) Obligation:

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

ORDERED_IN_G([]) → U1_G(true_in_)
ORDERED_IN_G([]) → TRUE_IN_
ORDERED_IN_G(.(X1, [])) → U2_G(X1, true_in_)
ORDERED_IN_G(.(X1, [])) → TRUE_IN_
ORDERED_IN_G(Xs) → U3_G(Xs, head_in_ga(Xs, X))
ORDERED_IN_G(Xs) → HEAD_IN_GA(Xs, X)
U3_G(Xs, head_out_ga(Xs, X)) → U4_G(Xs, X, tail_in_ga(Xs, Ys))
U3_G(Xs, head_out_ga(Xs, X)) → TAIL_IN_GA(Xs, Ys)
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → U5_G(Xs, X, Ys, head_in_ga(Ys, Y))
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → HEAD_IN_GA(Ys, Y)
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_G(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → TAIL_IN_GA(Ys, Zs)
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_G(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → LESS_IN_AA(X, s(Y))
LESS_IN_AA(0, Y) → U9_AA(Y, eq_in_aa(Y, s(X5)))
LESS_IN_AA(0, Y) → EQ_IN_AA(Y, s(X5))
LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
LESS_IN_AA(X, Y) → P_IN_AA(X, Px)
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U10_AA(X, Y, p_out_aa(X, Px)) → P_IN_AA(Y, Py)
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → U12_AA(X, Y, less_in_aa(Px, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_G(Xs, ordered_in_a(.(Y, Zs)))
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A([]) → U1_A(true_in_)
ORDERED_IN_A([]) → TRUE_IN_
ORDERED_IN_A(.(X1, [])) → U2_A(X1, true_in_)
ORDERED_IN_A(.(X1, [])) → TRUE_IN_
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
ORDERED_IN_A(Xs) → HEAD_IN_AA(Xs, X)
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U3_A(Xs, head_out_aa(Xs, X)) → TAIL_IN_AA(Xs, Ys)
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → HEAD_IN_AA(Ys, Y)
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → TAIL_IN_AA(Ys, Zs)
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → LESS_IN_AA(X, s(Y))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_A(Xs, ordered_in_a(.(Y, Zs)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g(x1)
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x1, x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x1, x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x1, x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x1, x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
ORDERED_IN_G(x1)  =  ORDERED_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
U3_G(x1, x2)  =  U3_G(x1, x2)
HEAD_IN_GA(x1, x2)  =  HEAD_IN_GA(x1)
U4_G(x1, x2, x3)  =  U4_G(x1, x3)
TAIL_IN_GA(x1, x2)  =  TAIL_IN_GA(x1)
U5_G(x1, x2, x3, x4)  =  U5_G(x1, x3, x4)
U6_G(x1, x2, x3, x4, x5)  =  U6_G(x1, x5)
U7_G(x1, x2, x3, x4, x5, x6)  =  U7_G(x1, x6)
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U9_AA(x1, x2)  =  U9_AA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)
U12_AA(x1, x2, x3)  =  U12_AA(x3)
U8_G(x1, x2)  =  U8_G(x1, x2)
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
HEAD_IN_AA(x1, x2)  =  HEAD_IN_AA
U4_A(x1, x2, x3)  =  U4_A(x3)
TAIL_IN_AA(x1, x2)  =  TAIL_IN_AA
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)
U8_A(x1, x2)  =  U8_A(x2)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Complex Obligation (AND)

(11) Obligation:

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

LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g(x1)
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x1, x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x1, x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x1, x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x1, x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)

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

(12) UsableRulesProof (EQUIVALENT transformation)

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

(13) Obligation:

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

LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)

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

(14) PiDPToQDPProof (SOUND transformation)

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

(15) Obligation:

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

LESS_IN_AA → U10_AA(p_in_aa)
U10_AA(p_out_aa) → U11_AA(p_in_aa)
U11_AA(p_out_aa) → LESS_IN_AA

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(16) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LESS_IN_AA → U10_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

LESS_IN_AA → U10_AA(p_out_aa)

(17) Obligation:

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

U10_AA(p_out_aa) → U11_AA(p_in_aa)
U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(18) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U10_AA(p_out_aa) → U11_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U10_AA(p_out_aa) → U11_AA(p_out_aa)

(19) Obligation:

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

U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)
U10_AA(p_out_aa) → U11_AA(p_out_aa)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(20) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(21) Obligation:

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

U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)
U10_AA(p_out_aa) → U11_AA(p_out_aa)

R is empty.
The set Q consists of the following terms:

p_in_aa

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

(22) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

p_in_aa

(23) Obligation:

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

U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)
U10_AA(p_out_aa) → U11_AA(p_out_aa)

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

(24) 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 = LESS_IN_AA evaluates to t =LESS_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

LESS_IN_AA → U10_AA(p_out_aa)
with rule LESS_IN_AA → U10_AA(p_out_aa) at position [] and matcher [ ]

U10_AA(p_out_aa) → U11_AA(p_out_aa)
with rule U10_AA(p_out_aa) → U11_AA(p_out_aa) at position [] and matcher [ ]

U11_AA(p_out_aa) → LESS_IN_AA
with rule U11_AA(p_out_aa) → LESS_IN_AA

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.

(25) FALSE

(26) Obligation:

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

U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g(x1)
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga(x1)
U4_g(x1, x2, x3)  =  U4_g(x1, x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x1, x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x1, x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x1, x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x1, x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x1, x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2, x3)  =  U4_A(x3)
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)

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

(27) UsableRulesProof (EQUIVALENT transformation)

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

(28) Obligation:

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

U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))

The TRS R consists of the following rules:

less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
eq_in_aa(X, X) → eq_out_aa(X, X)
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2, x3)  =  U4_A(x3)
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)

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

(29) PiDPToQDPProof (SOUND transformation)

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

(30) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_in_aa)
U3_A(head_out_aa) → U4_A(tail_in_aa)
U4_A(tail_out_aa) → U5_A(head_in_aa)
U5_A(head_out_aa) → U6_A(tail_in_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(31) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ORDERED_IN_A → U3_A(head_in_aa) at position [0] we obtained the following new rules [LPAR04]:

ORDERED_IN_A → U3_A(head_out_aa)

(32) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U3_A(head_out_aa) → U4_A(tail_in_aa)
U4_A(tail_out_aa) → U5_A(head_in_aa)
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(33) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_A(head_out_aa) → U4_A(tail_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U3_A(head_out_aa) → U4_A(tail_out_aa)

(34) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U4_A(tail_out_aa) → U5_A(head_in_aa)
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(35) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U4_A(tail_out_aa) → U5_A(head_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U4_A(tail_out_aa) → U5_A(head_out_aa)

(36) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(37) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(38) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)

The TRS R consists of the following rules:

tail_in_aa → tail_out_aa
less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(39) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

head_in_aa

(40) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)

The TRS R consists of the following rules:

tail_in_aa → tail_out_aa
less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(41) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_A(head_out_aa) → U6_A(tail_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U5_A(head_out_aa) → U6_A(tail_out_aa)

(42) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)

The TRS R consists of the following rules:

tail_in_aa → tail_out_aa
less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(43) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(44) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(45) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

tail_in_aa

(46) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(47) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U6_A(tail_out_aa) → U7_A(less_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(U9_aa(eq_in_aa))
U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa))

(48) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U9_aa(eq_in_aa))
U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa))

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(49) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U6_A(tail_out_aa) → U7_A(U9_aa(eq_in_aa)) at position [0,0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa))

(50) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa))
U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa))

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(51) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa)) at position [0,0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(U10_aa(p_out_aa))

(52) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa))
U6_A(tail_out_aa) → U7_A(U10_aa(p_out_aa))

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(53) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa)) at position [0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(less_out_aa)

(54) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U10_aa(p_out_aa))
U6_A(tail_out_aa) → U7_A(less_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(55) 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 = ORDERED_IN_A evaluates to t =ORDERED_IN_A

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

ORDERED_IN_A → U3_A(head_out_aa)
with rule ORDERED_IN_A → U3_A(head_out_aa) at position [] and matcher [ ]

U3_A(head_out_aa) → U4_A(tail_out_aa)
with rule U3_A(head_out_aa) → U4_A(tail_out_aa) at position [] and matcher [ ]

U4_A(tail_out_aa) → U5_A(head_out_aa)
with rule U4_A(tail_out_aa) → U5_A(head_out_aa) at position [] and matcher [ ]

U5_A(head_out_aa) → U6_A(tail_out_aa)
with rule U5_A(head_out_aa) → U6_A(tail_out_aa) at position [] and matcher [ ]

U6_A(tail_out_aa) → U7_A(less_out_aa)
with rule U6_A(tail_out_aa) → U7_A(less_out_aa) at position [] and matcher [ ]

U7_A(less_out_aa) → ORDERED_IN_A
with rule U7_A(less_out_aa) → ORDERED_IN_A

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.

(56) FALSE

(57) PrologToPiTRSProof (SOUND transformation)

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

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga
U4_g(x1, x2, x3)  =  U4_g(x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(58) Obligation:

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

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga
U4_g(x1, x2, x3)  =  U4_g(x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)

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

ORDERED_IN_G([]) → U1_G(true_in_)
ORDERED_IN_G([]) → TRUE_IN_
ORDERED_IN_G(.(X1, [])) → U2_G(X1, true_in_)
ORDERED_IN_G(.(X1, [])) → TRUE_IN_
ORDERED_IN_G(Xs) → U3_G(Xs, head_in_ga(Xs, X))
ORDERED_IN_G(Xs) → HEAD_IN_GA(Xs, X)
U3_G(Xs, head_out_ga(Xs, X)) → U4_G(Xs, X, tail_in_ga(Xs, Ys))
U3_G(Xs, head_out_ga(Xs, X)) → TAIL_IN_GA(Xs, Ys)
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → U5_G(Xs, X, Ys, head_in_ga(Ys, Y))
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → HEAD_IN_GA(Ys, Y)
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_G(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → TAIL_IN_GA(Ys, Zs)
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_G(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → LESS_IN_AA(X, s(Y))
LESS_IN_AA(0, Y) → U9_AA(Y, eq_in_aa(Y, s(X5)))
LESS_IN_AA(0, Y) → EQ_IN_AA(Y, s(X5))
LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
LESS_IN_AA(X, Y) → P_IN_AA(X, Px)
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U10_AA(X, Y, p_out_aa(X, Px)) → P_IN_AA(Y, Py)
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → U12_AA(X, Y, less_in_aa(Px, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_G(Xs, ordered_in_a(.(Y, Zs)))
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A([]) → U1_A(true_in_)
ORDERED_IN_A([]) → TRUE_IN_
ORDERED_IN_A(.(X1, [])) → U2_A(X1, true_in_)
ORDERED_IN_A(.(X1, [])) → TRUE_IN_
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
ORDERED_IN_A(Xs) → HEAD_IN_AA(Xs, X)
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U3_A(Xs, head_out_aa(Xs, X)) → TAIL_IN_AA(Xs, Ys)
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → HEAD_IN_AA(Ys, Y)
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → TAIL_IN_AA(Ys, Zs)
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → LESS_IN_AA(X, s(Y))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_A(Xs, ordered_in_a(.(Y, Zs)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga
U4_g(x1, x2, x3)  =  U4_g(x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
ORDERED_IN_G(x1)  =  ORDERED_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x2)
U3_G(x1, x2)  =  U3_G(x1, x2)
HEAD_IN_GA(x1, x2)  =  HEAD_IN_GA(x1)
U4_G(x1, x2, x3)  =  U4_G(x3)
TAIL_IN_GA(x1, x2)  =  TAIL_IN_GA(x1)
U5_G(x1, x2, x3, x4)  =  U5_G(x3, x4)
U6_G(x1, x2, x3, x4, x5)  =  U6_G(x5)
U7_G(x1, x2, x3, x4, x5, x6)  =  U7_G(x6)
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U9_AA(x1, x2)  =  U9_AA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)
U12_AA(x1, x2, x3)  =  U12_AA(x3)
U8_G(x1, x2)  =  U8_G(x2)
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
HEAD_IN_AA(x1, x2)  =  HEAD_IN_AA
U4_A(x1, x2, x3)  =  U4_A(x3)
TAIL_IN_AA(x1, x2)  =  TAIL_IN_AA
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)
U8_A(x1, x2)  =  U8_A(x2)

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

(60) Obligation:

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

ORDERED_IN_G([]) → U1_G(true_in_)
ORDERED_IN_G([]) → TRUE_IN_
ORDERED_IN_G(.(X1, [])) → U2_G(X1, true_in_)
ORDERED_IN_G(.(X1, [])) → TRUE_IN_
ORDERED_IN_G(Xs) → U3_G(Xs, head_in_ga(Xs, X))
ORDERED_IN_G(Xs) → HEAD_IN_GA(Xs, X)
U3_G(Xs, head_out_ga(Xs, X)) → U4_G(Xs, X, tail_in_ga(Xs, Ys))
U3_G(Xs, head_out_ga(Xs, X)) → TAIL_IN_GA(Xs, Ys)
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → U5_G(Xs, X, Ys, head_in_ga(Ys, Y))
U4_G(Xs, X, tail_out_ga(Xs, Ys)) → HEAD_IN_GA(Ys, Y)
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_G(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U5_G(Xs, X, Ys, head_out_ga(Ys, Y)) → TAIL_IN_GA(Ys, Zs)
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_G(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_G(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → LESS_IN_AA(X, s(Y))
LESS_IN_AA(0, Y) → U9_AA(Y, eq_in_aa(Y, s(X5)))
LESS_IN_AA(0, Y) → EQ_IN_AA(Y, s(X5))
LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
LESS_IN_AA(X, Y) → P_IN_AA(X, Px)
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U10_AA(X, Y, p_out_aa(X, Px)) → P_IN_AA(Y, Py)
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → U12_AA(X, Y, less_in_aa(Px, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_G(Xs, ordered_in_a(.(Y, Zs)))
U7_G(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A([]) → U1_A(true_in_)
ORDERED_IN_A([]) → TRUE_IN_
ORDERED_IN_A(.(X1, [])) → U2_A(X1, true_in_)
ORDERED_IN_A(.(X1, [])) → TRUE_IN_
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
ORDERED_IN_A(Xs) → HEAD_IN_AA(Xs, X)
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U3_A(Xs, head_out_aa(Xs, X)) → TAIL_IN_AA(Xs, Ys)
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → HEAD_IN_AA(Ys, Y)
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → TAIL_IN_AA(Ys, Zs)
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → LESS_IN_AA(X, s(Y))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_A(Xs, ordered_in_a(.(Y, Zs)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga
U4_g(x1, x2, x3)  =  U4_g(x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
ORDERED_IN_G(x1)  =  ORDERED_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x2)
U3_G(x1, x2)  =  U3_G(x1, x2)
HEAD_IN_GA(x1, x2)  =  HEAD_IN_GA(x1)
U4_G(x1, x2, x3)  =  U4_G(x3)
TAIL_IN_GA(x1, x2)  =  TAIL_IN_GA(x1)
U5_G(x1, x2, x3, x4)  =  U5_G(x3, x4)
U6_G(x1, x2, x3, x4, x5)  =  U6_G(x5)
U7_G(x1, x2, x3, x4, x5, x6)  =  U7_G(x6)
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U9_AA(x1, x2)  =  U9_AA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
P_IN_AA(x1, x2)  =  P_IN_AA
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)
U12_AA(x1, x2, x3)  =  U12_AA(x3)
U8_G(x1, x2)  =  U8_G(x2)
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U1_A(x1)  =  U1_A(x1)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
HEAD_IN_AA(x1, x2)  =  HEAD_IN_AA
U4_A(x1, x2, x3)  =  U4_A(x3)
TAIL_IN_AA(x1, x2)  =  TAIL_IN_AA
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)
U8_A(x1, x2)  =  U8_A(x2)

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

(61) DependencyGraphProof (EQUIVALENT transformation)

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

(62) Complex Obligation (AND)

(63) Obligation:

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

LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga
U4_g(x1, x2, x3)  =  U4_g(x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)

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

(64) UsableRulesProof (EQUIVALENT transformation)

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

(65) Obligation:

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

LESS_IN_AA(X, Y) → U10_AA(X, Y, p_in_aa(X, Px))
U10_AA(X, Y, p_out_aa(X, Px)) → U11_AA(X, Y, Px, p_in_aa(Y, Py))
U11_AA(X, Y, Px, p_out_aa(Y, Py)) → LESS_IN_AA(Px, Py)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
LESS_IN_AA(x1, x2)  =  LESS_IN_AA
U10_AA(x1, x2, x3)  =  U10_AA(x3)
U11_AA(x1, x2, x3, x4)  =  U11_AA(x4)

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

(66) PiDPToQDPProof (SOUND transformation)

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

(67) Obligation:

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

LESS_IN_AA → U10_AA(p_in_aa)
U10_AA(p_out_aa) → U11_AA(p_in_aa)
U11_AA(p_out_aa) → LESS_IN_AA

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(68) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule LESS_IN_AA → U10_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

LESS_IN_AA → U10_AA(p_out_aa)

(69) Obligation:

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

U10_AA(p_out_aa) → U11_AA(p_in_aa)
U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(70) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U10_AA(p_out_aa) → U11_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U10_AA(p_out_aa) → U11_AA(p_out_aa)

(71) Obligation:

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

U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)
U10_AA(p_out_aa) → U11_AA(p_out_aa)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(72) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(73) Obligation:

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

U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)
U10_AA(p_out_aa) → U11_AA(p_out_aa)

R is empty.
The set Q consists of the following terms:

p_in_aa

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

(74) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

p_in_aa

(75) Obligation:

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

U11_AA(p_out_aa) → LESS_IN_AA
LESS_IN_AA → U10_AA(p_out_aa)
U10_AA(p_out_aa) → U11_AA(p_out_aa)

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

(76) 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 = LESS_IN_AA evaluates to t =LESS_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

LESS_IN_AA → U10_AA(p_out_aa)
with rule LESS_IN_AA → U10_AA(p_out_aa) at position [] and matcher [ ]

U10_AA(p_out_aa) → U11_AA(p_out_aa)
with rule U10_AA(p_out_aa) → U11_AA(p_out_aa) at position [] and matcher [ ]

U11_AA(p_out_aa) → LESS_IN_AA
with rule U11_AA(p_out_aa) → LESS_IN_AA

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.

(77) FALSE

(78) Obligation:

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

U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))

The TRS R consists of the following rules:

ordered_in_g([]) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → ordered_out_g([])
ordered_in_g(.(X1, [])) → U2_g(X1, true_in_)
U2_g(X1, true_out_) → ordered_out_g(.(X1, []))
ordered_in_g(Xs) → U3_g(Xs, head_in_ga(Xs, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(X, X3), X) → head_out_ga(.(X, X3), X)
U3_g(Xs, head_out_ga(Xs, X)) → U4_g(Xs, X, tail_in_ga(Xs, Ys))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, Xs), Xs) → tail_out_ga(.(X4, Xs), Xs)
U4_g(Xs, X, tail_out_ga(Xs, Ys)) → U5_g(Xs, X, Ys, head_in_ga(Ys, Y))
U5_g(Xs, X, Ys, head_out_ga(Ys, Y)) → U6_g(Xs, X, Ys, Y, tail_in_ga(Ys, Zs))
U6_g(Xs, X, Ys, Y, tail_out_ga(Ys, Zs)) → U7_g(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)
U7_g(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_g(Xs, ordered_in_a(.(Y, Zs)))
ordered_in_a([]) → U1_a(true_in_)
U1_a(true_out_) → ordered_out_a([])
ordered_in_a(.(X1, [])) → U2_a(X1, true_in_)
U2_a(X1, true_out_) → ordered_out_a(.(X1, []))
ordered_in_a(Xs) → U3_a(Xs, head_in_aa(Xs, X))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
U3_a(Xs, head_out_aa(Xs, X)) → U4_a(Xs, X, tail_in_aa(Xs, Ys))
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U4_a(Xs, X, tail_out_aa(Xs, Ys)) → U5_a(Xs, X, Ys, head_in_aa(Ys, Y))
U5_a(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_a(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))
U6_a(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_a(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_a(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → U8_a(Xs, ordered_in_a(.(Y, Zs)))
U8_a(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_a(Xs)
U8_g(Xs, ordered_out_a(.(Y, Zs))) → ordered_out_g(Xs)

The argument filtering Pi contains the following mapping:
ordered_in_g(x1)  =  ordered_in_g(x1)
[]  =  []
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
ordered_out_g(x1)  =  ordered_out_g
.(x1, x2)  =  .(x1, x2)
U2_g(x1, x2)  =  U2_g(x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
head_in_ga(x1, x2)  =  head_in_ga(x1)
head_out_ga(x1, x2)  =  head_out_ga
U4_g(x1, x2, x3)  =  U4_g(x3)
tail_in_ga(x1, x2)  =  tail_in_ga(x1)
tail_out_ga(x1, x2)  =  tail_out_ga(x2)
U5_g(x1, x2, x3, x4)  =  U5_g(x3, x4)
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
U7_g(x1, x2, x3, x4, x5, x6)  =  U7_g(x6)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
U8_g(x1, x2)  =  U8_g(x2)
ordered_in_a(x1)  =  ordered_in_a
U1_a(x1)  =  U1_a(x1)
ordered_out_a(x1)  =  ordered_out_a
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
U4_a(x1, x2, x3)  =  U4_a(x3)
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
U5_a(x1, x2, x3, x4)  =  U5_a(x4)
U6_a(x1, x2, x3, x4, x5)  =  U6_a(x5)
U7_a(x1, x2, x3, x4, x5, x6)  =  U7_a(x6)
U8_a(x1, x2)  =  U8_a(x2)
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2, x3)  =  U4_A(x3)
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)

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

(79) UsableRulesProof (EQUIVALENT transformation)

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

(80) Obligation:

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

U6_A(Xs, X, Ys, Y, tail_out_aa(Ys, Zs)) → U7_A(Xs, X, Ys, Y, Zs, less_in_aa(X, s(Y)))
U7_A(Xs, X, Ys, Y, Zs, less_out_aa(X, s(Y))) → ORDERED_IN_A(.(Y, Zs))
ORDERED_IN_A(Xs) → U3_A(Xs, head_in_aa(Xs, X))
U3_A(Xs, head_out_aa(Xs, X)) → U4_A(Xs, X, tail_in_aa(Xs, Ys))
U4_A(Xs, X, tail_out_aa(Xs, Ys)) → U5_A(Xs, X, Ys, head_in_aa(Ys, Y))
U5_A(Xs, X, Ys, head_out_aa(Ys, Y)) → U6_A(Xs, X, Ys, Y, tail_in_aa(Ys, Zs))

The TRS R consists of the following rules:

less_in_aa(0, Y) → U9_aa(Y, eq_in_aa(Y, s(X5)))
less_in_aa(X, Y) → U10_aa(X, Y, p_in_aa(X, Px))
head_in_aa([], X2) → head_out_aa([], X2)
head_in_aa(.(X, X3), X) → head_out_aa(.(X, X3), X)
tail_in_aa([], []) → tail_out_aa([], [])
tail_in_aa(.(X4, Xs), Xs) → tail_out_aa(.(X4, Xs), Xs)
U9_aa(Y, eq_out_aa(Y, s(X5))) → less_out_aa(0, Y)
U10_aa(X, Y, p_out_aa(X, Px)) → U11_aa(X, Y, Px, p_in_aa(Y, Py))
eq_in_aa(X, X) → eq_out_aa(X, X)
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U11_aa(X, Y, Px, p_out_aa(Y, Py)) → U12_aa(X, Y, less_in_aa(Px, Py))
U12_aa(X, Y, less_out_aa(Px, Py)) → less_out_aa(X, Y)

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
less_in_aa(x1, x2)  =  less_in_aa
U9_aa(x1, x2)  =  U9_aa(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
less_out_aa(x1, x2)  =  less_out_aa
U10_aa(x1, x2, x3)  =  U10_aa(x3)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U11_aa(x1, x2, x3, x4)  =  U11_aa(x4)
U12_aa(x1, x2, x3)  =  U12_aa(x3)
head_in_aa(x1, x2)  =  head_in_aa
head_out_aa(x1, x2)  =  head_out_aa
tail_in_aa(x1, x2)  =  tail_in_aa
tail_out_aa(x1, x2)  =  tail_out_aa
ORDERED_IN_A(x1)  =  ORDERED_IN_A
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2, x3)  =  U4_A(x3)
U5_A(x1, x2, x3, x4)  =  U5_A(x4)
U6_A(x1, x2, x3, x4, x5)  =  U6_A(x5)
U7_A(x1, x2, x3, x4, x5, x6)  =  U7_A(x6)

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

(81) PiDPToQDPProof (SOUND transformation)

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

(82) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_in_aa)
U3_A(head_out_aa) → U4_A(tail_in_aa)
U4_A(tail_out_aa) → U5_A(head_in_aa)
U5_A(head_out_aa) → U6_A(tail_in_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(83) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ORDERED_IN_A → U3_A(head_in_aa) at position [0] we obtained the following new rules [LPAR04]:

ORDERED_IN_A → U3_A(head_out_aa)

(84) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U3_A(head_out_aa) → U4_A(tail_in_aa)
U4_A(tail_out_aa) → U5_A(head_in_aa)
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(85) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_A(head_out_aa) → U4_A(tail_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U3_A(head_out_aa) → U4_A(tail_out_aa)

(86) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U4_A(tail_out_aa) → U5_A(head_in_aa)
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(87) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U4_A(tail_out_aa) → U5_A(head_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U4_A(tail_out_aa) → U5_A(head_out_aa)

(88) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
head_in_aa → head_out_aa
tail_in_aa → tail_out_aa
U9_aa(eq_out_aa) → less_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
eq_in_aa → eq_out_aa
p_in_aa → p_out_aa
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(89) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(90) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)

The TRS R consists of the following rules:

tail_in_aa → tail_out_aa
less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
head_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(91) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

head_in_aa

(92) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
U5_A(head_out_aa) → U6_A(tail_in_aa)
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)

The TRS R consists of the following rules:

tail_in_aa → tail_out_aa
less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(93) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_A(head_out_aa) → U6_A(tail_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U5_A(head_out_aa) → U6_A(tail_out_aa)

(94) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)

The TRS R consists of the following rules:

tail_in_aa → tail_out_aa
less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(95) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(96) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
tail_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(97) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

tail_in_aa

(98) Obligation:

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

U6_A(tail_out_aa) → U7_A(less_in_aa)
U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(99) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U6_A(tail_out_aa) → U7_A(less_in_aa) at position [0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(U9_aa(eq_in_aa))
U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa))

(100) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U9_aa(eq_in_aa))
U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa))

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(101) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U6_A(tail_out_aa) → U7_A(U9_aa(eq_in_aa)) at position [0,0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa))

(102) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa))
U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa))

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(103) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U6_A(tail_out_aa) → U7_A(U10_aa(p_in_aa)) at position [0,0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(U10_aa(p_out_aa))

(104) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa))
U6_A(tail_out_aa) → U7_A(U10_aa(p_out_aa))

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(105) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U6_A(tail_out_aa) → U7_A(U9_aa(eq_out_aa)) at position [0] we obtained the following new rules [LPAR04]:

U6_A(tail_out_aa) → U7_A(less_out_aa)

(106) Obligation:

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

U7_A(less_out_aa) → ORDERED_IN_A
ORDERED_IN_A → U3_A(head_out_aa)
U3_A(head_out_aa) → U4_A(tail_out_aa)
U4_A(tail_out_aa) → U5_A(head_out_aa)
U5_A(head_out_aa) → U6_A(tail_out_aa)
U6_A(tail_out_aa) → U7_A(U10_aa(p_out_aa))
U6_A(tail_out_aa) → U7_A(less_out_aa)

The TRS R consists of the following rules:

less_in_aa → U9_aa(eq_in_aa)
less_in_aa → U10_aa(p_in_aa)
p_in_aa → p_out_aa
U10_aa(p_out_aa) → U11_aa(p_in_aa)
U11_aa(p_out_aa) → U12_aa(less_in_aa)
U12_aa(less_out_aa) → less_out_aa
eq_in_aa → eq_out_aa
U9_aa(eq_out_aa) → less_out_aa

The set Q consists of the following terms:

less_in_aa
U9_aa(x0)
U10_aa(x0)
eq_in_aa
p_in_aa
U11_aa(x0)
U12_aa(x0)

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

(107) 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 = ORDERED_IN_A evaluates to t =ORDERED_IN_A

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

ORDERED_IN_A → U3_A(head_out_aa)
with rule ORDERED_IN_A → U3_A(head_out_aa) at position [] and matcher [ ]

U3_A(head_out_aa) → U4_A(tail_out_aa)
with rule U3_A(head_out_aa) → U4_A(tail_out_aa) at position [] and matcher [ ]

U4_A(tail_out_aa) → U5_A(head_out_aa)
with rule U4_A(tail_out_aa) → U5_A(head_out_aa) at position [] and matcher [ ]

U5_A(head_out_aa) → U6_A(tail_out_aa)
with rule U5_A(head_out_aa) → U6_A(tail_out_aa) at position [] and matcher [ ]

U6_A(tail_out_aa) → U7_A(less_out_aa)
with rule U6_A(tail_out_aa) → U7_A(less_out_aa) at position [] and matcher [ ]

U7_A(less_out_aa) → ORDERED_IN_A
with rule U7_A(less_out_aa) → ORDERED_IN_A

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.

(108) FALSE