PrintForm
Definitions
det
automata
Sections
AutomataTheory
Doc
At:
reach
lemma
1
2
2
1
1
1
2
1
2
1.
Alph:
Type
2.
S:
ActionSet(Alph)
3.
si:
S.car
4.
nn:
5.
f:
nn
Alph
6.
g:
Alph
nn
7.
Fin(S.car)
8.
InvFuns(
nn; Alph; f; g)
9.
n:
10.
0 < n
11.
RL:
{y:{x:(S.car*)| 0 < ||x|| & ||x||
n-1+1 }| y[(||y||-1)] = si }
12.
||RL|| = n-1+1
13.
i:
||RL||, j:
i.
RL[i] = RL[j]
14.
s:S.car. mem_f(S.car;s;RL)
(
w:Alph*. (S:w
si) = s)
15.
k:
. k
nn
(
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:w
si) = s)))
16.
RLa:
S.car*
17.
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)
18.
a:Alph. g(a) < nn
mem_f(S.car;S.act(a,hd(RL));RL)
mem_f(S.car;S.act(a,hd(RL));RLa)
19.
s:S.car. mem_f(S.car;s;RLa)
(
w:Alph*. (S:w
si) = s)
20.
La':
S.car*
21.
t:S.car. mem_f(S.car;t;RLa)
mem_f(S.car;t;RL)
mem_f(S.car;t;La')
22.
t:S.car. mem_f(S.car;t;La')
mem_f(S.car;t;RLa)
23.
||La'||
1
mem_f(S.car;hd(La');RL)
24.
||La'||
1
25.
i:
(||RL||+1)
26.
j:
i
27.
j = 0
(hd(La').RL)[i] = (hd(La').RL)[j]
By:
Assert (1
j)
THEN
Assert (1
i)
THEN
Unfold `select` 0
THEN
RecUnfold `nth_tl` 0
THEN
SplitOnConclITE
THEN
Auto
THEN
SplitOnConclITE
Generated subgoal:
1
28.
1
j
29.
1
i
30.
0 < i
31.
0 < j
hd(nth_tl(i-1;tl((hd(La').RL)))) = hd(nth_tl(j-1;tl((hd(La').RL))))
About: