let I, O be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: according to FSM_2:def 5 :: thesis: 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 S₁[ 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 S₁[m] by A3, A5;
consider m being Nat such that
A7: S₁[m] and
A8: for k being Nat st S₁[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 ; :: 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 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 :: thesis: 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; :: thesis: ( (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 ; :: thesis: (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; :: thesis: verum

end;

let w1 be FinSequence of I; :: thesis: 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 ; :: 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 that
A15: i <= (len w1) + 1 and
A16: w1 . 1 = s and
A17: i < m ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum