let IAlph, OAlph be non empty set ; :: thesis: for Ctfsm being non empty finite connected Mealy-FSM of IAlph,OAlph holds the_reduction_of Ctfsm is connected
let Ctfsm be non empty finite connected Mealy-FSM of IAlph,OAlph; :: thesis: the_reduction_of Ctfsm is connected
set c = Ctfsm;
set rtfsm = the_reduction_of Ctfsm;
assume not the_reduction_of Ctfsm is connected ; :: thesis: contradiction
then consider Q being State of (the_reduction_of Ctfsm) such that
A1: not Q is accessible by Def22;
A2: the carrier of (the_reduction_of Ctfsm) = final_states_partition Ctfsm by Def18;
A3: Q in the carrier of (the_reduction_of Ctfsm) ;
reconsider Q' = Q as Subset of Ctfsm by A2, TARSKI:def 3;
Q' in final_states_partition Ctfsm by A3, Def18;
then consider q being Element of Ctfsm such that
A4: q in Q by Th11;
q is accessible by Def22;
then consider w being FinSequence of IAlph such that
A5: the InitS of Ctfsm,w -leads_to q by Def21;
A6: (the InitS of Ctfsm,w -admissible ) . ((len w) + 1) = q by A5, Def3;
A7: the InitS of Ctfsm in the InitS of (the_reduction_of Ctfsm) by Def18;
( 1 <= (len w) + 1 & (len w) + 1 <= (len w) + 1 ) by NAT_1:11;
then A8: (len w) + 1 in Seg ((len w) + 1) by FINSEQ_1:3;
then A9: q in (the InitS of (the_reduction_of Ctfsm),w -admissible ) . ((len w) + 1) by A6, A7, Th57;
(len w) + 1 in Seg (len (the InitS of (the_reduction_of Ctfsm),w -admissible )) by A8, Def2;
then (len w) + 1 in dom (the InitS of (the_reduction_of Ctfsm),w -admissible ) by FINSEQ_1:def 3;
then A10: (the InitS of (the_reduction_of Ctfsm),w -admissible ) . ((len w) + 1) in the carrier of (the_reduction_of Ctfsm) by FINSEQ_2:13;
then reconsider QQ = (the InitS of (the_reduction_of Ctfsm),w -admissible ) . ((len w) + 1) as Subset of Ctfsm by A2;
( Q' = QQ or Q' misses QQ ) by A2, A10, EQREL_1:def 6;
then the InitS of (the_reduction_of Ctfsm),w -leads_to Q by A4, A9, Def3, XBOOLE_0:3;
hence contradiction by A1, Def21; :: thesis: verum