PrintForm
Definitions
exponent
Sections
AutomataTheory
Doc
At:
auto2
lemma
5
1
1
1
1
1
1
2
1
1
1
3
1.
Alph:
Type
2.
n:
3.
n1:
4.
f:
n1
Alph
5.
Bij(
n1; Alph; f)
6.
f:((
n
n1)
(n1
n)). Bij(
n
n1;
(n1
n); f)
7.
f1:
(
n
n1)
(n1
n)
8.
g:
(n1
n)
n
n1
9.
InvFuns(
n
n1;
(n1
n); f1; g)
10.
a1:
(n1
n)
11.
a2:
(n1
n)
((f o g(a2))[
n])
{l:(Alph*)| ||l|| = n }
By:
Analyze
Generated subgoals:
None
About:
n1
Alphn1; Alph; f)
f:((nn1)(n1
n)). Bij(nn1; (n1n); f)nn1)(n1n)(n1n)nn1nn1; (n1n); f1; g)(n1n)(n1n)
((f o g(a2))[n]) 
{l:(Alph*)| ||l|| = n }
