Nuprl - Pf auto2_lemma

PrintForm Definitions exponent Sections AutomataTheory Doc

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)

f:((n1n){l:(Alph*)| ||l|| = n }). Bij((n1n); {l:(Alph*)| ||l|| = n }; f)

By: Witness z.(f o g(z))[n]

Generated subgoals:

1 10. z: (n1n)
((f o g(z))[n]) {l:(Alph*)| ||l|| = n }

2 Bij((n1n); {l:(Alph*)| ||l|| = n }; z.(f o g(z))[n])

About:

1	10. `z:` `(n1n)` `((f o g(z))[n]) {l:(Alph*)\| \|\|l\|\| = n }`
2	`Bij((n1n); {l:(Alph*)\| \|\|l\|\| = n }; z.(f o g(z))[n])`