0 QTRS
↳1 QTRSToCSRProof (⇔)
↳2 CSR
↳3 PoloCSRProof (⇔)
↳4 CSR
↳5 PoloCSRProof (⇔)
↳6 CSR
↳7 PoloCSRProof (⇔)
↳8 CSR
↳9 CSRInnermostProof (⇔)
↳10 CSR
↳11 CSDependencyPairsProof (⇔)
↳12 QCSDP
↳13 QCSDependencyGraphProof (⇔)
↳14 AND
↳15 QCSDP
↳16 QCSDPSubtermProof (⇔)
↳17 QCSDP
↳18 PIsEmptyProof (⇔)
↳19 TRUE
↳20 QCSDP
↳21 QCSUsableRulesProof (⇔)
↳22 QCSDP
↳23 QCSDPMuMonotonicPoloProof (⇔)
↳24 QCSDP
↳25 QCSDependencyGraphProof (⇔)
↳26 TRUE
↳27 QCSDP
↳28 QCSDPReductionPairProof (⇔)
↳29 QCSDP
↳30 QCSDependencyGraphProof (⇔)
↳31 TRUE
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(and(X1, X2)) → and(active(X1), X2)
cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))
proper(nil) → ok(nil)
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))
isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(zeros) → mark(cons(0, zeros))
active(U11(tt, L)) → mark(s(length(L)))
active(and(tt, X)) → mark(X)
active(isNat(0)) → mark(tt)
active(isNat(length(V1))) → mark(isNatList(V1))
active(isNat(s(V1))) → mark(isNat(V1))
active(isNatIList(V)) → mark(isNatList(V))
active(isNatIList(zeros)) → mark(tt)
active(isNatIList(cons(V1, V2))) → mark(and(isNat(V1), isNatIList(V2)))
active(isNatList(nil)) → mark(tt)
active(isNatList(cons(V1, V2))) → mark(and(isNat(V1), isNatList(V2)))
active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U11(and(isNatList(L), isNat(N)), L))
active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X1, X2)) → U11(active(X1), X2)
active(s(X)) → s(active(X))
active(length(X)) → length(active(X))
active(and(X1, X2)) → and(active(X1), X2)
cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X1), X2) → mark(U11(X1, X2))
s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))
and(mark(X1), X2) → mark(and(X1, X2))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(U11(X1, X2)) → U11(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))
proper(isNatList(X)) → isNatList(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))
proper(nil) → ok(nil)
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X1), ok(X2)) → ok(U11(X1, X2))
s(ok(X)) → ok(s(X))
length(ok(X)) → ok(length(X))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
isNat(ok(X)) → ok(isNat(X))
isNatList(ok(X)) → ok(isNatList(X))
isNatIList(ok(X)) → ok(isNatIList(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set
Used ordering:
length(nil) → 0
POL(0) = 0
POL(U11(x1, x2)) = 2·x1 + 2·x2
POL(and(x1, x2)) = 2·x1 + x2
POL(cons(x1, x2)) = x1 + 2·x2
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = 2·x1
POL(isNatList(x1)) = 0
POL(length(x1)) = 2·x1
POL(nil) = 2
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set
Used ordering:
isNatIList(V) → isNatList(V)
isNatIList(zeros) → tt
POL(0) = 0
POL(U11(x1, x2)) = 2·x1 + 2·x2
POL(and(x1, x2)) = 2·x1 + x2
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = 2
POL(isNatList(x1)) = 0
POL(length(x1)) = x1
POL(nil) = 1
POL(s(x1)) = 2·x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(length(V1)) → isNatList(V1)
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(nil) → tt
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
nil: empty set
Used ordering:
isNat(length(V1)) → isNatList(V1)
isNatList(nil) → tt
POL(0) = 0
POL(U11(x1, x2)) = 1 + 2·x1 + 2·x2
POL(and(x1, x2)) = x1 + 2·x2
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 1 + 2·x1
POL(nil) = 2
POL(s(x1)) = x1
POL(tt) = 0
POL(zeros) = 0
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros: empty set
cons: {1}
0: empty set
U11: {1}
tt: empty set
s: {1}
length: {1}
and: {1}
isNat: empty set
isNatList: empty set
isNatIList: empty set
Innermost Strategy.
U11'(tt, L) → LENGTH(L)
ISNAT(s(V1)) → ISNAT(V1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
ISNATILIST(cons(V1, V2)) → ISNAT(V1)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
ISNATLIST(cons(V1, V2)) → ISNAT(V1)
LENGTH(cons(N, L)) → U11'(and(isNatList(L), isNat(N)), L)
LENGTH(cons(N, L)) → AND(isNatList(L), isNat(N))
LENGTH(cons(N, L)) → ISNATLIST(L)
U11'(tt, L) → L
AND(tt, X) → X
zeros
isNatIList(x0)
isNatList(x0)
isNat(x0)
U11'(tt, L) → U(L)
AND(tt, X) → U(X)
U(zeros) → ZEROS
U(isNatIList(x0)) → ISNATILIST(x0)
U(isNatList(x0)) → ISNATLIST(x0)
U(isNat(x0)) → ISNAT(x0)
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
ISNAT(s(V1)) → ISNAT(V1)
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ISNAT(s(V1)) → ISNAT(V1)
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
AND(tt, X) → U(X)
U(isNatIList(x0)) → ISNATILIST(x0)
U(isNatList(x0)) → ISNATLIST(x0)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
zeros → cons(0, zeros)
U11(tt, x0) → s(length(x0))
and(tt, x0) → x0
isNatIList(cons(x0, x1)) → and(isNat(x0), isNatIList(x1))
isNatList(cons(x0, x1)) → and(isNat(x0), isNatList(x1))
length(cons(x0, x1)) → U11(and(isNatList(x1), isNat(x0)), x1)
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
AND(tt, X) → U(X)
U(isNatIList(x0)) → ISNATILIST(x0)
U(isNatList(x0)) → ISNATLIST(x0)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
AND(tt, X) → U(X)
U(isNatIList(x0)) → ISNATILIST(x0)
U(isNatList(x0)) → ISNATLIST(x0)
ISNATLIST(cons(V1, V2)) → AND(isNat(V1), isNatList(V2))
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
POL(0) = 2
POL(AND(x1, x2)) = 2 + x1 + 2·x2
POL(ISNATILIST(x1)) = 1 + 2·x1
POL(ISNATLIST(x1)) = 2·x1
POL(U(x1)) = 1 + x1
POL(cons(x1, x2)) = 2 + 2·x1 + 2·x2
POL(isNat(x1)) = 1 + 2·x1
POL(isNatIList(x1)) = 1 + 2·x1
POL(isNatList(x1)) = 2·x1
POL(s(x1)) = 2 + 2·x1
POL(tt) = 2
ISNATILIST(cons(V1, V2)) → AND(isNat(V1), isNatIList(V2))
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
LENGTH(cons(N, L)) → U11'(and(isNatList(L), isNat(N)), L)
U11'(tt, L) → LENGTH(L)
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))
POL( and(x1, x2) ) = max{0, x1 + x2 - 1}
POL( tt ) = 1
POL( isNatList(x1) ) = max{0, -1}
POL( cons(x1, x2) ) = max{0, x2 - 1}
POL( isNat(x1) ) = 1
POL( 0 ) = 2
POL( s(x1) ) = 1
POL( zeros ) = 2
POL( isNatIList(x1) ) = 1
POL( LENGTH(x1) ) = 1
POL( U11'(x1, x2) ) = x1
and(tt, X) → X
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
zeros → cons(0, zeros)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
LENGTH(cons(N, L)) → U11'(and(isNatList(L), isNat(N)), L)
U11'(tt, L) → LENGTH(L)
zeros → cons(0, zeros)
U11(tt, L) → s(length(L))
and(tt, X) → X
isNat(0) → tt
isNat(s(V1)) → isNat(V1)
isNatIList(cons(V1, V2)) → and(isNat(V1), isNatIList(V2))
isNatList(cons(V1, V2)) → and(isNat(V1), isNatList(V2))
length(cons(N, L)) → U11(and(isNatList(L), isNat(N)), L)
zeros
U11(tt, x0)
and(tt, x0)
isNat(0)
isNat(s(x0))
isNatIList(cons(x0, x1))
isNatList(cons(x0, x1))
length(cons(x0, x1))