let IAlph, OAlph be non empty set ; 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; 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; 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; 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; ( 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
; ( crq21,crq22 -are_equivalent or not q1u,q2u -are_equivalent )
assume
not crq21,crq22 -are_equivalent
; 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
; verum