Nuprl - Pf pump_theorem 1 1 1 1 1 1 1 1 1 1 1 2 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 2 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
7. g o f = Id
8. f o g = Id
9. A: Alph*
10. N < ||A||
11. i: ||A||
12. j: ||A||
13. i < j
14. f((S:A[||A||-i..||A||]s)) = f((S:A[||A||-j..||A||]s))
15. (S:A[||A||-i..||A||]s) = (S:A[||A||-j..||A||]s)
16. 0 = 0

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

By: Inst Thm* S:ActionSet(Alph), s:S.car, L1,L2,L:Alph*. (S:L1s) = (S:L2s) (S:L @ L1s) = (S:L @ L2s) [Alph;S;s;A[||A||-i..||A||];A[||A||-j..||A||];A[0..||A||-j]]

Generated subgoals:

1 (S:A[||A||-i..||A||]s) = (S:A[||A||-j..||A||]s)

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

About:

1	`(S:A[\|\|A\|\|-i..\|\|A\|\|]s) = (S:A[\|\|A\|\|-j..\|\|A\|\|]s)`
2	17. `(S:(A[0..\|\|A\|\|-j]) @ (A[\|\|A\|\|-i..\|\|A\|\|])s) = (S:(A[0..\|\|A\|\|-j]) @ (A[\|\|A\|\|-j..\|\|A\|\|])s)` `(S:(A[0..\|\|A\|\|-j]) @ (A[\|\|A\|\|-i..\|\|A\|\|])s) = (S:As)`