let k be Nat; :: thesis: for IAlph, OAlph being non empty set
for tfsm being non empty Mealy-FSM over IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty Mealy-FSM over IAlph,OAlph holds (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
let tfsm be non empty Mealy-FSM over IAlph,OAlph; :: thesis: (k + 1) -eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
set K = k -eq_states_partition tfsm;
set K1 = (k + 1) -eq_states_partition tfsm;
set S = the carrier of tfsm;
let X be set ; :: according to SETFAM_1:def 2 :: thesis: ( not X in (k + 1) -eq_states_partition tfsm or ex b₁ being set st
( b₁ in k -eq_states_partition tfsm & X c= b₁ ) )
assume A1: X in (k + 1) -eq_states_partition tfsm ; :: thesis: ex b₁ being set st
( b₁ in k -eq_states_partition tfsm & X c= b₁ )
then reconsider X9 = X as Subset of the carrier of tfsm ;
consider q being Element of the carrier of tfsm such that
A2: q in X by A1, FINSEQ_4:87;
reconsider Y = (proj (k -eq_states_partition tfsm)) . q as Element of k -eq_states_partition tfsm ;
take Y ; :: thesis: ( Y in k -eq_states_partition tfsm & X c= Y )
thus Y in k -eq_states_partition tfsm ; :: thesis: X c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Y )
assume A3: x in X ; :: thesis: x in Y
then x in X9 ;
then reconsider x9 = x as Element of the carrier of tfsm ;
reconsider X9 = X9 as Element of Class ((k + 1) -eq_states_EqR tfsm) by A1;
consider Q being object such that
Q in the carrier of tfsm and
A4: X9 = Class (((k + 1) -eq_states_EqR tfsm),Q) by EQREL_1:def 3;
[x9,Q] in (k + 1) -eq_states_EqR tfsm by A3, A4, EQREL_1:19;
then A5: [Q,x9] in (k + 1) -eq_states_EqR tfsm by EQREL_1:6;
[q,Q] in (k + 1) -eq_states_EqR tfsm by A2, A4, EQREL_1:19;
then [q,x9] in (k + 1) -eq_states_EqR tfsm by A5, EQREL_1:7;
then k + 1 -equivalent q,x9 by Def12;
then k -equivalent q,x9 by Th26;
then [q,x9] in k -eq_states_EqR tfsm by Def12;
then A6: [x9,q] in k -eq_states_EqR tfsm by EQREL_1:6;
reconsider Y9 = Y as Element of Class (k -eq_states_EqR tfsm) ;
consider Q being object such that
A7: Q in the carrier of tfsm and
A8: Y9 = Class ((k -eq_states_EqR tfsm),Q) by EQREL_1:def 3;
reconsider Q = Q as Element of the carrier of tfsm by A7;
q in Y by EQREL_1:def 9;
then Class ((k -eq_states_EqR tfsm),Q) = Class ((k -eq_states_EqR tfsm),q) by A8, EQREL_1:23;
hence x in Y by A6, A8, EQREL_1:19; :: thesis: verum