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

PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 5 1 1 1 1 1 1 2 1 1 1 1 2 1 1 1 2 1 2 1

1. Alph: Type
2. n:
3. n1:
4. f: n1Alph
5. a1,a2:n1. f(a1) = f(a2) a1 = a2
6. f:((nn1)(n1n)). Bij(nn1; (n1n); f)
7. f1: (nn1)(n1n)
8. g: (n1n)nn1
9. g o f1 = Id
10. f1 o g = Id
11. a1: (n1n)
12. a2: (n1n)
13. ((f o g(a1))[n]) = ((f o g(a2))[n]) {l:(Alph*)| ||l|| = n }
14. (i.(f o g(a1))(i)) = (i.(f o g(a2))(i)) nAlph
15. i:n. f(g(a1,i)) = f(g(a2,i))
16. i:n. g(a1,i) = g(a2,i)

a1 = a2

By: Assert (g(a1) = g(a2))

Generated subgoals:

1 g(a1) = g(a2)

2 17. g(a1) = g(a2)
a1 = a2

About: