let I, O 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 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 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 t being Element of O st t is_result_of s,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 t being Element of O st t is_result_of s,M )
assume A1: ( M is calculating_type & s leads_to_final_state_of M & not the InitS of M in the FinalS of M ) ; :: thesis: ex t being Element of O st t is_result_of s,M
then consider q being State of M such that
A2: ( q is_accessible_via s & q in the FinalS of M ) by Def5;
consider w being FinSequence of I such that
A3: the InitS of M,<*s*> ^ w -leads_to q by A2, Def2;
A4: (GEN (<*s*> ^ w),the InitS of M) . ((len (<*s*> ^ w)) + 1) = q by A3, FSM_1:def 3;
consider m being non empty Element of NAT such that
A5: ( ( 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 ) ) by A1, Th18;
A6: ( not (len (<*s*> ^ w)) + 1 is empty & (<*s*> ^ w) . 1 = s & (len (<*s*> ^ w)) + 1 <= (len (<*s*> ^ w)) + 1 ) by FINSEQ_1:58;
then A7: (len (<*s*> ^ w)) + 1 >= m by A2, A4, A5;
then (GEN (<*s*> ^ w),the InitS of M) . m in the FinalS of M by A5, A6;
then reconsider t = the OFun of M . ((GEN (<*s*> ^ w),the InitS of M) . m) as Element of O by FUNCT_2:7;
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 empty 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 empty 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 A8: 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 empty 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:58;
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, A5, A7, A8, Def1; :: thesis: for n being non empty 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 empty 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 A5, A8; :: thesis: verum