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]

proof

let w be FinSequence of IAlph; :: according to FSM_1:def 11 :: thesis: ( len w <= 1 implies (qa,w) -response = (qb,w) -response )
assume len w <= 1 ; :: thesis: (qa,w) -response = (qb,w) -response
then len w <= k by A1, XXREAL_0:2;
hence (qa,w) -response = (qb,w) -response by A2, Def11; :: thesis: verum

end;

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 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] :: thesis: verum

proof

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 )
set sw = <*s*> ^ w;
A5: len <*s*> = 1 by FINSEQ_1:57;
assume len w <= k1 ; :: thesis: (( 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:9;
len (<*s*> ^ w) = (len <*s*>) + (len w) by FINSEQ_1:35
.= 1 + (len w) by FINSEQ_1:57 ;
then A7: (qa,(<*s*> ^ w)) -response = (qb,(<*s*> ^ w)) -response by A2, A4, A6, Def11;
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;
0 + 1 in Seg (0 + 1) by FINSEQ_1:6;
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)] by FINSEQ_1:def 8
.= ((qa,<*s*>) -response) . 1 by A9, Def6
.= ((qb,<*s*>) -response) . 1 by A3, A5, Def11
.= the OFun of tfsm . [(((qb,<*s*>) -admissible) . 1),(<*s*> . 1)] by A9, Def6
.= the OFun of tfsm . [(((qb,<*s*>) -admissible) . 1),s] by FINSEQ_1:def 8
.= 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:46; :: thesis: verum

end;

end;

assume that
A10: 1 -equivalent qa,qb and
A11: 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: verum

proof

let w be FinSequence of IAlph; :: according to FSM_1:def 11 :: thesis: ( len w <= k implies (qa,w) -response = (qb,w) -response )
assume A12: len w <= k ; :: thesis: (qa,w) -response = (qb,w) -response

per cases ( w = <*> IAlph or not w is empty ) ;

suppose A13: w = <*> IAlph ; :: thesis: (qa,w) -response = (qb,w) -response

hence (qa,w) -response = <*> OAlph by Th24
.= (qb,w) -response by A13, Th24 ;
:: thesis: verum

end;

suppose not w is empty ; :: thesis: (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:111;
reconsider k1 = k - 1 as Element of NAT by A1, INT_1:18;
A15: len <*s*> = 1 by FINSEQ_1:57;
len w = (len <*s*>) + (len w9) by A14, FINSEQ_1:35
.= (len w9) + 1 by FINSEQ_1:57 ;
then A16: ((len w9) + 1) - 1 <= k1 by A12, XREAL_1:11;
0 + 1 in Seg (0 + 1) by FINSEQ_1:6;
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, Th35;
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)] by FINSEQ_1:def 8
.= ((qa,<*s*>) -response) . 1 by A17, Def6
.= ((qb,<*s*>) -response) . 1 by A10, A15, Def11
.= the OFun of tfsm . [(((qb,<*s*>) -admissible) . 1),(<*s*> . 1)] by A17, Def6
.= the OFun of tfsm . [(((qb,<*s*>) -admissible) . 1),s] by FINSEQ_1:def 8
.= the OFun of tfsm . [qb,s] by Def2 ;
hence (qa,w) -response = (qb,w) -response by A18, A19, A16, Def11; :: thesis: verum

end;

end;

end;