YES
proof of Transformed_CSR_04_LengthOfFiniteLists_nokinds_GM.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 jera 20211004 unpublished


Termination w.r.t. Q of the given QTRS could be proven:

(0) QTRS
(1) QTRSRRRProof [EQUIVALENT, 67 ms]
(2) QTRS
(3) QTRSRRRProof [EQUIVALENT, 0 ms]
(4) QTRS
(5) QTRSRRRProof [EQUIVALENT, 0 ms]
(6) QTRS
(7) QTRSRRRProof [EQUIVALENT, 12 ms]
(8) QTRS
(9) QTRSRRRProof [EQUIVALENT, 0 ms]
(10) QTRS
(11) RisEmptyProof [EQUIVALENT, 0 ms]
(12) YES


----------------------------------------

(0)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   a__zeros -> cons(0, zeros)
   a__U11(tt, L) -> s(a__length(mark(L)))
   a__and(tt, X) -> mark(X)
   a__isNat(0) -> tt
   a__isNat(length(V1)) -> a__isNatList(V1)
   a__isNat(s(V1)) -> a__isNat(V1)
   a__isNatIList(V) -> a__isNatList(V)
   a__isNatIList(zeros) -> tt
   a__isNatIList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2))
   a__isNatList(nil) -> tt
   a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
   a__length(nil) -> 0
   a__length(cons(N, L)) -> a__U11(a__and(a__isNatList(L), isNat(N)), L)
   mark(zeros) -> a__zeros
   mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
   mark(length(X)) -> a__length(mark(X))
   mark(and(X1, X2)) -> a__and(mark(X1), X2)
   mark(isNat(X)) -> a__isNat(X)
   mark(isNatList(X)) -> a__isNatList(X)
   mark(isNatIList(X)) -> a__isNatIList(X)
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(0) -> 0
   mark(tt) -> tt
   mark(s(X)) -> s(mark(X))
   mark(nil) -> nil
   a__zeros -> zeros
   a__U11(X1, X2) -> U11(X1, X2)
   a__length(X) -> length(X)
   a__and(X1, X2) -> and(X1, X2)
   a__isNat(X) -> isNat(X)
   a__isNatList(X) -> isNatList(X)
   a__isNatIList(X) -> isNatIList(X)

Q is empty.

----------------------------------------

(1) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 1
   POL(U11(x_1, x_2)) = x_1 + x_2
   POL(a__U11(x_1, x_2)) = x_1 + x_2
   POL(a__and(x_1, x_2)) = x_1 + x_2
   POL(a__isNat(x_1)) = x_1
   POL(a__isNatIList(x_1)) = 2 + 2*x_1
   POL(a__isNatList(x_1)) = x_1
   POL(a__length(x_1)) = x_1
   POL(a__zeros) = 1
   POL(and(x_1, x_2)) = x_1 + x_2
   POL(cons(x_1, x_2)) = x_1 + 2*x_2
   POL(isNat(x_1)) = x_1
   POL(isNatIList(x_1)) = 1 + 2*x_1
   POL(isNatList(x_1)) = x_1
   POL(length(x_1)) = x_1
   POL(mark(x_1)) = 1 + x_1
   POL(nil) = 2
   POL(s(x_1)) = x_1
   POL(tt) = 1
   POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   a__isNatIList(V) -> a__isNatList(V)
   a__isNatIList(zeros) -> tt
   a__isNatIList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatIList(V2))
   a__isNatList(nil) -> tt
   a__length(nil) -> 0
   mark(isNat(X)) -> a__isNat(X)
   mark(isNatList(X)) -> a__isNatList(X)
   mark(0) -> 0
   mark(tt) -> tt
   mark(nil) -> nil
   a__zeros -> zeros
   a__isNatIList(X) -> isNatIList(X)




----------------------------------------

(2)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   a__zeros -> cons(0, zeros)
   a__U11(tt, L) -> s(a__length(mark(L)))
   a__and(tt, X) -> mark(X)
   a__isNat(0) -> tt
   a__isNat(length(V1)) -> a__isNatList(V1)
   a__isNat(s(V1)) -> a__isNat(V1)
   a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
   a__length(cons(N, L)) -> a__U11(a__and(a__isNatList(L), isNat(N)), L)
   mark(zeros) -> a__zeros
   mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
   mark(length(X)) -> a__length(mark(X))
   mark(and(X1, X2)) -> a__and(mark(X1), X2)
   mark(isNatIList(X)) -> a__isNatIList(X)
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(s(X)) -> s(mark(X))
   a__U11(X1, X2) -> U11(X1, X2)
   a__length(X) -> length(X)
   a__and(X1, X2) -> and(X1, X2)
   a__isNat(X) -> isNat(X)
   a__isNatList(X) -> isNatList(X)

Q is empty.

----------------------------------------

(3) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(U11(x_1, x_2)) = x_1 + 2*x_2
   POL(a__U11(x_1, x_2)) = x_1 + 2*x_2
   POL(a__and(x_1, x_2)) = x_1 + x_2
   POL(a__isNat(x_1)) = 2 + x_1
   POL(a__isNatIList(x_1)) = x_1
   POL(a__isNatList(x_1)) = 2 + x_1
   POL(a__length(x_1)) = 2 + 2*x_1
   POL(a__zeros) = 0
   POL(and(x_1, x_2)) = x_1 + x_2
   POL(cons(x_1, x_2)) = x_1 + 2*x_2
   POL(isNat(x_1)) = x_1
   POL(isNatIList(x_1)) = 1 + 2*x_1
   POL(isNatList(x_1)) = x_1
   POL(length(x_1)) = 2 + 2*x_1
   POL(mark(x_1)) = x_1
   POL(s(x_1)) = x_1
   POL(tt) = 2
   POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   a__and(tt, X) -> mark(X)
   a__isNat(length(V1)) -> a__isNatList(V1)
   mark(isNatIList(X)) -> a__isNatIList(X)
   a__isNat(X) -> isNat(X)
   a__isNatList(X) -> isNatList(X)




----------------------------------------

(4)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   a__zeros -> cons(0, zeros)
   a__U11(tt, L) -> s(a__length(mark(L)))
   a__isNat(0) -> tt
   a__isNat(s(V1)) -> a__isNat(V1)
   a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
   a__length(cons(N, L)) -> a__U11(a__and(a__isNatList(L), isNat(N)), L)
   mark(zeros) -> a__zeros
   mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
   mark(length(X)) -> a__length(mark(X))
   mark(and(X1, X2)) -> a__and(mark(X1), X2)
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(s(X)) -> s(mark(X))
   a__U11(X1, X2) -> U11(X1, X2)
   a__length(X) -> length(X)
   a__and(X1, X2) -> and(X1, X2)

Q is empty.

----------------------------------------

(5) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(U11(x_1, x_2)) = 2 + x_1 + x_2
   POL(a__U11(x_1, x_2)) = 2 + x_1 + x_2
   POL(a__and(x_1, x_2)) = x_1 + x_2
   POL(a__isNat(x_1)) = 2 + x_1
   POL(a__isNatList(x_1)) = x_1
   POL(a__length(x_1)) = 2 + x_1
   POL(a__zeros) = 2
   POL(and(x_1, x_2)) = x_1 + x_2
   POL(cons(x_1, x_2)) = 2 + x_1 + 2*x_2
   POL(isNat(x_1)) = 1 + x_1
   POL(isNatList(x_1)) = x_1
   POL(length(x_1)) = 2 + x_1
   POL(mark(x_1)) = 2 + x_1
   POL(s(x_1)) = x_1
   POL(tt) = 2
   POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   a__length(cons(N, L)) -> a__U11(a__and(a__isNatList(L), isNat(N)), L)




----------------------------------------

(6)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   a__zeros -> cons(0, zeros)
   a__U11(tt, L) -> s(a__length(mark(L)))
   a__isNat(0) -> tt
   a__isNat(s(V1)) -> a__isNat(V1)
   a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
   mark(zeros) -> a__zeros
   mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
   mark(length(X)) -> a__length(mark(X))
   mark(and(X1, X2)) -> a__and(mark(X1), X2)
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(s(X)) -> s(mark(X))
   a__U11(X1, X2) -> U11(X1, X2)
   a__length(X) -> length(X)
   a__and(X1, X2) -> and(X1, X2)

Q is empty.

----------------------------------------

(7) QTRSRRRProof (EQUIVALENT)
Used ordering:
Polynomial interpretation [POLO]:

   POL(0) = 0
   POL(U11(x_1, x_2)) = 2*x_1 + 2*x_2
   POL(a__U11(x_1, x_2)) = 2*x_1 + 2*x_2
   POL(a__and(x_1, x_2)) = x_1 + x_2
   POL(a__isNat(x_1)) = 2 + x_1
   POL(a__isNatList(x_1)) = 2 + 2*x_1
   POL(a__length(x_1)) = x_1
   POL(a__zeros) = 1
   POL(and(x_1, x_2)) = x_1 + x_2
   POL(cons(x_1, x_2)) = 2*x_1 + x_2
   POL(isNatList(x_1)) = x_1
   POL(length(x_1)) = x_1
   POL(mark(x_1)) = x_1
   POL(s(x_1)) = 2 + 2*x_1
   POL(tt) = 2
   POL(zeros) = 1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   a__U11(tt, L) -> s(a__length(mark(L)))
   a__isNat(s(V1)) -> a__isNat(V1)




----------------------------------------

(8)
Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:

   a__zeros -> cons(0, zeros)
   a__isNat(0) -> tt
   a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
   mark(zeros) -> a__zeros
   mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
   mark(length(X)) -> a__length(mark(X))
   mark(and(X1, X2)) -> a__and(mark(X1), X2)
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(s(X)) -> s(mark(X))
   a__U11(X1, X2) -> U11(X1, X2)
   a__length(X) -> length(X)
   a__and(X1, X2) -> and(X1, X2)

Q is empty.

----------------------------------------

(9) QTRSRRRProof (EQUIVALENT)
Used ordering:
Knuth-Bendix order [KBO] with precedence:mark_1 > a__zeros > s_1 > a__U11_2 > isNatList_1 > 0 > U11_2 > cons_2 > a__isNat_1 > a__and_2 > and_2 > a__length_1 > length_1 > a__isNatList_1 > tt > zeros

and weight map:

   a__zeros=3
   0=2
   zeros=1
   tt=4
   a__isNat_1=2
   a__isNatList_1=4
   isNatList_1=1
   mark_1=2
   length_1=1
   a__length_1=1
   s_1=1
   cons_2=0
   a__and_2=0
   U11_2=0
   a__U11_2=0
   and_2=0

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

   a__zeros -> cons(0, zeros)
   a__isNat(0) -> tt
   a__isNatList(cons(V1, V2)) -> a__and(a__isNat(V1), isNatList(V2))
   mark(zeros) -> a__zeros
   mark(U11(X1, X2)) -> a__U11(mark(X1), X2)
   mark(length(X)) -> a__length(mark(X))
   mark(and(X1, X2)) -> a__and(mark(X1), X2)
   mark(cons(X1, X2)) -> cons(mark(X1), X2)
   mark(s(X)) -> s(mark(X))
   a__U11(X1, X2) -> U11(X1, X2)
   a__length(X) -> length(X)
   a__and(X1, X2) -> and(X1, X2)




----------------------------------------

(10)
Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.

----------------------------------------

(11) RisEmptyProof (EQUIVALENT)
The TRS R is empty. Hence, termination is trivially proven.
----------------------------------------

(12)
YES