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_{1}[ 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_{1}[m]
by A3, A5;

consider m being Nat such that

A7: S_{1}[m]
and

A8: for k being Nat st S_{1}[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 ) )

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

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

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

consider m being Nat such that

A7: S

A8: for k being Nat st S

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: for j being non zero Element of NAT st j <= (len w1) + 1 & w1 . 1 = s & j < m holds 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;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

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