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:
n
Alph
6.
Bij(
n; Alph; f)
7.
n1:
8.
f1:
n1
S.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:
1
6.
b:Alph.
a:
n. f(a) = b
7.
n1:
8.
f1:
n1
S.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: