let I be non empty set ; for S being non empty FSM over I st ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) holds
S is calculating_type
let S be non empty FSM over I; ( ( for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S) ) implies S is calculating_type )
assume A1:
for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 & len w1 = len w2 holds
GEN (w1, the InitS of S) = GEN (w2, the InitS of S)
; S is calculating_type
now for w1, w2 being FinSequence of I st w1 . 1 = w2 . 1 holds
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable let w1,
w2 be
FinSequence of
I;
( w1 . 1 = w2 . 1 implies GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable )assume A2:
w1 . 1
= w2 . 1
;
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable thus
GEN (
w1, the
InitS of
S),
GEN (
w2, the
InitS of
S)
are_c=-comparable
verumproof
per cases
( w1 = <*> I or w2 = <*> I or ( w1 <> {} & w2 <> {} ) )
;
suppose A3:
(
w1 <> {} &
w2 <> {} )
;
GEN (w1, the InitS of S), GEN (w2, the InitS of S) are_c=-comparable reconsider v1 =
w2 | (Seg (len w1)),
v2 =
w1 | (Seg (len w2)) as
FinSequence of
I by FINSEQ_1:18;
(
len w1 <= len w2 or
len w2 <= len w1 )
;
then A4:
( (
v1 = w2 &
len v2 = len w2 &
len w1 >= len w2 ) or (
len v1 = len w1 &
v2 = w1 &
len w1 <= len w2 ) )
by FINSEQ_1:17, FINSEQ_2:20;
A5:
len w1 >= 0 + 1
by A3, NAT_1:13;
A6:
len w2 >= 0 + 1
by A3, NAT_1:13;
A7:
v1 . 1
= w2 . 1
by A4, A5, FINSEQ_6:128;
v2 . 1
= w1 . 1
by A4, A6, FINSEQ_6:128;
then A8:
(
GEN (
v1, the
InitS of
S)
= GEN (
w1, the
InitS of
S) or
GEN (
v2, the
InitS of
S)
= GEN (
w2, the
InitS of
S) )
by A1, A2, A4, A7;
consider s1 being
FinSequence such that A9:
w2 = v1 ^ s1
by FINSEQ_1:80;
consider s2 being
FinSequence such that A10:
w1 = v2 ^ s2
by FINSEQ_1:80;
reconsider s1 =
s1,
s2 =
s2 as
FinSequence of
I by A9, A10, FINSEQ_1:36;
v1 <> {}
then
1
<= len v1
by NAT_1:14;
then A13:
ex
WI being
Element of
I ex
QI,
QI1 being
State of
S st
(
WI = v1 . (len v1) &
QI = (GEN (v1, the InitS of S)) . (len v1) &
QI1 = (GEN (v1, the InitS of S)) . ((len v1) + 1) &
WI -succ_of QI = QI1 )
by FSM_1:def 2;
v2 <> {}
then
1
<= len v2
by NAT_1:14;
then
ex
WI2 being
Element of
I ex
QI2,
QI12 being
State of
S st
(
WI2 = v2 . (len v2) &
QI2 = (GEN (v2, the InitS of S)) . (len v2) &
QI12 = (GEN (v2, the InitS of S)) . ((len v2) + 1) &
WI2 -succ_of QI2 = QI12 )
by FSM_1:def 2;
then reconsider q1 =
(GEN (v1, the InitS of S)) . ((len v1) + 1),
q2 =
(GEN (v2, the InitS of S)) . ((len v2) + 1) as
State of
S by A13;
A16:
(GEN (s1,q1)) . 1
= q1
by FSM_1:def 2;
A17:
(GEN (s2,q2)) . 1
= q2
by FSM_1:def 2;
A18:
len (GEN (v1, the InitS of S)) = (len v1) + 1
by FSM_1:def 2;
A19:
len (GEN (v2, the InitS of S)) = (len v2) + 1
by FSM_1:def 2;
the
InitS of
S,
v1 -leads_to q1
;
then A20:
GEN (
w2, the
InitS of
S) =
(Del ((GEN (v1, the InitS of S)),((len v1) + 1))) ^ (GEN (s1,q1))
by A9, FSM_1:8
.=
(GEN (v1, the InitS of S)) ^ (Del ((GEN (s1,q1)),1))
by A16, A18, Lm2
;
the
InitS of
S,
v2 -leads_to q2
;
then GEN (
w1, the
InitS of
S) =
(Del ((GEN (v2, the InitS of S)),((len v2) + 1))) ^ (GEN (s2,q2))
by A10, FSM_1:8
.=
(GEN (v2, the InitS of S)) ^ (Del ((GEN (s2,q2)),1))
by A17, A19, Lm2
;
then
(
GEN (
w1, the
InitS of
S)
c= GEN (
w2, the
InitS of
S) or
GEN (
w2, the
InitS of
S)
c= GEN (
w1, the
InitS of
S) )
by A8, A20, TREES_1:1;
hence
GEN (
w1, the
InitS of
S),
GEN (
w2, the
InitS of
S)
are_c=-comparable
;
verum end;
end; end;
hence
S is calculating_type
by Th5; verum