(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt) → tt
a__U21(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isNatList(V2))
a__U52(tt) → tt
a__U61(tt, L, N) → a__U62(a__isNat(N), L)
a__U62(tt, L) → s(a__length(mark(L)))
a__isNat(0) → tt
a__isNat(length(V1)) → a__U11(a__isNatList(V1))
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatIList(V) → a__U31(a__isNatList(V))
a__isNatIList(zeros) → tt
a__isNatIList(cons(V1, V2)) → a__U41(a__isNat(V1), V2)
a__isNatList(nil) → tt
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(nil) → 0
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(length(X)) → a__length(mark(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(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1)) = x1
POL(U21(x1)) = x1
POL(U31(x1)) = x1
POL(U41(x1, x2)) = x1 + x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = x1 + x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = x1 + 2·x2 + x3
POL(U62(x1, x2)) = x1 + 2·x2
POL(a__U11(x1)) = x1
POL(a__U21(x1)) = x1
POL(a__U31(x1)) = x1
POL(a__U41(x1, x2)) = x1 + x2
POL(a__U42(x1)) = x1
POL(a__U51(x1, x2)) = x1 + x2
POL(a__U52(x1)) = x1
POL(a__U61(x1, x2, x3)) = x1 + 2·x2 + x3
POL(a__U62(x1, x2)) = x1 + 2·x2
POL(a__isNat(x1)) = x1
POL(a__isNatIList(x1)) = x1
POL(a__isNatList(x1)) = x1
POL(a__length(x1)) = 2·x1
POL(a__zeros) = 0
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 2·x1
POL(mark(x1)) = x1
POL(nil) = 1
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a__isNatList(nil) → tt
a__length(nil) → 0
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt) → tt
a__U21(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isNatList(V2))
a__U52(tt) → tt
a__U61(tt, L, N) → a__U62(a__isNat(N), L)
a__U62(tt, L) → s(a__length(mark(L)))
a__isNat(0) → tt
a__isNat(length(V1)) → a__U11(a__isNatList(V1))
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatIList(V) → a__U31(a__isNatList(V))
a__isNatIList(zeros) → tt
a__isNatIList(cons(V1, V2)) → a__U41(a__isNat(V1), V2)
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(length(X)) → a__length(mark(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(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1)) = x1
POL(U21(x1)) = x1
POL(U31(x1)) = x1
POL(U41(x1, x2)) = 1 + x1 + x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = x1 + x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = x1 + 2·x2 + 2·x3
POL(U62(x1, x2)) = x1 + 2·x2
POL(a__U11(x1)) = x1
POL(a__U21(x1)) = x1
POL(a__U31(x1)) = x1
POL(a__U41(x1, x2)) = 1 + x1 + x2
POL(a__U42(x1)) = x1
POL(a__U51(x1, x2)) = x1 + x2
POL(a__U52(x1)) = x1
POL(a__U61(x1, x2, x3)) = x1 + 2·x2 + 2·x3
POL(a__U62(x1, x2)) = x1 + 2·x2
POL(a__isNat(x1)) = 2·x1
POL(a__isNatIList(x1)) = 1 + x1
POL(a__isNatList(x1)) = x1
POL(a__length(x1)) = 2·x1
POL(a__zeros) = 0
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = 2·x1
POL(isNatIList(x1)) = 1 + x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 2·x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(tt) = 0
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__U31(a__isNatList(V))
a__isNatIList(zeros) → tt
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt) → tt
a__U21(tt) → tt
a__U31(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isNatList(V2))
a__U52(tt) → tt
a__U61(tt, L, N) → a__U62(a__isNat(N), L)
a__U62(tt, L) → s(a__length(mark(L)))
a__isNat(0) → tt
a__isNat(length(V1)) → a__U11(a__isNatList(V1))
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatIList(cons(V1, V2)) → a__U41(a__isNat(V1), V2)
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(length(X)) → a__length(mark(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(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(5) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1)) = 2·x1
POL(U21(x1)) = x1
POL(U31(x1)) = 1 + x1
POL(U41(x1, x2)) = 2·x1 + 2·x2
POL(U42(x1)) = 2·x1
POL(U51(x1, x2)) = x1 + 2·x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(U62(x1, x2)) = x1 + 2·x2
POL(a__U11(x1)) = 2·x1
POL(a__U21(x1)) = x1
POL(a__U31(x1)) = 1 + x1
POL(a__U41(x1, x2)) = 2·x1 + 2·x2
POL(a__U42(x1)) = 2·x1
POL(a__U51(x1, x2)) = x1 + 2·x2
POL(a__U52(x1)) = x1
POL(a__U61(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(a__U62(x1, x2)) = x1 + 2·x2
POL(a__isNat(x1)) = x1
POL(a__isNatIList(x1)) = x1
POL(a__isNatList(x1)) = x1
POL(a__length(x1)) = 2·x1
POL(a__zeros) = 0
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 2·x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a__U31(tt) → tt
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt) → tt
a__U21(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isNatList(V2))
a__U52(tt) → tt
a__U61(tt, L, N) → a__U62(a__isNat(N), L)
a__U62(tt, L) → s(a__length(mark(L)))
a__isNat(0) → tt
a__isNat(length(V1)) → a__U11(a__isNatList(V1))
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatIList(cons(V1, V2)) → a__U41(a__isNat(V1), V2)
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(length(X)) → a__length(mark(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(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(7) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1)) = x1
POL(U21(x1)) = x1
POL(U31(x1)) = x1
POL(U41(x1, x2)) = x1 + 2·x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = x1 + x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3
POL(U62(x1, x2)) = 1 + x1 + 2·x2
POL(a__U11(x1)) = x1
POL(a__U21(x1)) = x1
POL(a__U31(x1)) = x1
POL(a__U41(x1, x2)) = x1 + 2·x2
POL(a__U42(x1)) = x1
POL(a__U51(x1, x2)) = x1 + x2
POL(a__U52(x1)) = x1
POL(a__U61(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3
POL(a__U62(x1, x2)) = 1 + x1 + 2·x2
POL(a__isNat(x1)) = x1
POL(a__isNatIList(x1)) = 2·x1
POL(a__isNatList(x1)) = x1
POL(a__length(x1)) = 1 + 2·x1
POL(a__zeros) = 0
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = 2·x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 1 + 2·x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a__isNat(length(V1)) → a__U11(a__isNatList(V1))
(8) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U11(tt) → tt
a__U21(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isNatList(V2))
a__U52(tt) → tt
a__U61(tt, L, N) → a__U62(a__isNat(N), L)
a__U62(tt, L) → s(a__length(mark(L)))
a__isNat(0) → tt
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatIList(cons(V1, V2)) → a__U41(a__isNat(V1), V2)
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(length(X)) → a__length(mark(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(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(9) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1)) = 1 + x1
POL(U21(x1)) = x1
POL(U31(x1)) = 2·x1
POL(U41(x1, x2)) = x1 + 2·x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = 2·x1 + 2·x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = x1 + 2·x2 + 2·x3
POL(U62(x1, x2)) = 2·x1 + 2·x2
POL(a__U11(x1)) = 1 + x1
POL(a__U21(x1)) = x1
POL(a__U31(x1)) = 2·x1
POL(a__U41(x1, x2)) = x1 + 2·x2
POL(a__U42(x1)) = x1
POL(a__U51(x1, x2)) = 2·x1 + 2·x2
POL(a__U52(x1)) = x1
POL(a__U61(x1, x2, x3)) = x1 + 2·x2 + 2·x3
POL(a__U62(x1, x2)) = 2·x1 + 2·x2
POL(a__isNat(x1)) = x1
POL(a__isNatIList(x1)) = 2·x1
POL(a__isNatList(x1)) = 2·x1
POL(a__length(x1)) = 2·x1
POL(a__zeros) = 0
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = 2·x1
POL(isNatList(x1)) = 2·x1
POL(length(x1)) = 2·x1
POL(mark(x1)) = x1
POL(nil) = 0
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a__U11(tt) → tt
(10) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U21(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U51(tt, V2) → a__U52(a__isNatList(V2))
a__U52(tt) → tt
a__U61(tt, L, N) → a__U62(a__isNat(N), L)
a__U62(tt, L) → s(a__length(mark(L)))
a__isNat(0) → tt
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatIList(cons(V1, V2)) → a__U41(a__isNat(V1), V2)
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(isNatIList(X)) → a__isNatIList(X)
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(isNatList(X)) → a__isNatList(X)
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(isNat(X)) → a__isNat(X)
mark(length(X)) → a__length(mark(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(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(11) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 1
POL(U11(x1)) = x1
POL(U21(x1)) = x1
POL(U31(x1)) = x1
POL(U41(x1, x2)) = 1 + x1 + x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = x1 + x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = x1 + x2 + x3
POL(U62(x1, x2)) = x1 + x2
POL(a__U11(x1)) = x1
POL(a__U21(x1)) = x1
POL(a__U31(x1)) = x1
POL(a__U41(x1, x2)) = 1 + x1 + x2
POL(a__U42(x1)) = x1
POL(a__U51(x1, x2)) = x1 + x2
POL(a__U52(x1)) = x1
POL(a__U61(x1, x2, x3)) = x1 + x2 + x3
POL(a__U62(x1, x2)) = x1 + x2
POL(a__isNat(x1)) = x1
POL(a__isNatIList(x1)) = 2 + x1
POL(a__isNatList(x1)) = x1
POL(a__length(x1)) = x1
POL(a__zeros) = 1
POL(cons(x1, x2)) = x1 + 2·x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = 2 + x1
POL(isNatList(x1)) = x1
POL(length(x1)) = x1
POL(mark(x1)) = 1 + x1
POL(nil) = 0
POL(s(x1)) = x1
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__U51(tt, V2) → a__U52(a__isNatList(V2))
a__U61(tt, L, N) → a__U62(a__isNat(N), L)
a__isNatIList(cons(V1, V2)) → a__U41(a__isNat(V1), V2)
mark(isNatIList(X)) → a__isNatIList(X)
mark(isNatList(X)) → a__isNatList(X)
mark(isNat(X)) → a__isNat(X)
mark(0) → 0
mark(tt) → tt
mark(nil) → nil
a__zeros → zeros
(12) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U21(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U52(tt) → tt
a__U62(tt, L) → s(a__length(mark(L)))
a__isNat(0) → tt
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
a__U11(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(13) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1)) = 2·x1
POL(U21(x1)) = x1
POL(U31(x1)) = 2·x1
POL(U41(x1, x2)) = x1 + 2·x2
POL(U42(x1)) = x1
POL(U51(x1, x2)) = x1 + 2·x2
POL(U52(x1)) = x1
POL(U61(x1, x2, x3)) = x1 + 2·x2 + 2·x3
POL(U62(x1, x2)) = 2 + x1 + 2·x2
POL(a__U11(x1)) = 2·x1
POL(a__U21(x1)) = x1
POL(a__U31(x1)) = 2·x1
POL(a__U41(x1, x2)) = x1 + 2·x2
POL(a__U42(x1)) = x1
POL(a__U51(x1, x2)) = x1 + 2·x2
POL(a__U52(x1)) = x1
POL(a__U61(x1, x2, x3)) = x1 + 2·x2 + 2·x3
POL(a__U62(x1, x2)) = 2 + x1 + 2·x2
POL(a__isNat(x1)) = 2·x1
POL(a__isNatIList(x1)) = x1
POL(a__isNatList(x1)) = 2·x1
POL(a__length(x1)) = 2·x1
POL(a__zeros) = 0
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = 2·x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = 2·x1
POL(length(x1)) = 2·x1
POL(mark(x1)) = x1
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
a__U62(tt, L) → s(a__length(mark(L)))
(14) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U21(tt) → tt
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__U42(tt) → tt
a__U52(tt) → tt
a__isNat(0) → tt
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
mark(s(X)) → s(mark(X))
a__U11(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
Q is empty.
(15) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 0
POL(U11(x1)) = 1 + x1
POL(U21(x1)) = 1 + x1
POL(U31(x1)) = 1 + x1
POL(U41(x1, x2)) = 1 + x1 + x2
POL(U42(x1)) = 1 + x1
POL(U51(x1, x2)) = 1 + x1 + 2·x2
POL(U52(x1)) = 1 + x1
POL(U61(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(U62(x1, x2)) = 1 + x1 + x2
POL(a__U11(x1)) = 2 + x1
POL(a__U21(x1)) = 2 + x1
POL(a__U31(x1)) = 2 + x1
POL(a__U41(x1, x2)) = 2 + x1 + 2·x2
POL(a__U42(x1)) = 2 + x1
POL(a__U51(x1, x2)) = 2 + x1 + 2·x2
POL(a__U52(x1)) = 2 + x1
POL(a__U61(x1, x2, x3)) = 2 + x1 + x2 + x3
POL(a__U62(x1, x2)) = 2 + x1 + 2·x2
POL(a__isNat(x1)) = 2 + 2·x1
POL(a__isNatIList(x1)) = 2 + 2·x1
POL(a__isNatList(x1)) = 2 + x1
POL(a__length(x1)) = 2 + x1
POL(a__zeros) = 2
POL(cons(x1, x2)) = 2 + 2·x1 + 2·x2
POL(isNat(x1)) = 1 + x1
POL(isNatIList(x1)) = 1 + x1
POL(isNatList(x1)) = 1 + x1
POL(length(x1)) = 1 + x1
POL(mark(x1)) = 2 + 2·x1
POL(s(x1)) = 1 + x1
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__U21(tt) → tt
a__U42(tt) → tt
a__U52(tt) → tt
mark(s(X)) → s(mark(X))
a__U11(X) → U11(X)
a__U21(X) → U21(X)
a__U31(X) → U31(X)
a__U41(X1, X2) → U41(X1, X2)
a__U42(X) → U42(X)
a__isNatIList(X) → isNatIList(X)
a__U51(X1, X2) → U51(X1, X2)
a__U52(X) → U52(X)
a__isNatList(X) → isNatList(X)
a__U61(X1, X2, X3) → U61(X1, X2, X3)
a__U62(X1, X2) → U62(X1, X2)
a__isNat(X) → isNat(X)
a__length(X) → length(X)
(16) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
a__zeros → cons(0, zeros)
a__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__isNat(0) → tt
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
Q is empty.
(17) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:
mark1 > azeros > cons2
mark1 > azeros > 0
mark1 > azeros > zeros
mark1 > aU412 > aU421
mark1 > aU412 > aisNatIList1
mark1 > alength1 > aisNatList1 > aisNat1 > tt
mark1 > alength1 > aisNatList1 > aisNat1 > aU211
mark1 > alength1 > aisNatList1 > aU512
mark1 > alength1 > aU613
mark1 > aU111
mark1 > aU311
mark1 > aU521
mark1 > aU622
Status:
trivial
With 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__U41(tt, V2) → a__U42(a__isNatIList(V2))
a__isNat(0) → tt
a__isNat(s(V1)) → a__U21(a__isNat(V1))
a__isNatList(cons(V1, V2)) → a__U51(a__isNat(V1), V2)
a__length(cons(N, L)) → a__U61(a__isNatList(L), L, N)
mark(zeros) → a__zeros
mark(U11(X)) → a__U11(mark(X))
mark(U21(X)) → a__U21(mark(X))
mark(U31(X)) → a__U31(mark(X))
mark(U41(X1, X2)) → a__U41(mark(X1), X2)
mark(U42(X)) → a__U42(mark(X))
mark(U51(X1, X2)) → a__U51(mark(X1), X2)
mark(U52(X)) → a__U52(mark(X))
mark(U61(X1, X2, X3)) → a__U61(mark(X1), X2, X3)
mark(U62(X1, X2)) → a__U62(mark(X1), X2)
mark(length(X)) → a__length(mark(X))
mark(cons(X1, X2)) → cons(mark(X1), X2)
(18) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(19) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(20) TRUE
(21) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(22) TRUE
(23) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(24) TRUE