let OAlph, IAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM of 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 Element of 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 of IAlph,OAlph; :: thesis: 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 Element of 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; :: thesis: 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 Element of NAT st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] ) ) )
let k be Nat; :: thesis: ( 1 <= k implies ( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Element of 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
; :: thesis: ( k -equivalent qa,qb iff ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Element of NAT st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] ) ) )
hereby :: thesis: ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Element of 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
;
:: thesis: ( 1 -equivalent qa,qb & ( for s being Element of IAlph
for k1 being Element of 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
:: thesis: for s being Element of IAlph
for k1 being Element of 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;
:: thesis: for k1 being Element of NAT st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s]let k1 be
Element of
NAT ;
:: thesis: ( k1 = k - 1 implies k1 -equivalent the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s] )assume A4:
k1 = k - 1
;
:: thesis: k1 -equivalent the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s]set qa' = the
Tran of
tfsm . [qa,s];
set qb' = the
Tran of
tfsm . [qb,s];
thus
k1 -equivalent the
Tran of
tfsm . [qa,s],the
Tran of
tfsm . [qb,s]
:: thesis: verumproof
let w be
FinSequence of
IAlph;
:: according to FSM_1:def 11 :: thesis: ( len w <= k1 implies (the Tran of tfsm . [qa,s]),w -response = (the Tran of tfsm . [qb,s]),w -response )
assume A5:
len w <= k1
;
:: thesis: (the Tran of tfsm . [qa,s]),w -response = (the Tran of tfsm . [qb,s]),w -response
set sw =
<*s*> ^ w;
A6:
len (<*s*> ^ w) =
(len <*s*>) + (len w)
by FINSEQ_1:35
.=
1
+ (len w)
by FINSEQ_1:57
;
A7:
(len w) + 1
<= k1 + 1
by A5, XREAL_1:9;
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 Th35;
A9:
(
0 + 1
in Seg (0 + 1) &
len <*s*> = 1 )
by FINSEQ_1:6, FINSEQ_1:57;
then A10:
1
in dom <*s*>
by FINSEQ_1:def 3;
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)]
by FINSEQ_1:def 8
.=
(qa,<*s*> -response ) . 1
by A10, Def6
.=
(qb,<*s*> -response ) . 1
by A3, A9, Def11
.=
the
OFun of
tfsm . [((qb,<*s*> -admissible ) . 1),(<*s*> . 1)]
by A10, Def6
.=
the
OFun of
tfsm . [((qb,<*s*> -admissible ) . 1),s]
by FINSEQ_1:def 8
.=
the
OFun of
tfsm . [qb,s]
by Def2
;
qa,
(<*s*> ^ w) -response = qb,
(<*s*> ^ w) -response
by A2, A4, A6, A7, Def11;
hence
(the Tran of tfsm . [qa,s]),
w -response = (the Tran of tfsm . [qb,s]),
w -response
by A8, A11, FINSEQ_1:46;
:: thesis: verum
end;
end;
assume that
A12:
1 -equivalent qa,qb
and
A13:
for s being Element of IAlph
for k1 being Element of NAT st k1 = k - 1 holds
k1 -equivalent the Tran of tfsm . [qa,s],the Tran of tfsm . [qb,s]
; :: thesis: k -equivalent qa,qb
thus
k -equivalent qa,qb
:: thesis: verumproof
let w be
FinSequence of
IAlph;
:: according to FSM_1:def 11 :: thesis: ( len w <= k implies qa,w -response = qb,w -response )
assume A14:
len w <= k
;
:: thesis: qa,w -response = qb,w -response
per cases
( w = <*> IAlph or not w is empty )
;
suppose
not
w is
empty
;
:: thesis: qa,w -response = qb,w -response then consider s being
Element of
IAlph,
w' being
FinSequence of
IAlph such that A16:
(
s = w . 1 &
w = <*s*> ^ w' )
by FINSEQ_3:111;
set qa' = the
Tran of
tfsm . [qa,s];
set qb' = the
Tran of
tfsm . [qb,s];
A17:
(
qa,
w -response = <*(the OFun of tfsm . [qa,s])*> ^ ((the Tran of tfsm . [qa,s]),w' -response ) &
qb,
w -response = <*(the OFun of tfsm . [qb,s])*> ^ ((the Tran of tfsm . [qb,s]),w' -response ) )
by A16, Th35;
A18:
(
0 + 1
in Seg (0 + 1) &
len <*s*> = 1 )
by FINSEQ_1:6, FINSEQ_1:57;
then A19:
1
in dom <*s*>
by FINSEQ_1:def 3;
A20: 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)]
by FINSEQ_1:def 8
.=
(qa,<*s*> -response ) . 1
by A19, Def6
.=
(qb,<*s*> -response ) . 1
by A12, A18, Def11
.=
the
OFun of
tfsm . [((qb,<*s*> -admissible ) . 1),(<*s*> . 1)]
by A19, Def6
.=
the
OFun of
tfsm . [((qb,<*s*> -admissible ) . 1),s]
by FINSEQ_1:def 8
.=
the
OFun of
tfsm . [qb,s]
by Def2
;
reconsider k1 =
k - 1 as
Element of
NAT by A1, INT_1:18;
A21:
k1 -equivalent the
Tran of
tfsm . [qa,s],the
Tran of
tfsm . [qb,s]
by A13;
len w =
(len <*s*>) + (len w')
by A16, FINSEQ_1:35
.=
(len w') + 1
by FINSEQ_1:57
;
then
((len w') + 1) - 1
<= k1
by A14, XREAL_1:11;
hence
qa,
w -response = qb,
w -response
by A17, A20, A21, Def11;
:: thesis: verum end;
end;