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
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
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
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 )
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
(GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2
let s1, s2 be 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 q be State of S; ( q <> the InitS of S implies (GEN (<*s1*>,q)) . 2 = (GEN (<*s2*>,q)) . 2 )
assume A3:
q <> the InitS of S
; (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; verum