let IAlph, OAlph be non empty set ; :: thesis: for CRtfsm1, CRtfsm2 being non empty finite reduced connected Mealy-FSM of 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 of IAlph,OAlph; :: thesis: ( 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 A1:
( the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,CRtfsm2 -are_equivalent )
; :: thesis: CRtfsm1,CRtfsm2 -are_isomorphic
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));
set Srtfsm1 = the carrier of CRtfsm1;
set Srtfsm2 = the carrier of CRtfsm2;
A2:
the carrier of (the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) = final_states_partition (CRtfsm1 -Mealy_union CRtfsm2)
by Def18;
defpred S1[ set , set ] means ex part being Element of the carrier of (the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) st
( $1 in part & $2 in part \ {$1} );
A17:
for x being set st x in the carrier of CRtfsm1 holds
ex y being set st S1[x,y]
proof
let x be
set ;
:: thesis: ( x in the carrier of CRtfsm1 implies ex y being set st S1[x,y] )
assume A18:
x in the
carrier of
CRtfsm1
;
:: thesis: ex y being set st S1[x,y]
then
x in the
carrier of
CRtfsm1 \/ the
carrier of
CRtfsm2
by XBOOLE_0:def 3;
then A19:
x in the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by Def24;
union the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) = the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, EQREL_1:def 6;
then consider part being
set such that A20:
(
x in part &
part in the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) )
by A19, TARSKI:def 4;
reconsider part =
part as
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) by A20;
set xs =
{x};
consider p,
y being
Element of
part such that A21:
(
p in the
carrier of
CRtfsm1 &
y in the
carrier of
CRtfsm2 & ( for
z being
Element of
part holds
(
z = p or
z = y ) ) )
by A1, Th80;
x <> y
by A1, A18, A21, XBOOLE_0:3;
then A22:
y in part \ {x}
by A20, ZFMISC_1:64;
set IT =
y;
take
y
;
:: thesis: S1[x,y]
thus
S1[
x,
y]
by A20, A22;
:: thesis: verum
end;
consider f being Function such that
A23:
( dom f = the carrier of CRtfsm1 & ( for x being set st x in the carrier of CRtfsm1 holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A17);
A24:
f is one-to-one
proof
now let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies not x1 <> x2 )assume A25:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: not x1 <> x2assume A26:
x1 <> x2
;
:: thesis: contradictionconsider part1 being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A27:
(
x1 in part1 &
f . x1 in part1 \ {x1} )
by A23, A25;
consider part2 being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A28:
(
x2 in part2 &
f . x2 in part2 \ {x2} )
by A23, A25;
A29:
part1 is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
part2 is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
then
(
part1 = part2 or
part1 misses part2 )
by A2, A29, EQREL_1:def 6;
hence
contradiction
by A1, A23, A25, A26, A27, A28, Th78, XBOOLE_0:3;
:: thesis: verum end;
hence
f is
one-to-one
by FUNCT_1:def 8;
:: thesis: verum
end;
A30:
rng f = the carrier of CRtfsm2
proof
now assume A31:
( not
rng f c= the
carrier of
CRtfsm2 or not the
carrier of
CRtfsm2 c= rng f )
;
:: thesis: contradictionper cases
( not rng f c= the carrier of CRtfsm2 or not the carrier of CRtfsm2 c= rng f )
by A31;
suppose
not the
carrier of
CRtfsm2 c= rng f
;
:: thesis: contradictionthen consider y1 being
set such that A38:
(
y1 in the
carrier of
CRtfsm2 & not
y1 in rng f )
by TARSKI:def 3;
y1 in the
carrier of
CRtfsm1 \/ the
carrier of
CRtfsm2
by A38, XBOOLE_0:def 3;
then A39:
y1 in the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by Def24;
union the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) = the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, EQREL_1:def 6;
then consider Z being
set such that A40:
(
y1 in Z &
Z in the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) )
by A39, TARSKI:def 4;
reconsider Z =
Z as
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) by A40;
consider q1,
q2 being
Element of
Z such that A41:
(
q1 in the
carrier of
CRtfsm1 &
q2 in the
carrier of
CRtfsm2 & ( for
q being
Element of
Z holds
(
q = q1 or
q = q2 ) ) )
by A1, Th80;
consider F being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A42:
(
q1 in F &
f . q1 in F \ {q1} )
by A23, A41;
A43:
Z is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
F is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
then A44:
(
Z = F or
Z misses F )
by A2, A43, EQREL_1:def 6;
A45:
f . q1 in F
by A42;
now assume A46:
y1 <> f . q1
;
:: thesis: contradiction
Z is
Subset of
(the carrier of CRtfsm1 \/ the carrier of CRtfsm2)
by A43, Def24;
then A47:
(
f . q1 in the
carrier of
CRtfsm1 or
f . q1 in the
carrier of
CRtfsm2 )
by A40, A42, A44, A45, XBOOLE_0:3, XBOOLE_0:def 3;
hence
contradiction
by A1, A38, A40, A42, A44, A46, A47, Th79, XBOOLE_0:3;
:: thesis: verum end; hence
contradiction
by A23, A38, A41, FUNCT_1:def 5;
:: thesis: verum end; end;
hence
rng f = the
carrier of
CRtfsm2
by XBOOLE_0:def 10;
:: thesis: verum
end;
then reconsider f = f as Function of the carrier of CRtfsm1,the carrier of CRtfsm2 by A23, FUNCT_2:3;
( f is one-to-one & f is onto )
by A24, A30, FUNCT_2:def 3;
then A49:
f is bijective
;
A50:
f . the InitS of CRtfsm1 = the InitS of CRtfsm2
proof
assume A51:
f . the
InitS of
CRtfsm1 <> the
InitS of
CRtfsm2
;
:: thesis: contradiction
consider Q being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A52:
( the
InitS of
CRtfsm1 in Q & the
InitS of
CRtfsm2 in Q &
Q = the
InitS of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) )
by A1, Th75;
consider part being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A53:
( the
InitS of
CRtfsm1 in part &
f . the
InitS of
CRtfsm1 in part \ {the InitS of CRtfsm1} )
by A23;
A54:
Q is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
part is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
then
(
Q = part or
Q misses part )
by A2, A54, EQREL_1:def 6;
hence
contradiction
by A1, A51, A52, A53, Th79, XBOOLE_0:3;
:: thesis: verum
end;
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;
:: thesis: 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;
:: thesis: ( 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 )
A55:
the
carrier of
(CRtfsm1 -Mealy_union CRtfsm2) = the
carrier of
CRtfsm1 \/ the
carrier of
CRtfsm2
by Def24;
then reconsider q' =
q as
Element of
(CRtfsm1 -Mealy_union CRtfsm2) by XBOOLE_0:def 3;
f . q in rng f
by A23, FUNCT_1:def 5;
then reconsider fq' =
f . q' as
Element of
(CRtfsm1 -Mealy_union CRtfsm2) by A55, XBOOLE_0:def 3;
A56:
final_states_partition (CRtfsm1 -Mealy_union CRtfsm2) is
final
by Def15;
consider part being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A57:
(
q in part &
f . q in part \ {q} )
by A23;
A58:
q',
fq' -are_equivalent
by A2, A56, A57, Def14;
set qu = the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q',s];
set qfu = the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq',s];
set q1 = the
Tran of
CRtfsm1 . [q,s];
set fq =
f . q;
set q2 = the
Tran of
CRtfsm2 . [(f . q),s];
the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q',s],the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq',s] -are_equivalent
by A58, Th36;
then consider X being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A59:
( the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q',s] in X & the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq',s] in X )
by A2, A56, Def14;
A60:
dom the
Tran of
CRtfsm1 = [:the carrier of CRtfsm1,IAlph:]
by FUNCT_2:def 1;
A61:
the
carrier of
CRtfsm1 /\ the
carrier of
CRtfsm2 = {}
by A1, XBOOLE_0:def 7;
(dom the Tran of CRtfsm1) /\ (dom the Tran of CRtfsm2) =
[:the carrier of CRtfsm1,IAlph:] /\ [:the carrier of CRtfsm2,IAlph:]
by A60, FUNCT_2:def 1
.=
[:{} ,IAlph:]
by A61, ZFMISC_1:122
.=
{}
by ZFMISC_1:113
;
then A62:
dom the
Tran of
CRtfsm1 misses dom the
Tran of
CRtfsm2
by XBOOLE_0:def 7;
A63: the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [q',s] =
(the Tran of CRtfsm1 +* the Tran of CRtfsm2) . [q',s]
by Def24
.=
the
Tran of
CRtfsm1 . [q,s]
by A60, A62, FUNCT_4:17
;
A64:
dom the
Tran of
CRtfsm2 = [:the carrier of CRtfsm2,IAlph:]
by FUNCT_2:def 1;
A65: the
Tran of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq',s] =
(the Tran of CRtfsm1 +* the Tran of CRtfsm2) . [fq',s]
by Def24
.=
the
Tran of
CRtfsm2 . [(f . q),s]
by A64, FUNCT_4:14
;
consider XX being
Element of the
carrier of
(the_reduction_of (CRtfsm1 -Mealy_union CRtfsm2)) such that A66:
( the
Tran of
CRtfsm1 . [q,s] in XX &
f . (the Tran of CRtfsm1 . [q,s]) in XX \ {(the Tran of CRtfsm1 . [q,s])} )
by A23;
A67:
X is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
now assume A68:
f . (the Tran of CRtfsm1 . [q,s]) <> the
Tran of
CRtfsm2 . [(f . q),s]
;
:: thesis: contradiction
XX is
Subset of
(CRtfsm1 -Mealy_union CRtfsm2)
by A2, TARSKI:def 3;
then
(
X = XX or
X misses XX )
by A2, A67, EQREL_1:def 6;
hence
contradiction
by A1, A59, A63, A65, A66, A68, Th79, XBOOLE_0:3;
:: thesis: verum end;
hence
f . (the Tran of CRtfsm1 . q,s) = the
Tran of
CRtfsm2 . (f . q),
s
;
:: thesis: the OFun of CRtfsm1 . q,s = the OFun of CRtfsm2 . (f . q),s
A69:
dom the
OFun of
CRtfsm1 = [:the carrier of CRtfsm1,IAlph:]
by FUNCT_2:def 1;
A70:
dom the
OFun of
CRtfsm2 = [:the carrier of CRtfsm2,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 A69, ZFMISC_1:122
.=
{}
by A61, ZFMISC_1:113
;
then
dom the
OFun of
CRtfsm1 misses dom the
OFun of
CRtfsm2
by XBOOLE_0:def 7;
hence the
OFun of
CRtfsm1 . q,
s =
(the OFun of CRtfsm1 +* the OFun of CRtfsm2) . [q,s]
by A69, FUNCT_4:17
.=
the
OFun of
(CRtfsm1 -Mealy_union CRtfsm2) . [q',s]
by Def24
.=
the
OFun of
(CRtfsm1 -Mealy_union CRtfsm2) . [fq',s]
by A58, Th36
.=
(the OFun of CRtfsm1 +* the OFun of CRtfsm2) . [(f . q),s]
by Def24
.=
the
OFun of
CRtfsm2 . (f . q),
s
by A70, FUNCT_4:14
;
:: thesis: verum
end;
hence
CRtfsm1,CRtfsm2 -are_isomorphic
by A49, A50, Def19; :: thesis: verum