let I be non empty set ; :: thesis: for S being non empty FSM over I st S is regular & S is calculating_type holds
for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2]
let S be non empty FSM over I; :: thesis: ( S is regular & S is calculating_type implies for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2] )
assume that
A1: S is regular and
A2: S is calculating_type ; :: thesis: for s1, s2 being Element of I
for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2]
let s1, s2 be Element of I; :: thesis: for q being State of S st q <> the InitS of S holds
the Tran of S . [q,s1] = the Tran of S . [q,s2]
let q be State of S; :: thesis: ( q <> the InitS of S implies the Tran of S . [q,s1] = the Tran of S . [q,s2] )
assume A3: q <> the InitS of S ; :: thesis: the Tran of S . [q,s1] = the Tran of S . [q,s2]
set w1 = <*s1*>;
set w2 = <*s2*>;
A4: len <*s1*> = 0 + 1 by FINSEQ_1:39;
reconsider j = len <*s1*> as non zero Element of NAT ;
consider WI being Element of I, QI, QI1 being State of S such that
A5: WI = <*s1*> . j and
A6: QI = (GEN (<*s1*>,q)) . j and
A7: QI1 = (GEN (<*s1*>,q)) . (j + 1) and
A8: WI -succ_of QI = QI1 by A4, FSM_1:def 2;
WI = s1 by A4, A5;
then A9: QI1 = s1 -succ_of q by A4, A6, A8, FSM_1:def 2;
A10: len <*s2*> = 0 + 1 by FINSEQ_1:39;
reconsider h = len <*s2*> as non zero Element of NAT ;
consider WI2 being Element of I, QI2, QI12 being State of S such that
A11: WI2 = <*s2*> . h and
A12: QI2 = (GEN (<*s2*>,q)) . h and
A13: QI12 = (GEN (<*s2*>,q)) . (h + 1) and
A14: WI2 -succ_of QI2 = QI12 by A10, FSM_1:def 2;
A15: QI2 = q by A10, A12, FSM_1:def 2;
WI2 = s2 by A10, A11;
hence the Tran of S . [q,s1] = the Tran of S . [q,s2] by A1, A2, A3, A4, A7, A9, A10, A13, A14, A15, Th14; :: thesis: verum