and(tt, T) → T
isNatIList(IL) → isNatList(activate(IL))
isNat(n__0) → tt
isNat(n__s(N)) → isNat(activate(N))
isNat(n__length(L)) → isNatList(activate(L))
isNatIList(n__zeros) → tt
isNatIList(n__cons(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
isNatList(n__nil) → tt
isNatList(n__cons(N, L)) → and(isNat(activate(N)), isNatList(activate(L)))
isNatList(n__take(N, IL)) → and(isNat(activate(N)), isNatIList(activate(IL)))
zeros → cons(0, n__zeros)
take(0, IL) → uTake1(isNatIList(IL))
uTake1(tt) → nil
take(s(M), cons(N, IL)) → uTake2(and(isNat(M), and(isNat(N), isNatIList(activate(IL)))), M, N, activate(IL))
uTake2(tt, M, N, IL) → cons(activate(N), n__take(activate(M), activate(IL)))
length(cons(N, L)) → uLength(and(isNat(N), isNatList(activate(L))), activate(L))
uLength(tt, L) → s(length(activate(L)))
0 → n__0
s(X) → n__s(X)
length(X) → n__length(X)
zeros → n__zeros
cons(X1, X2) → n__cons(X1, X2)
nil → n__nil
take(X1, X2) → n__take(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(n__length(X)) → length(X)
activate(n__zeros) → zeros
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__nil) → nil
activate(n__take(X1, X2)) → take(X1, X2)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Infered types.
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Heuristically decided to analyse the following defined symbols:
isNatIList', isNatList', activate', isNat', length'
They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))
The following defined symbols remain to be analysed:
isNatList', isNatIList', activate', isNat', length'
They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'
Could not prove a rewrite lemma for the defined symbol isNatList'.
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))
The following defined symbols remain to be analysed:
isNat', isNatIList', activate', length'
They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'
Proved the following rewrite lemma:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + n41)
Induction Base:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0)) →RΩ(1)
tt'
Induction Step:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(_$n42, 1))) →RΩ(1)
isNat'(activate'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n42))) →RΩ(1)
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_$n42)) →IH
tt'
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + n41)
Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))
The following defined symbols remain to be analysed:
activate', isNatIList', isNatList', length'
They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'
Could not prove a rewrite lemma for the defined symbol activate'.
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + n41)
Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))
The following defined symbols remain to be analysed:
length', isNatIList', isNatList'
They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'
Could not prove a rewrite lemma for the defined symbol length'.
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + n41)
Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))
The following defined symbols remain to be analysed:
isNatIList', isNatList'
They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'
Could not prove a rewrite lemma for the defined symbol isNatIList'.
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + n41)
Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))
The following defined symbols remain to be analysed:
isNatList'
They will be analysed ascendingly in the following order:
isNatIList' = isNatList'
isNatIList' = activate'
isNatIList' = isNat'
isNatIList' = length'
isNatList' = activate'
isNatList' = isNat'
isNatList' = length'
activate' = isNat'
activate' = length'
isNat' = length'
Could not prove a rewrite lemma for the defined symbol isNatList'.
Rules:
and'(tt', T) → T
isNatIList'(IL) → isNatList'(activate'(IL))
isNat'(n__0') → tt'
isNat'(n__s'(N)) → isNat'(activate'(N))
isNat'(n__length'(L)) → isNatList'(activate'(L))
isNatIList'(n__zeros') → tt'
isNatIList'(n__cons'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
isNatList'(n__nil') → tt'
isNatList'(n__cons'(N, L)) → and'(isNat'(activate'(N)), isNatList'(activate'(L)))
isNatList'(n__take'(N, IL)) → and'(isNat'(activate'(N)), isNatIList'(activate'(IL)))
zeros' → cons'(0', n__zeros')
take'(0', IL) → uTake1'(isNatIList'(IL))
uTake1'(tt') → nil'
take'(s'(M), cons'(N, IL)) → uTake2'(and'(isNat'(M), and'(isNat'(N), isNatIList'(activate'(IL)))), M, N, activate'(IL))
uTake2'(tt', M, N, IL) → cons'(activate'(N), n__take'(activate'(M), activate'(IL)))
length'(cons'(N, L)) → uLength'(and'(isNat'(N), isNatList'(activate'(L))), activate'(L))
uLength'(tt', L) → s'(length'(activate'(L)))
0' → n__0'
s'(X) → n__s'(X)
length'(X) → n__length'(X)
zeros' → n__zeros'
cons'(X1, X2) → n__cons'(X1, X2)
nil' → n__nil'
take'(X1, X2) → n__take'(X1, X2)
activate'(n__0') → 0'
activate'(n__s'(X)) → s'(X)
activate'(n__length'(X)) → length'(X)
activate'(n__zeros') → zeros'
activate'(n__cons'(X1, X2)) → cons'(X1, X2)
activate'(n__nil') → nil'
activate'(n__take'(X1, X2)) → take'(X1, X2)
activate'(X) → X
Types:
and' :: tt' → tt' → tt'
tt' :: tt'
isNatIList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
isNatList' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
activate' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
isNat' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → tt'
n__0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
n__take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
zeros' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
cons' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
0' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
take' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake1' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
nil' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
s' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uTake2' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
length' :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
uLength' :: tt' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take' → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_hole_tt'1 :: tt'
_hole_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'2 :: n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3 :: Nat → n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'
Lemmas:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + n41)
Generator Equations:
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(0) ⇔ n__0'
_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(+(x, 1)) ⇔ n__s'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
isNat'(_gen_n__0':n__s':n__length':n__zeros':n__cons':n__nil':n__take'3(_n41)) → tt', rt ∈ Ω(1 + n41)