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