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 holds
for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2
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 holds
for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2
let M be non empty Moore-SM_Final of I,O; :: thesis: ( M is calculating_type & s leads_to_final_state_of M implies for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2 )
assume A1: ( M is calculating_type & s leads_to_final_state_of M ) ; :: thesis: for t1, t2 being Element of O st t1 is_result_of s,M & t2 is_result_of s,M holds
t1 = t2
let t1, t2 be Element of O; :: thesis: ( t1 is_result_of s,M & t2 is_result_of s,M implies t1 = t2 )
given m being non empty Element of NAT such that A2: for w1 being FinSequence of I st w1 . 1 = s holds
( ( m <= (len w1) + 1 implies ( t1 = 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 ) ) ; :: according to FSM_2:def 8 :: thesis: ( not t2 is_result_of s,M or t1 = t2 )
given o being non empty Element of NAT such that A3: for w2 being FinSequence of I st w2 . 1 = s holds
( ( o <= (len w2) + 1 implies ( t2 = the OFun of M . ((GEN w2,the InitS of M) . o) & (GEN w2,the InitS of M) . o in the FinalS of M ) ) & ( for p being non empty Element of NAT st p < o & p <= (len w2) + 1 holds
not (GEN w2,the InitS of M) . p in the FinalS of M ) ) ; :: according to FSM_2:def 8 :: thesis: t1 = t2
consider q being State of M such that
A4: ( q is_accessible_via s & q in the FinalS of M ) by A1, Def5;
consider w being FinSequence of I such that
A5: the InitS of M,<*s*> ^ w -leads_to q by A4, Def2;
set w1 = <*s*> ^ w;
A6: (GEN (<*s*> ^ w),the InitS of M) . ((len (<*s*> ^ w)) + 1) = q by A5, FSM_1:def 3;
( not (len (<*s*> ^ w)) + 1 is empty & (<*s*> ^ w) . 1 = s ) by FINSEQ_1:58;
then A7: ( (len (<*s*> ^ w)) + 1 >= m & o <= (len (<*s*> ^ w)) + 1 ) by A2, A3, A4, A6;
A8: ( o < m or o = m or o > m ) by XXREAL_0:1;
(<*s*> ^ w) . 1 = s by FINSEQ_1:58;
then ( t1 = the OFun of M . ((GEN (<*s*> ^ w),the InitS of M) . m) & (GEN (<*s*> ^ w),the InitS of M) . m in the FinalS of M & t2 = the OFun of M . ((GEN (<*s*> ^ w),the InitS of M) . o) & (GEN (<*s*> ^ w),the InitS of M) . o in the FinalS of M & ( for n being non empty Element of NAT st n < m & n <= (len (<*s*> ^ w)) + 1 holds
not (GEN (<*s*> ^ w),the InitS of M) . n in the FinalS of M ) & ( for n being non empty Element of NAT st n < o & n <= (len (<*s*> ^ w)) + 1 holds
not (GEN (<*s*> ^ w),the InitS of M) . n in the FinalS of M ) ) by A2, A3, A7;
hence t1 = t2 by A7, A8; :: thesis: verum