zeros → cons(0, n__zeros)
U11(tt, L) → U12(tt, activate(L))
U12(tt, L) → s(length(activate(L)))
length(nil) → 0
length(cons(N, L)) → U11(tt, activate(L))
zeros → n__zeros
activate(n__zeros) → zeros
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) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
length'(nil') → 0'
length'(cons'(N, L)) → U11'(tt', activate'(L))
zeros' → n__zeros'
activate'(n__zeros') → zeros'
activate'(X) → X
Sliced the following arguments:
cons'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
zeros' → cons'(n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
length'(nil') → 0'
length'(cons'(L)) → U11'(tt', activate'(L))
zeros' → n__zeros'
activate'(n__zeros') → zeros'
activate'(X) → X
Infered types.
Rules:
zeros' → cons'(n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
length'(nil') → 0'
length'(cons'(L)) → U11'(tt', activate'(L))
zeros' → n__zeros'
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
zeros' :: n__zeros':cons':nil'
cons' :: n__zeros':cons':nil' → n__zeros':cons':nil'
n__zeros' :: n__zeros':cons':nil'
U11' :: tt' → n__zeros':cons':nil' → s':0'
tt' :: tt'
U12' :: tt' → n__zeros':cons':nil' → s':0'
activate' :: n__zeros':cons':nil' → n__zeros':cons':nil'
s' :: s':0' → s':0'
length' :: n__zeros':cons':nil' → s':0'
nil' :: n__zeros':cons':nil'
0' :: s':0'
_hole_n__zeros':cons':nil'1 :: n__zeros':cons':nil'
_hole_s':0'2 :: s':0'
_hole_tt'3 :: tt'
_gen_n__zeros':cons':nil'4 :: Nat → n__zeros':cons':nil'
_gen_s':0'5 :: Nat → s':0'
Heuristically decided to analyse the following defined symbols:
length'
Rules:
zeros' → cons'(n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
length'(nil') → 0'
length'(cons'(L)) → U11'(tt', activate'(L))
zeros' → n__zeros'
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
zeros' :: n__zeros':cons':nil'
cons' :: n__zeros':cons':nil' → n__zeros':cons':nil'
n__zeros' :: n__zeros':cons':nil'
U11' :: tt' → n__zeros':cons':nil' → s':0'
tt' :: tt'
U12' :: tt' → n__zeros':cons':nil' → s':0'
activate' :: n__zeros':cons':nil' → n__zeros':cons':nil'
s' :: s':0' → s':0'
length' :: n__zeros':cons':nil' → s':0'
nil' :: n__zeros':cons':nil'
0' :: s':0'
_hole_n__zeros':cons':nil'1 :: n__zeros':cons':nil'
_hole_s':0'2 :: s':0'
_hole_tt'3 :: tt'
_gen_n__zeros':cons':nil'4 :: Nat → n__zeros':cons':nil'
_gen_s':0'5 :: Nat → s':0'
Generator Equations:
_gen_n__zeros':cons':nil'4(0) ⇔ n__zeros'
_gen_n__zeros':cons':nil'4(+(x, 1)) ⇔ cons'(_gen_n__zeros':cons':nil'4(x))
_gen_s':0'5(0) ⇔ 0'
_gen_s':0'5(+(x, 1)) ⇔ s'(_gen_s':0'5(x))
The following defined symbols remain to be analysed:
length'
Could not prove a rewrite lemma for the defined symbol length'.
Rules:
zeros' → cons'(n__zeros')
U11'(tt', L) → U12'(tt', activate'(L))
U12'(tt', L) → s'(length'(activate'(L)))
length'(nil') → 0'
length'(cons'(L)) → U11'(tt', activate'(L))
zeros' → n__zeros'
activate'(n__zeros') → zeros'
activate'(X) → X
Types:
zeros' :: n__zeros':cons':nil'
cons' :: n__zeros':cons':nil' → n__zeros':cons':nil'
n__zeros' :: n__zeros':cons':nil'
U11' :: tt' → n__zeros':cons':nil' → s':0'
tt' :: tt'
U12' :: tt' → n__zeros':cons':nil' → s':0'
activate' :: n__zeros':cons':nil' → n__zeros':cons':nil'
s' :: s':0' → s':0'
length' :: n__zeros':cons':nil' → s':0'
nil' :: n__zeros':cons':nil'
0' :: s':0'
_hole_n__zeros':cons':nil'1 :: n__zeros':cons':nil'
_hole_s':0'2 :: s':0'
_hole_tt'3 :: tt'
_gen_n__zeros':cons':nil'4 :: Nat → n__zeros':cons':nil'
_gen_s':0'5 :: Nat → s':0'
Generator Equations:
_gen_n__zeros':cons':nil'4(0) ⇔ n__zeros'
_gen_n__zeros':cons':nil'4(+(x, 1)) ⇔ cons'(_gen_n__zeros':cons':nil'4(x))
_gen_s':0'5(0) ⇔ 0'
_gen_s':0'5(+(x, 1)) ⇔ s'(_gen_s':0'5(x))
No more defined symbols left to analyse.