let IAlph, OAlph be non empty set ; for Ctfsm1, Ctfsm2 being non empty finite connected Mealy-FSM of 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 of 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 of 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 Th81;
A5:
the_reduction_of Ctfsm1,Ctfsm1 -are_equivalent
by Th58;
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 Th58;
fsm2, the_reduction_of Ctfsm2 -are_equivalent
by A4, Th82;
then A7:
fsm2,Ctfsm2 -are_equivalent
by A6, Th30;
A9:
fsm1 is connected
proof
assume
not
fsm1 is
connected
;
contradiction
then consider q1 being
Element of the
carrier of
fsm1 such that A10:
not
q1 is
accessible
by Def22;
consider Tf being
Function of the
carrier of
fsm1, the
carrier of
(the_reduction_of Ctfsm1) such that A11:
Tf is
bijective
and A12:
(
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, Def19;
A13:
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 A14:
the
InitS of
(the_reduction_of Ctfsm1),
w -leads_to Tf . q1
by Def21;
A15:
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 A12, Th60;
then A16:
(Tf ") . (Tf . ((( the InitS of fsm1,w) -admissible) . ((len w) + 1))) = (Tf ") . (Tf . q1)
by A14, Def3;
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 A15, 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 A13, FINSEQ_2:11;
then (( the InitS of fsm1,w) -admissible) . ((len w) + 1) =
(Tf ") . (Tf . q1)
by A11, A16, FUNCT_1:34
.=
q1
by A11, A13, FUNCT_1:34
;
then
the
InitS of
fsm1,
w -leads_to q1
by Def3;
hence
contradiction
by A10, Def21;
verum
end;
A18:
fsm2 is connected
proof
assume
not
fsm2 is
connected
;
contradiction
then consider q1 being
Element of the
carrier of
fsm2 such that A19:
not
q1 is
accessible
by Def22;
consider Tf being
Function of the
carrier of
fsm2, the
carrier of
(the_reduction_of Ctfsm2) such that A20:
Tf is
bijective
and A21:
(
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, Def19;
A22:
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 A23:
the
InitS of
(the_reduction_of Ctfsm2),
w -leads_to Tf . q1
by Def21;
A24:
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 A21, Th60;
then A25:
(Tf ") . (Tf . ((( the InitS of fsm2,w) -admissible) . ((len w) + 1))) = (Tf ") . (Tf . q1)
by A23, Def3;
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 A24, 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 A22, FINSEQ_2:11;
then (( the InitS of fsm2,w) -admissible) . ((len w) + 1) =
(Tf ") . (Tf . q1)
by A20, A25, FUNCT_1:34
.=
q1
by A20, A22, FUNCT_1:34
;
then
the
InitS of
fsm2,
w -leads_to q1
by Def3;
hence
contradiction
by A19, Def21;
verum
end;
fsm1, the_reduction_of Ctfsm1 -are_equivalent
by A3, Th82;
then
fsm1,Ctfsm1 -are_equivalent
by A5, Th30;
then A26:
fsm1,Ctfsm2 -are_equivalent
by A1, Th30;
reconsider fsm1 = fsm1, fsm2 = fsm2 as non empty finite reduced Mealy-FSM of IAlph,OAlph by A3, A4, Th65;
fsm1,fsm2 -are_isomorphic
by A2, A9, A18, A7, A26, Th30, Th83;
then
fsm1, the_reduction_of Ctfsm2 -are_isomorphic
by A4, Th59;
hence
the_reduction_of Ctfsm1, the_reduction_of Ctfsm2 -are_isomorphic
by A3, Th59; verum