Nuprl - Pf reach_lemma 1 1 2

PrintForm Definitions det automata Sections AutomataTheory Doc

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)

||[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))))

By: Reduce 0

Generated subgoals:

1 9. s: S.car
10. si = s False
w:Alph*. (S:wsi) = s

2 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))

About:

1	9. `s:` `S.car` 10. `si = s False` `w:Alph*. (S:wsi) = s`
2	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))`