PrintForm Definitions languages Sections AutomataTheory Doc

At: lang power functionality 1 1 1 2 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)

l:Alph*. if n=0 else ((Ln-1)L) fi(l) if n=0 else ((L'n-1)L') fi(l)

By: Analyze 0

Generated subgoal:

19. l: Alph*
if n=0 else ((Ln-1)L) fi(l) if n=0 else ((L'n-1)L') fi(l)


About:
alllistapplyifthenelsenatural_number
subtractuniverseintless_than