let O, I be non empty set ; :: thesis: for s being Element of I
for M being non empty Moore-SM_Final of I,O st M is calculating_type & s leads_to_final_state_of M & not the InitS of M in the FinalS of M holds
ex m being non empty 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 empty 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; :: thesis: for M being non empty Moore-SM_Final of I,O st M is calculating_type & s leads_to_final_state_of M & not the InitS of M in the FinalS of M holds
ex m being non empty 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 empty 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 of I,O; :: thesis: ( M is calculating_type & s leads_to_final_state_of M & not the InitS of M in the FinalS of M implies ex m being non empty 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 empty 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 ; :: thesis: ( not s leads_to_final_state_of M or the InitS of M in the FinalS of M or ex m being non empty 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 empty 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 & q in the FinalS of M ) ; :: according to FSM_2:def 5 :: thesis: ( the InitS of M in the FinalS of M or ex m being non empty 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 empty 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
A3: the InitS of M,<*s*> ^ w -leads_to q by A2, Def2;
assume not the InitS of M in the FinalS of M ; :: thesis: ex m being non empty 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 empty 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 ) )
defpred S₁[ Nat] means ( (GEN (<*s*> ^ w),the InitS of M) . $1 in the FinalS of M & $1 >= 1 & $1 <= (len (<*s*> ^ w)) + 1 );
( (len (<*s*> ^ w)) + 1 >= 1 & q = (GEN (<*s*> ^ w),the InitS of M) . ((len (<*s*> ^ w)) + 1) ) by A3, FSM_1:def 3, NAT_1:11;
then A4: ex m being Nat st S₁[m] by A2;
consider m being Nat such that
A5: S₁[m] and
A6: for k being Nat st S₁[k] holds
m <= k from NAT_1:sch 5(A4);
reconsider m = m as non empty Element of NAT by A5, ORDINAL1:def 13;
take m ; :: thesis: ( ( 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 empty 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 :: thesis: for w being FinSequence of I
for j being non empty 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; :: thesis: ( (len w1) + 1 >= m & w1 . 1 = s implies (GEN w1,the InitS of M) . m in the FinalS of M )
assume A7: ( (len w1) + 1 >= m & w1 . 1 = s ) ; :: thesis: (GEN w1,the InitS of M) . m in the FinalS of M
(<*s*> ^ w) . 1 = s by FINSEQ_1:58;
then GEN w1,the InitS of M, GEN (<*s*> ^ w),the InitS of M are_c=-comparable by A1, A7, Th4;
then A8: ( 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 ) by XBOOLE_0:def 9;
A9: 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 ;
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 ;
then ( m in dom (GEN (<*s*> ^ w),the InitS of M) & m in dom (GEN w1,the InitS of M) ) by A5, A7, A9, FINSEQ_1:3;
hence (GEN w1,the InitS of M) . m in the FinalS of M by A5, A8, GRFUNC_1:8; :: thesis: verum

end;

let w1 be FinSequence of I; :: thesis: for j being non empty 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 empty Element of NAT ; :: thesis: ( i <= (len w1) + 1 & w1 . 1 = s & i < m implies not (GEN w1,the InitS of M) . i in the FinalS of M )
assume A10: ( i <= (len w1) + 1 & w1 . 1 = s & i < m ) ; :: thesis: not (GEN w1,the InitS of M) . i in the FinalS of M
(<*s*> ^ w) . 1 = s by FINSEQ_1:58;
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 ) by XBOOLE_0:def 9;
A12: ( 1 <= i & i <= (len (<*s*> ^ w)) + 1 & i <= (len w1) + 1 ) by A5, A10, NAT_1:14, XXREAL_0: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 ;
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 A14: ( i in dom (GEN (<*s*> ^ w),the InitS of M) & i in dom (GEN w1,the InitS of M) ) by A12, A13, FINSEQ_1:3;
assume (GEN w1,the InitS of M) . i in the FinalS of M ; :: thesis: contradiction
then (GEN (<*s*> ^ w),the InitS of M) . i in the FinalS of M by A11, A14, GRFUNC_1:8;
hence contradiction by A6, A10, A12; :: thesis: verum