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

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