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