let k be Nat; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph st k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm holds
k -eq_states_partition tfsm is final
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph st k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm holds
k -eq_states_partition tfsm is final
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: ( k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm implies k -eq_states_partition tfsm is final )
set S = the carrier of tfsm;
set kpart = k -eq_states_partition tfsm;
set k1part = (k + 1) -eq_states_partition tfsm;
set keq = k -eq_states_EqR tfsm;
assume A1: k -eq_states_partition tfsm = (k + 1) -eq_states_partition tfsm ; :: thesis: k -eq_states_partition tfsm is final

now :: thesis: for qa, qb being Element of tfsm holds
( ( qa,qb -are_equivalent implies ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) ) & ( ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) implies qa,qb -are_equivalent ) )

let qa, qb be Element of tfsm; :: thesis: ( ( qa,qb -are_equivalent implies ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) ) & ( ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) implies qa,qb -are_equivalent ) )

hereby :: thesis: ( ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X ) implies qa,qb -are_equivalent )

reconsider X = Class ((k -eq_states_EqR tfsm),qb) as Element of k -eq_states_partition tfsm by EQREL_1:def 3;
assume A2: qa,qb -are_equivalent ; :: thesis: ex X being Element of k -eq_states_partition tfsm st
( qa in X & qb in X )
take X = X; :: thesis: ( qa in X & qb in X )
k -equivalent qa,qb by A2;
then [qa,qb] in k -eq_states_EqR tfsm by Def12;
hence ( qa in X & qb in X ) by EQREL_1:19, EQREL_1:20; :: thesis: verum

end;

given X being Element of k -eq_states_partition tfsm such that A3: qa in X and
A4: qb in X ; :: thesis: qa,qb -are_equivalent
consider qc being object such that
qc in the carrier of tfsm and
A5: X = Class ((k -eq_states_EqR tfsm),qc) by EQREL_1:def 3;
[qb,qc] in k -eq_states_EqR tfsm by A4, A5, EQREL_1:19;
then A6: [qc,qb] in k -eq_states_EqR tfsm by EQREL_1:6;
[qa,qc] in k -eq_states_EqR tfsm by A3, A5, EQREL_1:19;
then A7: [qa,qb] in k -eq_states_EqR tfsm by A6, EQREL_1:7;
then A8: k -equivalent qa,qb by Def12;
thus qa,qb -are_equivalent :: thesis: verum

proof

let w be FinSequence of IAlph; :: according to FSM_1:def 10 :: thesis: (qa,w) -response = (qb,w) -response
consider n being Nat such that
A9: dom w = Seg n by FINSEQ_1:def 2;
n in NAT by ORDINAL1:def 12;
then A10: n = len w by A9, FINSEQ_1:def 3;

per cases ( n <= k or n > k ) ;

suppose n <= k ; :: thesis: (qa,w) -response = (qb,w) -response

hence (qa,w) -response = (qb,w) -response by A8, A10; :: thesis: verum

end;

suppose n > k ; :: thesis: (qa,w) -response = (qb,w) -response

then ex m being Element of NAT st
( n = k + m & 1 <= m ) by FINSEQ_4:84;
then n -eq_states_partition tfsm = k -eq_states_partition tfsm by A1, Th29;
then [qa,qb] in n -eq_states_EqR tfsm by A7, FINSEQ_4:86;
then n -equivalent qa,qb by Def12;
hence (qa,w) -response = (qb,w) -response by A10; :: thesis: verum

end;

end;

end;

end;

hence k -eq_states_partition tfsm is final ; :: thesis: verum