Thms
list
3
autom
Sections
AutomataTheory
Doc
add_action
Def
(+f)(l) == Case of l; nil
nil ; h.l'
[h; f(h)/ (+f)(l')] (recursive)
Thm*
St:Type, l:St*, f:(St
St). (+f)(l)
St*
About:
nil ; h.l' [h; f(h)/ (+f)(l')] (recursive)
St:Type, l:St*, f:(St
St). (+f)(l) 
St* nil ; h.l' [h; f(h)/ (+f)(l')] (recursive)
