Nuprl - Pf auto2_lemma_5 1 1 1 1 1 1 2 2 1 1 2 1

PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 5 1 1 1 1 1 1 2 2 1 1 2 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 }
11. a: (n1n)
12. f o g(a) = (z:||b||. b[z]) nAlph

a:(n1n). ((f o g(a))[n]) = b {l:(Alph*)| ||l|| = n }

By: ApFunToHypEquands `x' ((x)[||b||]) (Alph*) 12

Generated subgoals:

1 13. x: nAlph
x ||b||Alph

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

About:

1	13. `x:` `nAlph` `x \|\|b\|\|Alph`
2	13. `((f o g(a))[\|\|b\|\|]) = ((z:\|\|b\|\|. b[z])[\|\|b\|\|])` `a:(n1n). ((f o g(a))[n]) = b {l:(Alph*)\| \|\|l\|\| = n }`