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 t being Element of O st t is_result_of s,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 t being Element of O st t is_result_of s,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 t being Element of O st t is_result_of s,M )

assume that

A1: M is calculating_type and

A2: s leads_to_final_state_of M ; :: thesis: ex t being Element of O st t is_result_of s,M

consider q being State of M such that

A3: q is_accessible_via s and

A4: q in the FinalS of M by A2;

consider w being FinSequence of I such that

A5: the InitS of M,<*s*> ^ w -leads_to q by A3;

A6: (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) = q by A5;

consider m being non zero Element of NAT such that

A7: 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 and

A8: 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 by A1, A2, Th18;

A9: (<*s*> ^ w) . 1 = s by FINSEQ_1:41;

then A10: (len (<*s*> ^ w)) + 1 >= m by A4, A6, A8;

then (GEN ((<*s*> ^ w), the InitS of M)) . m in the FinalS of M by A7, A9;

then reconsider t = the OFun of M . ((GEN ((<*s*> ^ w), the InitS of M)) . m) as Element of O by FUNCT_2:5;

take t ; :: thesis: t is_result_of s,M

take m ; :: according to FSM_2:def 8 :: thesis: for w being FinSequence of I st w . 1 = s holds

( ( m <= (len w) + 1 implies ( t = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds

not (GEN (w, the InitS of M)) . n in the FinalS of M ) )

let w1 be FinSequence of I; :: thesis: ( w1 . 1 = s implies ( ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M ) ) )

assume A11: w1 . 1 = s ; :: thesis: ( ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M ) )

(<*s*> ^ w) . 1 = s by FINSEQ_1:41;

hence ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) by A1, A7, A10, A11; :: thesis: for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M

thus for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M by A8, A11; :: 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 t being Element of O st t is_result_of s,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 t being Element of O st t is_result_of s,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 t being Element of O st t is_result_of s,M )

assume that

A1: M is calculating_type and

A2: s leads_to_final_state_of M ; :: thesis: ex t being Element of O st t is_result_of s,M

consider q being State of M such that

A3: q is_accessible_via s and

A4: q in the FinalS of M by A2;

consider w being FinSequence of I such that

A5: the InitS of M,<*s*> ^ w -leads_to q by A3;

A6: (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) = q by A5;

consider m being non zero Element of NAT such that

A7: 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 and

A8: 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 by A1, A2, Th18;

A9: (<*s*> ^ w) . 1 = s by FINSEQ_1:41;

then A10: (len (<*s*> ^ w)) + 1 >= m by A4, A6, A8;

then (GEN ((<*s*> ^ w), the InitS of M)) . m in the FinalS of M by A7, A9;

then reconsider t = the OFun of M . ((GEN ((<*s*> ^ w), the InitS of M)) . m) as Element of O by FUNCT_2:5;

take t ; :: thesis: t is_result_of s,M

take m ; :: according to FSM_2:def 8 :: thesis: for w being FinSequence of I st w . 1 = s holds

( ( m <= (len w) + 1 implies ( t = the OFun of M . ((GEN (w, the InitS of M)) . m) & (GEN (w, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w) + 1 holds

not (GEN (w, the InitS of M)) . n in the FinalS of M ) )

let w1 be FinSequence of I; :: thesis: ( w1 . 1 = s implies ( ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M ) ) )

assume A11: w1 . 1 = s ; :: thesis: ( ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) & ( for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M ) )

(<*s*> ^ w) . 1 = s by FINSEQ_1:41;

hence ( m <= (len w1) + 1 implies ( t = the OFun of M . ((GEN (w1, the InitS of M)) . m) & (GEN (w1, the InitS of M)) . m in the FinalS of M ) ) by A1, A7, A10, A11; :: thesis: for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M

thus for n being non zero Element of NAT st n < m & n <= (len w1) + 1 holds

not (GEN (w1, the InitS of M)) . n in the FinalS of M by A8, A11; :: thesis: verum