let I, O be non empty set ; for s being Element of I
for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex m being non zero Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
let s be Element of I; for M being non empty Moore-SM_Final over I,O st M is calculating_type & s leads_to_final_state_of M holds
ex m being non zero Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
let M be non empty Moore-SM_Final over I,O; ( M is calculating_type & s leads_to_final_state_of M implies ex m being non zero Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) )
assume A1:
M is calculating_type
; ( not s leads_to_final_state_of M or ex m being non zero Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) ) )
given q being State of M such that A2:
q is_accessible_via s
and
A3:
q in the FinalS of M
; FSM_2:def 5 ex m being non zero Element of NAT st
( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
consider w being FinSequence of I such that
A4:
the InitS of M,<*s*> ^ w -leads_to q
by A2;
defpred S1[ Nat] means ( (GEN ((<*s*> ^ w), the InitS of M)) . $1 in the FinalS of M & $1 >= 1 & $1 <= (len (<*s*> ^ w)) + 1 );
A5:
(len (<*s*> ^ w)) + 1 >= 1
by NAT_1:11;
q = (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1)
by A4;
then A6:
ex m being Nat st S1[m]
by A3, A5;
consider m being Nat such that
A7:
S1[m]
and
A8:
for k being Nat st S1[k] holds
m <= k
from NAT_1:sch 5(A6);
reconsider m = m as non zero Element of NAT by A7, ORDINAL1:def 12;
take
m
; ( ( for w being FinSequence of I st (len w) + 1 >= m & w . 1 = s holds
(GEN (w, the InitS of M)) . m in the FinalS of M ) & ( for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M ) )
hereby for w being FinSequence of I
for j being non zero Element of NAT st j <= (len w) + 1 & w . 1 = s & j < m holds
not (GEN (w, the InitS of M)) . j in the FinalS of M
let w1 be
FinSequence of
I;
( (len w1) + 1 >= m & w1 . 1 = s implies (GEN (w1, the InitS of M)) . m in the FinalS of M )assume that A9:
(len w1) + 1
>= m
and A10:
w1 . 1
= s
;
(GEN (w1, the InitS of M)) . m in the FinalS of M
(<*s*> ^ w) . 1
= s
by FINSEQ_1:41;
then
GEN (
w1, the
InitS of
M),
GEN (
(<*s*> ^ w), the
InitS of
M)
are_c=-comparable
by A1, A10, Th4;
then A11:
(
GEN (
w1, the
InitS of
M)
c= GEN (
(<*s*> ^ w), the
InitS of
M) or
GEN (
(<*s*> ^ w), the
InitS of
M)
c= GEN (
w1, the
InitS of
M) )
;
A12:
dom (GEN ((<*s*> ^ w), the InitS of M)) =
Seg (len (GEN ((<*s*> ^ w), the InitS of M)))
by FINSEQ_1:def 3
.=
Seg ((len (<*s*> ^ w)) + 1)
by FSM_1:def 2
;
A13:
dom (GEN (w1, the InitS of M)) =
Seg (len (GEN (w1, the InitS of M)))
by FINSEQ_1:def 3
.=
Seg ((len w1) + 1)
by FSM_1:def 2
;
A14:
m in dom (GEN ((<*s*> ^ w), the InitS of M))
by A7, A12, FINSEQ_1:1;
m in dom (GEN (w1, the InitS of M))
by A7, A9, A13, FINSEQ_1:1;
hence
(GEN (w1, the InitS of M)) . m in the
FinalS of
M
by A7, A11, A14, GRFUNC_1:2;
verum
end;
let w1 be FinSequence of I; for j being non zero Element of NAT st j <= (len w1) + 1 & w1 . 1 = s & j < m holds
not (GEN (w1, the InitS of M)) . j in the FinalS of M
let i be non zero Element of NAT ; ( i <= (len w1) + 1 & w1 . 1 = s & i < m implies not (GEN (w1, the InitS of M)) . i in the FinalS of M )
assume that
A15:
i <= (len w1) + 1
and
A16:
w1 . 1 = s
and
A17:
i < m
; not (GEN (w1, the InitS of M)) . i in the FinalS of M
(<*s*> ^ w) . 1 = s
by FINSEQ_1:41;
then
GEN (w1, the InitS of M), GEN ((<*s*> ^ w), the InitS of M) are_c=-comparable
by A1, A16, Th4;
then A18:
( GEN (w1, the InitS of M) c= GEN ((<*s*> ^ w), the InitS of M) or GEN ((<*s*> ^ w), the InitS of M) c= GEN (w1, the InitS of M) )
;
A19:
1 <= i
by NAT_1:14;
A20:
i <= (len (<*s*> ^ w)) + 1
by A7, A17, XXREAL_0:2;
A21: dom (GEN (w1, the InitS of M)) =
Seg (len (GEN (w1, the InitS of M)))
by FINSEQ_1:def 3
.=
Seg ((len w1) + 1)
by FSM_1:def 2
;
dom (GEN ((<*s*> ^ w), the InitS of M)) =
Seg (len (GEN ((<*s*> ^ w), the InitS of M)))
by FINSEQ_1:def 3
.=
Seg ((len (<*s*> ^ w)) + 1)
by FSM_1:def 2
;
then A22:
i in dom (GEN ((<*s*> ^ w), the InitS of M))
by A19, A20, FINSEQ_1:1;
A23:
i in dom (GEN (w1, the InitS of M))
by A15, A19, A21, FINSEQ_1:1;
assume
(GEN (w1, the InitS of M)) . i in the FinalS of M
; contradiction
then
(GEN ((<*s*> ^ w), the InitS of M)) . i in the FinalS of M
by A18, A22, A23, GRFUNC_1:2;
hence
contradiction
by A8, A17, A19, A20; verum