TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60011 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (3852ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (5ms), ReductionPairSAT (7527ms)].
| – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (1028ms), PolynomialLinearRange4iUR (66ms), DependencyGraph (1035ms), PolynomialLinearRange8NegiUR (54ms), DependencyGraph (1031ms), ReductionPairSAT (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| isNatIList#(n__cons(V1, V2)) | → | U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | | U41#(tt, V1, V2) | → | U42#(isNat(activate(V1)), activate(V2)) |
| U42#(tt, V2) | → | isNatIList#(activate(V2)) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, V1) | → | U12(isNatList(activate(V1))) |
| U12(tt) | → | tt | | U21(tt, V1) | → | U22(isNat(activate(V1))) |
| U22(tt) | → | tt | | U31(tt, V) | → | U32(isNatList(activate(V))) |
| U32(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isNat(activate(V1)), activate(V2)) |
| U42(tt, V2) | → | U43(isNatIList(activate(V2))) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNat(activate(V1)), activate(V2)) | | U52(tt, V2) | → | U53(isNatList(activate(V2))) |
| U53(tt) | → | tt | | U61(tt, L) | → | s(length(activate(L))) |
| and(tt, X) | → | activate(X) | | isNat(n__0) | → | tt |
| isNat(n__length(V1)) | → | U11(isNatIListKind(activate(V1)), activate(V1)) | | isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)), activate(V1)) |
| isNatIList(V) | → | U31(isNatIListKind(activate(V)), activate(V)) | | isNatIList(n__zeros) | → | tt |
| isNatIList(n__cons(V1, V2)) | → | U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | | isNatIListKind(n__nil) | → | tt |
| isNatIListKind(n__zeros) | → | tt | | isNatIListKind(n__cons(V1, V2)) | → | and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| isNatKind(n__0) | → | tt | | isNatKind(n__length(V1)) | → | isNatIListKind(activate(V1)) |
| isNatKind(n__s(V1)) | → | isNatKind(activate(V1)) | | isNatList(n__nil) | → | tt |
| isNatList(n__cons(V1, V2)) | → | U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U61(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)) | | zeros | → | n__zeros |
| 0 | → | n__0 | | length(X) | → | n__length(X) |
| s(X) | → | n__s(X) | | cons(X1, X2) | → | n__cons(X1, X2) |
| isNatIListKind(X) | → | n__isNatIListKind(X) | | nil | → | n__nil |
| and(X1, X2) | → | n__and(X1, X2) | | isNat(X) | → | n__isNat(X) |
| isNatKind(X) | → | n__isNatKind(X) | | activate(n__zeros) | → | zeros |
| activate(n__0) | → | 0 | | activate(n__length(X)) | → | length(activate(X)) |
| activate(n__s(X)) | → | s(activate(X)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__isNatIListKind(X)) | → | isNatIListKind(X) | | activate(n__nil) | → | nil |
| activate(n__and(X1, X2)) | → | and(activate(X1), X2) | | activate(n__isNat(X)) | → | isNat(X) |
| activate(n__isNatKind(X)) | → | isNatKind(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, n__s, isNat, activate, n__0, U43, U61, U42, U41, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, n__isNat, and, n__and, n__cons, 0, isNatList, U51, s, tt, zeros, U53, U52, U11, U12, U31, U32, n__isNatKind, nil
Open Dependency Pair Problem 3
Dependency Pairs
| and#(tt, X) | → | activate#(X) | | U11#(tt, V1) | → | isNatList#(activate(V1)) |
| activate#(n__and(X1, X2)) | → | activate#(X1) | | U51#(tt, V1, V2) | → | isNat#(activate(V1)) |
| U51#(tt, V1, V2) | → | activate#(V2) | | U51#(tt, V1, V2) | → | activate#(V1) |
| activate#(n__length(X)) | → | activate#(X) | | activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) |
| activate#(n__s(X)) | → | activate#(X) | | U52#(tt, V2) | → | isNatList#(activate(V2)) |
| U51#(tt, V1, V2) | → | U52#(isNat(activate(V1)), activate(V2)) | | isNatKind#(n__length(V1)) | → | activate#(V1) |
| isNatKind#(n__s(V1)) | → | activate#(V1) | | isNatList#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | | activate#(n__isNat(X)) | → | isNat#(X) |
| length#(cons(N, L)) | → | U61#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)) | | isNat#(n__s(V1)) | → | activate#(V1) |
| isNat#(n__length(V1)) | → | activate#(V1) | | isNatIListKind#(n__cons(V1, V2)) | → | activate#(V2) |
| activate#(n__isNatIListKind(X)) | → | isNatIListKind#(X) | | isNatList#(n__cons(V1, V2)) | → | U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) |
| U52#(tt, V2) | → | activate#(V2) | | length#(cons(N, L)) | → | and#(isNatList(activate(L)), n__isNatIListKind(activate(L))) |
| U21#(tt, V1) | → | activate#(V1) | | isNatKind#(n__length(V1)) | → | isNatIListKind#(activate(V1)) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V2) | | isNatIListKind#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) |
| U11#(tt, V1) | → | activate#(V1) | | isNat#(n__length(V1)) | → | U11#(isNatIListKind(activate(V1)), activate(V1)) |
| isNatList#(n__cons(V1, V2)) | → | and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) | | activate#(n__length(X)) | → | length#(activate(X)) |
| U61#(tt, L) | → | length#(activate(L)) | | length#(cons(N, L)) | → | isNatList#(activate(L)) |
| activate#(n__isNatKind(X)) | → | isNatKind#(X) | | U61#(tt, L) | → | activate#(L) |
| length#(cons(N, L)) | → | and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))) | | isNatIListKind#(n__cons(V1, V2)) | → | and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V1) | | isNat#(n__length(V1)) | → | isNatIListKind#(activate(V1)) |
| isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | | U21#(tt, V1) | → | isNat#(activate(V1)) |
| isNatIListKind#(n__cons(V1, V2)) | → | activate#(V1) | | isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)), activate(V1)) |
| isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) | | length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, V1) | → | U12(isNatList(activate(V1))) |
| U12(tt) | → | tt | | U21(tt, V1) | → | U22(isNat(activate(V1))) |
| U22(tt) | → | tt | | U31(tt, V) | → | U32(isNatList(activate(V))) |
| U32(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isNat(activate(V1)), activate(V2)) |
| U42(tt, V2) | → | U43(isNatIList(activate(V2))) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNat(activate(V1)), activate(V2)) | | U52(tt, V2) | → | U53(isNatList(activate(V2))) |
| U53(tt) | → | tt | | U61(tt, L) | → | s(length(activate(L))) |
| and(tt, X) | → | activate(X) | | isNat(n__0) | → | tt |
| isNat(n__length(V1)) | → | U11(isNatIListKind(activate(V1)), activate(V1)) | | isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)), activate(V1)) |
| isNatIList(V) | → | U31(isNatIListKind(activate(V)), activate(V)) | | isNatIList(n__zeros) | → | tt |
| isNatIList(n__cons(V1, V2)) | → | U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | | isNatIListKind(n__nil) | → | tt |
| isNatIListKind(n__zeros) | → | tt | | isNatIListKind(n__cons(V1, V2)) | → | and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| isNatKind(n__0) | → | tt | | isNatKind(n__length(V1)) | → | isNatIListKind(activate(V1)) |
| isNatKind(n__s(V1)) | → | isNatKind(activate(V1)) | | isNatList(n__nil) | → | tt |
| isNatList(n__cons(V1, V2)) | → | U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U61(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)) | | zeros | → | n__zeros |
| 0 | → | n__0 | | length(X) | → | n__length(X) |
| s(X) | → | n__s(X) | | cons(X1, X2) | → | n__cons(X1, X2) |
| isNatIListKind(X) | → | n__isNatIListKind(X) | | nil | → | n__nil |
| and(X1, X2) | → | n__and(X1, X2) | | isNat(X) | → | n__isNat(X) |
| isNatKind(X) | → | n__isNatKind(X) | | activate(n__zeros) | → | zeros |
| activate(n__0) | → | 0 | | activate(n__length(X)) | → | length(activate(X)) |
| activate(n__s(X)) | → | s(activate(X)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__isNatIListKind(X)) | → | isNatIListKind(X) | | activate(n__nil) | → | nil |
| activate(n__and(X1, X2)) | → | and(activate(X1), X2) | | activate(n__isNat(X)) | → | isNat(X) |
| activate(n__isNatKind(X)) | → | isNatKind(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, n__s, isNat, activate, n__0, U43, U61, U42, U41, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, n__isNat, and, n__and, n__cons, 0, isNatList, U51, s, tt, zeros, U53, U52, U11, U12, U31, U32, n__isNatKind, nil
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| and#(tt, X) | → | activate#(X) | | U11#(tt, V1) | → | isNatList#(activate(V1)) |
| isNatIList#(V) | → | U31#(isNatIListKind(activate(V)), activate(V)) | | U51#(tt, V1, V2) | → | activate#(V1) |
| activate#(n__and(X1, X2)) | → | and#(activate(X1), X2) | | zeros# | → | 0# |
| U21#(tt, V1) | → | U22#(isNat(activate(V1))) | | activate#(n__cons(X1, X2)) | → | cons#(activate(X1), X2) |
| activate#(n__cons(X1, X2)) | → | activate#(X1) | | activate#(n__isNat(X)) | → | isNat#(X) |
| U42#(tt, V2) | → | U43#(isNatIList(activate(V2))) | | isNatIList#(n__cons(V1, V2)) | → | U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) |
| isNat#(n__s(V1)) | → | activate#(V1) | | isNat#(n__length(V1)) | → | activate#(V1) |
| isNatIListKind#(n__cons(V1, V2)) | → | activate#(V2) | | activate#(n__isNatIListKind(X)) | → | isNatIListKind#(X) |
| length#(nil) | → | 0# | | U52#(tt, V2) | → | activate#(V2) |
| length#(cons(N, L)) | → | and#(isNatList(activate(L)), n__isNatIListKind(activate(L))) | | isNatKind#(n__length(V1)) | → | isNatIListKind#(activate(V1)) |
| isNatIList#(V) | → | isNatIListKind#(activate(V)) | | isNatList#(n__cons(V1, V2)) | → | activate#(V2) |
| isNatIListKind#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) | | isNatList#(n__cons(V1, V2)) | → | and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| isNatIList#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) | | activate#(n__length(X)) | → | length#(activate(X)) |
| U11#(tt, V1) | → | U12#(isNatList(activate(V1))) | | U61#(tt, L) | → | s#(length(activate(L))) |
| U41#(tt, V1, V2) | → | activate#(V1) | | length#(cons(N, L)) | → | isNatList#(activate(L)) |
| activate#(n__isNatKind(X)) | → | isNatKind#(X) | | U61#(tt, L) | → | activate#(L) |
| length#(cons(N, L)) | → | and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))) | | isNatIList#(n__cons(V1, V2)) | → | and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| activate#(n__0) | → | 0# | | U41#(tt, V1, V2) | → | U42#(isNat(activate(V1)), activate(V2)) |
| isNatKind#(n__s(V1)) | → | isNatKind#(activate(V1)) | | isNatIListKind#(n__cons(V1, V2)) | → | activate#(V1) |
| isNat#(n__s(V1)) | → | U21#(isNatKind(activate(V1)), activate(V1)) | | isNat#(n__s(V1)) | → | isNatKind#(activate(V1)) |
| activate#(n__zeros) | → | zeros# | | isNatIList#(n__cons(V1, V2)) | → | activate#(V2) |
| activate#(n__and(X1, X2)) | → | activate#(X1) | | U51#(tt, V1, V2) | → | isNat#(activate(V1)) |
| activate#(n__length(X)) | → | activate#(X) | | U51#(tt, V1, V2) | → | activate#(V2) |
| activate#(n__s(X)) | → | activate#(X) | | isNatKind#(n__length(V1)) | → | activate#(V1) |
| U52#(tt, V2) | → | isNatList#(activate(V2)) | | U51#(tt, V1, V2) | → | U52#(isNat(activate(V1)), activate(V2)) |
| isNatKind#(n__s(V1)) | → | activate#(V1) | | isNatList#(n__cons(V1, V2)) | → | isNatKind#(activate(V1)) |
| U31#(tt, V) | → | activate#(V) | | U42#(tt, V2) | → | activate#(V2) |
| isNatIList#(V) | → | activate#(V) | | length#(cons(N, L)) | → | U61#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)) |
| U42#(tt, V2) | → | isNatIList#(activate(V2)) | | isNatList#(n__cons(V1, V2)) | → | U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) |
| U41#(tt, V1, V2) | → | isNat#(activate(V1)) | | zeros# | → | cons#(0, n__zeros) |
| U21#(tt, V1) | → | activate#(V1) | | U31#(tt, V) | → | isNatList#(activate(V)) |
| isNat#(n__length(V1)) | → | U11#(isNatIListKind(activate(V1)), activate(V1)) | | U11#(tt, V1) | → | activate#(V1) |
| U41#(tt, V1, V2) | → | activate#(V2) | | U52#(tt, V2) | → | U53#(isNatList(activate(V2))) |
| U31#(tt, V) | → | U32#(isNatList(activate(V))) | | U61#(tt, L) | → | length#(activate(L)) |
| activate#(n__nil) | → | nil# | | isNatIListKind#(n__cons(V1, V2)) | → | and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| isNatList#(n__cons(V1, V2)) | → | activate#(V1) | | isNat#(n__length(V1)) | → | isNatIListKind#(activate(V1)) |
| U21#(tt, V1) | → | isNat#(activate(V1)) | | activate#(n__s(X)) | → | s#(activate(X)) |
| isNatIList#(n__cons(V1, V2)) | → | activate#(V1) | | length#(cons(N, L)) | → | activate#(L) |
Rewrite Rules
| zeros | → | cons(0, n__zeros) | | U11(tt, V1) | → | U12(isNatList(activate(V1))) |
| U12(tt) | → | tt | | U21(tt, V1) | → | U22(isNat(activate(V1))) |
| U22(tt) | → | tt | | U31(tt, V) | → | U32(isNatList(activate(V))) |
| U32(tt) | → | tt | | U41(tt, V1, V2) | → | U42(isNat(activate(V1)), activate(V2)) |
| U42(tt, V2) | → | U43(isNatIList(activate(V2))) | | U43(tt) | → | tt |
| U51(tt, V1, V2) | → | U52(isNat(activate(V1)), activate(V2)) | | U52(tt, V2) | → | U53(isNatList(activate(V2))) |
| U53(tt) | → | tt | | U61(tt, L) | → | s(length(activate(L))) |
| and(tt, X) | → | activate(X) | | isNat(n__0) | → | tt |
| isNat(n__length(V1)) | → | U11(isNatIListKind(activate(V1)), activate(V1)) | | isNat(n__s(V1)) | → | U21(isNatKind(activate(V1)), activate(V1)) |
| isNatIList(V) | → | U31(isNatIListKind(activate(V)), activate(V)) | | isNatIList(n__zeros) | → | tt |
| isNatIList(n__cons(V1, V2)) | → | U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | | isNatIListKind(n__nil) | → | tt |
| isNatIListKind(n__zeros) | → | tt | | isNatIListKind(n__cons(V1, V2)) | → | and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| isNatKind(n__0) | → | tt | | isNatKind(n__length(V1)) | → | isNatIListKind(activate(V1)) |
| isNatKind(n__s(V1)) | → | isNatKind(activate(V1)) | | isNatList(n__nil) | → | tt |
| isNatList(n__cons(V1, V2)) | → | U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | | length(nil) | → | 0 |
| length(cons(N, L)) | → | U61(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)) | | zeros | → | n__zeros |
| 0 | → | n__0 | | length(X) | → | n__length(X) |
| s(X) | → | n__s(X) | | cons(X1, X2) | → | n__cons(X1, X2) |
| isNatIListKind(X) | → | n__isNatIListKind(X) | | nil | → | n__nil |
| and(X1, X2) | → | n__and(X1, X2) | | isNat(X) | → | n__isNat(X) |
| isNatKind(X) | → | n__isNatKind(X) | | activate(n__zeros) | → | zeros |
| activate(n__0) | → | 0 | | activate(n__length(X)) | → | length(activate(X)) |
| activate(n__s(X)) | → | s(activate(X)) | | activate(n__cons(X1, X2)) | → | cons(activate(X1), X2) |
| activate(n__isNatIListKind(X)) | → | isNatIListKind(X) | | activate(n__nil) | → | nil |
| activate(n__and(X1, X2)) | → | and(activate(X1), X2) | | activate(n__isNat(X)) | → | isNat(X) |
| activate(n__isNatKind(X)) | → | isNatKind(X) | | activate(X) | → | X |
Original Signature
Termination of terms over the following signature is verified: n__isNatIListKind, isNatIListKind, activate, isNat, n__s, U61, U43, n__0, U42, U41, length, n__nil, n__zeros, U21, U22, cons, isNatIList, n__length, isNatKind, n__isNat, and, n__and, n__cons, 0, s, U51, isNatList, zeros, tt, U53, U52, U11, U12, U31, U32, nil, n__isNatKind
Strategy
The following SCCs where found
| isNatIList#(n__cons(V1, V2)) → U41#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) | U41#(tt, V1, V2) → U42#(isNat(activate(V1)), activate(V2)) |
| U42#(tt, V2) → isNatIList#(activate(V2)) |
| and#(tt, X) → activate#(X) | U11#(tt, V1) → isNatList#(activate(V1)) |
| U51#(tt, V1, V2) → isNat#(activate(V1)) | activate#(n__and(X1, X2)) → activate#(X1) |
| activate#(n__length(X)) → activate#(X) | U51#(tt, V1, V2) → activate#(V1) |
| U51#(tt, V1, V2) → activate#(V2) | activate#(n__and(X1, X2)) → and#(activate(X1), X2) |
| activate#(n__s(X)) → activate#(X) | isNatKind#(n__length(V1)) → activate#(V1) |
| U51#(tt, V1, V2) → U52#(isNat(activate(V1)), activate(V2)) | U52#(tt, V2) → isNatList#(activate(V2)) |
| isNatKind#(n__s(V1)) → activate#(V1) | isNatList#(n__cons(V1, V2)) → isNatKind#(activate(V1)) |
| activate#(n__cons(X1, X2)) → activate#(X1) | activate#(n__isNat(X)) → isNat#(X) |
| length#(cons(N, L)) → U61#(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))), activate(L)) | isNat#(n__length(V1)) → activate#(V1) |
| isNat#(n__s(V1)) → activate#(V1) | activate#(n__isNatIListKind(X)) → isNatIListKind#(X) |
| isNatIListKind#(n__cons(V1, V2)) → activate#(V2) | isNatList#(n__cons(V1, V2)) → U51#(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1), activate(V2)) |
| length#(cons(N, L)) → and#(isNatList(activate(L)), n__isNatIListKind(activate(L))) | U52#(tt, V2) → activate#(V2) |
| U21#(tt, V1) → activate#(V1) | isNatList#(n__cons(V1, V2)) → activate#(V2) |
| isNatKind#(n__length(V1)) → isNatIListKind#(activate(V1)) | isNatIListKind#(n__cons(V1, V2)) → isNatKind#(activate(V1)) |
| isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1)) | U11#(tt, V1) → activate#(V1) |
| isNatList#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) | activate#(n__length(X)) → length#(activate(X)) |
| U61#(tt, L) → length#(activate(L)) | length#(cons(N, L)) → isNatList#(activate(L)) |
| activate#(n__isNatKind(X)) → isNatKind#(X) | U61#(tt, L) → activate#(L) |
| length#(cons(N, L)) → and#(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(n__isNat(N), n__isNatKind(N))) | isNatIListKind#(n__cons(V1, V2)) → and#(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) |
| isNatList#(n__cons(V1, V2)) → activate#(V1) | isNat#(n__length(V1)) → isNatIListKind#(activate(V1)) |
| isNatIListKind#(n__cons(V1, V2)) → activate#(V1) | U21#(tt, V1) → isNat#(activate(V1)) |
| isNatKind#(n__s(V1)) → isNatKind#(activate(V1)) | isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1)) |
| length#(cons(N, L)) → activate#(L) | isNat#(n__s(V1)) → isNatKind#(activate(V1)) |