PrintForm Definitions languages Sections AutomataTheory Doc

At: lang power functionality 1 1 1

1. Alph: Type
2. L: LangOver(Alph)
3. L': LangOver(Alph)
4. n:
5. n':
6. L = L'

(Ln) = (L'n)

By: NatInd 4

Generated subgoals:

14. n':
5. L = L'
(L0) = (L'0)
24. n':
5. L = L'
6. n:
7. 0 < n
8. (Ln-1) = (L'n-1)
(Ln) = (L'n)


About:
universenatural_number