PrintForm Definitions languages Sections AutomataTheory Doc

At: lang power functionality 1 1 1 2 1 1 1

1. Alph: Type
2. L: LangOver(Alph)
3. L': LangOver(Alph)
4. n':
5. L = L'
6. n:
7. 0 < n
8. (Ln-1) = (L'n-1)
9. l: Alph*

if n=0 else ((Ln-1)L) fi(l) if n=0 else ((L'n-1)L') fi(l)

By: SplitOnConclITE

Generated subgoals:

110. n = 0
(l) (l)
210. n = 0
((Ln-1)L)(l) ((L'n-1)L')(l)


About:
applyifthenelsenatural_numbersubtractuniverseintless_thanlist