let IAlph, OAlph be non empty set ; for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qb being State of tfsm
for k being Nat st 1 <= k holds
( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) ) )
let tfsm be non empty Mealy-FSM over IAlph,OAlph; for qa, qb being State of tfsm
for k being Nat st 1 <= k holds
( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) ) )
let qa, qb be State of tfsm; for k being Nat st 1 <= k holds
( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) ) )
let k be Nat; ( 1 <= k implies ( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) ) ) )
set OF = the OFun of tfsm;
assume A1:
1 <= k
; ( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) ) )
hereby ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) implies k -equivalent qa,qb )
assume A2:
k -equivalent qa,
qb
;
( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] ) )thus A3:
1
-equivalent qa,
qb
by A1, XXREAL_0:2, A2;
for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s]let s be
Element of
IAlph;
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s]let k1 be
Nat;
( k1 = k - 1 implies k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s] )assume A4:
k1 = k - 1
;
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s]set qb9 = the
Tran of
tfsm . [qb,s];
set qa9 = the
Tran of
tfsm . [qa,s];
thus
k1 -equivalent the
Tran of
tfsm . [qa,s], the
Tran of
tfsm . [qb,s]
verumproof
let w be
FinSequence of
IAlph;
FSM_1:def 11 ( len w <= k1 implies (( the Tran of tfsm . [qa,s]),w) -response = (( the Tran of tfsm . [qb,s]),w) -response )
set sw =
<*s*> ^ w;
A5:
len <*s*> = 1
by FINSEQ_1:40;
assume
len w <= k1
;
(( the Tran of tfsm . [qa,s]),w) -response = (( the Tran of tfsm . [qb,s]),w) -response
then A6:
(len w) + 1
<= k1 + 1
by XREAL_1:7;
len (<*s*> ^ w) =
(len <*s*>) + (len w)
by FINSEQ_1:22
.=
1
+ (len w)
by FINSEQ_1:40
;
then A7:
(
qa,
(<*s*> ^ w))
-response = (
qb,
(<*s*> ^ w))
-response
by A2, A4, A6;
A8:
( (
qa,
(<*s*> ^ w))
-response = <*( the OFun of tfsm . [qa,s])*> ^ ((( the Tran of tfsm . [qa,s]),w) -response) & (
qb,
(<*s*> ^ w))
-response = <*( the OFun of tfsm . [qb,s])*> ^ ((( the Tran of tfsm . [qb,s]),w) -response) )
by Th18;
0 + 1
in Seg (0 + 1)
by FINSEQ_1:4;
then A9:
1
in dom <*s*>
by A5, FINSEQ_1:def 3;
the
OFun of
tfsm . [qa,s] =
the
OFun of
tfsm . [(((qa,<*s*>) -admissible) . 1),s]
by Def2
.=
the
OFun of
tfsm . [(((qa,<*s*>) -admissible) . 1),(<*s*> . 1)]
.=
((qa,<*s*>) -response) . 1
by A9, Def6
.=
((qb,<*s*>) -response) . 1
by A3, A5
.=
the
OFun of
tfsm . [(((qb,<*s*>) -admissible) . 1),(<*s*> . 1)]
by A9, Def6
.=
the
OFun of
tfsm . [(((qb,<*s*>) -admissible) . 1),s]
.=
the
OFun of
tfsm . [qb,s]
by Def2
;
hence
(
( the Tran of tfsm . [qa,s]),
w)
-response = (
( the Tran of tfsm . [qb,s]),
w)
-response
by A8, A7, FINSEQ_1:33;
verum
end;
end;
assume that
A10:
1 -equivalent qa,qb
and
A11:
for s being Element of IAlph
for k1 being Nat st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s], the Tran of tfsm . [qb,s]
; k -equivalent qa,qb
thus
k -equivalent qa,qb
verumproof
let w be
FinSequence of
IAlph;
FSM_1:def 11 ( len w <= k implies (qa,w) -response = (qb,w) -response )
assume A12:
len w <= k
;
(qa,w) -response = (qb,w) -response
per cases
( w = <*> IAlph or not w is empty )
;
suppose
not
w is
empty
;
(qa,w) -response = (qb,w) -response then consider s being
Element of
IAlph,
w9 being
FinSequence of
IAlph such that
s = w . 1
and A14:
w = <*s*> ^ w9
by FINSEQ_3:102;
reconsider k1 =
k - 1 as
Element of
NAT by A1, INT_1:5;
A15:
len <*s*> = 1
by FINSEQ_1:40;
len w =
(len <*s*>) + (len w9)
by A14, FINSEQ_1:22
.=
(len w9) + 1
by FINSEQ_1:40
;
then A16:
((len w9) + 1) - 1
<= k1
by A12, XREAL_1:9;
0 + 1
in Seg (0 + 1)
by FINSEQ_1:4;
then A17:
1
in dom <*s*>
by A15, FINSEQ_1:def 3;
set qa9 = the
Tran of
tfsm . [qa,s];
set qb9 = the
Tran of
tfsm . [qb,s];
A18:
( (
qa,
w)
-response = <*( the OFun of tfsm . [qa,s])*> ^ ((( the Tran of tfsm . [qa,s]),w9) -response) & (
qb,
w)
-response = <*( the OFun of tfsm . [qb,s])*> ^ ((( the Tran of tfsm . [qb,s]),w9) -response) )
by A14, Th18;
A19:
k1 -equivalent the
Tran of
tfsm . [qa,s], the
Tran of
tfsm . [qb,s]
by A11;
the
OFun of
tfsm . [qa,s] =
the
OFun of
tfsm . [(((qa,<*s*>) -admissible) . 1),s]
by Def2
.=
the
OFun of
tfsm . [(((qa,<*s*>) -admissible) . 1),(<*s*> . 1)]
.=
((qa,<*s*>) -response) . 1
by A17, Def6
.=
((qb,<*s*>) -response) . 1
by A10, A15
.=
the
OFun of
tfsm . [(((qb,<*s*>) -admissible) . 1),(<*s*> . 1)]
by A17, Def6
.=
the
OFun of
tfsm . [(((qb,<*s*>) -admissible) . 1),s]
.=
the
OFun of
tfsm . [qb,s]
by Def2
;
hence
(
qa,
w)
-response = (
qb,
w)
-response
by A18, A19, A16;
verum end;
end;