PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach aux 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. Fin(S.car)

RL:S.car*. s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)
By:
Analyze -1
THEN
RWH (LemmaC Thm* (f:(AB). Bij(A; B; f)) (A ~ B)) -1
THEN
Analyze -1
THEN
Analyze -1
Generated subgoal:

19. 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)

About:
existslistallequaluniversefunctionnatural_number