PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 5 1 1 1 1 1 1 2 2 1 1 1
1. Alph: Type
2. n:
3. n1:
4. f: n1Alph
5. Bij(n1; Alph; f)
6. f:((nn1)(n1n)). Bij(nn1; (n1n); f)
7. f1: (nn1)(n1n)
8. g: (n1n)nn1
9. InvFuns(nn1; (n1n); f1; g)
10. b: {l:(Alph*)| ||l|| = n }

a:(n1n). f o g(a) = (z:||b||. b[z]) nAlph
By: Inst Thm* f:(AB). Bij(A; B; f) (g:(BA). InvFuns(A; B; f; g)) [n1;Alph;f]
Generated subgoal:

111. g:(Alphn1). InvFuns(n1; Alph; f; g)
a:(n1n). f o g(a) = (z:||b||. b[z]) nAlph

About:
existsnatural_numberequalfunctionapply
universesetlistint