zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(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)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(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__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Infered types.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Heuristically decided to analyse the following defined symbols:
length', activate', and', isNat', isNatList', isNatIList'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
The following defined symbols remain to be analysed:
and', length', activate', isNat', isNatList', isNatIList'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Could not prove a rewrite lemma for the defined symbol and'.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
The following defined symbols remain to be analysed:
activate', length', isNat', isNatList', isNatIList'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Proved the following rewrite lemma:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)
Induction Base:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, 0)))
Induction Step:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, +(_$n11, 1)))) →RΩ(1)
length'(activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _$n11)))) →IH
length'(_*3)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Lemmas:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
The following defined symbols remain to be analysed:
length', and', isNat', isNatList', isNatIList'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Could not prove a rewrite lemma for the defined symbol length'.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Lemmas:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
The following defined symbols remain to be analysed:
isNatList', and', isNat', isNatIList'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Could not prove a rewrite lemma for the defined symbol isNatList'.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Lemmas:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
The following defined symbols remain to be analysed:
isNat', and', isNatIList'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Could not prove a rewrite lemma for the defined symbol isNat'.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Lemmas:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
The following defined symbols remain to be analysed:
isNatIList', and'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Could not prove a rewrite lemma for the defined symbol isNatIList'.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Lemmas:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
The following defined symbols remain to be analysed:
and'
They will be analysed ascendingly in the following order:
length' = activate'
length' = and'
length' = isNat'
length' = isNatList'
length' = isNatIList'
activate' = and'
activate' = isNat'
activate' = isNatList'
activate' = isNatIList'
and' = isNat'
and' = isNatList'
and' = isNatIList'
isNat' = isNatList'
isNat' = isNatIList'
isNatList' = isNatIList'
Could not prove a rewrite lemma for the defined symbol and'.
Rules:
zeros' → cons'(0', n__zeros')
U11'(tt', L) → s'(length'(activate'(L)))
and'(tt', X) → activate'(X)
isNat'(n__0') → tt'
isNat'(n__length'(V1)) → isNatList'(activate'(V1))
isNat'(n__s'(V1)) → isNat'(activate'(V1))
isNatIList'(V) → isNatList'(activate'(V))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatIList'(activate'(V2)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(V1, V2)) → and'(isNat'(activate'(V1)), n__isNatList'(activate'(V2)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(and'(isNatList'(activate'(L)), n__isNat'(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)
isNatIList'(X) → n__isNatIList'(X)
nil' → n__nil'
isNatList'(X) → n__isNatList'(X)
isNat'(X) → n__isNat'(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__isNatIList'(X)) → isNatIList'(X)
activate'(n__nil') → nil'
activate'(n__isNatList'(X)) → isNatList'(X)
activate'(n__isNat'(X)) → isNat'(X)
activate'(X) → X
Types:
zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__zeros' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
U11' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
tt' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
activate' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
and' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__0' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__length' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__s' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__cons' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatIList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNatList' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
nil' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
n__isNat' :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat' → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_hole_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'1 :: n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2 :: Nat → n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'
Lemmas:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)
Generator Equations:
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(0) ⇔ n__zeros'
_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(x, 1)) ⇔ n__length'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
activate'(_gen_n__zeros':tt':n__0':n__length':n__s':n__cons':n__isNatIList':n__nil':n__isNatList':n__isNat'2(+(1, _n10))) → _*3, rt ∈ Ω(n10)