PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach lemma 1 1 2 2 2 1 1 2 1 1
1. Alph: Type
2. S: ActionSet(Alph)
3. si: S.car
4. nn:
5. f: nnAlph
6. g: Alphnn
7. Fin(S.car)
8. InvFuns(nn; Alph; f; g)
9. k:
10. 0 < k
11. knn
12. RLa: S.car*
13. i:{1..1}, a:Alph. si = S.act(a,[si][i]) False mem_f(S.car;S.act(a,[si][i]);RLa)
14. a:Alph. g(a) < k-1 si = S.act(a,si) False mem_f(S.car;S.act(a,si);RLa)
15. s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)
16. a: Alph
17. g(a) < k
18. g(a) < k-1
19. g(a) = k-1 nn

f(k-1) = a
By:
Analyze 8
THEN
RWH (RevHypC -1) 0
THEN
RWH add_composeC 0
Generated subgoal:

18. g o f = Id
9. f o g = Id
10. k:
11. 0 < k
12. knn
13. RLa: S.car*
14. i:{1..1}, a:Alph. si = S.act(a,[si][i]) False mem_f(S.car;S.act(a,[si][i]);RLa)
15. a:Alph. g(a) < k-1 si = S.act(a,si) False mem_f(S.car;S.act(a,si);RLa)
16. s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)
17. a: Alph
18. g(a) < k
19. g(a) < k-1
20. g(a) = k-1 nn
(f o g)(a) = a

About:
equalapplysubtractnatural_numberuniversefunctionintless_than
listallorconsnilfalseimpliesexists