let IAlph, OAlph be non empty set ; for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM over IAlph,OAlph st the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent holds
CRtfsm1,CRtfsm2 -are_isomorphic
let CRtfsm1, CRtfsm2 be non empty finite reduced connected Mealy-FSM over IAlph,OAlph; ( the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent implies CRtfsm1,CRtfsm2 -are_isomorphic )
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume that
A1:
the carrier of CRtfsm1 misses the carrier of CRtfsm2
and
A2:
CRtfsm1,CRtfsm2 -are_equivalent
; CRtfsm1,CRtfsm2 -are_isomorphic
set Srtfsm2 = the carrier of CRtfsm2;
set Srtfsm1 = the carrier of CRtfsm1;
set UN = CRtfsm1 -Mealy_union CRtfsm2;
set RUN = the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2);
set SRUN = the carrier of (the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2));
defpred S1[ object , object ] means ex part being Element of the carrier of (the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) st
( $1 in part & $2 in part \ {$1} );
A3:
the carrier of (the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) = final_states_partition (CRtfsm1 -Mealy_union CRtfsm2)
by Def18;
A4:
for x being object st x in the carrier of CRtfsm1 holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in the carrier of CRtfsm1 implies ex y being object st S1[x,y] )
set xs =
{x};
A5:
union the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) = the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by A3, EQREL_1:def 4;
assume A6:
x in the
carrier of
CRtfsm1
;
ex y being object st S1[x,y]
then
x in the
carrier of
CRtfsm1 \/ the
carrier of
CRtfsm2
by XBOOLE_0:def 3;
then
x in the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by Def24;
then consider part being
set such that A7:
x in part
and A8:
part in the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2))
by A5, TARSKI:def 4;
reconsider part =
part as
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) by A8;
consider p,
y being
Element of
part such that
p in the
carrier of
CRtfsm1
and A9:
y in the
carrier of
CRtfsm2
and
for
z being
Element of
part holds
(
z = p or
z = y )
by A1, A2, Th61;
set IT =
y;
take
y
;
S1[x,y]
x <> y
by A1, A6, A9, XBOOLE_0:3;
then
y in part \ {x}
by A7, ZFMISC_1:56;
hence
S1[
x,
y]
by A7;
verum
end;
consider f being Function such that
A10:
( dom f = the carrier of CRtfsm1 & ( for x being object st x in the carrier of CRtfsm1 holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A4);
now ( rng f c= the carrier of CRtfsm2 & the carrier of CRtfsm2 c= rng f )assume A11:
( not
rng f c= the
carrier of
CRtfsm2 or not the
carrier of
CRtfsm2 c= rng f )
;
contradictionper cases
( not rng f c= the carrier of CRtfsm2 or not the carrier of CRtfsm2 c= rng f )
by A11;
suppose A21:
not the
carrier of
CRtfsm2 c= rng f
;
contradictionA22:
union the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) = the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by A3, EQREL_1:def 4;
consider y1 being
object such that A23:
y1 in the
carrier of
CRtfsm2
and A24:
not
y1 in rng f
by A21;
y1 in the
carrier of
CRtfsm1 \/ the
carrier of
CRtfsm2
by A23, XBOOLE_0:def 3;
then
y1 in the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by Def24;
then consider Z being
set such that A25:
y1 in Z
and A26:
Z in the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2))
by A22, TARSKI:def 4;
reconsider Z =
Z as
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) by A26;
A27:
Z is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A3, TARSKI:def 3;
consider q1,
q2 being
Element of
Z such that A28:
q1 in the
carrier of
CRtfsm1
and
q2 in the
carrier of
CRtfsm2
and
for
q being
Element of
Z holds
(
q = q1 or
q = q2 )
by A1, A2, Th61;
consider F being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A29:
q1 in F
and A30:
f . q1 in F \ {q1}
by A10, A28;
F is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A3, TARSKI:def 3;
then A31:
(
Z = F or
Z misses F )
by A3, A27, EQREL_1:def 4;
A32:
f . q1 in F
by A30;
now not y1 <> f . q1
Z is
Subset of
( the carrier of CRtfsm1 \/ the carrier of CRtfsm2)
by A27, Def24;
then A35:
(
f . q1 in the
carrier of
CRtfsm1 or
f . q1 in the
carrier of
CRtfsm2 )
by A25, A29, A31, A32, XBOOLE_0:3, XBOOLE_0:def 3;
assume
y1 <> f . q1
;
contradictionhence
contradiction
by A23, A25, A29, A30, A31, A35, A33, Th60, XBOOLE_0:3;
verum end; hence
contradiction
by A10, A24, A28, FUNCT_1:def 3;
verum end; end;
then A36:
rng f = the carrier of CRtfsm2
;
A37:
now for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
not x1 <> x2let x1,
x2 be
object ;
( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies not x1 <> x2 )assume that A38:
x1 in dom f
and A39:
x2 in dom f
and A40:
f . x1 = f . x2
;
not x1 <> x2consider part1 being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A41:
(
x1 in part1 &
f . x1 in part1 \ {x1} )
by A10, A38;
consider part2 being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A42:
(
x2 in part2 &
f . x2 in part2 \ {x2} )
by A10, A39;
assume A43:
x1 <> x2
;
contradiction
(
part1 is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2) &
part2 is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2) )
by A3, TARSKI:def 3;
then
(
part1 = part2 or
part1 misses part2 )
by A3, EQREL_1:def 4;
hence
contradiction
by A1, A10, A38, A39, A40, A43, A41, A42, Th59, XBOOLE_0:3;
verum end;
reconsider f = f as Function of the carrier of CRtfsm1, the carrier of CRtfsm2 by A10, A36, FUNCT_2:1;
A44:
f . the InitS of CRtfsm1 = the InitS of CRtfsm2
A48:
for q being State of CRtfsm1
for s being Element of IAlph holds
( f . ( the Tran of CRtfsm1 . (q,s)) = the Tran of CRtfsm2 . ((f . q),s) & the OFun of CRtfsm1 . (q,s) = the OFun of CRtfsm2 . ((f . q),s) )
proof
let q be
State of
CRtfsm1;
for s being Element of IAlph holds
( f . ( the Tran of CRtfsm1 . (q,s)) = the Tran of CRtfsm2 . ((f . q),s) & the OFun of CRtfsm1 . (q,s) = the OFun of CRtfsm2 . ((f . q),s) )let s be
Element of
IAlph;
( f . ( the Tran of CRtfsm1 . (q,s)) = the Tran of CRtfsm2 . ((f . q),s) & the OFun of CRtfsm1 . (q,s) = the OFun of CRtfsm2 . ((f . q),s) )
set q1 = the
Tran of
CRtfsm1 . [q,s];
set fq =
f . q;
set q2 = the
Tran of
CRtfsm2 . [(f . q),s];
A49:
dom the
Tran of
CRtfsm2 = [: the carrier of CRtfsm2,IAlph:]
by FUNCT_2:def 1;
A50:
the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2) = the
carrier of
CRtfsm1 \/ the
carrier of
CRtfsm2
by Def24;
then reconsider q9 =
q as
Element of
(CRtfsm1 -Mealy_union CRtfsm2) by XBOOLE_0:def 3;
f . q in rng f
by A10, FUNCT_1:def 3;
then reconsider fq9 =
f . q9 as
Element of
(CRtfsm1 -Mealy_union CRtfsm2) by A50, XBOOLE_0:def 3;
set qu = the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q9,s];
set qfu = the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq9,s];
A51: the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq9,s] =
( the Tran of CRtfsm1 +* the Tran of CRtfsm2) . [fq9,s]
by Def24
.=
the
Tran of
CRtfsm2 . [(f . q),s]
by A49, FUNCT_4:13
;
consider XX being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A52:
( the
Tran of
CRtfsm1 . [q,s] in XX &
f . ( the Tran of CRtfsm1 . [q,s]) in XX \ {( the Tran of CRtfsm1 . [q,s])} )
by A10;
A53:
final_states_partition (CRtfsm1 -Mealy_union CRtfsm2) is
final
by Def15;
ex
part being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) st
(
q in part &
f . q in part \ {q} )
by A10;
then A54:
q9,
fq9 -are_equivalent
by A3, A53;
then
the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q9,s], the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq9,s] -are_equivalent
by Th19;
then consider X being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A55:
( the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q9,s] in X & the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq9,s] in X )
by A3, A53;
A56:
the
carrier of
CRtfsm1 /\ the
carrier of
CRtfsm2 = {}
by A1;
A57:
dom the
Tran of
CRtfsm1 = [: the carrier of CRtfsm1,IAlph:]
by FUNCT_2:def 1;
then (dom the Tran of CRtfsm1) /\ (dom the Tran of CRtfsm2) =
[: the carrier of CRtfsm1,IAlph:] /\ [: the carrier of CRtfsm2,IAlph:]
by FUNCT_2:def 1
.=
[:{},IAlph:]
by A56, ZFMISC_1:99
.=
{}
by ZFMISC_1:90
;
then A58:
dom the
Tran of
CRtfsm1 misses dom the
Tran of
CRtfsm2
;
A59: the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q9,s] =
( the Tran of CRtfsm1 +* the Tran of CRtfsm2) . [q9,s]
by Def24
.=
the
Tran of
CRtfsm1 . [q,s]
by A57, A58, FUNCT_4:16
;
A60:
X is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A3, TARSKI:def 3;
now not f . ( the Tran of CRtfsm1 . [q,s]) <> the Tran of CRtfsm2 . [(f . q),s]
XX is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A3, TARSKI:def 3;
then A61:
(
X = XX or
X misses XX )
by A3, A60, EQREL_1:def 4;
assume
f . ( the Tran of CRtfsm1 . [q,s]) <> the
Tran of
CRtfsm2 . [(f . q),s]
;
contradictionhence
contradiction
by A55, A59, A51, A52, A61, Th60, XBOOLE_0:3;
verum end;
hence
f . ( the Tran of CRtfsm1 . (q,s)) = the
Tran of
CRtfsm2 . (
(f . q),
s)
;
the OFun of CRtfsm1 . (q,s) = the OFun of CRtfsm2 . ((f . q),s)
A62:
dom the
OFun of
CRtfsm2 = [: the carrier of CRtfsm2,IAlph:]
by FUNCT_2:def 1;
A63:
dom the
OFun of
CRtfsm1 = [: the carrier of CRtfsm1,IAlph:]
by FUNCT_2:def 1;
then (dom the OFun of CRtfsm1) /\ (dom the OFun of CRtfsm2) =
[:( the carrier of CRtfsm1 /\ the carrier of CRtfsm2),IAlph:]
by A62, ZFMISC_1:99
.=
{}
by A56, ZFMISC_1:90
;
then
dom the
OFun of
CRtfsm1 misses dom the
OFun of
CRtfsm2
;
hence the
OFun of
CRtfsm1 . (
q,
s) =
( the OFun of CRtfsm1 +* the OFun of CRtfsm2) . [q,s]
by A63, FUNCT_4:16
.=
the
OFun of
(CRtfsm1 -Mealy_union CRtfsm2) . [q9,s]
by Def24
.=
the
OFun of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq9,s]
by A54, Th19
.=
( the OFun of CRtfsm1 +* the OFun of CRtfsm2) . [(f . q),s]
by Def24
.=
the
OFun of
CRtfsm2 . (
(f . q),
s)
by A62, FUNCT_4:13
;
verum
end;
( f is one-to-one & f is onto )
by A37, A36, FUNCT_1:def 4, FUNCT_2:def 3;
hence
CRtfsm1,CRtfsm2 -are_isomorphic
by A44, A48; verum