PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: back listify 1 2 1 1 1 2 1 1 1

1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. n:
5. f: nAlph
6. Bij(n; Alph; f)
7. n1:
8. f1: n1S.car
9. b:S.car. a:n1. f1(a) = b
10. BL: S.car*
11. t: S.car
12. a: Alph
13. S.act(a,t) = s
14. a1: n1
15. f1(a1) = t

mem_f(S.car;s;(y.S.act(f(y),t))[n])

By:
Thin -1
THEN
Thin -1
THEN
Analyze 6
THEN
Thin 6
THEN
Unfold `surject` 6
THEN
InstHyp [a] 6
THEN
Analyze -1


Generated subgoal:

16. b:Alph. a:n. f(a) = b
7. n1:
8. f1: n1S.car
9. b:S.car. a:n1. f1(a) = b
10. BL: S.car*
11. t: S.car
12. a: Alph
13. S.act(a,t) = s
14. a@0: n
15. f(a@0) = a
mem_f(S.car;s;(y.S.act(f(y),t))[n])


About:
lambdaapplynatural_numberuniversefunction
allexistsequallist