PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach lemma 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)

RL:{y:{x:(S.car*)| 0 < ||x|| & ||x||0+1 }| y[(||y||-1)] = si }. (s:S.car. (w:Alph*. (S:wsi) = s) mem_f(S.car;s;RL)) ||RL|| = 0+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))))
By:
InstConcl [[si]]
THEN
Sel 2 (Analyze 0)
Generated subgoals:

1 [si] {y:{x:(S.car*)| 0 < ||x|| & ||x||0+1 }| y[(||y||-1)] = si }
2 ||[si]|| = 0+1 & (i:||[si]||, j:i. [si][i] = [si][j]) & (s:S.car. mem_f(S.car;s;[si]) (w:Alph*. (S:wsi) = s)) & (k:. knn (RLa:S.car*. (i:{1..||[si]||}, a:Alph. mem_f(S.car;S.act(a,[si][i]);[si]) mem_f(S.car;S.act(a,[si][i]);RLa)) & (a:Alph. g(a) < k mem_f(S.car;S.act(a,hd([si]));[si]) mem_f(S.car;S.act(a,hd([si]));RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s))))
39. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||0+1 }| y[(||y||-1)] = si }
10. k:
11. knn
12. RLa: S.car*
13. a: Alph
14. g(a) < k
||RL||1
49. RL: {y:{x:(S.car*)| 0 < ||x|| & ||x||0+1 }| y[(||y||-1)] = si }
10. k:
11. knn
12. RLa: S.car*
13. a: Alph
14. g(a) < k
||RL||1

About:
existssetlistandless_thannatural_numberadd
equalsubtractorallintimpliesapply
consniluniversefunctionmember