PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: length reverse 1 2 1 1

1. T: Type
2. l: T*
3. u: T
4. v: T*
5. ||rev(v)|| = ||v||

||rev(v)||+||[u]|| = ||v||+1

By: Reduce 0

Generated subgoals:

None


About:
equalintaddconsnilnatural_numberuniverselist