PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach aux 1 1 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. Fin(S.car)
5. n:
6. f: nAlph
7. g: Alphn
8. InvFuns(n; Alph; f; g)
9. n1:
10. f1: n1S.car
11. g1: S.carn1
12. InvFuns(n1; S.car; f1; g1)

RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)
By:
Inst Thm* S:ActionSet(Alph), si:S.car, nn:, f:(nnAlph), g:(Alphnn). Fin(S.car) InvFuns(nn; Alph; f; g) (n:. RL:{y:{x:(S.car*)| 0 < ||x|| & ||x||n+1 }| y[(||y||-1)] = si }. (s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)) ||RL|| = n+1 & (i:||RL||, j:i. RL[i] = RL[j]) & (s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s)) & (k:. knn (RLa:S.car*. (i:{1..||RL||}, a:Alph. mem_f(S.car;S.act(a,RL[i]);RL) mem_f(S.car;S.act(a,RL[i]);RLa)) & (a:Alph. g(a) < k mem_f(S.car;S.act(a,hd(RL));RL) mem_f(S.car;S.act(a,hd(RL));RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s))))) [Alph;S;si;n;f;g;n1]
THEN
GenExRepD
Generated subgoals:

113. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||n1+1 }| y[(||y||-1)] = si }
14. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)
RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)
213. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||n1+1 }| y[(||y||-1)] = si }
14. ||RL|| = n1+1
15. i:||RL||, j:i. RL[i] = RL[j]
16. s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s)
17. k:. kn (RLa:S.car*. (i:{1..||RL||}, a:Alph. mem_f(S.car;S.act(a,RL[i]);RL) mem_f(S.car;S.act(a,RL[i]);RLa)) & (a:Alph. g(a) < k mem_f(S.car;S.act(a,hd(RL));RL) mem_f(S.car;S.act(a,hd(RL));RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)))
RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)

About:
existslistallequaluniversefunctionnatural_number