Nuprl - Pf pump_theorem 1 1 1 1 1 1 1 1 1 1 1 1 1

PrintForm Definitions action sets Sections AutomataTheory Doc

At: pump theorem 1 1 1 1 1 1 1 1 1 1 1 1 1

1. Alph: Type
2. S: ActionSet(Alph)
3. N:
4. s: S.car
5. f: S.carN
6. g:(NS.car). InvFuns(S.car; N; f; g)
7. A: Alph*
8. N < ||A||
9. i: ||A||
10. j: ||A||
11. i < j
12. (i.f((S:A[||A||-i..||A||]s)))(i) = (i.f((S:A[||A||-i..||A||]s)))(j) N

0 < ||A[||A||-j..||A||-i]||

By: Inst Thm* as:T*, i:{0...||as||}, j:{i...||as||}. ||as[i..j]|| = j-i [Alph;A;||A||-j;||A||-i] THEN SupInf

Generated subgoals:

None

About: