PrintForm Definitions exponent Sections AutomataTheory Doc

At: auto2 lemma 5 1 1 1 1 1 1 2 2 1 1 1 1 1 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. g o f1 = Id
10. f1 o g = Id
11. b: Alph*
12. ||b|| = n
13. g1: Alphn1
14. InvFuns(n1; Alph; f; g1)

g(f1(g1 o (z:||b||. b[z]))) = g1 o (z:||b||. b[z]) nn1
By: RWH add_composeC 0
Generated subgoal:

1 (g o f1)(g1 o (z:||b||. b[z])) = g1 o (z:||b||. b[z]) nn1

About:
equalfunctionnatural_numberapplyuniverseexistslistint