PrintForm Definitions languages Sections AutomataTheory Doc

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

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

By: Eval [`lang_eq`] 0

Generated subgoal:

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


About:
ifthenelsenatural_numbersubtractuniverseint
less_thanalllistapply