PrintForm Definitions action sets Sections AutomataTheory Doc

At: pump theorem 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||

a,b,c:Alph*. 0 < ||b|| & A = ((a @ b) @ c) & (k:. (S:(a @ (bk)) @ cs) = (S:As))
By: Inst Thm* n:{1...}, m:{n+1...}, f:(mn). i,j:m. i < j & f(i) = f(j) [N;||A||;i.f((S:A[||A||-i..||A||]s))]
Generated subgoal:

19. i,j:||A||. i < j & (i.f((S:A[||A||-i..||A||]s)))(i) = (i.f((S:A[||A||-i..||A||]s)))(j) N
a,b,c:Alph*. 0 < ||b|| & A = ((a @ b) @ c) & (k:. (S:(a @ (bk)) @ cs) = (S:As))

About:
existslistandless_thannatural_numberequal
alllambdaapplysubtractuniversefunction