let IAlph, OAlph be non empty set ; :: thesis: for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for CRtfsm1, CRtfsm2 being non empty reduced connected Mealy-FSM over IAlph,OAlph
for q1u, q2u being State of tfsm
for crq21, crq22 being State of CRtfsm2 st crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent holds
not q1u,q2u -are_equivalent
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; :: thesis: for CRtfsm1, CRtfsm2 being non empty reduced connected Mealy-FSM over IAlph,OAlph
for q1u, q2u being State of tfsm
for crq21, crq22 being State of CRtfsm2 st crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent holds
not q1u,q2u -are_equivalent
let CRtfsm1, CRtfsm2 be non empty reduced connected Mealy-FSM over IAlph,OAlph; :: thesis: for q1u, q2u being State of tfsm
for crq21, crq22 being State of CRtfsm2 st crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent holds
not q1u,q2u -are_equivalent
let q1u, q2u be State of tfsm; :: thesis: for crq21, crq22 being State of CRtfsm2 st crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent holds
not q1u,q2u -are_equivalent
let crq21, crq22 be State of CRtfsm2; :: thesis: ( crq21 = q1u & crq22 = q2u & tfsm = CRtfsm1 -Mealy_union CRtfsm2 & not crq21,crq22 -are_equivalent implies not q1u,q2u -are_equivalent )
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
set q1 = crq21;
set q2 = crq22;
assume that
A1: crq21 = q1u and
A2: crq22 = q2u and
A3: tfsm = CRtfsm1 -Mealy_union CRtfsm2 ; :: thesis: ( crq21,crq22 -are_equivalent or not q1u,q2u -are_equivalent )
assume not crq21,crq22 -are_equivalent ; :: thesis: not q1u,q2u -are_equivalent
then consider w being FinSequence of IAlph such that
A4: (crq21,w) -response <> (crq22,w) -response ;
(q1u,w) -response = (crq21,w) -response by A1, A3, Th55;
then (q1u,w) -response <> (q2u,w) -response by A2, A3, A4, Th55;
hence not q1u,q2u -are_equivalent ; :: thesis: verum