PrintForm Definitions exponent Sections AutomataTheory Doc

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

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. z: (n1n)

||(f o g(z))[n]|| = n

By: Inst Thm* m,n:, f:({m..n}T). n < m ||listify(f; m; n)|| = n-m [Alph;0;n;f o g(z)]

Generated subgoal:

111. n < 0 ||(f o g(z))[n]|| = n-0
||(f o g(z))[n]|| = n


About:
equalintapplynatural_numberuniversefunctionexists