let I be non empty set ; 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; ( 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
; 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; 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; ( 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
; 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, FINSEQ_1:def 8;
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, FINSEQ_1:def 8;
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; verum