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

PrintForm Definitions action sets Sections AutomataTheory Doc

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

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

k:. (S:((A[0..||A||-j]) @ (A[||A||-j..||A||-i]k)) @ (A[||A||-i..||A||])s) = (S:As)

By: Unfold `inv_funs` 7

Generated subgoal:

1 7. g o f = Id & f o g = Id
8. A: Alph*
9. N < ||A||
10. i: ||A||
11. j: ||A||
12. i < j
13. (i.f((S:A[||A||-i..||A||]s)))(i) = (i.f((S:A[||A||-i..||A||]s)))(j) N
k:. (S:((A[0..||A||-j]) @ (A[||A||-j..||A||-i]k)) @ (A[||A||-i..||A||])s) = (S:As)

About: