PrintForm Definitions det automata Sections AutomataTheory Doc

At: reach lemma 1 1 2 2
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. knn

RLa:S.car*. (i:{1..1}, a:Alph. si = S.act(a,[si][i]) False mem_f(S.car;S.act(a,[si][i]);RLa)) & (a:Alph. g(a) < k si = S.act(a,si) False mem_f(S.car;S.act(a,si);RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s))
By: NatInd 9
Generated subgoals:

1 0nn (RLa:S.car*. (i:{1..1}, a:Alph. si = S.act(a,[si][i]) False mem_f(S.car;S.act(a,[si][i]);RLa)) & (a:Alph. g(a) < 0 si = S.act(a,si) False mem_f(S.car;S.act(a,si);RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)))
29. k:
10. 0 < k
11. k-1nn (RLa:S.car*. (i:{1..1}, a:Alph. si = S.act(a,[si][i]) False mem_f(S.car;S.act(a,[si][i]);RLa)) & (a:Alph. g(a) < k-1 si = S.act(a,si) False mem_f(S.car;S.act(a,si);RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)))
knn (RLa:S.car*. (i:{1..1}, a:Alph. si = S.act(a,[si][i]) False mem_f(S.car;S.act(a,[si][i]);RLa)) & (a:Alph. g(a) < k si = S.act(a,si) False mem_f(S.car;S.act(a,si);RLa)) & (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)))

About:
existslistandallnatural_numberorequalapply
consnilfalseimpliesless_thanuniversefunction