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 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 over I,O st 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 over I,O; :: thesis: ( 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: 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 zero 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 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 ) ) ; :: according to FSM_2:def 8 :: thesis: ( not t2 is_result_of s,M or t1 = t2 )
given o being non zero 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 zero 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 and
A5: q in the FinalS of M by A1;
consider w being FinSequence of I such that
A6: the InitS of M,<*s*> ^ w -leads_to q by A4;
set w1 = <*s*> ^ w;
A7: (GEN ((<*s*> ^ w), the InitS of M)) . ((len (<*s*> ^ w)) + 1) = q by A6;
A8: (<*s*> ^ w) . 1 = s by FINSEQ_1:41;
then A9: (len (<*s*> ^ w)) + 1 >= m by A2, A5, A7;
A10: o <= (len (<*s*> ^ w)) + 1 by A3, A5, A7, A8;
A11: ( o < m or o = m or o > m ) by XXREAL_0:1;
A12: (<*s*> ^ w) . 1 = s by FINSEQ_1:41;
then A13: t1 = the OFun of M . ((GEN ((<*s*> ^ w), the InitS of M)) . m) by A2, A9;
A14: (GEN ((<*s*> ^ w), the InitS of M)) . m in the FinalS of M by A2, A9, A12;
(GEN ((<*s*> ^ w), the InitS of M)) . o in the FinalS of M by A3, A10, A12;
hence t1 = t2 by A2, A3, A9, A10, A11, A12, A13, A14; :: thesis: verum