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

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