let IAlph, OAlph be non empty set ; for Ctfsm1, Ctfsm2 being non empty finite connected Mealy-FSM over IAlph,OAlph st Ctfsm1,Ctfsm2 -are_equivalent holds
the_reduction_of Ctfsm1, the_reduction_of Ctfsm2 -are_isomorphic
let Ctfsm1, Ctfsm2 be non empty finite connected Mealy-FSM over IAlph,OAlph; ( Ctfsm1,Ctfsm2 -are_equivalent implies the_reduction_of Ctfsm1, the_reduction_of Ctfsm2 -are_isomorphic )
assume A1:
Ctfsm1,Ctfsm2 -are_equivalent
; the_reduction_of Ctfsm1, the_reduction_of Ctfsm2 -are_isomorphic
set rtfsm2 = the_reduction_of Ctfsm2;
set rtfsm1 = the_reduction_of Ctfsm1;
consider fsm1, fsm2 being non empty finite Mealy-FSM over IAlph,OAlph such that
A2:
the carrier of fsm1 misses the carrier of fsm2
and
A3:
fsm1, the_reduction_of Ctfsm1 -are_isomorphic
and
A4:
fsm2, the_reduction_of Ctfsm2 -are_isomorphic
by Th62;
A5:
the_reduction_of Ctfsm1,Ctfsm1 -are_equivalent
by Th41;
set Srtfsm1 = the carrier of (the_reduction_of Ctfsm1);
set Srtfsm2 = the carrier of (the_reduction_of Ctfsm2);
set ISrtfsm1 = the InitS of (the_reduction_of Ctfsm1);
set ISrtfsm2 = the InitS of (the_reduction_of Ctfsm2);
set Sfsm1 = the carrier of fsm1;
set Sfsm2 = the carrier of fsm2;
set ISfsm1 = the InitS of fsm1;
set ISfsm2 = the InitS of fsm2;
A6:
the_reduction_of Ctfsm2,Ctfsm2 -are_equivalent
by Th41;
fsm2, the_reduction_of Ctfsm2 -are_equivalent
by A4, Th63;
then A7:
fsm2,Ctfsm2 -are_equivalent
by A6, Th15;
A8:
fsm1 is connected
proof
assume
not
fsm1 is
connected
;
contradiction
then consider q1 being
Element of the
carrier of
fsm1 such that A9:
not
q1 is
accessible
;
consider Tf being
Function of the
carrier of
fsm1, the
carrier of
(the_reduction_of Ctfsm1) such that A10:
Tf is
bijective
and A11:
(
Tf . the
InitS of
fsm1 = the
InitS of
(the_reduction_of Ctfsm1) & ( for
q being
State of
fsm1 for
s being
Element of
IAlph holds
(
Tf . ( the Tran of fsm1 . (q,s)) = the
Tran of
(the_reduction_of Ctfsm1) . (
(Tf . q),
s) & the
OFun of
fsm1 . (
q,
s)
= the
OFun of
(the_reduction_of Ctfsm1) . (
(Tf . q),
s) ) ) )
by A3;
A12:
dom Tf = the
carrier of
fsm1
by FUNCT_2:def 1;
set q =
Tf . q1;
Tf . q1 is
accessible
by Def22;
then consider w being
FinSequence of
IAlph such that A13:
the
InitS of
(the_reduction_of Ctfsm1),
w -leads_to Tf . q1
;
A14:
1
<= (len w) + 1
by NAT_1:11;
then
Tf . ((( the InitS of fsm1,w) -admissible) . ((len w) + 1)) = (( the InitS of (the_reduction_of Ctfsm1),w) -admissible) . ((len w) + 1)
by A11, Th43;
then A15:
(Tf ") . (Tf . ((( the InitS of fsm1,w) -admissible) . ((len w) + 1))) = (Tf ") . (Tf . q1)
by A13;
len (( the InitS of fsm1,w) -admissible) = (len w) + 1
by Def2;
then
(len w) + 1
in Seg (len (( the InitS of fsm1,w) -admissible))
by A14, FINSEQ_1:1;
then
(len w) + 1
in dom (( the InitS of fsm1,w) -admissible)
by FINSEQ_1:def 3;
then
(( the InitS of fsm1,w) -admissible) . ((len w) + 1) in dom Tf
by A12, FINSEQ_2:11;
then (( the InitS of fsm1,w) -admissible) . ((len w) + 1) =
(Tf ") . (Tf . q1)
by A10, A15, FUNCT_1:34
.=
q1
by A10, A12, FUNCT_1:34
;
then
the
InitS of
fsm1,
w -leads_to q1
;
hence
contradiction
by A9;
verum
end;
A16:
fsm2 is connected
proof
assume
not
fsm2 is
connected
;
contradiction
then consider q1 being
Element of the
carrier of
fsm2 such that A17:
not
q1 is
accessible
;
consider Tf being
Function of the
carrier of
fsm2, the
carrier of
(the_reduction_of Ctfsm2) such that A18:
Tf is
bijective
and A19:
(
Tf . the
InitS of
fsm2 = the
InitS of
(the_reduction_of Ctfsm2) & ( for
q being
State of
fsm2 for
s being
Element of
IAlph holds
(
Tf . ( the Tran of fsm2 . (q,s)) = the
Tran of
(the_reduction_of Ctfsm2) . (
(Tf . q),
s) & the
OFun of
fsm2 . (
q,
s)
= the
OFun of
(the_reduction_of Ctfsm2) . (
(Tf . q),
s) ) ) )
by A4;
A20:
dom Tf = the
carrier of
fsm2
by FUNCT_2:def 1;
set q =
Tf . q1;
Tf . q1 is
accessible
by Def22;
then consider w being
FinSequence of
IAlph such that A21:
the
InitS of
(the_reduction_of Ctfsm2),
w -leads_to Tf . q1
;
A22:
1
<= (len w) + 1
by NAT_1:11;
then
Tf . ((( the InitS of fsm2,w) -admissible) . ((len w) + 1)) = (( the InitS of (the_reduction_of Ctfsm2),w) -admissible) . ((len w) + 1)
by A19, Th43;
then A23:
(Tf ") . (Tf . ((( the InitS of fsm2,w) -admissible) . ((len w) + 1))) = (Tf ") . (Tf . q1)
by A21;
len (( the InitS of fsm2,w) -admissible) = (len w) + 1
by Def2;
then
(len w) + 1
in Seg (len (( the InitS of fsm2,w) -admissible))
by A22, FINSEQ_1:1;
then
(len w) + 1
in dom (( the InitS of fsm2,w) -admissible)
by FINSEQ_1:def 3;
then
(( the InitS of fsm2,w) -admissible) . ((len w) + 1) in dom Tf
by A20, FINSEQ_2:11;
then (( the InitS of fsm2,w) -admissible) . ((len w) + 1) =
(Tf ") . (Tf . q1)
by A18, A23, FUNCT_1:34
.=
q1
by A18, A20, FUNCT_1:34
;
then
the
InitS of
fsm2,
w -leads_to q1
;
hence
contradiction
by A17;
verum
end;
fsm1, the_reduction_of Ctfsm1 -are_equivalent
by A3, Th63;
then
fsm1,Ctfsm1 -are_equivalent
by A5, Th15;
then A24:
fsm1,Ctfsm2 -are_equivalent
by A1, Th15;
reconsider fsm1 = fsm1, fsm2 = fsm2 as non empty finite reduced Mealy-FSM over IAlph,OAlph by A3, A4, Th47;
fsm1,fsm2 -are_isomorphic
by A2, A8, A16, A7, A24, Th15, Th64;
then
fsm1, the_reduction_of Ctfsm2 -are_isomorphic
by A4, Th42;
hence
the_reduction_of Ctfsm1, the_reduction_of Ctfsm2 -are_isomorphic
by A3, Th42; verum