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
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
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
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 )
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
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
let s1, s2 be Element of I; :: thesis: for q being State of S st q <> the InitS of S holds
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
let q be State of S; :: thesis: ( q <> the InitS of S implies (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 )
assume A3: q <> the InitS of S ; :: thesis: (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
q is accessible by A1;
then consider w being FinSequence of I such that
A4: the InitS of S,w -leads_to q ;
w <> {} by FSM_1:def 2, A3, A4;
then consider x being Element of I, w9 being FinSequence of I such that
w . 1 = x and
A5: w = <*x*> ^ w9 by FINSEQ_3:102;
set w1 = w ^ <*s1*>;
set w2 = w ^ <*s2*>;
len <*x*> = 1 by FINSEQ_1:39;
then (len <*x*>) + (len w9) >= 1 by NAT_1:11;
then len w >= 1 by A5, FINSEQ_1:22;
then A6: 1 in dom w by FINSEQ_3:25;
then w . 1 = (w ^ <*s1*>) . 1 by FINSEQ_1:def 7;
then A7: (w ^ <*s1*>) . 1 = (w ^ <*s2*>) . 1 by A6, FINSEQ_1:def 7;
A8: len <*s1*> = 1 by FINSEQ_1:39;
then A9: len (w ^ <*s1*>) = (len w) + 1 by FINSEQ_1:22;
A10: len <*s2*> = 1 by FINSEQ_1:39;
then A11: len (w ^ <*s2*>) = (len w) + 1 by FINSEQ_1:22;
A12: len (w ^ <*s1*>) = len (w ^ <*s2*>) by A9, A10, FINSEQ_1:22;
set p = Del ((GEN (w, the InitS of S)),((len w) + 1));
set p1 = GEN (<*s1*>,q);
A13: GEN ((w ^ <*s1*>), the InitS of S) = (Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q)) by A4, FSM_1:8;
A14: len (GEN (w, the InitS of S)) = (len w) + 1 by FSM_1:def 2;
then A15: len (Del ((GEN (w, the InitS of S)),((len w) + 1))) = len w by PRE_POLY:12;
A16: len (GEN (<*s1*>,q)) = (len <*s1*>) + 1 by FSM_1:def 2
.= 1 + 1 by FINSEQ_1:39 ;
A17: len (GEN ((w ^ <*s1*>), the InitS of S)) = len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q))) by A4, FSM_1:8
.= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s1*>,q))) by FINSEQ_1:22
.= (len w) + (1 + 1) by A14, A16, PRE_POLY:12
.= ((len w) + 1) + 1
.= (len (w ^ <*s1*>)) + 1 by A8, FINSEQ_1:22 ;
A18: (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + 1 <= (len (w ^ <*s1*>)) + 1 by A9, A15, NAT_1:11;
len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s1*>,q))) = (len (w ^ <*s1*>)) + 1 by A4, A17, FSM_1:8;
then (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s1*>,q))) = (len (w ^ <*s1*>)) + 1 by FINSEQ_1:22;
then A19: (GEN ((w ^ <*s1*>), the InitS of S)) . ((len (w ^ <*s1*>)) + 1) = (GEN (<*s1*>,q)) . (((len (w ^ <*s1*>)) + 1) - (len (Del ((GEN (w, the InitS of S)),((len w) + 1))))) by A13, A18, FINSEQ_1:23
.= (GEN (<*s1*>,q)) . (((len (w ^ <*s1*>)) + 1) - (len w)) by A14, PRE_POLY:12
.= (GEN (<*s1*>,q)) . ((((len w) + 1) + 1) - (len w)) by A8, FINSEQ_1:22
.= (GEN (<*s1*>,q)) . 2 ;
set p2 = GEN (<*s2*>,q);
A20: GEN ((w ^ <*s2*>), the InitS of S) = (Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q)) by A4, FSM_1:8;
A21: len (GEN (<*s2*>,q)) = (len <*s2*>) + 1 by FSM_1:def 2
.= 1 + 1 by FINSEQ_1:39 ;
A22: len (GEN ((w ^ <*s2*>), the InitS of S)) = len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q))) by A4, FSM_1:8
.= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s2*>,q))) by FINSEQ_1:22
.= (len w) + (1 + 1) by A14, A21, PRE_POLY:12
.= ((len w) + 1) + 1
.= (len (w ^ <*s2*>)) + 1 by A10, FINSEQ_1:22 ;
(len w) + 1 <= (len (w ^ <*s2*>)) + 1 by A11, NAT_1:11;
then A23: (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + 1 <= (len (w ^ <*s2*>)) + 1 by A14, PRE_POLY:12;
len ((Del ((GEN (w, the InitS of S)),((len w) + 1))) ^ (GEN (<*s2*>,q))) = (len (w ^ <*s2*>)) + 1 by A4, A22, FSM_1:8;
then (len (w ^ <*s2*>)) + 1 <= (len (Del ((GEN (w, the InitS of S)),((len w) + 1)))) + (len (GEN (<*s2*>,q))) by FINSEQ_1:22;
then (GEN ((w ^ <*s2*>), the InitS of S)) . ((len (w ^ <*s2*>)) + 1) = (GEN (<*s2*>,q)) . (((len (w ^ <*s2*>)) + 1) - (len (Del ((GEN (w, the InitS of S)),((len w) + 1))))) by A20, A23, FINSEQ_1:23
.= (GEN (<*s2*>,q)) . (((len (w ^ <*s2*>)) + 1) - (len w)) by A14, PRE_POLY:12
.= (GEN (<*s2*>,q)) . ((((len w) + 1) + 1) - (len w)) by A10, FINSEQ_1:22
.= (GEN (<*s2*>,q)) . 2 ;
hence (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 by A2, A7, A12, A19; :: thesis: verum