At: pump theorem 1 1 1 1 1 1 1 1 1 1 1 1 2
1. Alph: Type
2. S: ActionSet(Alph)
3. N: 
4. s: S.car
5. f: S.car
N
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
A = (((A[0..||A||-j]) @ (A[||A||-j..||A||-i])) @ (A[||A||-i..||A||]))
By: RW
(SweepUpC
(LemmaC
Thm* 
as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j]) @ (as[j..k])) = (as[i..k])))
0
Generated subgoal:| 1 | A = (A[0..||A||]) |
About:
