:: Minimization of finite state machines
:: by Miroslava Kaloper and Piotr Rudnicki
::
:: Received November 18, 1994
:: Copyright (c) 1994-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, NAT_1, ARYTM_3, XXREAL_0, CARD_1, XBOOLE_0,
FUNCT_1, FUNCT_2, RELAT_1, EQREL_1, FINSET_1, CARD_3, SETFAM_1, TARSKI,
STRUCT_0, ZFMISC_1, FINSEQ_1, ORDINAL4, FINSEQ_3, ARYTM_1, MCART_1,
LATTICES, INT_1, RELAT_2, FUNCOP_1, FUNCT_4, FSM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, INT_1, SETFAM_1, FINSET_1, STRUCT_0, XTUPLE_0, MCART_1,
DOMAIN_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1,
XXREAL_0, FUNCT_4, FINSEQ_1, FINSEQ_3, EQREL_1;
constructors FUNCT_4, REAL_1, NAT_1, NAT_D, MEMBERED, FUNCOP_1, FINSEQ_3,
BORSUK_1, BINOP_1, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, INT_1, EQREL_1, STRUCT_0, FINSEQ_1, CARD_1,
RELSET_1, XTUPLE_0, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, SETFAM_1, XBOOLE_0;
equalities BINOP_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, SUBSET_1, MCART_1, RELSET_1, NAT_1, INT_1, FINSEQ_1,
FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2, FUNCT_4, EQREL_1,
ZFMISC_1, XBOOLE_0, XBOOLE_1, RELAT_1, XREAL_1, BINOP_1, XXREAL_0,
ORDINAL1;
schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, RECDEF_1, EQREL_1, BINOP_1,
CLASSES1;
begin :: Definitions and terminology for FSM
reserve m, n, i, k for Nat;
definition
let IAlph be set;
struct (1-sorted) FSM over IAlph (# carrier -> set, Tran -> Function of [:
the carrier, IAlph :], the carrier, InitS -> Element of the carrier #);
end;
definition
let IAlph be set, fsm be FSM over IAlph;
mode State of fsm is Element of fsm;
end;
registration
let X be set;
cluster non empty finite for FSM over X;
existence
proof
set A = the non empty finite set,T = the Function of [: A, X :], A,I =the
Element of A;
take S = FSM (# A, T, I #);
thus S is non empty;
thus thesis;
end;
end;
reserve IAlph, OAlph for non empty set,
fsm for non empty FSM over IAlph,
s for Element of IAlph,
w, w1, w2 for FinSequence of IAlph,
q, q9, q1, q2 for State of fsm;
definition
let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let s be Element of IAlph, q be State of fsm;
func s -succ_of q -> State of fsm equals
(the Tran of fsm).[q, s];
correctness;
end;
definition
let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let q be State of fsm;
let w be FinSequence of IAlph;
func (q, w)-admissible -> FinSequence of the carrier of fsm means
:Def2:
it.
1 = q & len it = len w + 1 & for i being Nat st 1 <= i & i <= len w ex wi being
Element of IAlph, qi, qi1 being State of fsm st wi = w.i & qi = it.i & qi1 = it
.(i+1) & wi-succ_of qi = qi1;
existence
proof
set N = len w + 1;
set D = the carrier of fsm;
defpred P[Nat, set, set] means ex wn being Element of IAlph, q9
, q99 being Element of D st w.$1 = wn & q9 = $2 & q99 = $3 & wn-succ_of q9 =
q99;
A1: for n being Nat st 1 <= n & n < N holds for x being Element
of D ex y being Element of D st P[n, x, y]
proof
let n be Nat;
assume
A2: 1 <= n;
assume n < N;
then n <= len w by NAT_1:13;
then n in dom w by A2,FINSEQ_3:25;
then reconsider wn = w.n as Element of IAlph by FINSEQ_2:11;
let x be Element of D;
wn-succ_of x = (the Tran of fsm).[x, wn];
hence thesis;
end;
consider p being FinSequence of D such that
A3: len p = N & (p.1 = q or N = 0) & for n being Nat st 1
<= n & n < N holds P[n, p.n, p.(n+1)] from RECDEF_1:sch 4 (A1);
take p;
thus p.1 = q by A3;
thus len p = len w + 1 by A3;
let i be Nat;
assume
A4: 1 <= i;
assume i <= len w;
then i in NAT & i < N by NAT_1:13,ORDINAL1:def 12;
hence thesis by A3,A4;
end;
uniqueness
proof
let qs1, qs2 be FinSequence of the carrier of fsm such that
A5: qs1.1 = q and
A6: len qs1 = len w + 1 and
A7: for i being Nat st 1 <= i & i <= len w ex wi being Element of
IAlph, qs1i, qs1i1 being State of fsm st wi=w.i & qs1i=qs1.i & qs1i1 = qs1.(i+
1) & wi-succ_of qs1i = qs1i1 and
A8: qs2.1 = q and
A9: len qs2 = len w + 1 and
A10: for i being Nat st 1 <= i & i <= len w ex wi being Element of
IAlph, qs2i, qs2i1 being State of fsm st wi = w.i & qs2i = qs2.i & qs2i1 = qs2
.(i+1) & wi-succ_of qs2i = qs2i1;
defpred P[Nat] means 1<=$1 & $1<=len qs1 implies qs1.$1 = qs2.$1;
A11: now
let k be Nat;
assume
A12: P[k];
thus P[k+1]
proof
assume that
1 <= k+1 and
A13: k+1 <= len qs1;
A14: 0 = k or 0 < k & 0+1 = 1;
per cases by A14,NAT_1:13;
suppose
0 = k;
hence thesis by A5,A8;
end;
suppose
A15: 1 <= k;
A16: k <= len w by A6,A13,XREAL_1:6;
then (ex i1 being Element of IAlph,qs1i,qs1i1 being State of fsm st
i1 = w.k & qs1i = qs1.k & qs1i1 = qs1.(k+1) & i1-succ_of qs1i = qs1i1 )& ex i2
being Element of IAlph,qs2i,qs2i1 being State of fsm st i2 = w.k & qs2i = qs2.k
& qs2i1 = qs2.(k+1) & i2-succ_of qs2i = qs2i1 by A7,A10,A15;
hence thesis by A6,A12,A15,A16,NAT_1:12;
end;
end;
end;
A17: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A17,A11);
hence thesis by A6,A9,FINSEQ_1:14;
end;
end;
theorem Th1:
(q, <*>IAlph)-admissible = <*q*>
proof
set eis = <*>IAlph;
A1: for i being Nat st 1 <= i & i <= len eis ex wi being Element of IAlph,
qi, qi1 being State of fsm st wi=eis.i & qi=<*q*>.i & qi1=<*q*>.(i+1)& wi
-succ_of qi=qi1;
len <*q*> = len eis + 1 & <*q*>.1 = q by FINSEQ_1:40;
hence thesis by A1,Def2;
end;
definition
let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let w be FinSequence of IAlph;
let q1, q2 be State of fsm;
pred q1, w-leads_to q2 means
(q1, w)-admissible.(len w + 1) = q2;
end;
theorem Th2:
q, <*>IAlph-leads_to q
proof
set eis = <*>IAlph;
(q, eis)-admissible = <*q*> by Th1;
hence thesis;
end;
definition
let IAlph be non empty set;
let fsm be non empty FSM over IAlph;
let w be FinSequence of IAlph;
let qseq be FinSequence of the carrier of fsm;
pred qseq is_admissible_for w means
ex q1 being State of fsm st q1 = qseq.1 & (q1, w)-admissible = qseq;
end;
theorem
<*q*> is_admissible_for <*>IAlph
proof
(q, <*>IAlph)-admissible = <*q*> & q = <*q*>.1 by Th1;
hence thesis;
end;
definition
let IAlph, fsm, q, w;
func q leads_to_under w -> State of fsm means
:Def5:
q, w-leads_to it;
existence
proof
len (q, w)-admissible=len w +1 & len w +1 in Seg (len w +1) by Def2,
FINSEQ_1:4;
then len w +1 in dom (q, w)-admissible by FINSEQ_1:def 3;
then reconsider IT =(q,w)-admissible.(len w +1) as Element of fsm by
FINSEQ_2:11;
take IT;
thus thesis;
end;
uniqueness;
end;
theorem
((q, w)-admissible).(len (q, w)-admissible) = q9 iff q, w -leads_to q9
by Def2;
theorem Th5:
for k st 1 <= k & k <= len w1 holds
(q1,w1^w2)-admissible.k = (q1,w1)-admissible.k
proof
set q1w = (q1,w1^w2)-admissible;
set q1w1 = (q1,w1)-admissible;
defpred P[Nat] means 1 <= $1 & $1 <= len w1 implies q1w.$1 = q1w1
.$1;
A1: now
let k be Nat;
assume
A2: P[k];
thus P[k+1]
proof
assume that
1 <= k+1 and
A3: k+1 <= len w1;
A4: 0 = k or 0 < k & 0 + 1= 1;
per cases by A3,A4,NAT_1:13;
suppose
A5: k = 0;
hence q1w.(k+1) = q1 by Def2
.= q1w1.(k+1) by A5,Def2;
end;
suppose
A6: 1 <= k & k <= len w1;
len w1 <= len w1 + len w2 by NAT_1:11;
then k <= len w1 + len w2 by A6,XXREAL_0:2;
then k <= len (w1^w2) by FINSEQ_1:22;
then
A7: ex wk being Element of IAlph,qwk,qwk1 being State of fsm st wk = (
w1^w2).k & qwk = q1w.k & qwk1 = q1w.(k+1) & wk-succ_of qwk = qwk1 by A6,Def2;
(ex w1k being Element of IAlph, qw1k, qw1k1 being State of fsm st
w1k = w1.k & qw1k = q1w1.k & qw1k1 = q1w1.(k+1) & w1k-succ_of qw1k = qw1k1 )& k
in dom w1 by A6,Def2,FINSEQ_3:25;
hence thesis by A2,A6,A7,FINSEQ_1:def 7;
end;
end;
end;
A8: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2 (A8,A1 );
end;
theorem Th6:
q1,w1-leads_to q2 implies (q1,w1^w2)-admissible.(len w1 + 1) = q2
proof
assume
A1: q1,w1-leads_to q2;
set q1w1 = (q1,w1)-admissible;
set q1w = (q1,w1^w2)-admissible;
per cases;
suppose
A2: len w1 = 0;
q1w1.1=q1 & q1w1.(len w1 + 1)=q2 by A1,Def2;
hence thesis by A2,Def2;
end;
suppose
A3: len w1 > 0;
0+1 = 1;
then
A4: 1 <= len w1 by A3,NAT_1:13;
then consider
w1k being Element of IAlph, qw1k, qw1k1 being State of fsm such
that
A5: w1k = w1.(len w1) and
A6: qw1k = q1w1.(len w1) and
A7: qw1k1 = q1w1.((len w1)+1) and
A8: w1k-succ_of qw1k = qw1k1 by Def2;
len (w1^w2) = len w1 + len w2 by FINSEQ_1:22;
then len w1 <= len (w1^w2) by NAT_1:12;
then consider
wk being Element of IAlph,qwk,qwk1 being State of fsm such that
A9: wk = (w1^w2).(len w1) and
A10: qwk = q1w.(len w1) & qwk1 = q1w.((len w1)+1) & wk-succ_of qwk =
qwk1 by A4,Def2;
len w1 in Seg len w1 by A3,FINSEQ_1:3;
then len w1 in dom w1 by FINSEQ_1:def 3;
then wk = w1k by A9,A5,FINSEQ_1:def 7;
hence (q1,w1^w2)-admissible.(len w1 + 1) = qw1k1 by A4,A10,A6,A8,Th5
.= q2 by A1,A7;
end;
end;
theorem Th7:
q1,w1-leads_to q2 implies for k st 1 <= k & k <= len w2 + 1
holds (q1,w1^w2)-admissible.(len w1 + k) = (q2,w2)-admissible.k
proof
set q1w = (q1,w1^w2)-admissible;
set q2w2 = (q2,w2)-admissible;
defpred P[Nat] means 1 <= $1 & $1 <= len w2 + 1 implies q1w.(len
w1 + $1) = q2w2.$1;
assume
A1: q1,w1-leads_to q2;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: 1 <= k & k <= len w2 + 1 implies q1w.(len w1 + k) = q2w2.k;
assume that
1 <= k+1 and
A4: k+1 <= len w2 + 1;
per cases;
suppose
A5: k = 0;
hence q1w.(len w1 + (k+1)) = q2 by A1,Th6
.= q2w2.(k+1) by A5,Def2;
end;
suppose
A6: 0 < k;
A7: k <= len w2 by A4,XREAL_1:6;
A8: 0+1 = 1;
then 1 <= k by A6,NAT_1:13;
then
A9: (ex w2i being Element of IAlph,q2i,q2i1 being State of fsm st w2i =
w2.k & q2i = q2w2.k & q2i1 = q2w2.(k+1) & w2i-succ_of q2i = q2i1 )& k in dom w2
by A7,Def2,FINSEQ_3:25;
len (w1^w2) = len w1 + len w2 by FINSEQ_1:22;
then
A10: len w1 + k <= len (w1^w2) by A7,XREAL_1:7;
1 <= len w1 + k by A6,A8,NAT_1:13;
then
ex wi being Element of IAlph, qi,qi1 being State of fsm st wi = (w1^
w2).(len w1 + k) & qi = q1w.(len w1 + k) & qi1 = q1w.((len w1 + k)+1 ) & wi
-succ_of qi = qi1 by A10,Def2;
hence thesis by A3,A4,A6,A8,A9,FINSEQ_1:def 7,NAT_1:13;
end;
end;
A11: P[0];
thus for n being Nat holds P[n] from NAT_1:sch 2(A11,A2);
end;
theorem Th8:
q1,w1-leads_to q2 implies (q1,w1^w2)-admissible = Del((q1,w1)
-admissible,(len w1 + 1))^(q2,w2)-admissible
proof
set q1w = (q1,w1^w2)-admissible;
set q1w1 = (q1,w1)-admissible;
set q2w2 = (q2,w2)-admissible;
set Dw1 = Del ((q1,w1)-admissible,(len w1+1));
A1: len q1w1 = len w1 + 1 by Def2;
len q1w1 = len w1 + 1 & dom q1w1 = Seg (len q1w1) by Def2,FINSEQ_1:def 3;
then len w1+1 in dom q1w1 by FINSEQ_1:3;
then
A2: ex m be Nat st len q1w1 = m + 1 & len Dw1 = m by FINSEQ_3:104;
A3: len q1w = len (w1^w2) +1 by Def2
.= len w1 + len w2 +1 by FINSEQ_1:22
.= len Dw1 +(len w2 +1) by A2,A1
.=len Dw1 + len q2w2 by Def2
.= len (Dw1^q2w2) by FINSEQ_1:22;
assume
A4: q1,w1-leads_to q2;
now
let k be Nat;
assume
A5: 1 <= k & k <= len q1w;
per cases by A5,NAT_1:13;
suppose
A6: 1 <= k & k <= len w1;
then
A7: k < len w1 + 1 by NAT_1:13;
A8: k in dom Dw1 by A2,A1,A6,FINSEQ_3:25;
thus q1w.k = q1w1.k by A6,Th5
.= Dw1.k by A7,FINSEQ_3:110
.= (Dw1^q2w2).k by A8,FINSEQ_1:def 7;
end;
suppose
A9: len w1+1 <= k & k <= len q1w;
then k <= len Dw1 + len q2w2 by A3,FINSEQ_1:22;
then
A10: (Dw1^q2w2).k = q2w2.(k - len w1) by A2,A1,A9,FINSEQ_1:23;
len w1 + 1 - len w1 <= k - len w1 by A9,XREAL_1:9;
then reconsider i = k - len w1 as Element of NAT by INT_1:3;
A11: k = len w1 + i;
len q1w = len (w1^w2) + 1 by Def2;
then k <= len w1 + len w2 +1 by A9,FINSEQ_1:22;
then k <= len w1 + (len w2 +1);
then
A12: i <= len w2 +1 by A11,XREAL_1:6;
1 <= i by A9,A11,XREAL_1:6;
hence q1w.k = (Dw1^q2w2).k by A4,A11,A12,A10,Th7;
end;
end;
hence thesis by A3,FINSEQ_1:14;
end;
begin :: Mealy and Moore machines and their responses
definition
let IAlph be set, OAlph be non empty set;
struct (FSM over IAlph) Mealy-FSM over IAlph, OAlph (# carrier -> set, Tran
-> Function of [: the carrier, IAlph :], the carrier, OFun -> Function of [:
the carrier, IAlph :], OAlph, InitS -> Element of the carrier #);
struct (FSM over IAlph) Moore-FSM over IAlph, OAlph (# carrier -> set, Tran
-> Function of [: the carrier, IAlph :], the carrier, OFun -> Function of the
carrier, OAlph, InitS -> Element of the carrier #);
end;
registration
let IAlph be set, X be finite non empty set, T be Function of [: X, IAlph :]
, X, I be Element of X;
cluster FSM (# X, T, I #) -> finite non empty;
coherence;
end;
registration
let IAlph be set, OAlph be non empty set, X be finite non empty set, T be
Function of [: X, IAlph :], X, O be Function of [: X, IAlph :], OAlph, I be
Element of X;
cluster Mealy-FSM (# X, T, O, I #) -> finite non empty;
coherence;
end;
registration
let IAlph be set, OAlph be non empty set, X be finite non empty set, T be
Function of [: X, IAlph :], X, O be Function of X, OAlph, I be Element of X;
cluster Moore-FSM (# X, T, O, I #) -> finite non empty;
coherence;
end;
registration
let IAlph be set, OAlph be non empty set;
cluster finite non empty for Mealy-FSM over IAlph, OAlph;
existence
proof
set X = the finite non empty set,T = the Function of [: X, IAlph :], X,O =the
Function of [: X, IAlph :], OAlph,I = the Element of X;
take Mealy-FSM (# X, T, O, I #);
thus thesis;
end;
cluster finite non empty for Moore-FSM over IAlph, OAlph;
existence
proof
set X = the finite non empty set,T = the Function of [: X, IAlph :], X,O =the
Function of X, OAlph,I = the Element of X;
take Moore-FSM (# X, T, O, I #);
thus thesis;
end;
end;
reserve tfsm, tfsm1, tfsm2, tfsm3 for non empty Mealy-FSM over IAlph, OAlph,
sfsm for non empty Moore-FSM over IAlph, OAlph,
qs for State of sfsm,
q, q1, q2 , q3, qa, qb, qc, qa9, qt, q1t, q2t for State of tfsm,
q11, q12 for State of tfsm1,
q21, q22 for State of tfsm2;
definition
let IAlph, OAlph, tfsm, qt, w;
func (qt, w)-response -> FinSequence of OAlph means
:Def6:
len it = len w &
for i st i in dom w holds it.i = (the OFun of tfsm).[(qt, w)-admissible.i, w.i]
;
existence
proof
set qs = (qt, w)-admissible;
deffunc F(Nat) = (the OFun of tfsm).[qs.$1, w.$1];
consider p being FinSequence such that
A1: len p = len w & for i being Nat st i in dom p holds p.i = F(i)
from FINSEQ_1:sch 2;
A2: Seg len w = dom w by FINSEQ_1:def 3;
rng p c= OAlph
proof
let y be object;
assume y in rng p;
then consider x being object such that
A3: x in dom p and
A4: y = p.x by FUNCT_1:def 3;
reconsider x as Nat by A3;
x <= len p by A3,FINSEQ_3:25;
then
A5: x <= len p + 1 by NAT_1:12;
A6: len qs = len p + 1 by A1,Def2;
dom p = Seg len p by FINSEQ_1:def 3;
then reconsider wx = w.x as Element of IAlph by A2,A1,A3,FINSEQ_2:11;
1 <= x by A3,FINSEQ_3:25;
then x in dom qs by A6,A5,FINSEQ_3:25;
then reconsider qsx = qs.x as Element of tfsm by FINSEQ_2:11;
p.x = (the OFun of tfsm).[qsx, wx] by A1,A3;
hence thesis by A4;
end;
then reconsider p9 = p as FinSequence of OAlph by FINSEQ_1:def 4;
dom p = dom w by A1,FINSEQ_3:29;
then for i being Nat st i in dom w holds p9.i = (the OFun of
tfsm ).[qs.i, w.i] by A1;
hence thesis by A1;
end;
uniqueness
proof
let it1, it2 be FinSequence of OAlph;
set qs = (qt, w)-admissible;
assume that
A7: len it1 = len w and
A8: for i being Nat st i in dom w holds it1.i = (the OFun
of tfsm).[qs.i, w.i];
assume that
A9: len it2 = len w and
A10: for i being Nat st i in dom w holds it2.i = (the OFun
of tfsm).[qs.i, w.i];
A11: dom w = dom it1 by A7,FINSEQ_3:29;
now
thus len it1 = len it2 by A7,A9;
let i be Nat;
assume 1 <= i & i <= len it1;
then
A12: i in dom it1 by FINSEQ_3:25;
then it1.i = (the OFun of tfsm).[qs.i, w.i] by A8,A11;
hence it1.i = it2.i by A10,A11,A12;
end;
hence thesis by FINSEQ_1:14;
end;
end;
theorem Th9:
(qt, <*>IAlph)-response = <*>OAlph
proof
len (qt, <*>IAlph)-response = len <*>IAlph by Def6
.= 0;
hence thesis;
end;
definition
let IAlph, OAlph, sfsm, qs, w;
func (qs, w)-response -> FinSequence of OAlph means
:Def7:
len it = len w +
1 & for i st i in Seg (len w + 1) holds it.i = (the OFun of sfsm).((qs, w)
-admissible.i);
existence
proof
set qs9 = (qs, w)-admissible;
deffunc F(Nat) = (the OFun of sfsm).(qs9.$1);
consider p being FinSequence such that
A1: len p = len qs9 & for i being Nat st i in dom p holds p.i = F(i)
from FINSEQ_1:sch 2;
A2: Seg len qs9 = dom qs9 by FINSEQ_1:def 3;
rng p c= OAlph
proof
let y be object;
assume y in rng p;
then consider x being object such that
A3: x in dom p and
A4: y = p.x by FUNCT_1:def 3;
reconsider x as Nat by A3;
dom p = Seg len p by FINSEQ_1:def 3;
then reconsider qsx = qs9.x as State of sfsm by A2,A1,A3,FINSEQ_2:11;
p.x = (the OFun of sfsm).qsx by A1,A3;
hence thesis by A4;
end;
then reconsider p9 = p as FinSequence of OAlph by FINSEQ_1:def 4;
A5: len qs9 = len w + 1 by Def2;
dom p = dom qs9 by A1,FINSEQ_3:29;
then for i being Nat st i in dom qs9 holds p9.i = (the OFun of
sfsm).(qs9.i) by A1;
hence thesis by A2,A1,A5;
end;
uniqueness
proof
let it1, it2 be FinSequence of OAlph;
set qs9 = (qs, w)-admissible;
assume that
A6: len it1 = len w + 1 and
A7: for i being Nat st i in Seg (len w + 1) holds it1.i =
( the OFun of sfsm).(qs9.i);
assume that
A8: len it2 = len w + 1 and
A9: for i being Nat st i in Seg (len w + 1) holds it2.i =
( the OFun of sfsm).(qs9.i);
now
thus len it1 = len it2 by A6,A8;
let i be Nat;
assume 1 <= i & i <= len it1;
then
A10: i in Seg len it1 by FINSEQ_1:1;
then it1.i = (the OFun of sfsm).(qs9.i) by A6,A7;
hence it1.i = it2.i by A6,A9,A10;
end;
hence thesis by FINSEQ_1:14;
end;
end;
theorem Th10:
((qs, w)-response).1 = (the OFun of sfsm).qs
proof
1 <= len w + 1 by NAT_1:12;
then 1 in Seg (len w + 1) by FINSEQ_1:1;
hence ((qs, w)-response).1 = (the OFun of sfsm).((qs, w)-admissible.1) by
Def7
.= (the OFun of sfsm).qs by Def2;
end;
theorem Th11:
q1t,w1-leads_to q2t implies (q1t,w1^w2)-response = (q1t,w1)
-response ^ (q2t,w2)-response
proof
set q1w1 = (q1t,w1)-response, q2w2 = (q2t,w2)-response;
set q1w1w2 = (q1t, w1^w2)-response;
set Dq1w1w2a = Del((q1t,w1)-admissible,(len w1 + 1));
set OF = the OFun of tfsm;
assume
A1: q1t,w1-leads_to q2t;
A2: now
dom (q1t,w1)-admissible =Seg (len (q1t,w1)-admissible)by FINSEQ_1:def 3;
then dom (q1t,w1)-admissible = Seg (len w1 + 1) by Def2;
then len w1 + 1 in dom (q1t,w1)-admissible by FINSEQ_1:3;
then consider m being Nat such that
A3: len (q1t,w1)-admissible = m+1 and
A4: len Dq1w1w2a = m by FINSEQ_3:104;
A5: m+1 = len w1 + 1 by A3,Def2;
A6: len q1w1 = len w1 by Def6;
let k be Nat;
assume that
A7: 1 <= k and
A8: k <= len q1w1w2;
per cases by A7,A8,NAT_1:13;
suppose
A9: 1 <= k & k <= len q1w1;
then
A10: k <= len w1 by Def6;
then
A11: k in dom w1 by A9,FINSEQ_3:25;
A12: k in dom Dq1w1w2a by A4,A5,A9,A10,FINSEQ_3:25;
A13: k < len w1 + 1 by A10,NAT_1:13;
A14: k in dom q1w1 by A9,FINSEQ_3:25;
k <= len (w1^w2) by A8,Def6;
then k in dom (w1^w2) by A7,FINSEQ_3:25;
hence q1w1w2.k = OF.[(q1t,w1^w2)-admissible.k,(w1^w2).k] by Def6
.= OF.[(Dq1w1w2a ^ (q2t,w2)-admissible).k,(w1^w2).k] by A1,Th8
.= OF.[Dq1w1w2a.k,(w1^w2).k] by A12,FINSEQ_1:def 7
.= OF.[Dq1w1w2a.k,w1.k] by A11,FINSEQ_1:def 7
.= OF.[(q1t,w1)-admissible.k, w1.k] by A13,FINSEQ_3:110
.= (q1t,w1)-response.k by A11,Def6
.= ((q1t,w1)-response ^ (q2t,w2)-response).k by A14,FINSEQ_1:def 7;
end;
suppose
A15: len q1w1 + 1 <= k & k <= len q1w1w2;
then
A16: len q1w1 + 1 - len q1w1 <= k - len q1w1 by XREAL_1:9;
then reconsider p = k - len q1w1 as Element of NAT by INT_1:3;
A17: len q1w1w2 = len (w1^w2) by Def6
.= len w1 + len w2 by FINSEQ_1:22;
then k <= len q1w1 + len w2 by A15,Def6;
then k - len q1w1 <= len q1w1 + len w2 - len q1w1 by XREAL_1:9;
then
A18: p in dom w2 by A16,FINSEQ_3:25;
A19: len Dq1w1w2a + 1 <= k by A4,A5,A15,Def6;
A20: len w1 + 1 <= k by A15,Def6;
A21: len q1w1w2 = len (w1^w2) by Def6
.= len w1 + len w2 by FINSEQ_1:22
.= len q1w1 + len w2 by Def6
.= len q1w1 + len q2w2 by Def6;
then
A22: (q1w1^q2w2).k = (q2t,w2)-response.p by A15,FINSEQ_1:23
.= OF.[(q2t,w2)-admissible.p,w2.p] by A18,Def6
.= OF.[(q2t,w2)-admissible.(k-len w1),w2.(k-len q1w1)] by Def6
.= OF.[(q2t,w2)-admissible.(k-len w1),w2.(k-len w1)] by Def6;
len w2 <= len w2 + 1 by NAT_1:11;
then
A23: len Dq1w1w2a + len w2 <= len Dq1w1w2a + (len w2 +1) by XREAL_1:6;
k <= len Dq1w1w2a + len w2 by A4,A5,A6,A15,A21,Def6;
then k <= len Dq1w1w2a + (len w2 + 1) by A23,XXREAL_0:2;
then
A24: k <= len Dq1w1w2a + len (q2t,w2) -admissible by Def2;
k <= len (w1^w2) by A8,Def6;
then k in dom (w1^w2) by A7,FINSEQ_3:25;
then q1w1w2.k = OF.[(q1t,w1^w2)-admissible.k,(w1^w2).k] by Def6
.= OF.[( Del((q1t,w1)-admissible,(len w1 + 1)) ^ (q2t,w2)-admissible
).k, (w1^w2).k] by A1,Th8
.= OF.[(q2t,w2)-admissible.(k - len Dq1w1w2a),(w1^w2).k] by A19,A24,
FINSEQ_1:23
.= OF.[(q2t,w2)-admissible.(k - len w1 ),w2.(k-len w1)] by A4,A5,A15
,A17,A20,FINSEQ_1:23;
hence q1w1w2.k = (q1w1 ^ q2w2).k by A22;
end;
end;
len q1w1w2 = len (w1^w2) by Def6
.= len w1 + len w2 by FINSEQ_1:22
.= len q1w1 + len w2 by Def6
.= len q1w1 + len q2w2 by Def6
.= len (q1w1 ^ q2w2) by FINSEQ_1:22;
hence thesis by A2,FINSEQ_1:14;
end;
theorem Th12:
q11, w1 -leads_to q12 & q21, w1 -leads_to q22 & (q12,w2)
-response <> (q22,w2)-response implies (q11,w1^w2)-response <> (q21,w1^w2)
-response
proof
assume that
A1: q11, w1 -leads_to q12 and
A2: q21, w1 -leads_to q22 and
A3: (q12,w2)-response <> (q22,w2)-response;
set r12 = (q12,w2)-response, r22 = (q22,w2)-response;
A4: len r22 = len w2 by Def6;
set w = w1 ^ w2;
set r1w1 = (q11,w1)-response, r2w1 = (q21,w1)-response;
assume
A5: (q11,w1^w2)-response = (q21,w1^w2)-response;
set r21 = (q21,w)-response;
A6: r21 = r2w1 ^ r22 by A2,Th11;
set r11 = (q11,w)-response;
A7: r11 = r1w1 ^ r12 by A1,Th11;
A8: len r1w1 = len w1 by Def6;
A9: len r12 = len w2 by Def6;
then
A10: dom w2 = Seg len r12 by FINSEQ_1:def 3;
then dom w2 = dom r12 by FINSEQ_1:def 3;
then consider j being Nat such that
A11: j in dom w2 and
A12: r12.j <> r22.j by A3,A9,A4,FINSEQ_2:9;
A13: len r2w1 = len w1 by Def6;
j in dom r12 by A10,A11,FINSEQ_1:def 3;
then
A14: r11.(len w1 + j)=r12.j by A8,A7,FINSEQ_1:def 7;
j in dom r22 by A9,A4,A10,A11,FINSEQ_1:def 3;
hence contradiction by A5,A13,A12,A6,A14,FINSEQ_1:def 7;
end;
reserve OAlphf for finite non empty set,
tfsmf for finite non empty Mealy-FSM over IAlph, OAlphf,
sfsmf for finite non empty Moore-FSM over IAlph, OAlphf;
definition
let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph, OAlph;
let sfsm be non empty Moore-FSM over IAlph, OAlph;
pred tfsm is_similar_to sfsm means
for tw being FinSequence of IAlph holds
<*(the OFun of sfsm).(the InitS of sfsm)*>^((the InitS of tfsm, tw)-response) =
(the InitS of sfsm, tw)-response;
end;
theorem
for sfsm being non empty finite Moore-FSM over IAlph, OAlph ex tfsm
being non empty finite Mealy-FSM over IAlph, OAlph st tfsm is_similar_to sfsm
proof
let sfsm be non empty finite Moore-FSM over IAlph, OAlph;
set S = the carrier of sfsm, T = the Tran of sfsm;
set sOF = the OFun of sfsm, IS = the InitS of sfsm;
deffunc F(Element of S,Element of IAlph) = sOF.(T.[$1, $2]);
consider tOF being Function of [: S, IAlph:], OAlph such that
A1: for q being Element of S, s be Element of IAlph holds tOF.(q, s) = F
(q,s) from BINOP_1:sch 4;
take tfsm = Mealy-FSM (# S, T, tOF, IS #);
let tw be FinSequence of IAlph;
set tIS = the InitS of tfsm;
set twa = (tIS, tw)-admissible;
set swa = (IS, tw)-admissible;
defpred P[Nat] means $1 in Seg (len tw + 1) implies twa.$1 = swa.
$1;
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A3: i in Seg (len tw + 1) implies twa.i = swa.i;
assume (i+1) in Seg (len tw + 1);
then
A4: i+1 <= len tw + 1 by FINSEQ_1:1;
per cases by A4,XREAL_1:6;
suppose
A5: i = 0;
twa.1=the InitS of tfsm by Def2;
hence thesis by A5,Def2;
end;
suppose
A6: i > 0 & i <= len tw;
then
A7: i<=len tw + 1 by NAT_1:13;
A8: 0+1=1 implies 1 <= i & i <= len tw by A6,NAT_1:13;
then (ex twi being Element of IAlph, tqi, tqi1 being Element of tfsm st
twi = tw.i & tqi = twa.i & tqi1 = twa.(i+1) & twi-succ_of tqi = tqi1 )& ex swi
being Element of IAlph, sqi, sqi1 being Element of sfsm st swi = tw.i & sqi =
swa.i & sqi1 = swa.(i+1) & swi-succ_of sqi = sqi1 by Def2;
hence thesis by A3,A8,A7,FINSEQ_1:1;
end;
end;
A9: P[0] by FINSEQ_1:1;
A10: for i being Nat holds P[i] from NAT_1:sch 2( A9, A2 );
now
thus len (<*sOF.IS*>^((tIS, tw)-response)) = len <*sOF.IS*> + len ((
tIS, tw)-response) by FINSEQ_1:22
.= 1+len ((tIS, tw)-response) by FINSEQ_1:40
.=len tw +1 by Def6;
then
A11: dom (<*sOF.IS*>^((tIS, tw)-response)) = Seg (len tw + 1) by FINSEQ_1:def 3
;
thus len ((IS, tw)-response) = len tw + 1 by Def7;
let i be Nat;
assume
A12: i in dom (<*sOF.IS*>^((tIS, tw)-response));
then
A13: 1 <= i by A11,FINSEQ_1:1;
A14: i <= len tw + 1 by A11,A12,FINSEQ_1:1;
per cases by A13,XXREAL_0:1;
suppose
A15: i = 1;
then i in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then i in dom <*sOF.IS*> by FINSEQ_1:38;
hence (<*sOF.IS*>^((tIS, tw)-response)).i = <*sOF.IS*>.i by
FINSEQ_1:def 7
.= sOF.IS by A15
.= ((IS, tw)-response).i by A15,Th10;
end;
suppose
1 < i;
then consider j being Element of NAT such that
A16: j = i - 1 and
A17: 1 <= j by INT_1:51;
A18: i = j + 1 by A16;
then
A19: j <= len tw by A14,XREAL_1:6;
then consider
swj being Element of IAlph, swaj, swai being Element of sfsm
such that
A20: swj = tw.j & swaj = swa.j and
A21: swai = swa.(j+1) & swj-succ_of swaj = swai by A17,Def2;
A22: j in Seg len tw by A17,A19,FINSEQ_1:1;
then
A23: j in dom tw by FINSEQ_1:def 3;
j <= len tw + 1 by A19,NAT_1:12;
then
A24: j in Seg (len tw + 1) by A17,FINSEQ_1:1;
len ((tIS, tw)-response) = len tw by Def6;
then len <*sOF.IS*> = 1 & j in dom ((tIS, tw)-response) by A22,
FINSEQ_1:40,def 3;
then (<*sOF.IS*>^((tIS, tw)-response)).i = (tIS, tw)-response.j by A18,
FINSEQ_1:def 7
.= (the OFun of tfsm).[(tIS, tw)-admissible.j, tw.j] by A23,Def6
.= tOF.((IS, tw)-admissible.j, tw.j) by A10,A24
.= sOF.(T.(swaj, swj)) by A1,A20
.= (IS, tw)-response.i by A11,A12,A16,A21,Def7;
hence (<*sOF.IS*>^((tIS, tw)-response)).i = (IS, tw)-response.i;
end;
end;
hence thesis by FINSEQ_2:9;
end;
theorem
ex sfsmf st tfsmf is_similar_to sfsmf
proof
set S = the carrier of tfsmf, T = the Tran of tfsmf;
set tOF = the OFun of tfsmf, IS = the InitS of tfsmf;
set sS = [: S, OAlphf :];
deffunc F(Element of sS,Element of IAlph) = [ T.[$1`1, $2], tOF.[$1`1, $2]];
consider sT being Function of [:sS, IAlph:], sS such that
A1: for q being Element of sS, s being Element of IAlph holds sT.(q, s)
= F(q,s) from BINOP_1:sch 4;
set sSs = sS, sTs = sT;
set r0 = the Element of OAlphf;
deffunc F(Element of S,Element of OAlphf) = $2;
consider sOF being Function of sS, OAlphf such that
A2: for q being Element of S, r being Element of OAlphf holds sOF.(q, r)
= F(q,r) from BINOP_1:sch 4;
set sI = [IS, r0];
reconsider sOFs = sOF as Function of sSs, OAlphf;
reconsider sfsmf = Moore-FSM (# sSs, sTs, sOFs, sI #) as finite non empty
Moore-FSM over IAlph, OAlphf;
take sfsmf;
reconsider SI = sI as Element of sfsmf;
thus tfsmf is_similar_to sfsmf
proof
let tw be FinSequence of IAlph;
set twa = (the InitS of tfsmf, tw)-admissible;
set swa = (the InitS of sfsmf, tw)-admissible;
defpred P[Nat] means $1 in Seg (len tw + 1) implies twa.$1 = (
swa.$1)`1;
A3: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A4: P[i];
assume i+1 in Seg (len tw +1);
then
A5: i+1 <= len tw +1 by FINSEQ_1:1;
per cases by A5,XREAL_1:6;
suppose
A6: i = 0;
twa.1 = IS by Def2
.= [IS, r0]`1
.= (swa.1)`1 by Def2;
hence thesis by A6;
end;
suppose
A7: i > 0 & i <= len tw;
then
A8: i <= len tw + 1 by NAT_1:13;
A9: 0+1=1 implies 1 <= i & i <= len tw by A7,NAT_1:13;
then
A10: ex twi being Element of IAlph, tqi, tqi1 being Element of tfsmf st
twi = tw.i & tqi = twa.i & tqi1 = twa.(i+1) & twi-succ_of tqi = tqi1
by Def2;
consider swi being Element of IAlph, sqi, sqi1 being Element of sfsmf
such that
A11: swi = tw.i & sqi = swa.i & sqi1 = swa.(i+1) and
A12: swi-succ_of sqi = sqi1 by A9,Def2;
sqi1 = sT.(sqi, swi) by A12
.= [T.[sqi`1, swi], tOF.[sqi`1, swi]] by A1;
hence thesis by A4,A9,A8,A10,A11,FINSEQ_1:1;
end;
end;
A13: P[0] by FINSEQ_1:1;
A14: for i being Nat holds P[i] from NAT_1:sch 2 ( A13, A3 );
now
thus len (<*sOF.sI*>^((IS, tw)-response)) = len <*sOF.sI*> + len ((
IS, tw)-response) by FINSEQ_1:22
.= 1 + len ((IS, tw)-response) by FINSEQ_1:40
.= len tw + 1 by Def6;
then
A15: dom (<*sOF.sI*>^((IS, tw)-response)) = Seg (len tw + 1) by FINSEQ_1:def 3
;
thus len ((SI, tw)-response) = len tw + 1 by Def7;
let i be Nat;
assume
A16: i in dom (<*sOF.sI*>^((IS, tw)-response));
then
A17: 1 <= i by A15,FINSEQ_1:1;
A18: i <= len tw + 1 by A15,A16,FINSEQ_1:1;
per cases by A17,XXREAL_0:1;
suppose
A19: i = 1;
then i in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then i in dom <*sOF.sI*> by FINSEQ_1:38;
hence (<*sOF.sI*>^((IS, tw)-response)).i = <*sOF.sI*>.i by
FINSEQ_1:def 7
.= sOF.sI by A19
.= ((SI, tw)-response).i by A19,Th10;
end;
suppose
1 < i;
then consider j being Element of NAT such that
A20: j = i-1 and
A21: 1 <= j by INT_1:51;
A22: i = j + 1 by A20;
then
A23: j <= len tw by A18,XREAL_1:6;
then consider
swj being Element of IAlph, swaj, swai being Element of sfsmf
such that
A24: swj = tw.j and
A25: swaj = swa.j and
A26: swai = swa.(j+1) & swj-succ_of swaj = swai by A21,Def2;
j <= len tw + 1 by A23,NAT_1:12;
then
A27: j in Seg (len tw + 1) by A21,FINSEQ_1:1;
reconsider swaj as Element of sS;
A28: j in Seg len tw by A21,A23,FINSEQ_1:1;
then
A29: j in dom tw by FINSEQ_1:def 3;
len ((IS, tw)-response) = len tw by Def6;
then len <*sOF.sI*> = 1 & j in dom ((IS, tw)-response) by A28,
FINSEQ_1:40,def 3;
hence
(<*sOF.sI*>^((IS, tw)-response)).i = ((IS, tw)-response).j by A22,
FINSEQ_1:def 7
.= tOF.((IS, tw)-admissible.j, tw.j) by A29,Def6
.= tOF.(swaj`1, tw.j) by A14,A27,A25
.= sOF.(T.(swaj`1, swj), tOF.(swaj`1, swj)) by A2,A24
.= sOF.(sT.(swaj, swj)) by A1
.= (SI, tw)-response.i by A15,A16,A20,A26,Def7;
end;
end;
hence thesis by FINSEQ_2:9;
end;
end;
begin :: Equivalence of states and machines (for Mealy machines)
definition
let IAlph, OAlph be non empty set, tfsm1, tfsm2 be non empty Mealy-FSM over
IAlph, OAlph;
pred tfsm1, tfsm2-are_equivalent means
for w being FinSequence of
IAlph holds (the InitS of tfsm1,w)-response = (the InitS of tfsm2,w)-response;
reflexivity;
symmetry;
end;
theorem Th15:
tfsm1, tfsm2-are_equivalent & tfsm2, tfsm3-are_equivalent
implies tfsm1, tfsm3-are_equivalent
proof
assume that
A1: tfsm1, tfsm2-are_equivalent and
A2: tfsm2, tfsm3-are_equivalent;
let w1 be FinSequence of IAlph;
set IS3 = the InitS of tfsm3;
set IS1 = the InitS of tfsm1, IS2 = the InitS of tfsm2;
thus (IS1, w1)-response = (IS2, w1)-response by A1
.= (IS3, w1)-response by A2;
end;
definition
let IAlph, OAlph, tfsm, qa, qb;
pred qa, qb-are_equivalent means
for w holds (qa, w)-response = (qb, w)-response;
reflexivity;
symmetry;
end;
theorem
q1, q2-are_equivalent & q2, q3-are_equivalent implies q1, q3 -are_equivalent
proof
assume that
A1: q1, q2-are_equivalent and
A2: q2, q3-are_equivalent;
thus q1, q3-are_equivalent
proof
let w be FinSequence of IAlph;
(q1, w)-response = (q2, w)-response by A1;
hence thesis by A2;
end;
end;
theorem Th17:
qa9 = (the Tran of tfsm).[qa, s] implies for i st i in Seg (len
w + 1) holds (qa, <*s*>^w)-admissible.(i+1) = (qa9, w)-admissible.i
proof
set sw = (<*s*>^w);
A1: len sw = len <*s*> + len w by FINSEQ_1:22
.= len w + 1 by FINSEQ_1:40;
defpred P[Nat] means $1 in Seg (len w + 1) implies (qa, <*s*>^w)
-admissible.($1+1) = (qa9, w)-admissible.$1;
A2: sw.1 = s by FINSEQ_1:41;
assume
A3: qa9 = (the Tran of tfsm).[qa, s];
A4: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat;
assume
A5: j in Seg (len w + 1) implies (qa, <*s*>^w)-admissible.(j+1) = (qa9
, w)-admissible.j;
assume
A6: j+1 in Seg (len w + 1);
per cases;
suppose
A7: j = 0;
set aadm = (qa, sw)-admissible;
1 <= len sw by A1,A6,A7,FINSEQ_1:1;
then
A8: ex swi1 being Element of IAlph, a1, a11 being Element of tfsm st
swi1 = sw.1 & a1 = aadm.1 & a11 = aadm.(1+1) & swi1-succ_of a1 = a11 by
Def2;
(qa9, w)-admissible.1 = qa9 by Def2;
hence thesis by A3,A2,A7,A8,Def2;
end;
suppose
A9: j <> 0;
set aadm = (qa, sw)-admissible, aadm9 = (qa9, w)-admissible;
A10: j in Seg len w by A6,A9,FINSEQ_1:61;
then
A11: j <= len w by FINSEQ_1:1;
then 1 <= j+1 & j+1 <= len sw by A1,NAT_1:12,XREAL_1:7;
then
A12: ex swj1 being Element of IAlph, aj1, aj11 being Element of tfsm st
swj1 = sw.(j+1) & aj1 = aadm.(j+1) & aj11 = aadm.(j+1+1) & swj1 -succ_of aj1 =
aj11 by Def2;
1 <= j by A10,FINSEQ_1:1;
then
A13: ex wj being Element of IAlph, aj9, aj19 being Element of tfsm st wj
= w.j & aj9 = aadm9.j & aj19 = aadm9.(j+1) & wj-succ_of aj9 = aj19 by A11,Def2;
j in dom w by A10,FINSEQ_1:def 3;
hence thesis by A5,A6,A9,A12,A13,FINSEQ_1:61,FINSEQ_3:103;
end;
end;
A14: P[0] by FINSEQ_1:1;
thus for i being Nat holds P[i] from NAT_1:sch 2(A14,A4);
end;
theorem Th18:
qa9 = (the Tran of tfsm).[qa, s] implies (qa, <*s*>^w)-response
= <*(the OFun of tfsm).[qa, s]*>^(qa9, w)-response
proof
set OF=the OFun of tfsm;
set asresp = OF.[qa, s];
A1: len (<*s*>^w) = len <*s*> + len w by FINSEQ_1:22
.= 1+len w by FINSEQ_1:40;
assume
A2: qa9 = (the Tran of tfsm).[qa, s];
now
thus len ((qa, <*s*>^w)-response) = 1 + len w by A1,Def6;
then
A3: dom (qa, <*s*>^w)-response = Seg (1 + len w) by FINSEQ_1:def 3;
thus
A4: len (<*asresp*>^(qa9, w)-response) = len <*asresp*> + len ((qa9,
w)-response) by FINSEQ_1:22
.= 1 + len ((qa9, w)-response) by FINSEQ_1:40
.= 1 + len w by Def6;
let j be Nat;
assume
A5: j in dom (qa, <*s*>^w)-response;
then
A6: 1 <= j by A3,FINSEQ_1:1;
A7: j <= 1 + len w by A3,A5,FINSEQ_1:1;
A8: j in dom(<*s*>^w) by A1,A3,A5,FINSEQ_1:def 3;
per cases by A6,XXREAL_0:1;
suppose
A9: j = 1;
thus (qa, <*s*>^w)-response.j = OF.[(qa, <*s*>^w)-admissible.j, (<*s*>^w
).j] by A8,Def6
.= OF.[qa,(<*s*>^w).j] by A9,Def2
.= asresp by A9,FINSEQ_1:41
.= (<*asresp*>^(qa9, w)-response).j by A9,FINSEQ_1:41;
end;
suppose
A10: j > 1;
then consider i being Element of NAT such that
A11: i = j - 1 and
A12: 1 <= i by INT_1:51;
j <= len w + 1 by A3,A5,FINSEQ_1:1;
then j - 1 <= len w + 1-1 by XREAL_1:9;
then
A13: i in Seg len w by A11,A12,FINSEQ_1:1;
then
A14: i in Seg (1 + len w) by FINSEQ_2:8;
i+1 in Seg (1 + len w) by A13,FINSEQ_1:60;
then
A15: i+1 in dom(<*s*>^w) by A1,FINSEQ_1:def 3;
A16: i in dom w by A13,FINSEQ_1:def 3;
len <*asresp*> = 1 by FINSEQ_1:40;
then (<*asresp*>^((qa9, w)-response)).j = (qa9, w)-response.i by A4,A7
,A10,A11,FINSEQ_1:24
.= OF.[(qa9, w)-admissible.i, w.i] by A16,Def6
.= OF.[(qa9, w)-admissible.i, (<*s*>^w).(i+1)] by A16,FINSEQ_3:103
.= OF.[(qa, <*s*>^w)-admissible.(i+1), (<*s*>^w).(i+1)]by A2,A14,Th17
.= ((qa, <*s*>^w)-response).j by A11,A15,Def6;
hence (qa, <*s*>^w)-response.j = (<*asresp*>^(qa9, w)-response).j;
end;
end;
hence thesis by FINSEQ_2:9;
end;
theorem Th19:
qa, qb-are_equivalent iff for s holds (the OFun of tfsm).[qa, s]
= (the OFun of tfsm).[qb, s] & (the Tran of tfsm).[qa, s], (the Tran of tfsm).[
qb, s]-are_equivalent
proof
set OF= the OFun of tfsm;
hereby
assume
A1: qa, qb-are_equivalent;
let s be Element of IAlph;
set qa9 = (the Tran of tfsm).[qa, s];
set qb9 = (the Tran of tfsm).[qb, s];
len <*s*> = 1 by FINSEQ_1:40;
then
A2: 1 in dom <*s*> by FINSEQ_3:25;
thus
A3: OF.[qa, s] = OF.[(qa, <*s*>)-admissible.1, s] by Def2
.= OF.[(qa, <*s*>)-admissible.1, <*s*>.1]
.= (qa, <*s*>)-response.1 by A2,Def6
.= (qb, <*s*>)-response.1 by A1
.= OF.[(qb, <*s*>)-admissible.1, <*s*>.1] by A2,Def6
.= OF.[(qb,<*s*>)-admissible.1,s]
.= OF.[qb,s] by Def2;
now
let w be FinSequence of IAlph;
A4: (qa, <*s*>^w)-response = <*OF.[qa,s]*>^(qa9, w)-response & (qb, <*s
*>^w) -response = <*OF.[qb,s]*>^(qb9, w)-response by Th18;
(qa, <*s*>^w)-response = (qb, <*s*>^w)-response by A1;
hence (qa9, w)-response = (qb9, w)-response by A3,A4,FINSEQ_1:33;
end;
hence
(the Tran of tfsm).[qa, s], (the Tran of tfsm).[qb, s]-are_equivalent;
end;
assume
A5: for s being Element of IAlph holds (the OFun of tfsm).[qa, s] = (the
OFun of tfsm).[qb, s] & (the Tran of tfsm).[qa, s], (the Tran of tfsm).[qb, s]
-are_equivalent;
let w be FinSequence of IAlph;
per cases;
suppose
A6: w = <*>IAlph;
hence (qa, w)-response = <*>OAlph by Th9
.= (qb, w)-response by A6,Th9;
end;
suppose
w <> {};
then consider
s being Element of IAlph, wt being FinSequence of IAlph such that
s = w.1 and
A7: w = <*s*>^wt by FINSEQ_3:102;
set bsresp =(the OFun of tfsm).[qb,s];
set asresp =(the OFun of tfsm).[qa,s];
set qb9 = (the Tran of tfsm).[qb, s];
set qa9 = (the Tran of tfsm).[qa, s];
qa9, qb9-are_equivalent by A5;
then
A8: (qa9, wt)-response = (qb9, wt)-response;
thus (qa, w)-response = <*asresp*>^(qa9, wt)-response by A7,Th18
.= <*bsresp*>^(qb9,wt)-response by A5,A8
.= (qb,w)-response by A7,Th18;
end;
end;
theorem
qa, qb-are_equivalent implies for w, i st i in dom w ex qai, qbi being
State of tfsm st qai = (qa, w)-admissible.i & qbi = ((qb, w)-admissible.i) &
qai, qbi-are_equivalent
proof
assume
A1: qa, qb-are_equivalent;
let w be FinSequence of IAlph;
defpred P[Nat] means $1 in Seg len w implies ex qai, qbi being
Element of tfsm st qai = (qa, w)-admissible.$1 & qbi = ((qb, w)-admissible.$1)
& qai, qbi-are_equivalent;
A2: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A3: i in Seg len w implies ex qai, qbi being Element of tfsm st qai =
(qa, w)-admissible.i & qbi = (qb, w)-admissible.i & qai, qbi-are_equivalent;
A4: i=0 or 0<i & 0+1=1;
assume (i+1) in Seg len w;
then i+1<=len w by FINSEQ_1:1;
then
A5: 0 = i or 1 <= i & i <= len w by A4,NAT_1:13;
per cases by A5,FINSEQ_1:1;
suppose
A6: i = 0;
reconsider qai = (qa,w)-admissible.1, qbi = (qb,w)-admissible.1 as
Element of tfsm by Def2;
take qai, qbi;
thus qai = (qa, w)-admissible.(i+1) by A6;
thus qbi = (qb, w)-admissible.(i+1) by A6;
qai = qa by Def2;
hence thesis by A1,Def2;
end;
suppose
A7: i in Seg len w;
then
A8: 1 <= i & i <= len w by FINSEQ_1:1;
then consider
wi being Element of IAlph, qai9, qai19 being Element of tfsm
such that
A9: wi = w.i & qai9 = (qa, w)-admissible.i and
A10: qai19 = (qa, w)-admissible.(i+1) and
A11: wi-succ_of qai9 = qai19 by Def2;
take qai19;
consider wi9 being Element of IAlph, qbi9, qbi19 being Element of tfsm
such that
A12: wi9 = w.i & qbi9 = (qb, w)-admissible.i and
A13: qbi19 = (qb, w)-admissible.(i+1) and
A14: wi9-succ_of qbi9 = qbi19 by A8,Def2;
take qbi19;
thus qai19 = (qa, w)-admissible.(i+1) by A10;
thus qbi19 = (qb, w)-admissible.(i+1) by A13;
thus thesis by A3,A7,A9,A11,A12,A14,Th19;
end;
end;
A15: Seg len w = dom w by FINSEQ_1:def 3;
A16: P[0] by FINSEQ_1:1;
for i being Nat holds P[i] from NAT_1:sch 2 (A16, A2);
hence thesis by A15;
end;
definition
let IAlph, OAlph,tfsm, qa, qb;
let k be Nat;
pred k-equivalent qa, qb means
for w st len w<=k holds (qa,w) -response = (qb,w)-response;
end;
theorem Th21:
for k be Nat holds k-equivalent qa, qa;
theorem Th22:
for k be Nat st k-equivalent qa, qb holds k-equivalent qb, qa;
theorem Th23:
for k be Nat st k-equivalent qa, qb & k-equivalent qb, qc holds
k-equivalent qa, qc
proof
let k be Nat;
assume that
A1: k-equivalent qa, qb and
A2: k-equivalent qb, qc;
thus k-equivalent qa, qc
proof
let w be FinSequence of IAlph;
assume
A3: len w <= k;
then (qa, w)-response = (qb, w)-response by A1;
hence thesis by A2,A3;
end;
end;
theorem
qa,qb-are_equivalent implies k-equivalent qa,qb;
theorem Th25:
0-equivalent qa, qb
proof
let w be FinSequence of IAlph;
assume len w <= 0;
then
A1: w = <*>IAlph;
hence (qa,w)-response=<*>OAlph by Th9
.=(qb,w)-response by A1,Th9;
end;
theorem Th26:
for k, m be Nat st (k+m)-equivalent qa, qb holds k-equivalent qa , qb
proof
let k, m be Nat;
assume
A1: (k+m)-equivalent qa, qb;
let w be FinSequence of IAlph;
A2: k <= k+m by NAT_1:11;
assume len w <= k;
then len w <= k+m by A2,XXREAL_0:2;
hence thesis by A1;
end;
theorem Th27:
for k be Nat st 1 <= k holds (k-equivalent qa, qb iff 1
-equivalent qa, qb & for s being Element of IAlph, k1 being Nat st
k1 = k - 1 holds k1-equivalent (the Tran of tfsm).[qa, s], (the Tran of tfsm).[
qb, s])
proof
let k be Nat;
set OF = the OFun of tfsm;
assume
A1: 1 <= k;
hereby
assume
A2: k-equivalent qa, qb;
thus
A3: 1-equivalent qa, qb
by A1,XXREAL_0:2,A2;
let s be Element of IAlph, k1 be Nat such that
A4: k1 = k - 1;
set qb9 = (the Tran of tfsm).[qb, s];
set qa9 = (the Tran of tfsm).[qa, s];
thus k1-equivalent qa9, qb9
proof
let w be FinSequence of IAlph;
set sw = <*s*>^w;
A5: len <*s*> = 1 by FINSEQ_1:40;
assume len w <= k1;
then
A6: len w + 1 <= k1 + 1 by XREAL_1:7;
len (<*s*>^w) = len <*s*> + len w by FINSEQ_1:22
.=1+ len w by FINSEQ_1:40;
then
A7: (qa, sw)-response = (qb, sw)-response by A2,A4,A6;
A8: (qa, sw)-response = <*OF.[qa, s]*>^(qa9, w)-response & (qb, sw)
-response = <*OF.[qb, s]*>^(qb9, w)-response by Th18;
0+1 in Seg (0+1) by FINSEQ_1:4;
then
A9: 1 in dom <*s*> by A5,FINSEQ_1:def 3;
OF.[qa, s] = OF.[(qa, <*s*>)-admissible.1, s] by Def2
.= OF.[(qa, <*s*>)-admissible.1, <*s*>.1]
.= (qa, <*s*>)-response.1 by A9,Def6
.= (qb, <*s*>)-response.1 by A3,A5
.= OF.[(qb, <*s*>)-admissible.1, <*s*>.1] by A9,Def6
.= OF.[(qb, <*s*>)-admissible.1, s]
.= OF.[qb, s] by Def2;
hence thesis by A8,A7,FINSEQ_1:33;
end;
end;
assume that
A10: 1-equivalent qa, qb and
A11: for s being Element of IAlph, k1 being Nat st k1 = k - 1
holds k1-equivalent (the Tran of tfsm).[qa, s],(the Tran of tfsm).[qb, s];
thus k-equivalent qa, qb
proof
let w be FinSequence of IAlph such that
A12: len w <= k;
per cases;
suppose
A13: w = <*>IAlph;
hence (qa,w)-response=<*>OAlph by Th9
.=(qb,w)-response by A13,Th9;
end;
suppose
w is non empty;
then consider
s being Element of IAlph, w9 being FinSequence of IAlph such
that
s = w.1 and
A14: w = <*s*>^w9 by FINSEQ_3:102;
reconsider k1 = k-1 as Element of NAT by A1,INT_1:5;
A15: len <*s*> = 1 by FINSEQ_1:40;
len w = len <*s*> + len w9 by A14,FINSEQ_1:22
.= len w9 + 1 by FINSEQ_1:40;
then
A16: len w9 + 1 - 1 <= k1 by A12,XREAL_1:9;
0+1 in Seg (0+1) by FINSEQ_1:4;
then
A17: 1 in dom <*s*> by A15,FINSEQ_1:def 3;
set qa9 = (the Tran of tfsm).[qa, s], qb9 = (the Tran of tfsm).[qb, s];
A18: (qa, w)-response = <*OF.[qa, s]*>^(qa9, w9)-response & (qb, w)
-response = <* OF.[qb, s]*>^(qb9, w9)-response by A14,Th18;
A19: k1-equivalent qa9, qb9 by A11;
OF.[qa, s] = OF.[(qa, <*s*>)-admissible.1, s] by Def2
.= OF.[(qa, <*s*>)-admissible.1, <*s*>.1]
.= (qa, <*s*>)-response.1 by A17,Def6
.= (qb, <*s*>)-response.1 by A10,A15
.= OF.[(qb, <*s*>)-admissible.1, <*s*>.1] by A17,Def6
.= OF.[(qb, <*s*>)-admissible.1, s]
.= OF.[qb, s] by Def2;
hence thesis by A18,A19,A16;
end;
end;
end;
definition
let IAlph, OAlph, tfsm;
let i be Nat;
func i-eq_states_EqR tfsm -> Equivalence_Relation of the carrier of tfsm
means
:Def12:
for qa, qb holds [qa, qb] in it iff i-equivalent qa, qb;
existence
proof
set S = the carrier of tfsm;
defpred P[object,object] means
ex qa, qb being Element of S st qa = $1 & qb =
$2 & i-equivalent qa, qb;
A1: for x, y being object st P[x,y] holds P[y, x] by Th22;
A2: for x, y, z being object st P[x,y] & P[y,z] holds P[x, z] by Th23;
A3: for x being object st x in S holds P[x, x] by Th21;
consider EqR being Equivalence_Relation of S such that
A4: for x, y being object holds [x, y] in EqR iff x in S & y in S & P[x,y
] from EQREL_1:sch 1 (A3, A1, A2);
take EqR;
let qa, qb be Element of S;
hereby
assume [qa, qb] in EqR;
then
ex qa9, qb9 being Element of S st qa9 = qa & qb9 = qb & i-equivalent
qa9, qb9 by A4;
hence i-equivalent qa, qb;
end;
assume i-equivalent qa, qb;
hence thesis by A4;
end;
uniqueness
proof
set S = the carrier of tfsm;
let IT1, IT2 be Equivalence_Relation of S;
assume
A5: for qa, qb being Element of S holds [qa,qb] in IT1 iff i
-equivalent qa, qb;
assume
A6: for qa, qb being Element of S holds [qa,qb] in IT2 iff i
-equivalent qa, qb;
assume IT1 <> IT2;
then consider x being object such that
A7: x in IT1 & not x in IT2 or x in IT2 & not x in IT1 by TARSKI:2;
per cases by A7;
suppose
A8: x in IT1 & not x in IT2;
then consider qa, qb being object such that
A9: x = [qa, qb] and
A10: qa in S & qb in S by RELSET_1:2;
reconsider qa, qb as Element of S by A10;
i-equivalent qa, qb by A5,A8,A9;
hence contradiction by A6,A8,A9;
end;
suppose
A11: x in IT2 & not x in IT1;
then consider qa, qb being object such that
A12: x = [qa, qb] and
A13: qa in S & qb in S by RELSET_1:2;
reconsider qa, qb as Element of S by A13;
i-equivalent qa, qb by A6,A11,A12;
hence contradiction by A5,A11,A12;
end;
end;
end;
definition
let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph, OAlph;
let i be Nat;
func i-eq_states_partition tfsm -> non empty a_partition of the carrier of
tfsm equals
Class (i-eq_states_EqR tfsm);
coherence;
end;
theorem Th28:
(k+1)-eq_states_partition tfsm is_finer_than k -eq_states_partition tfsm
proof
set K = k-eq_states_partition tfsm;
set K1 = (k+1)-eq_states_partition tfsm;
set S = the carrier of tfsm;
let X be set;
assume
A1: X in K1;
then reconsider X9 = X as Subset of S;
consider q being Element of S such that
A2: q in X by A1,FINSEQ_4:87;
reconsider Y = (proj K).q as Element of K;
take Y;
thus Y in K;
let x be object;
assume
A3: x in X;
then x in X9;
then reconsider x9=x as Element of S;
reconsider X9 as Element of Class ((k+1)-eq_states_EqR tfsm) by A1;
consider Q being object such that
Q in S and
A4: X9 = Class ((k+1)-eq_states_EqR tfsm, Q) by EQREL_1:def 3;
[x9, Q] in (k+1)-eq_states_EqR tfsm by A3,A4,EQREL_1:19;
then
A5: [Q, x9] in (k+1)-eq_states_EqR tfsm by EQREL_1:6;
[q, Q] in (k+1)-eq_states_EqR tfsm by A2,A4,EQREL_1:19;
then [q, x9] in (k+1)-eq_states_EqR tfsm by A5,EQREL_1:7;
then (k+1)-equivalent q, x9 by Def12;
then k-equivalent q, x9 by Th26;
then [q, x9] in k-eq_states_EqR tfsm by Def12;
then
A6: [x9, q] in k-eq_states_EqR tfsm by EQREL_1:6;
reconsider Y9 = Y as Element of Class (k-eq_states_EqR tfsm);
consider Q being object such that
A7: Q in S and
A8: Y9 = Class (k-eq_states_EqR tfsm, Q) by EQREL_1:def 3;
reconsider Q as Element of S by A7;
q in Y by EQREL_1:def 9;
then Class(k-eq_states_EqR tfsm,Q)=Class(k-eq_states_EqR tfsm,q)by A8,
EQREL_1:23;
hence thesis by A6,A8,EQREL_1:19;
end;
theorem Th29:
for k be Nat holds Class (k-eq_states_EqR tfsm) = Class ((k+1)
-eq_states_EqR tfsm)implies for m be Nat holds Class ((k+m)-eq_states_EqR tfsm)
= Class (k-eq_states_EqR tfsm)
proof
let k be Nat;
set S = the carrier of tfsm;
set CEk = Class (k-eq_states_EqR tfsm);
set Ek = (k-eq_states_EqR tfsm);
set CEk1 = Class ((k+1)-eq_states_EqR tfsm);
set Ek1 = ((k+1)-eq_states_EqR tfsm);
defpred P[Nat] means Class ((k+$1)-eq_states_EqR tfsm) = CEk;
assume CEk = CEk1;
then
A1: Ek = Ek1 by FINSEQ_4:86;
A2: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
set CEkm=Class ((k+m)-eq_states_EqR tfsm);
set Ekm=((k+m)-eq_states_EqR tfsm);
set CEkm1 = Class ((k+(m+1))-eq_states_EqR tfsm);
set Ekm1 = ((k+(m+1))-eq_states_EqR tfsm);
assume CEkm = CEk;
then
A3: Ekm = Ek by FINSEQ_4:86;
now
let x be object;
reconsider xx=x as set by TARSKI:1;
hereby
assume
A4: x in CEkm1;
then reconsider x9 = x as Subset of S;
consider qa being object such that
A5: qa in S and
A6: x9 = Class (Ekm1, qa) by A4,EQREL_1:def 3;
reconsider qa as Element of S by A5;
A7: x9 c= S;
now
let y be object;
hereby
assume
A8: y in xx;
then reconsider y9 = y as Element of S by A7;
[y, qa] in Ekm1 by A6,A8,EQREL_1:19;
then (k+(m+1))-equivalent y9, qa by Def12;
then k-equivalent y9, qa by Th26;
then [y9, qa] in Ek by Def12;
hence y in Class (Ek, qa) by EQREL_1:19;
end;
assume
A9: y in Class (Ek, qa);
then reconsider y9 = y as Element of S;
[y9, qa] in Ek by A9,EQREL_1:19;
then
A10: (k+1)-equivalent y9, qa by A1,Def12;
A11: 1 <= k+1 by NAT_1:11;
A12: now
let s be Element of IAlph, k1 be Nat;
set Sy9 = (the Tran of tfsm).[y9, s];
set Sqa = (the Tran of tfsm).[qa, s];
k in NAT & k = k+1-1 by ORDINAL1:def 12;
then k-equivalent Sy9, Sqa by A10,A11,Th27;
then
A13: [Sy9, Sqa] in Ek by Def12;
assume k1 = k+m+1-1;
hence k1-equivalent Sy9, Sqa by A3,A13,Def12;
end;
1 <= k+m+1 & 1-equivalent y9, qa by A10,A11,Th27,NAT_1:11;
then (k+m+1)-equivalent y9, qa by A12,Th27;
then [y9, qa] in Ekm1 by Def12;
hence y in xx by A6,EQREL_1:19;
end;
then x = Class (Ek, qa) by TARSKI:2;
hence x in CEk by EQREL_1:def 3;
end;
assume
A14: x in CEk;
then reconsider x9 = x as Subset of S;
consider qa being object such that
A15: qa in S and
A16: x9 = Class (Ek, qa) by A14,EQREL_1:def 3;
reconsider qa as Element of S by A15;
now
let y be object;
hereby
assume
A17: y in xx;
then reconsider y9 = y as Element of S by A16;
[y9, qa] in Ek by A16,A17,EQREL_1:19;
then
A18: (k+1)-equivalent y9, qa by A1,Def12;
A19: 1 <= k+1 by NAT_1:11;
A20: now
let s be Element of IAlph, k1 be Nat;
set Sy9 = (the Tran of tfsm).[y9, s];
set Sqa = (the Tran of tfsm).[qa, s];
k in NAT & k = k+1-1 by ORDINAL1:def 12;
then k-equivalent Sy9, Sqa by A18,A19,Th27;
then
A21: [Sy9, Sqa] in Ek by Def12;
assume k1 = k+m+1-1;
hence k1-equivalent Sy9, Sqa by A3,A21,Def12;
end;
1 <= k+m+1 & 1-equivalent y9, qa by A18,A19,Th27,NAT_1:11;
then (k+m+1)-equivalent y9, qa by A20,Th27;
then [y9, qa] in Ekm1 by Def12;
hence y in Class (Ekm1, qa) by EQREL_1:19;
end;
assume
A22: y in Class (Ekm1, qa);
then reconsider y9 = y as Element of S;
[y, qa] in Ekm1 by A22,EQREL_1:19;
then (k+(m+1))-equivalent y9, qa by Def12;
then k-equivalent y9, qa by Th26;
then [y9, qa] in Ek by Def12;
hence y in xx by A16,EQREL_1:19;
end;
then x = Class (Ekm1, qa) by TARSKI:2;
hence x in CEkm1 by EQREL_1:def 3;
end;
hence CEkm1 = CEk by TARSKI:2;
end;
A23: P[0];
thus for m being Nat holds P[m] from NAT_1:sch 2(A23,A2);
end;
theorem
k-eq_states_partition tfsm = (k+1)-eq_states_partition tfsm implies
for m holds (k+m)-eq_states_partition tfsm = k-eq_states_partition tfsm by Th29
;
theorem Th31:
(k+1)-eq_states_partition tfsm <> k-eq_states_partition tfsm
implies for i st i <= k holds (i+1)-eq_states_partition tfsm <> i
-eq_states_partition tfsm
proof
assume
A1: (k+1)-eq_states_partition tfsm <> k-eq_states_partition tfsm;
let i be Nat such that
A2: i <= k;
A3: ex e being Nat st k+1 = i+e by A2,NAT_1:10,12;
assume
A4: (i+1)-eq_states_partition tfsm = i-eq_states_partition tfsm;
ex d being Nat st k = i+d by A2,NAT_1:10;
then k-eq_states_partition tfsm = i-eq_states_partition tfsm by A4,Th29;
hence contradiction by A1,A4,A3,Th29;
end;
theorem Th32:
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph
holds k-eq_states_partition tfsm = (k+1)-eq_states_partition tfsm or card (k
-eq_states_partition tfsm) < card ((k+1)-eq_states_partition tfsm)
proof
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
set kp = k-eq_states_partition tfsm;
set k1p = (k+1)-eq_states_partition tfsm;
card kp <= card k1p by Th28,FINSEQ_4:89;
then
A1: card kp = card k1p or card kp < card k1p by XXREAL_0:1;
assume kp <> k1p;
hence thesis by A1,Th28,FINSEQ_4:91;
end;
theorem Th33:
Class (0-eq_states_EqR tfsm, q) = the carrier of tfsm
proof
set 0e = 0-eq_states_EqR tfsm;
set S = the carrier of tfsm;
now
let z be object;
thus z in Class (0e, q) implies z in S;
assume z in S;
then reconsider z9 = z as Element of S;
0-equivalent z9, q by Th25;
then [z,q] in 0e by Def12;
hence z in Class (0e, q) by EQREL_1:19;
end;
hence thesis by TARSKI:2;
end;
theorem
0-eq_states_partition tfsm = { the carrier of tfsm }
proof
set S = the carrier of tfsm;
set SS = { the carrier of tfsm };
set 0p = 0-eq_states_partition tfsm;
set 0e = 0-eq_states_EqR tfsm;
now
set y = the Element of S;
let x be object;
hereby
assume
A1: x in 0p;
then reconsider x9 = x as Subset of S;
consider y being object such that
A2: y in S and
A3: x9 = Class (0e, y) by A1,EQREL_1:def 3;
reconsider y as Element of S by A2;
Class (0e, y) = S by Th33;
hence x in SS by A3,TARSKI:def 1;
end;
assume x in SS;
then
A4: x = S by TARSKI:def 1;
Class (0e, y) in Class 0e by EQREL_1:def 3;
hence x in 0p by A4,Th33;
end;
hence thesis by TARSKI:2;
end;
theorem Th35:
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph st n
+1 = card the carrier of tfsm holds (n+1)-eq_states_partition tfsm = n
-eq_states_partition tfsm
proof
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
assume
A1: n+1 = card the carrier of tfsm;
defpred P[Nat] means $1 <= n+1 implies card ($1
-eq_states_partition tfsm) > $1;
assume
A2: (n+1)-eq_states_partition tfsm <> n-eq_states_partition tfsm;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: k <= n+1 implies card (k-eq_states_partition tfsm) > k;
assume
A5: k+1 <= n+1;
then k <= n by XREAL_1:6;
then
A6: (k+1)-eq_states_partition tfsm<>k-eq_states_partition tfsm by A2,Th31;
k+1 <= card (k-eq_states_partition tfsm) by A4,A5,NAT_1:13;
hence thesis by A6,Th32,XXREAL_0:2;
end;
A7: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A7, A3);
then card ((n+1)-eq_states_partition tfsm) > n+1;
hence contradiction by A1,FINSEQ_4:88;
end;
definition
let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph, OAlph;
let IT be a_partition of the carrier of tfsm;
attr IT is final means
for qa, qb being State of tfsm holds qa, qb
-are_equivalent iff ex X being Element of IT st qa in X & qb in X;
end;
theorem
k-eq_states_partition tfsm is final implies (k+1)-eq_states_EqR tfsm =
k-eq_states_EqR tfsm
proof
set S = the carrier of tfsm;
set keq = k-eq_states_EqR tfsm;
set k1eq = (k+1)-eq_states_EqR tfsm;
set kpart = k-eq_states_partition tfsm;
assume
A1: k-eq_states_partition tfsm is final;
now
let x be object;
hereby
assume
A2: x in k1eq;
then consider a, b be object such that
A3: x=[a,b] and
A4: a in S and
A5: b in S by RELSET_1:2;
reconsider b as Element of S by A5;
reconsider a as Element of S by A4;
(k+1)-equivalent a,b by A2,A3,Def12;
then k-equivalent a,b by Th26;
hence x in keq by A3,Def12;
end;
assume
A6: x in keq;
then consider a, b be object such that
A7: x=[a,b] and
A8: a in S and
A9: b in S by RELSET_1:2;
reconsider b as Element of S by A9;
reconsider a as Element of S by A8;
reconsider cl = Class(keq,b) as Element of kpart by EQREL_1:def 3;
A10: b in cl by EQREL_1:20;
a in cl by A6,A7,EQREL_1:19;
then a,b-are_equivalent by A1,A10;
then (k+1)-equivalent a,b;
hence x in k1eq by A7,Def12;
end;
hence thesis by TARSKI:2;
end;
theorem Th37:
k-eq_states_partition tfsm = (k+1)-eq_states_partition tfsm
implies k-eq_states_partition tfsm is final
proof
set S = the carrier of tfsm;
set kpart = k-eq_states_partition tfsm;
set k1part = (k+1)-eq_states_partition tfsm;
set keq = k-eq_states_EqR tfsm;
assume
A1: kpart = k1part;
now
let qa, qb be Element of tfsm;
hereby
reconsider X= Class(keq,qb) as Element of kpart by EQREL_1:def 3;
assume
A2: qa,qb-are_equivalent;
take X;
k-equivalent qa,qb by A2;
then [qa,qb] in keq by Def12;
hence qa in X & qb in X by EQREL_1:19,20;
end;
given X being Element of kpart such that
A3: qa in X and
A4: qb in X;
consider qc being object such that
qc in S and
A5: X = Class(keq,qc) by EQREL_1:def 3;
[qb,qc] in keq by A4,A5,EQREL_1:19;
then
A6: [qc,qb] in keq by EQREL_1:6;
[qa,qc] in keq by A3,A5,EQREL_1:19;
then
A7: [qa,qb] in keq by A6,EQREL_1:7;
then
A8: k-equivalent qa,qb by Def12;
thus qa,qb-are_equivalent
proof
let w be FinSequence of IAlph;
consider n being Nat such that
A9: dom w=Seg n by FINSEQ_1:def 2;
n in NAT by ORDINAL1:def 12;
then
A10: n = len w by A9,FINSEQ_1:def 3;
per cases;
suppose
n <= k;
hence thesis by A8,A10;
end;
suppose
n > k;
then ex m be Element of NAT st n=k+m & 1 <= m by FINSEQ_4:84;
then n-eq_states_partition tfsm = kpart by A1,Th29;
then [qa,qb] in n-eq_states_EqR tfsm by A7,FINSEQ_4:86;
then n-equivalent qa,qb by Def12;
hence thesis by A10;
end;
end;
end;
hence thesis;
end;
theorem
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph st n+1 =
card the carrier of tfsm holds ex k being Nat st k <= n & k
-eq_states_partition tfsm is final
proof
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
assume
A1: n+1 = card the carrier of tfsm;
take n;
thus n <= n;
n-eq_states_partition tfsm = (n+1)-eq_states_partition tfsm by A1,Th35;
hence thesis by Th37;
end;
definition
let IAlph, OAlph;
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
func final_states_partition tfsm -> a_partition of the carrier of tfsm means
:Def15:
it is final;
existence
proof
reconsider n = card the carrier of tfsm as Nat;
consider m being Nat such that
A1: n=m+1 by NAT_1:6;
reconsider m as Nat;
take (m-eq_states_partition tfsm);
m-eq_states_partition tfsm=(m+1)-eq_states_partition tfsm by A1,Th35;
hence thesis by Th37;
end;
uniqueness
proof
let it1, it2 be a_partition of the carrier of tfsm;
assume that
A2: it1 is final and
A3: it2 is final;
now
assume it1 <> it2;
then not for X being object holds X in it1 iff X in it2 by TARSKI:2;
then consider X being set such that
A4: X in it1 & not X in it2 or not X in it1 & X in it2;
per cases by A4;
suppose
A5: X in it1 & not X in it2;
then reconsider X as Subset of tfsm;
consider qx be Element of tfsm such that
A6: qx in X by A5,FINSEQ_4:87;
union it2 = the carrier of tfsm by EQREL_1:def 4;
then consider Z being set such that
A7: qx in Z and
A8: Z in it2 by TARSKI:def 4;
reconsider Z as Subset of tfsm by A8;
set XZ= X\Z, ZX= Z\X, Y9= XZ \/ ZX;
Y9 <> {}
proof
assume
A9: Y9 = {};
then Z\X = {};
then
A10: Z c= X by XBOOLE_1:37;
X\Z = {} by A9;
then X c= Z by XBOOLE_1:37;
hence contradiction by A5,A8,A10,XBOOLE_0:def 10;
end;
then consider qy be Element of tfsm such that
A11: qy in Y9 by SUBSET_1:4;
reconsider X as Element of it1 by A5;
A12: now
assume
A13: qy in Z\X;
A14: not qx,qy-are_equivalent
proof
assume qx,qy-are_equivalent;
then consider Z9 be Element of it1 such that
A15: qx in Z9 and
A16: qy in Z9 by A2;
per cases;
suppose
X = Z9;
hence contradiction by A13,A16,XBOOLE_0:def 5;
end;
suppose
X <> Z9;
then X misses Z9 by EQREL_1:def 4;
then X /\ Z9 = {};
hence contradiction by A6,A15,XBOOLE_0:def 4;
end;
end;
qy in Z by A13,XBOOLE_0:def 5;
hence contradiction by A3,A7,A8,A14;
end;
now
assume
A17: qy in X\Z;
A18: not qx,qy-are_equivalent
proof
assume qx,qy-are_equivalent;
then consider Z9 be Element of it2 such that
A19: qx in Z9 and
A20: qy in Z9 by A3;
per cases;
suppose
Z = Z9;
hence contradiction by A17,A20,XBOOLE_0:def 5;
end;
suppose
Z <> Z9;
then Z misses Z9 by A8,EQREL_1:def 4;
then Z /\ Z9 = {};
hence contradiction by A7,A19,XBOOLE_0:def 4;
end;
end;
qy in X by A17,XBOOLE_0:def 5;
hence contradiction by A2,A6,A18;
end;
hence contradiction by A11,A12,XBOOLE_0:def 3;
end;
suppose
A21: not X in it1 & X in it2;
then reconsider X as Subset of tfsm;
consider qx be Element of tfsm such that
A22: qx in X by A21,FINSEQ_4:87;
union it1 = the carrier of tfsm by EQREL_1:def 4;
then consider Z being set such that
A23: qx in Z and
A24: Z in it1 by TARSKI:def 4;
reconsider Z as Subset of tfsm by A24;
set XZ= X\Z;
set ZX= Z\X;
set Y9= XZ \/ ZX;
Y9 <> {}
proof
assume
A25: Y9 = {};
then Z\X={};
then
A26: Z c= X by XBOOLE_1:37;
X\Z={} by A25;
then X c= Z by XBOOLE_1:37;
hence contradiction by A21,A24,A26,XBOOLE_0:def 10;
end;
then consider qy be Element of tfsm such that
A27: qy in Y9 by SUBSET_1:4;
reconsider X as Element of it2 by A21;
A28: now
assume
A29: qy in Z\X;
A30: not qx,qy-are_equivalent
proof
assume qx,qy-are_equivalent;
then consider Z9 be Element of it2 such that
A31: qx in Z9 and
A32: qy in Z9 by A3;
per cases;
suppose
X = Z9;
hence contradiction by A29,A32,XBOOLE_0:def 5;
end;
suppose
X <> Z9;
then X misses Z9 by EQREL_1:def 4;
then X /\ Z9 = {};
hence contradiction by A22,A31,XBOOLE_0:def 4;
end;
end;
qy in Z by A29,XBOOLE_0:def 5;
hence contradiction by A2,A23,A24,A30;
end;
now
assume
A33: qy in X\Z;
A34: not qx,qy-are_equivalent
proof
assume qx,qy-are_equivalent;
then consider Z9 be Element of it1 such that
A35: qx in Z9 and
A36: qy in Z9 by A2;
per cases;
suppose
Z = Z9;
hence contradiction by A33,A36,XBOOLE_0:def 5;
end;
suppose
Z <> Z9;
then Z misses Z9 by A24,EQREL_1:def 4;
then Z /\ Z9 = {};
hence contradiction by A23,A35,XBOOLE_0:def 4;
end;
end;
qy in X by A33,XBOOLE_0:def 5;
hence contradiction by A3,A22,A34;
end;
hence contradiction by A27,A28,XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
end;
theorem Th39:
for tfsm being finite non empty Mealy-FSM over IAlph, OAlph
holds n+1 = card the carrier of tfsm implies final_states_partition tfsm = n
-eq_states_partition tfsm
proof
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
assume n+1 = card the carrier of tfsm;
then (n+1)-eq_states_partition tfsm = n-eq_states_partition tfsm by Th35;
then n-eq_states_partition tfsm is final by Th37;
hence thesis by Def15;
end;
begin :: The reduction of a Mealy machine
reserve tfsm, rtfsm for finite non empty Mealy-FSM over IAlph, OAlph,
q for State of tfsm;
definition
let IAlph, OAlph be non empty set;
let tfsm be finite non empty Mealy-FSM over IAlph, OAlph;
let qf be Element of final_states_partition tfsm;
let s be Element of IAlph;
func (s,qf)-succ_class -> Element of final_states_partition tfsm means
:
Def16: ex q being State of tfsm, n being Nat st q in qf & (n+1) =
card the carrier of tfsm & it = Class(n-eq_states_EqR tfsm, (the Tran of tfsm).
[q,s]);
existence
proof
consider q1 be Element of tfsm such that
A1: q1 in qf by FINSEQ_4:87;
set q9 = (the Tran of tfsm).[q1,s];
set m = card the carrier of tfsm;
consider n being Nat such that
A2: m=n+1 by NAT_1:6;
reconsider n as Nat;
final_states_partition tfsm = n-eq_states_partition tfsm by A2,Th39;
then reconsider IT = Class(n-eq_states_EqR tfsm,q9) as Element of
final_states_partition tfsm by EQREL_1:def 3;
take IT;
thus thesis by A2,A1;
end;
uniqueness
proof
let it1, it2 be Element of final_states_partition tfsm;
given q1 be Element of tfsm, n1 being Nat such that
A3: q1 in qf and
A4: (n1+1) = card the carrier of tfsm & it1 = Class(n1-eq_states_EqR
tfsm, (the Tran of tfsm).[q1,s]);
set q19 = (the Tran of tfsm).[q1,s];
given q2 be Element of tfsm, n2 being Nat such that
A5: q2 in qf and
A6: (n2+1) = card the carrier of tfsm & it2 = Class(n2-eq_states_EqR
tfsm, (the Tran of tfsm).[q2,s]);
set q29 = (the Tran of tfsm).[q2,s], m=n1+1;
A7: 1 <= m & n1 = m-1 by NAT_1:11;
final_states_partition tfsm is final by Def15;
then q1,q2-are_equivalent by A3,A5;
then m-equivalent q1,q2;
then n1-equivalent q19,q29 by A7,Th27;
then [q19,q29] in n1-eq_states_EqR tfsm by Def12;
hence thesis by A4,A6,EQREL_1:35;
end;
end;
definition
let IAlph, OAlph, tfsm;
let qf be Element of final_states_partition tfsm, s;
func (qf,s)-class_response -> Element of OAlph means
:Def17:
ex q st q in qf & it = (the OFun of tfsm).[q,s];
existence
proof
consider q1 be Element of tfsm such that
A1: q1 in qf by FINSEQ_4:87;
take (the OFun of tfsm).[q1,s];
thus thesis by A1;
end;
uniqueness
proof
let it1, it2 be Element of OAlph;
given q1 be Element of tfsm such that
A2: q1 in qf and
A3: it1 = (the OFun of tfsm).[q1,s];
given q2 be Element of tfsm such that
A4: q2 in qf and
A5: it2 = (the OFun of tfsm).[q2,s];
final_states_partition tfsm is final by Def15;
then q1,q2-are_equivalent by A2,A4;
hence thesis by A3,A5,Th19;
end;
end;
definition
let IAlph, OAlph, tfsm;
func the_reduction_of tfsm -> strict Mealy-FSM over IAlph, OAlph means
:
Def18: the
carrier of it = final_states_partition tfsm & (for Q being State of
it, s for q being State of tfsm st q in Q holds (the Tran of tfsm).(q, s) in (
the Tran of it).(Q, s) & (the OFun of tfsm).(q, s) = (the OFun of it).(Q, s)) &
the InitS of tfsm in the InitS of it;
existence
proof
set part=final_states_partition tfsm;
reconsider m = card the carrier of tfsm as Nat;
set TR = the Tran of tfsm;
consider n be Nat such that
A1: m = n+1 by NAT_1:6;
reconsider n as Nat;
set IS = Class(n-eq_states_EqR tfsm, the InitS of tfsm);
part=n-eq_states_partition tfsm by A1,Th39;
then reconsider IS as Element of part by EQREL_1:def 3;
deffunc F(Element of part,Element of IAlph) = ($2,$1)-succ_class;
consider Trf being Function of [: part, IAlph:], part such that
A2: for q being Element of part for i being Element of IAlph holds Trf
.(q,i) = F(q,i) from BINOP_1:sch 4;
deffunc F(Element of part,Element of IAlph) = ($1,$2)-class_response;
consider OF being Function of [:part,IAlph:],OAlph such that
A3: for q being Element of part for i being Element of IAlph holds OF.
(q,i) =F(q,i) from BINOP_1:sch 4;
take IT = Mealy-FSM (# final_states_partition tfsm, Trf, OF, IS #);
now
reconsider a19 = 1 as Integer;
let Q be Element of IT, s, q such that
A4: q in Q;
reconsider s9 = s as Element of IAlph;
reconsider Q9 = Q as Element of final_states_partition tfsm;
consider Q1 being Element of tfsm, n1 being Nat such that
A5: Q1 in Q9 and
(n1+1) = card the carrier of tfsm and
A6: (s9,Q9)-succ_class = Class(n1-eq_states_EqR tfsm, TR.[Q1,s9]) by Def16;
final_states_partition tfsm is final by Def15;
then q, Q1-are_equivalent by A4,A5;
then
A7: (n1+1)-equivalent q,Q1;
reconsider n19 = n1 as Integer;
1 <= n1+1 & (n19 + a19) - a19 = n19 by NAT_1:11;
then n1-equivalent TR.[q,s9],TR.[Q1,s9]by A7,Th27;
then
A8: [TR.[q,s9],TR.[Q1,s9]] in n1-eq_states_EqR tfsm by Def12;
( the Tran of IT).(Q9,s9)=Class(n1-eq_states_EqR tfsm,TR.(Q1,s9)) by A2
,A6;
hence TR.[q, s] in (the Tran of IT).(Q, s) by A8,EQREL_1:19;
A9: (the OFun of IT).(Q9,s9) = (Q9,s9)-class_response by A3;
consider Q1 be Element of tfsm such that
A10: Q1 in Q9 and
A11: (Q9,s9)-class_response = (the OFun of tfsm).[Q1,s9] by Def17;
final_states_partition tfsm is final by Def15;
then q, Q1-are_equivalent by A4,A10;
hence (the OFun of tfsm).[q, s] = (the OFun of IT).[Q, s] by A9,A11,Th19;
end;
hence thesis by EQREL_1:20;
end;
uniqueness
proof
let it1, it2 be strict Mealy-FSM over IAlph,OAlph;
set TR = the Tran of tfsm;
assume that
A12: the carrier of it1 = final_states_partition tfsm and
A13: for Q being Element of it1, s, q st q in Q holds TR.(q, s) in (
the Tran of it1).(Q, s) & (the OFun of tfsm).(q, s) = (the OFun of it1).(Q, s)
and
A14: the InitS of tfsm in the InitS of it1;
assume that
A15: the carrier of it2 = final_states_partition tfsm and
A16: for Q being Element of it2, s, q st q in Q holds TR.(q, s) in (
the Tran of it2).(Q, s) & (the OFun of tfsm).(q, s) = (the OFun of it2).(Q, s)
and
A17: the InitS of tfsm in the InitS of it2;
A18: the OFun of it1 = the OFun of it2
proof
reconsider OF2 = the OFun of it2 as Function of [:
final_states_partition tfsm, IAlph :], OAlph by A15;
reconsider OF1 = the OFun of it1 as Function of [:
final_states_partition tfsm, IAlph :], OAlph by A12;
now
let Q be Element of final_states_partition tfsm, s;
consider q be Element of tfsm such that
A19: q in Q by FINSEQ_4:87;
thus OF1.(Q,s) = (the OFun of tfsm).(q,s) by A12,A13,A19
.= OF2.(Q,s) by A15,A16,A19;
end;
hence thesis by BINOP_1:2;
end;
A20: the Tran of it1 = the Tran of it2
proof
reconsider T2 = the Tran of it2 as Function of [: final_states_partition
tfsm, IAlph:],final_states_partition tfsm by A15;
reconsider T1 = the Tran of it1 as Function of [: final_states_partition
tfsm, IAlph:],final_states_partition tfsm by A12;
now
let Q be Element of final_states_partition tfsm, s;
reconsider T19 = T1.[Q,s], T29 = T2.[Q,s] as Subset of tfsm by
TARSKI:def 3;
A21: T19 = T29 or T19 misses T29 by EQREL_1:def 4;
consider q be Element of tfsm such that
A22: q in Q by FINSEQ_4:87;
TR.(q,s) in T1.(Q,s) & TR.(q,s) in T2.(Q,s) by A12,A13,A15,A16,A22;
hence T1.(Q,s) = T2.(Q,s) by A21,XBOOLE_0:3;
end;
hence thesis by BINOP_1:2;
end;
the InitS of it1 = the InitS of it2
proof
the InitS of it2 in final_states_partition tfsm by A15;
then reconsider IS2=the InitS of it2 as Subset of tfsm;
the InitS of it1 in final_states_partition tfsm by A12;
then reconsider IS1=the InitS of it1 as Subset of tfsm;
IS1 = IS2 or IS1 misses IS2 by A12,A15,EQREL_1:def 4;
hence thesis by A14,A17,XBOOLE_0:3;
end;
hence thesis by A12,A15,A20,A18;
end;
end;
registration
let IAlph, OAlph, tfsm;
cluster the_reduction_of tfsm -> non empty finite;
coherence
proof
the carrier of the_reduction_of tfsm = final_states_partition tfsm by Def18
;
hence thesis;
end;
end;
theorem Th40:
for qr being State of rtfsm st rtfsm = the_reduction_of tfsm & q
in qr holds for k being Nat st k in Seg (len w +1) holds (q,w)
-admissible.k in (qr,w)-admissible.k
proof
let qr be State of rtfsm;
set TR = the Tran of tfsm;
assume that
A1: rtfsm = the_reduction_of tfsm and
A2: q in qr;
defpred P[Nat] means $1 in Seg(len w +1) implies (q,w)-admissible
.$1 in (qr,w)-admissible.$1;
A3: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A4: k in Seg (len w + 1) implies (q,w)-admissible.k in (qr,w) -admissible.k;
assume
A5: (k+1) in Seg (len w + 1);
A6: k = 0 or 0 < k & 0+1 = 1;
per cases by A6,NAT_1:13;
suppose
A7: k = 0;
then (q,w)-admissible.(k+1) = q by Def2;
hence thesis by A2,A7,Def2;
end;
suppose
A8: 1 <= k;
A9: k+1 <= len w + 1 by A5,FINSEQ_1:1;
then
A10: k <= len w by XREAL_1:6;
then consider
w1i being Element of IAlph, q1i, q1i1 being Element of tfsm
such that
A11: w1i = w.k & q1i = (q,w)-admissible.k and
A12: q1i1 = (q,w)-admissible.(k+1) & w1i-succ_of q1i = q1i1 by A8,Def2;
consider w2i being Element of IAlph, q2i, q2i1 being Element of rtfsm
such that
A13: w2i = w.k & q2i = (qr,w)-admissible.k and
A14: q2i1 = (qr,w)-admissible.(k+1) & w2i-succ_of q2i = q2i1 by A8,A10,Def2;
k <= k+1 by NAT_1:11;
then k <= len w + 1 by A9,XXREAL_0:2;
then TR.(q1i,w1i) in (the Tran of rtfsm).(q2i,w2i) by A1,A4,A8,A11,A13
,Def18,FINSEQ_1:1;
hence thesis by A12,A14;
end;
end;
A15: P[0] by FINSEQ_1:1;
thus for k being Nat holds P[k] from NAT_1:sch 2(A15,A3 );
end;
theorem Th41:
tfsm, the_reduction_of tfsm-are_equivalent
proof
now
set rtfsm = the_reduction_of tfsm;
let w1 be FinSequence of IAlph;
set ad1 = (the InitS of tfsm,w1)-admissible;
set ad2 = (the InitS of rtfsm, w1)-admissible;
set r1=(the InitS of tfsm,w1)-response;
set r2=(the InitS of rtfsm,w1)-response;
A1: the InitS of tfsm in the InitS of rtfsm by Def18;
A2: now
let k be Nat;
assume that
A3: 1 <= k and
A4: k <= len r1;
k <= len w1 by A4,Def6;
then
A5: k in Seg len w1 by A3,FINSEQ_1:1;
then
A6: k in Seg (len w1 + 1) by FINSEQ_2:8;
then
A7: ad1.k in ad2.k by A1,Th40;
k in Seg len ad2 by A6,Def2;
then k in dom ad2 by FINSEQ_1:def 3;
then
A8: ad2.k is Element of rtfsm by FINSEQ_2:11;
k in Seg len ad1 by A6,Def2;
then k in dom ad1 by FINSEQ_1:def 3;
then
A9: ad1.k is Element of tfsm by FINSEQ_2:11;
A10: k in dom w1 by A5,FINSEQ_1:def 3;
then
A11: w1.k is Element of IAlph by FINSEQ_2:11;
thus r2.k = (the OFun of rtfsm).(ad2.k, w1.k) by A10,Def6
.= (the OFun of tfsm).(ad1.k, w1.k) by A9,A11,A8,A7,Def18
.= r1.k by A10,Def6;
end;
len r1 = len w1 by Def6
.= len r2 by Def6;
hence r1 = r2 by A2,FINSEQ_1:14;
end;
hence thesis;
end;
begin :: Machine Isomorphism
reserve qr1, qr2 for State of rtfsm,
Tf for Function of the carrier of tfsm1, the carrier of tfsm2;
definition
let IAlph, OAlph, tfsm1, tfsm2;
pred tfsm1, tfsm2-are_isomorphic means
ex Tf st Tf is bijective & Tf
.the InitS of tfsm1 = the InitS of tfsm2 & for q11, s holds Tf.((the Tran of
tfsm1).(q11,s))=(the Tran of tfsm2).(Tf.q11, s) & (the OFun of tfsm1).(q11,s) =
(the OFun of tfsm2).(Tf.q11, s);
reflexivity
proof
let tfsm1 be non empty Mealy-FSM over IAlph, OAlph;
take Tf = id the carrier of tfsm1;
thus Tf is bijective;
thus Tf.the InitS of tfsm1 = the InitS of tfsm1;
let q be Element of tfsm1, s;
thus Tf.((the Tran of tfsm1).(q, s)) = (the Tran of tfsm1).[q, s]
.= (the Tran of tfsm1).(Tf.q, s);
thus thesis;
end;
symmetry
proof
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph, OAlph;
given Tf being Function of the carrier of tfsm1, the carrier of tfsm2 such
that
A1: Tf is bijective and
A2: Tf.the InitS of tfsm1 = the InitS of tfsm2 and
A3: for q being Element of tfsm1, s being Element of IAlph holds Tf.((
the Tran of tfsm1).(q, s)) = (the Tran of tfsm2).(Tf.q, s) & (the OFun of tfsm1
).(q,s) = (the OFun of tfsm2).(Tf.q, s);
A4: dom Tf = the carrier of tfsm1 by FUNCT_2:def 1;
then
A5: rng(Tf") = the carrier of tfsm1 by A1,FUNCT_1:33;
A6: rng Tf = the carrier of tfsm2 by A1,FUNCT_2:def 3;
then the carrier of tfsm2 = dom(Tf") by A1,FUNCT_1:33;
then reconsider
Tf9 = Tf" as Function of the carrier of tfsm2, the carrier of
tfsm1 by A5,FUNCT_2:1;
take Tf9;
Tf9 is onto by A5,FUNCT_2:def 3;
hence Tf9 is bijective by A1;
thus the InitS of tfsm1 = Tf9.the InitS of tfsm2 by A1,A2,A4,FUNCT_1:34;
now
let q be Element of tfsm2, s be Element of IAlph;
A7: q = Tf.(Tf9.q) by A1,A6,FUNCT_1:35;
thus (the Tran of tfsm1).[Tf9.q, s] = Tf9.(Tf.((the Tran of tfsm1).(Tf9.
q, s))) by A1,A4,FUNCT_1:34
.= Tf9.((the Tran of tfsm2).(q,s)) by A3,A7;
thus (the OFun of tfsm1).(Tf9.q,s)= (the OFun of tfsm2).(q,s) by A3,A7;
end;
hence thesis;
end;
end;
theorem Th42:
tfsm1,tfsm2-are_isomorphic & tfsm2,tfsm3-are_isomorphic implies
tfsm1,tfsm3-are_isomorphic
proof
assume that
A1: tfsm1,tfsm2-are_isomorphic and
A2: tfsm2,tfsm3-are_isomorphic;
consider Tf1 being Function of the carrier of tfsm1, the carrier of tfsm2
such that
A3: Tf1 is bijective and
A4: Tf1.the InitS of tfsm1 = the InitS of tfsm2 and
A5: for q being Element of tfsm1, s1 being Element of IAlph holds Tf1.((
the Tran of tfsm1).(q, s1)) = (the Tran of tfsm2).(Tf1.q, s1) & (the OFun of
tfsm1).(q,s1) = (the OFun of tfsm2).(Tf1.q, s1) by A1;
consider Tf2 being Function of the carrier of tfsm2, the carrier of tfsm3
such that
A6: Tf2 is bijective and
A7: Tf2.the InitS of tfsm2 = the InitS of tfsm3 and
A8: for q being Element of tfsm2, s1 being Element of IAlph holds Tf2.((
the Tran of tfsm2).(q, s1)) = (the Tran of tfsm3).(Tf2.q, s1) & (the OFun of
tfsm2).(q,s1) = (the OFun of tfsm3).(Tf2.q, s1) by A2;
take Tf = Tf2 * Tf1;
thus Tf is bijective by A3,A6,FINSEQ_4:85;
A9: dom Tf1 = the carrier of tfsm1 by FUNCT_2:def 1;
hence Tf.the InitS of tfsm1 = the InitS of tfsm3 by A4,A7,FUNCT_1:13;
now
let q be Element of tfsm1, s1 be Element of IAlph;
thus (the Tran of tfsm3).[Tf.q, s1] = (the Tran of tfsm3).(Tf2.(Tf1.q), s1
) by A9,FUNCT_1:13
.= Tf2.((the Tran of tfsm2).(Tf1.q, s1)) by A8
.= Tf2.(Tf1.((the Tran of tfsm1).(q,s1))) by A5
.= Tf.((the Tran of tfsm1).(q, s1)) by A9,FUNCT_1:13;
thus (the OFun of tfsm3).[Tf.q, s1] = (the OFun of tfsm3).(Tf2.(Tf1.q), s1
) by A9,FUNCT_1:13
.= (the OFun of tfsm2).(Tf1.q, s1) by A8
.= (the OFun of tfsm1).(q,s1) by A5;
end;
hence thesis;
end;
theorem Th43:
(for q being State of tfsm1, s holds Tf.((the Tran of tfsm1).(q,
s)) = (the Tran of tfsm2).(Tf.q,s)) implies for k st 1 <= k & k <= len w + 1
holds Tf.((q11,w)-admissible.k) = (Tf.q11,w)-admissible.k
proof
defpred P[Nat] means 1 <= $1 & $1 <= len w + 1 implies Tf.((q11,w
)-admissible.$1) = (Tf.q11,w)-admissible.$1;
assume
A1: for q being State of tfsm1, s holds Tf.((the Tran of tfsm1).(q,s)) =
(the Tran of tfsm2).(Tf.q,s);
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: 1 <= k & k <= len w + 1 implies Tf.((q11,w)-admissible.k) = (Tf.
q11,w)-admissible.k;
assume that
1<=k+1 and
A4: k+1<=len w+1;
A5: k=0 or 0<k & 0 + 1 = 1;
per cases by A5,NAT_1:13;
suppose
A6: k = 0;
hence Tf.((q11,w)-admissible.(k+1)) = Tf.q11 by Def2
.= (Tf.q11,w)-admissible.(k+1) by A6,Def2;
end;
suppose
A7: 1 <= k;
A8: len w <= len w + 1 by NAT_1:11;
A9: k <= len w by A4,XREAL_1:6;
then consider
wi being Element of IAlph,qi,qi1 being State of tfsm1 such that
A10: wi = w.k & qi = (q11,w)-admissible.k and
A11: qi1 = (q11,w)-admissible.(k+1) & wi-succ_of qi =qi1 by A7,Def2;
consider wri being Element of IAlph, qri, qri1 being State of tfsm2 such
that
A12: wri = w.k & qri = (Tf.q11,w)-admissible.k and
A13: qri1 = (Tf.q11,w)-admissible.(k+1) & wri-succ_of qri = qri1 by A7,A9,Def2
;
thus Tf.((q11,w)-admissible.(k+1)) = Tf.((the Tran of tfsm1).(qi, wi))
by A11
.= (the Tran of tfsm2).(qri, wri) by A1,A3,A7,A9,A8,A10,A12,XXREAL_0:2
.= (Tf.q11,w)-admissible.(k+1) by A13;
end;
end;
A14: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A14, A2);
end;
theorem Th44:
( for q being State of tfsm1, s holds Tf.((the Tran of tfsm1).(q
, s)) = (the Tran of tfsm2).(Tf.q, s) & (the OFun of tfsm1).(q,s) = (the OFun
of tfsm2).(Tf.q, s)) implies (q11,q12-are_equivalent iff Tf.q11, Tf.q12
-are_equivalent)
proof
set Stfsm1 = the carrier of tfsm1;
set Stfsm2 = the carrier of tfsm2;
set OF1 = the OFun of tfsm1, OF2 = the OFun of tfsm2;
assume
A1: for q being Element of Stfsm1, s holds Tf.((the Tran of tfsm1).(q, s
)) = (the Tran of tfsm2).(Tf.q, s) & (the OFun of tfsm1).(q,s) = (the OFun of
tfsm2).(Tf.q, s);
hereby
reconsider Tq2 = Tf.q12 as Element of Stfsm2;
reconsider Tq1 = Tf.q11 as Element of Stfsm2;
assume
A2: q11,q12-are_equivalent;
now
let w be FinSequence of IAlph;
A3: now
let k be Nat;
assume that
A4: 1 <= k and
A5: k <= len (Tq1,w)-response;
len (Tq1,w)-response = len w by Def6;
then
A6: k in Seg len w by A4,A5,FINSEQ_1:1;
then
A7: k in Seg (len w + 1) by FINSEQ_2:8;
then
A8: k <= len w + 1 by FINSEQ_1:1;
len (q11,w)-admissible = len w + 1 by Def2;
then k in dom (q11,w)-admissible by A7,FINSEQ_1:def 3;
then reconsider q1a = (q11,w)-admissible.k as Element of Stfsm1 by
FINSEQ_2:11;
len (q12,w)-admissible = len w + 1 by Def2;
then k in dom (q12,w)-admissible by A7,FINSEQ_1:def 3;
then reconsider q2a = (q12,w)-admissible.k as Element of Stfsm1 by
FINSEQ_2:11;
A9: k in dom w by A6,FINSEQ_1:def 3;
then reconsider wk = w.k as Element of IAlph by FINSEQ_2:11;
thus (Tq1,w)-response.k=OF2.[(Tq1,w)-admissible.k, w.k] by A9,Def6
.= OF2.(Tf.q1a, wk) by A1,A4,A8,Th43
.= OF1.(q1a, wk) by A1
.= (q11,w)-response.k by A9,Def6
.= (q12,w)-response.k by A2
.= OF1.(q2a, wk) by A9,Def6
.= OF2.(Tf.q2a, wk) by A1
.= OF2.[(Tq2,w)-admissible.k, w.k] by A1,A4,A8,Th43
.= (Tq2,w)-response.k by A9,Def6;
end;
len(Tq1,w)-response=len w by Def6
.=len (Tq2,w)-response by Def6;
hence (Tq1,w)-response = (Tq2,w)-response by A3,FINSEQ_1:14;
end;
hence Tf.q11, Tf.q12-are_equivalent;
end;
assume
A10: Tf.q11, Tf.q12-are_equivalent;
now
let w be FinSequence of IAlph;
A11: now
let k be Nat;
assume that
A12: 1 <= k and
A13: k <= len (q11,w)-response;
len (q11,w)-response = len w by Def6;
then
A14: k in Seg len w by A12,A13,FINSEQ_1:1;
then
A15: k in Seg (len w + 1) by FINSEQ_2:8;
then
A16: k in NAT & k <= len w + 1 by FINSEQ_1:1;
len (q12,w)-admissible = len w + 1 by Def2;
then k in dom (q12,w)-admissible by A15,FINSEQ_1:def 3;
then reconsider q2a = (q12,w)-admissible.k as Element of Stfsm1 by
FINSEQ_2:11;
len (q11,w)-admissible = len w + 1 by Def2;
then k in dom (q11,w)-admissible by A15,FINSEQ_1:def 3;
then reconsider q1a = (q11,w)-admissible.k as Element of Stfsm1 by
FINSEQ_2:11;
A17: k in dom w by A14,FINSEQ_1:def 3;
then reconsider wk = w.k as Element of IAlph by FINSEQ_2:11;
thus (q11,w)-response.k = OF1.((q11,w)-admissible.k, w.k) by A17,Def6
.= OF2.(Tf.q1a, wk) by A1
.= OF2.[(Tf.q11,w)-admissible.k,wk] by A1,A12,A16,Th43
.= (Tf.q11,w)-response.k by A17,Def6
.= (Tf.q12,w)-response.k by A10
.= OF2.[(Tf.q12,w)-admissible.k, w.k] by A17,Def6
.= OF2.(Tf.q2a, wk) by A1,A12,A16,Th43
.= OF1.(q2a, w.k) by A1
.= (q12,w)-response.k by A17,Def6;
end;
len (q11,w)-response = len w by Def6
.= len (q12,w)-response by Def6;
hence (q11,w)-response = (q12,w)-response by A11,FINSEQ_1:14;
end;
hence thesis;
end;
theorem Th45:
rtfsm = the_reduction_of tfsm & qr1<>qr2 implies not qr1,qr2 -are_equivalent
proof
assume that
A1: rtfsm = the_reduction_of tfsm and
A2: qr1 <> qr2;
A3: the carrier of rtfsm = final_states_partition tfsm by A1,Def18;
then reconsider q19 = qr1 as Subset of tfsm by TARSKI:def 3;
consider x being Element of tfsm such that
A4: x in q19 by A3,FINSEQ_4:87;
reconsider q29 = qr2 as Subset of tfsm by A3,TARSKI:def 3;
consider y being Element of tfsm such that
A5: y in q29 by A3,FINSEQ_4:87;
A6: final_states_partition tfsm is final by Def15;
not x,y-are_equivalent
proof
assume x,y-are_equivalent;
then consider X being Element of rtfsm such that
A7: x in X & y in X by A3,A6;
A8: q29 misses q19 by A2,A3,EQREL_1:def 4;
X is Subset of tfsm by A3,TARSKI:def 3;
then X = q19 or X misses q19 by A3,EQREL_1:def 4;
hence contradiction by A4,A5,A7,A8,XBOOLE_0:3;
end;
then consider w being FinSequence of IAlph such that
A9: (x,w)-response <> (y,w)-response;
set q1adm = (qr1,w)-admissible, q2adm = (qr2,w)-admissible;
set xadm = (x,w)-admissible, yadm = (y,w)-admissible;
set xresp = (x,w)-response, yresp = (y,w)-response;
len xresp = len w by Def6
.= len yresp by Def6;
then consider k be Nat such that
A10: 1 <= k & k <= len xresp and
A11: xresp.k <> yresp.k by A9,FINSEQ_1:14;
len xresp = len w by Def6;
then
A12: k in Seg len w by A10,FINSEQ_1:1;
then k in Seg (len w + 1) by FINSEQ_2:8;
then
A13: yadm.k in q2adm.k by A1,A5,Th40;
set q1resp = (qr1,w)-response, q2resp = (qr2,w)-response;
A14: len q1adm = len w + 1 by Def2
.= len xresp + 1 by Def6;
k in Seg len xresp by A10,FINSEQ_1:1;
then
A15: k in Seg len q1adm by A14,FINSEQ_2:8;
then k in dom q1adm by FINSEQ_1:def 3;
then
A16: q1adm.k is Element of rtfsm by FINSEQ_2:11;
len q2adm = len w + 1 by Def2
.= len q1adm by Def2;
then k in dom q2adm by A15,FINSEQ_1:def 3;
then
A17: q2adm.k is Element of rtfsm by FINSEQ_2:11;
k in dom w by A12,FINSEQ_1:def 3;
then
A18: w.k is Element of IAlph by FINSEQ_2:11;
A19: len q1adm = len w + 1 by Def2
.= len xadm by Def2;
then k in dom xadm by A15,FINSEQ_1:def 3;
then
A20: xadm.k is Element of tfsm by FINSEQ_2:11;
len yadm = len w + 1 by Def2
.= len xadm by Def2;
then k in dom yadm by A15,A19,FINSEQ_1:def 3;
then
A21: yadm.k is Element of tfsm by FINSEQ_2:11;
k in Seg (len w + 1) by A12,FINSEQ_2:8;
then
A22: xadm.k in q1adm.k by A1,A4,Th40;
now
assume
A23: q1resp = q2resp;
len w = len xresp by Def6;
then
A24: k in dom w by A10,FINSEQ_3:25;
then
A25: xresp.k = (the OFun of tfsm).(xadm.k,w.k) by Def6;
A26: q2resp.k = (the OFun of rtfsm).(q2adm.k,w.k) by A24,Def6
.= (the OFun of tfsm).(yadm.k,w.k) by A1,A18,A17,A13,A21,Def18;
q1resp.k = (the OFun of rtfsm).(q1adm.k,w.k) by A24,Def6
.= (the OFun of tfsm).(xadm.k,w.k) by A1,A16,A18,A22,A20,Def18;
hence contradiction by A11,A23,A24,A26,A25,Def6;
end;
hence thesis;
end;
begin :: Reduced and Connected Machines
definition
let IAlph, OAlph be non empty set;
let IT be non empty Mealy-FSM over IAlph,OAlph;
attr IT is reduced means
:Def20:
for qa, qb being State of IT st qa <> qb holds not qa, qb-are_equivalent;
end;
registration
let IAlph,OAlph,tfsm;
cluster the_reduction_of tfsm -> reduced;
coherence
by Th45;
end;
registration
let IAlph, OAlph;
cluster reduced finite for non empty Mealy-FSM over IAlph,OAlph;
existence
proof
set M = the finite non empty Mealy-FSM over IAlph, OAlph;
take the_reduction_of M;
thus thesis;
end;
end;
reserve Rtfsm for reduced finite non empty Mealy-FSM over IAlph, OAlph;
theorem Th46:
Rtfsm, the_reduction_of Rtfsm-are_isomorphic
proof
set m = Rtfsm;
set rm = the_reduction_of m;
set fpm = final_states_partition m;
deffunc F(Element of m) = (proj fpm).$1;
consider Tf being Function of the carrier of m, fpm such that
A1: for q being Element of m holds Tf.q=F(q) from FUNCT_2:sch 4;
A2: now
assume not Tf is one-to-one;
then consider q1, q2 being object such that
A3: q1 in the carrier of m & q2 in the carrier of m and
A4: Tf.q1 = Tf.q2 and
A5: q1 <> q2 by FUNCT_2:19;
reconsider q1, q2 as State of m by A3;
Tf.q1 = (proj fpm).q1 by A1;
then
A6: q1 in Tf.q1 by EQREL_1:def 9;
A7: fpm is final by Def15;
Tf.q2 = (proj fpm).q2 by A1;
then
A8: q2 in Tf.q2 by EQREL_1:def 9;
not q1, q2-are_equivalent by A5,Def20;
hence contradiction by A4,A7,A6,A8;
end;
set Im1 = the InitS of m;
A9: fpm c= rng Tf
proof
let x be object;
assume
A10: x in fpm;
then reconsider pq=x as Subset of m;
consider q being Element of m such that
A11: q in pq by A10,FINSEQ_4:87;
pq = (proj fpm).q by A10,A11,EQREL_1:65;
then Tf.q = pq by A1;
hence thesis by FUNCT_2:4;
end;
rng Tf c= fpm by RELAT_1:def 19;
then rng Tf = fpm by A9;
then
A12: Tf is onto by FUNCT_2:def 3;
A13: the carrier of rm = fpm by Def18;
A14: now
let q be State of m, s be Element of IAlph;
reconsider Tfq = Tf.q as State of rm by Def18;
A15: (the Tran of rm).[Tfq, s] is State of rm;
Tf.q = (proj fpm).q by A1;
then
A16: q in Tf.q by EQREL_1:def 9;
then (the Tran of m).(q, s) in (the Tran of rm).(Tf.q, s) by A13,Def18;
then (the Tran of rm).[Tf.q, s] = (proj fpm).((the Tran of m).[q, s]) by
A13,A15,EQREL_1:65;
hence Tf.((the Tran of m).(q, s)) = (the Tran of rm).(Tf.q, s) by A1;
thus (the OFun of m).(q,s) = (the OFun of rm).(Tf.q, s) by A13,A16,Def18;
end;
the InitS of m in the InitS of rm by Def18;
then the InitS of rm = (proj fpm).Im1 by A13,EQREL_1:65;
then Tf.the InitS of m = the InitS of rm by A1;
hence thesis by A13,A2,A12,A14;
end;
theorem Th47:
tfsm is reduced iff ex M being finite non empty Mealy-FSM over
IAlph,OAlph st tfsm, the_reduction_of M-are_isomorphic
proof
set M = tfsm;
hereby
assume M is reduced;
then M, the_reduction_of M-are_isomorphic by Th46;
hence ex M being finite non empty Mealy-FSM over IAlph,OAlph st tfsm,
the_reduction_of M-are_isomorphic;
end;
given MM being finite non empty Mealy-FSM over IAlph,OAlph such that
A1: M, the_reduction_of MM-are_isomorphic;
set rMM = the_reduction_of MM;
consider Tf being Function of the carrier of M, the carrier of rMM such that
A2: Tf is bijective and
Tf.the InitS of M = the InitS of rMM and
A3: for q being State of M, s being Element of IAlph holds Tf.((the Tran
of M).(q, s)) = (the Tran of rMM).(Tf.q, s) & (the OFun of M).(q,s)=(the OFun
of rMM).(Tf.q, s) by A1;
let qa, qb be State of M;
assume qa <> qb;
then Tf.qa <> Tf.qb by A2,FUNCT_2:19;
then not Tf.qa, Tf.qb-are_equivalent by Th45;
hence thesis by A3,Th44;
end;
definition
let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
let IT be State of tfsm;
attr IT is accessible means
ex w st the InitS of tfsm, w-leads_to IT;
end;
definition
let IAlph, OAlph;
let IT be non empty Mealy-FSM over IAlph, OAlph;
attr IT is connected means
:Def22:
for q being State of IT holds q is accessible;
end;
registration
let IAlph, OAlph;
cluster connected for finite non empty Mealy-FSM over IAlph,OAlph;
existence
proof
set out = the Element of OAlph;
reconsider S = {1} as finite non empty set;
reconsider IS = 1 as Element of S by TARSKI:def 1;
set dF = [:S, IAlph:];
set Tr = dF --> IS;
reconsider T = Tr as Function of dF, S;
reconsider OF = dF --> out as Function of [:S, IAlph:], OAlph;
reconsider M = Mealy-FSM(#S, T, OF, IS#) as finite non empty Mealy-FSM
over IAlph, OAlph;
take M;
let q be State of M;
q = 1 & the InitS of M, <*>IAlph-leads_to the InitS of M by Th2,
TARSKI:def 1;
hence thesis;
end;
end;
reserve Ctfsm, Ctfsm1, Ctfsm2 for connected finite non empty Mealy-FSM over
IAlph, OAlph;
registration
let IAlph,OAlph,Ctfsm;
cluster the_reduction_of Ctfsm -> connected;
coherence
proof
set c = Ctfsm;
set rtfsm = the_reduction_of c;
A1: the InitS of c in the InitS of rtfsm by Def18;
assume not rtfsm is connected;
then consider Q be State of rtfsm such that
A2: not Q is accessible;
A3: the carrier of rtfsm = final_states_partition c by Def18;
then reconsider Q9 = Q as Subset of c by TARSKI:def 3;
Q in the carrier of rtfsm;
then Q9 in final_states_partition c by Def18;
then consider q be Element of c such that
A4: q in Q by FINSEQ_4:87;
q is accessible by Def22;
then consider w such that
A5: the InitS of c,w-leads_to q;
1 <= len w + 1 by NAT_1:11;
then
A6: len w + 1 in Seg (len w + 1) by FINSEQ_1:1;
then len w + 1 in Seg (len (the InitS of rtfsm,w)-admissible) by Def2;
then len w + 1 in dom (the InitS of rtfsm,w)-admissible by FINSEQ_1:def 3;
then
A7: (the InitS of rtfsm,w)-admissible.(len w + 1) in the carrier of rtfsm
by FINSEQ_2:11;
then reconsider
QQ = (the InitS of rtfsm,w)-admissible.(len w + 1) as Subset of c
by A3;
A8: Q9 = QQ or Q9 misses QQ by A3,A7,EQREL_1:def 4;
(the InitS of c,w)-admissible.(len w + 1) = q by A5;
then q in (the InitS of rtfsm,w)-admissible.(len w + 1) by A1,A6,Th40;
then the InitS of rtfsm,w-leads_to Q by A4,A8,XBOOLE_0:3;
hence contradiction by A2;
end;
end;
registration
let IAlph, OAlph;
cluster connected reduced finite for non empty Mealy-FSM over IAlph,OAlph;
existence
proof
set cm = the connected finite non empty Mealy-FSM over IAlph, OAlph;
take the_reduction_of cm;
thus thesis;
end;
end;
definition
let IAlph, OAlph;
let tfsm be non empty Mealy-FSM over IAlph,OAlph;
func accessibleStates tfsm -> set equals
{ q where q is State of tfsm : q is
accessible };
coherence;
end;
registration
let IAlph, OAlph, tfsm;
cluster accessibleStates tfsm -> finite non empty;
coherence
proof
set m = tfsm;
set AS = { q where q is State of m : q is accessible };
A1: AS c= the carrier of m
proof
let x be object;
assume x in AS;
then ex q being State of m st x = q & q is accessible;
hence thesis;
end;
the InitS of m,<*>IAlph-leads_to the InitS of m by Th2;
then the InitS of m is accessible;
then the InitS of m in AS;
hence thesis by A1;
end;
end;
theorem Th48:
accessibleStates tfsm c= the carrier of tfsm & for q holds q in
accessibleStates tfsm iff q is accessible
proof
set AS = { q where q is State of tfsm: q is accessible };
AS c= the carrier of tfsm
proof
let x be object;
assume x in AS;
then ex q being State of tfsm st x = q & q is accessible;
hence thesis;
end;
hence accessibleStates tfsm c= the carrier of tfsm;
let q be State of tfsm;
hereby
assume q in accessibleStates tfsm;
then ex q9 being State of tfsm st q9 = q & q9 is accessible;
hence q is accessible;
end;
thus thesis;
end;
theorem Th49:
(the Tran of tfsm)|[:accessibleStates tfsm, IAlph:] is Function
of [:accessibleStates tfsm, IAlph:], accessibleStates tfsm
proof
set cTran = (the Tran of tfsm) | [:accessibleStates tfsm, IAlph:];
A1: accessibleStates tfsm c= the carrier of tfsm by Th48;
then [:accessibleStates tfsm, IAlph:] c= [:the carrier of tfsm, IAlph:] by
ZFMISC_1:96;
then cTran is Function of [:accessibleStates tfsm, IAlph:], the carrier of
tfsm by FUNCT_2:32;
then
A2: dom cTran = [:accessibleStates tfsm, IAlph:] by FUNCT_2:def 1;
rng cTran c= accessibleStates tfsm
proof
set I = the InitS of tfsm;
let x be object;
assume
A3: x in rng cTran;
then consider d being object such that
A4: d in dom cTran and
A5: x = cTran.d by FUNCT_1:def 3;
A6: d`1 in accessibleStates tfsm by A2,A4,MCART_1:10;
then reconsider q = d`1 as State of tfsm by A1;
reconsider s = d`2 as Element of IAlph by A2,A4,MCART_1:10;
set qsa = (q, <*s*>)-admissible;
A7: qsa.1 = q & <*s*>.1 = s by Def2;
rng cTran c= the carrier of tfsm by RELAT_1:def 19;
then reconsider q1=x as State of tfsm by A3;
1 <= len <*s*> by FINSEQ_1:39;
then
A8: ex wi being Element of IAlph, qi, qi1 being State of tfsm st wi=<*s*>
.1 & qi=qsa.1 & qi1=qsa.(1+1) & wi-succ_of qi = qi1 by Def2;
(the Tran of tfsm).d = q1 by A2,A4,A5,FUNCT_1:49;
then
A9: qsa.(1+1) = q1 by A4,A7,A8,MCART_1:21;
1+1 =2;
then
A10: 2 <= len <*s*> + 1 by FINSEQ_1:39;
q is accessible by A6,Th48;
then consider w being FinSequence of IAlph such that
A11: I, w-leads_to q;
len (w^<*s*>) = len w + len <*s*> by FINSEQ_1:22;
then len(w^<*s*>)+1 =len w +1+1 by FINSEQ_1:39
.= len w +(1+1);
then (I, w^<*s*>)-admissible.(len (w^<*s*>) + 1) = q1 by A11,A9,A10,Th7;
then I,w^<*s*>-leads_to q1;
then q1 is accessible;
hence thesis;
end;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:4;
end;
theorem
for cTran being Function of [:accessibleStates tfsm, IAlph:],
accessibleStates tfsm, cOFun being Function of [:accessibleStates tfsm, IAlph:]
, OAlph, cInitS being Element of accessibleStates tfsm st cTran = (the Tran of
tfsm) | [:accessibleStates tfsm, IAlph:] & cOFun = (the OFun of tfsm) | [:
accessibleStates tfsm, IAlph:] & cInitS = the InitS of tfsm holds tfsm,
Mealy-FSM(#accessibleStates tfsm, cTran, cOFun, cInitS#) -are_equivalent
proof
set M = tfsm;
let cTran be Function of [:accessibleStates M, IAlph:], accessibleStates M,
cOFun be Function of [:accessibleStates M, IAlph:], OAlph, cInitS be Element of
accessibleStates M such that
A1: cTran = (the Tran of M) | [:accessibleStates M, IAlph:] and
A2: cOFun = (the OFun of M) | [:accessibleStates M, IAlph:] and
A3: cInitS = the InitS of M;
let w be FinSequence of IAlph;
set cm = Mealy-FSM(#accessibleStates M, cTran, cOFun, cInitS#);
set ma= (the InitS of M,w)-admissible;
set cma= (the InitS of cm, w)-admissible;
set mr = (the InitS of M, w)-response;
set cmr = (the InitS of cm, w)-response;
A4: now
defpred P[Nat] means $1 in dom ma implies ma.$1 = cma.$1;
thus len ma = len w + 1 & len cma = len w + 1 by Def2;
then
A5: dom ma = Seg(len w + 1) by FINSEQ_1:def 3;
A6: for k being Nat st P[k] holds P[k + 1]
proof
let j be Nat such that
A7: j in dom ma implies ma.j = cma.j;
A8: 0=j or 0<j & 0+1=1;
assume j+1 in dom ma;
then
A9: j+1<=len w + 1 by A5,FINSEQ_1:1;
then
A10: j<=len w by XREAL_1:6;
A11: j<len w +1 by A9,NAT_1:13;
per cases by A8,NAT_1:13;
suppose
A12: 0 = j;
hence ma.(j+1) = the InitS of M by Def2
.= cma.(j+1) by A3,A12,Def2;
end;
suppose
A13: 1 <= j;
then (ex mwj being Element of IAlph, mqj,mqj1 being State of M st mwj
= w.j & mqj = ma.j & mqj1 = ma.(j+1) & mwj-succ_of mqj = mqj1 )& ex cmwj being
Element of IAlph,cmqj,cmqj1 being State of cm st cmwj = w.j & cmqj = cma.j &
cmqj1 = cma.(j+1) & cmwj-succ_of cmqj=cmqj1 by A10,Def2;
hence thesis by A1,A5,A7,A11,A13,FINSEQ_1:1,FUNCT_1:49;
end;
end;
A14: P[0] by A5,FINSEQ_1:1;
thus for j be Nat holds P[j] from NAT_1:sch 2(A14, A6);
end;
then
A15: ma = cma by FINSEQ_2:9;
now
thus len mr = len w & len cmr = len w by Def6;
then
A16: dom mr = Seg len w by FINSEQ_1:def 3;
let j be Nat;
assume
A17: j in dom mr;
then
A18: j in dom w by A16,FINSEQ_1:def 3;
j in Seg (len w + 1) by A16,A17,FINSEQ_2:8;
then j in dom cma by A4,FINSEQ_1:def 3;
then
A19: cma.j in accessibleStates M by FINSEQ_2:11;
w.j in IAlph by A18,FINSEQ_2:11;
then
A20: [cma.j, w.j] in [:accessibleStates M, IAlph:] by A19,ZFMISC_1:87;
thus mr.j = (the OFun of M).[ma.j, w.j] by A18,Def6
.= cOFun.[cma.j, w.j] by A2,A15,A20,FUNCT_1:49
.= cmr.j by A18,Def6;
end;
hence thesis by FINSEQ_2:9;
end;
theorem
ex Ctfsm st the Tran of Ctfsm = (the Tran of tfsm)|[:accessibleStates
tfsm, IAlph:] & the OFun of Ctfsm = (the OFun of tfsm)|[:accessibleStates tfsm,
IAlph:] & the InitS of Ctfsm = the InitS of tfsm & tfsm, Ctfsm-are_equivalent
proof
set M = tfsm;
set I = the InitS of M;
accessibleStates M c= the carrier of M by Th48;
then [:accessibleStates M, IAlph:] c= [:the carrier of M, IAlph:] by
ZFMISC_1:96;
then reconsider cOFun = (the OFun of M) | [:accessibleStates M, IAlph:] as
Function of [:accessibleStates M, IAlph:], OAlph by FUNCT_2:32;
I, <*>IAlph-leads_to I by Th2;
then I is accessible;
then reconsider cInitS = the InitS of M as Element of accessibleStates M by
Th48;
reconsider cTran = (the Tran of M) | [:accessibleStates M, IAlph:] as
Function of [:accessibleStates M,IAlph:],accessibleStates M by Th49;
set cm = Mealy-FSM(#accessibleStates M, cTran, cOFun, cInitS#);
A1: now
let w be FinSequence of IAlph;
set ma= (the InitS of M,w)-admissible;
set cma= (the InitS of cm,w)-admissible;
now
defpred P[Nat] means $1 in dom ma implies ma.$1 = cma.$1;
thus len ma = len w + 1 & len cma = len w + 1 by Def2;
then
A2: dom ma = Seg (len w + 1) by FINSEQ_1:def 3;
A3: for k being Nat st P[k] holds P[k + 1]
proof
let j be Nat such that
A4: j in dom ma implies ma.j = cma.j;
A5: 0=j or 0<j & 0+1 = 1;
assume j+1 in dom ma;
then
A6: j+1<=len w +1 by A2,FINSEQ_1:1;
then
A7: j<=len w by XREAL_1:6;
A8: j<len w +1 by A6,NAT_1:13;
per cases by A5,NAT_1:13;
suppose
A9: 0 = j;
hence ma.(j+1) = the InitS of M by Def2
.= cma.(j+1) by A9,Def2;
end;
suppose
A10: 1 <= j;
then (ex mwj being Element of IAlph, mqj,mqj1 being State of M st
mwj = w.j & mqj = ma.j & mqj1 = ma.(j+1) & mwj-succ_of mqj = mqj1 )& ex cmwj
being Element of IAlph, cmqj, cmqj1 being State of cm st cmwj = w.j & cmqj =
cma.j & cmqj1 = cma.(j+1) & cmwj-succ_of cmqj=cmqj1 by A7,Def2;
hence thesis by A2,A4,A8,A10,FINSEQ_1:1,FUNCT_1:49;
end;
end;
A11: P[0] by A2,FINSEQ_1:1;
thus for j be Nat holds P[j] from NAT_1:sch 2(A11, A3);
end;
hence ma = cma by FINSEQ_2:9;
end;
now
let q be State of cm;
q in accessibleStates M & accessibleStates M c= the carrier of M by Th48;
then reconsider q9 = q as State of M;
q9 is accessible by Th48;
then consider w being FinSequence of IAlph such that
A12: the InitS of M, w-leads_to q9;
(the InitS of M, w)-admissible.(len w + 1) = q9 by A12;
then (the InitS of cm, w)-admissible.(len w + 1) = q by A1;
then the InitS of cm, w-leads_to q;
hence q is accessible;
end;
then reconsider
cm as connected finite non empty Mealy-FSM over IAlph, OAlph by Def22;
take cm;
thus the Tran of cm = (the Tran of M) | [:accessibleStates M, IAlph:];
thus the OFun of cm = (the OFun of M) | [:accessibleStates M, IAlph:];
thus the InitS of cm = the InitS of M;
let w be FinSequence of IAlph;
set ma= (the InitS of M,w)-admissible;
set cma= (the InitS of cm,w)-admissible;
set mr = (the InitS of M, w)-response;
set cmr = (the InitS of cm, w)-response;
A13: len cma = len w + 1 by Def2;
now
thus len mr = len w & len cmr = len w by Def6;
then
A14: dom mr = Seg len w by FINSEQ_1:def 3;
let j be Nat;
assume
A15: j in dom mr;
then
A16: j in dom w by A14,FINSEQ_1:def 3;
j in Seg (len w + 1) by A14,A15,FINSEQ_2:8;
then j in dom cma by A13,FINSEQ_1:def 3;
then
A17: cma.j in accessibleStates M by FINSEQ_2:11;
w.j in IAlph by A16,FINSEQ_2:11;
then
A18: [cma.j, w.j] in [:accessibleStates M, IAlph:] by A17,ZFMISC_1:87;
A19: [ma.j, w.j] = [cma.j, w.j] by A1;
thus mr.j = (the OFun of M).[ma.j, w.j] by A16,Def6
.= cOFun.[cma.j, w.j] by A19,A18,FUNCT_1:49
.= cmr.j by A16,Def6;
end;
hence thesis by FINSEQ_2:9;
end;
begin :: Machine union
definition
let IAlph be set, OAlph be non empty set;
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph, OAlph;
func tfsm1-Mealy_union tfsm2 -> strict Mealy-FSM over IAlph, OAlph means
:
Def24: the carrier of it = (the carrier of tfsm1) \/ (the carrier of tfsm2) &
the Tran of it = (the Tran of tfsm1) +* (the Tran of tfsm2) & the OFun of it =
(the OFun of tfsm1) +* (the OFun of tfsm2) & the InitS of it = the InitS of
tfsm1;
existence
proof
set Oftfsm1 = the OFun of tfsm1, Oftfsm2 = the OFun of tfsm2;
set Trtfsm1 = the Tran of tfsm1, Trtfsm2 = the Tran of tfsm2;
set Stfsm1 = the carrier of tfsm1, Stfsm2 = the carrier of tfsm2;
set Tr = Trtfsm1 +* Trtfsm2, Of = Oftfsm1 +* Oftfsm2;
reconsider S = Stfsm1 \/ Stfsm2 as non empty set;
rng Trtfsm1 c= Stfsm1 & rng Trtfsm2 c= Stfsm2 by RELAT_1:def 19;
then
A1: rng Tr c= rng Trtfsm1 \/ rng Trtfsm2 & rng Trtfsm1 \/ rng Trtfsm2 c=
Stfsm1 \/ Stfsm2 by FUNCT_4:17,XBOOLE_1:13;
dom Oftfsm1 = [: Stfsm1, IAlph :] & dom Oftfsm2 = [: Stfsm2, IAlph :]
by FUNCT_2:def 1;
then
A2: dom Of = [: Stfsm1, IAlph :] \/ [: Stfsm2, IAlph :] by FUNCT_4:def 1
.= [: Stfsm1 \/ Stfsm2, IAlph :] by ZFMISC_1:97;
rng Oftfsm1 c= OAlph & rng Oftfsm2 c= OAlph by RELAT_1:def 19;
then rng Of c= rng Oftfsm1 \/ rng Oftfsm2 & rng Oftfsm1 \/ rng Oftfsm2 c=
OAlph \/ OAlph by FUNCT_4:17,XBOOLE_1:13;
then reconsider Of as Function of [: S, IAlph :], OAlph by A2,FUNCT_2:2
,XBOOLE_1:1;
dom Trtfsm1 = [: Stfsm1, IAlph :] & dom Trtfsm2 = [: Stfsm2, IAlph :]
by FUNCT_2:def 1;
then dom Tr = [: Stfsm1, IAlph :] \/ [: Stfsm2, IAlph :] by FUNCT_4:def 1
.= [: Stfsm1 \/ Stfsm2, IAlph :] by ZFMISC_1:97;
then reconsider Tr as Function of [: S, IAlph :], S by A1,FUNCT_2:2
,XBOOLE_1:1;
reconsider IS = the InitS of tfsm1 as Element of S by XBOOLE_0:def 3;
take Mealy-FSM (# S, Tr, Of, IS #);
thus thesis;
end;
uniqueness;
end;
registration
let IAlph be set, OAlph be non empty set;
let tfsm1, tfsm2 be non empty finite Mealy-FSM over IAlph, OAlph;
cluster tfsm1-Mealy_union tfsm2 -> non empty finite;
coherence
proof
the carrier of tfsm1-Mealy_union tfsm2 = (the carrier of tfsm1) \/ (
the carrier of tfsm2) by Def24;
hence thesis;
end;
end;
theorem Th52:
tfsm = tfsm1-Mealy_union tfsm2 & the carrier of tfsm1 misses the
carrier of tfsm2 & q11 = q implies (q11,w)-admissible = (q,w)-admissible
proof
assume that
A1: tfsm = tfsm1-Mealy_union tfsm2 and
A2: (the carrier of tfsm1) misses (the carrier of tfsm2) and
A3: q11 = q;
set ad1 = (q11,w)-admissible, ad = (q,w)-admissible;
defpred P[Nat] means 1 <= $1 & $1 <= len ad1 implies ad1.$1 = ad.$1;
A4: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A5: 1 <= k & k <= len ad1 implies ad1.k = ad.k;
assume that
1 <= (k+1) and
A6: (k+1) <= len ad1;
A7: k = 0 or 0 < k & 0 + 1 = 1;
per cases by A7,NAT_1:13;
suppose
A8: k = 0;
hence ad1.(k+1) = q11 by Def2
.= ad.(k+1) by A3,A8,Def2;
end;
suppose
A9: 1 <= k;
(k+1) <= len w + 1 by A6,Def2;
then
A10: k <= len w by XREAL_1:6;
then consider
w1k being Element of IAlph, q1k, q1k1 being Element of tfsm1
such that
A11: w1k = w.k & q1k = ad1.k and
A12: q1k1 = ad1.(k+1) & w1k-succ_of q1k = q1k1 by A9,Def2;
A13: ex wk being Element of IAlph, qk, qk1 being Element of tfsm st wk =
w.k & qk = ad.k & qk1 = ad.(k+1) & wk-succ_of qk = qk1 by A9,A10,Def2;
len w <= len w + 1 by NAT_1:11;
then
A14: k <= len w + 1 by A10,XXREAL_0:2;
[:the carrier of tfsm1, IAlph :] misses [:the carrier of tfsm2,
IAlph :] by A2,ZFMISC_1:104;
then
dom (the Tran of tfsm2) = [:the carrier of tfsm2,IAlph:] & not [q1k
,w1k] in [:the carrier of tfsm2,IAlph:] by FUNCT_2:def 1,XBOOLE_0:3;
hence ad1.(k+1) = ((the Tran of tfsm1) +* (the Tran of tfsm2)).[q1k,w1k]
by A12,FUNCT_4:11
.= ad.(k+1) by A1,A5,A9,A11,A13,A14,Def2,Def24;
end;
end;
A15: P[0];
A16: for k being Nat holds P[k] from NAT_1:sch 2(A15, A4);
len ad1 = len w + 1 by Def2
.= len ad by Def2;
hence thesis by A16,FINSEQ_1:14;
end;
theorem Th53:
tfsm = tfsm1-Mealy_union tfsm2 & the carrier of tfsm1 misses the
carrier of tfsm2 & q11 = q implies (q11,w)-response = (q,w)-response
proof
set q1 = q11;
assume that
A1: tfsm = tfsm1-Mealy_union tfsm2 and
A2: (the carrier of tfsm1) misses (the carrier of tfsm2) and
A3: q1 = q;
set ad1 = (q1,w)-admissible;
set res = (q,w)-response, res1 = (q1,w)-response;
A4: len res1 = len w by Def6;
A5: now
let k be Nat;
A6: [:the carrier of tfsm1,IAlph :] misses [:the carrier of tfsm2,IAlph:]
by A2,ZFMISC_1:104;
assume 1 <= k & k <= len res1;
then
A7: k in Seg len w by A4,FINSEQ_1:1;
then
A8: k in dom w by FINSEQ_1:def 3;
k in Seg (len w + 1) by A7,FINSEQ_2:8;
then k in Seg len ad1 by Def2;
then k in dom ad1 by FINSEQ_1:def 3;
then
A9: ad1.k in the carrier of tfsm1 by FINSEQ_2:11;
w.k in IAlph by A8,FINSEQ_2:11;
then [ad1.k,w.k] in [: the carrier of tfsm1, IAlph :] by A9,ZFMISC_1:87;
then
A10: dom (the OFun of tfsm2) = [:the carrier of tfsm2,IAlph :] & not [ad1.
k,w.k] in [: the carrier of tfsm2, IAlph :] by A6,FUNCT_2:def 1,XBOOLE_0:3;
res1.k = (the OFun of tfsm1).[(q1,w)-admissible.k,w.k] by A8,Def6
.= ((the OFun of tfsm1) +* (the OFun of tfsm2)).[ad1.k,w.k] by A10,
FUNCT_4:11
.= ((the OFun of tfsm1) +* (the OFun of tfsm2)). [(q,w)-admissible.k,w
.k] by A1,A2,A3,Th52
.= (the OFun of tfsm).[(q,w)-admissible.k, w.k] by A1,Def24
.= res.k by A8,Def6;
hence res1.k = res.k;
end;
len res1 = len w by Def6
.= len res by Def6;
hence thesis by A5,FINSEQ_1:14;
end;
theorem Th54:
tfsm = tfsm1-Mealy_union tfsm2 & q21 = q implies (q21,w)
-admissible = (q,w)-admissible
proof
set q9 = q21;
assume that
A1: tfsm = tfsm1-Mealy_union tfsm2 and
A2: q9 = q;
set ad9 = (q9,w)-admissible, ad = (q,w)-admissible;
defpred P[Nat] means 1<=$1 & $1 <= len ad9 implies ad9.$1= ad.$1;
A3: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A4: 1 <= k & k <= len ad9 implies ad9.k = ad.k;
assume that
1 <= (k+1) and
A5: (k+1) <= len ad9;
A6: k = 0 or 0 < k & 0 + 1 = 1;
per cases by A6,NAT_1:13;
suppose
A7: k = 0;
hence ad9.(k+1) = q9 by Def2
.= ad.(k+1) by A2,A7,Def2;
end;
suppose
A8: 1 <= k;
k+1 <= len w + 1 by A5,Def2;
then
A9: k <= len w by XREAL_1:6;
then consider
w9k being Element of IAlph, q9k, q9k1 being Element of tfsm2
such that
A10: w9k = w.k & q9k = ad9.k and
A11: q9k1 = ad9.(k+1) & w9k-succ_of q9k = q9k1 by A8,Def2;
A12: ex wk being Element of IAlph, qk, qk1 being Element of tfsm st wk =
w.k & qk = ad.k & qk1 = ad.(k+1) & wk-succ_of qk = qk1 by A8,A9,Def2;
len w <= len w + 1 by NAT_1:11;
then
A13: k <= len w + 1 by A9,XXREAL_0:2;
dom (the Tran of tfsm2) = [:the carrier of tfsm2,IAlph:]by FUNCT_2:def 1;
hence ad9.(k+1) = ((the Tran of tfsm1) +* (the Tran of tfsm2)).[q9k,w9k]
by A11,FUNCT_4:13
.= ad.(k+1) by A1,A4,A8,A10,A12,A13,Def2,Def24;
end;
end;
A14: P[0];
A15: for k being Nat holds P[k] from NAT_1:sch 2(A14, A3);
len ad9 = len w + 1 by Def2
.= len ad by Def2;
hence thesis by A15,FINSEQ_1:14;
end;
theorem Th55:
tfsm = tfsm1-Mealy_union tfsm2 & q21 = q implies (q21,w)
-response = (q,w)-response
proof
set q9 = q21;
assume that
A1: tfsm = tfsm1-Mealy_union tfsm2 and
A2: q9 = q;
set ad9 = (q9,w)-admissible;
set res = (q,w)-response, res9 = (q9,w)-response;
A3: len res9 = len w by Def6;
A4: now
let k be Nat;
assume 1 <= k & k <= len res9;
then
A5: k in Seg len w by A3,FINSEQ_1:1;
then
A6: k in dom w by FINSEQ_1:def 3;
k in Seg (len w + 1) by A5,FINSEQ_2:8;
then k in Seg len ad9 by Def2;
then k in dom ad9 by FINSEQ_1:def 3;
then
A7: ad9.k in the carrier of tfsm2 by FINSEQ_2:11;
dom (the OFun of tfsm2) = [:the carrier of tfsm2,IAlph:] & w.k in
IAlph by A6,FINSEQ_2:11,FUNCT_2:def 1;
then
A8: [ad9.k, w.k ] in dom (the OFun of tfsm2) by A7,ZFMISC_1:87;
res9.k = (the OFun of tfsm2).[(q9,w)-admissible.k,w.k] by A6,Def6
.= ((the OFun of tfsm1) +* (the OFun of tfsm2)).[ad9.k,w.k] by A8,
FUNCT_4:13
.= ((the OFun of tfsm1) +* (the OFun of tfsm2)). [(q,w)-admissible.k,w
.k] by A1,A2,Th54
.= (the OFun of tfsm).[(q,w)-admissible.k, w.k] by A1,Def24
.= res.k by A6,Def6;
hence res9.k = res.k;
end;
len res9 = len w by Def6
.= len res by Def6;
hence thesis by A4,FINSEQ_1:14;
end;
reserve Rtfsm1, Rtfsm2 for reduced non empty Mealy-FSM over IAlph, OAlph;
theorem Th56:
tfsm = Rtfsm1-Mealy_union Rtfsm2 & the carrier of Rtfsm1 misses
the carrier of Rtfsm2 & Rtfsm1, Rtfsm2-are_equivalent implies ex Q being State
of the_reduction_of tfsm st the InitS of Rtfsm1 in Q & the InitS of Rtfsm2 in Q
& Q = the InitS of the_reduction_of tfsm
proof
set rtfsm1 = Rtfsm1;
set rtfsm2 = Rtfsm2;
assume that
A1: tfsm = rtfsm1-Mealy_union rtfsm2 and
A2: (the carrier of rtfsm1) misses (the carrier of rtfsm2) and
A3: rtfsm1, rtfsm2-are_equivalent;
set Srtfsm2 = the carrier of rtfsm2;
set Stfsm = the carrier of tfsm, Srtfsm1 = the carrier of rtfsm1;
Stfsm = Srtfsm1 \/ Srtfsm2 by A1,Def24;
then reconsider IS2 = the InitS of rtfsm2 as Element of Stfsm by
XBOOLE_0:def 3;
reconsider IS1 = the InitS of rtfsm1 as Element of Stfsm by A1,Def24;
now
let w be FinSequence of IAlph;
(the InitS of rtfsm1,w)-response = (the InitS of rtfsm2,w)-response by A3;
hence (IS1, w)-response = (the InitS of rtfsm2,w)-response by A1,A2,Th53
.= (IS2, w)-response by A1,Th55;
end;
then
A4: IS1,IS2-are_equivalent;
set RUN = the_reduction_of tfsm;
the InitS of tfsm = the InitS of rtfsm1 by A1,Def24;
then
A5: the InitS of rtfsm1 in the InitS of RUN by Def18;
set SRUN = the carrier of RUN;
A6: SRUN = final_states_partition tfsm by Def18;
final_states_partition tfsm is final by Def15;
then consider X being Element of SRUN such that
A7: IS1 in X and
A8: IS2 in X by A6,A4;
take X;
thus the InitS of rtfsm1 in X & the InitS of rtfsm2 in X by A7,A8;
X is Subset of Stfsm & the InitS of RUN is Subset of Stfsm by A6,TARSKI:def 3
;
then X = the InitS of RUN or X misses the InitS of RUN by A6,EQREL_1:def 4;
hence thesis by A7,A5,XBOOLE_0:3;
end;
reserve CRtfsm1, CRtfsm2 for connected reduced non empty Mealy-FSM over IAlph
, OAlph,
q1u, q2u for State of tfsm;
theorem Th57:
for crq11, crq12 being State of CRtfsm1 holds crq11 = q1u &
crq12 = q2u & the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm =
CRtfsm1-Mealy_union CRtfsm2 & not crq11, crq12-are_equivalent implies not q1u,
q2u-are_equivalent
proof
let crq11, crq12 be State of CRtfsm1;
set rtfsm1 = CRtfsm1, rtfsm2 = CRtfsm2, q1 = crq11, q2 = crq12;
assume that
A1: q1 = q1u and
A2: q2 = q2u and
A3: (the carrier of rtfsm1) misses (the carrier of rtfsm2) & tfsm =
rtfsm1 -Mealy_union rtfsm2;
assume not q1,q2-are_equivalent;
then consider w be FinSequence of IAlph such that
A4: (q1,w)-response <> (q2,w)-response;
(q1u,w)-response = (q1,w)-response by A1,A3,Th53;
then (q1u,w)-response <> (q2u,w)-response by A2,A3,A4,Th53;
hence thesis;
end;
theorem Th58:
for crq21, crq22 being State of CRtfsm2 holds crq21 = q1u &
crq22 = q2u & tfsm = CRtfsm1-Mealy_union CRtfsm2 & not crq21, crq22
-are_equivalent implies not q1u, q2u-are_equivalent
proof
let crq21, crq22 be State of CRtfsm2;
set rtfsm1 = CRtfsm1, rtfsm2 = CRtfsm2, q1 = crq21, q2 = crq22;
assume that
A1: q1 = q1u and
A2: q2 = q2u and
A3: tfsm = rtfsm1-Mealy_union rtfsm2;
assume not q1,q2-are_equivalent;
then consider w be FinSequence of IAlph such that
A4: (q1,w)-response <> (q2,w)-response;
(q1u,w)-response = (q1,w)-response by A1,A3,Th55;
then (q1u,w)-response <> (q2u,w)-response by A2,A3,A4,Th55;
hence thesis;
end;
reserve CRtfsm1, CRtfsm2 for connected reduced finite non empty Mealy-FSM
over IAlph, OAlph;
theorem Th59:
the carrier of CRtfsm1 misses the carrier of CRtfsm2 & tfsm =
CRtfsm1-Mealy_union CRtfsm2 implies for Q being State of the_reduction_of tfsm
holds not ex q1, q2 being Element of Q st q1 in the carrier of CRtfsm1 & q2 in
the carrier of CRtfsm1 & q1 <> q2
proof
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume that
A1: (the carrier of rtfsm1) misses (the carrier of rtfsm2) and
A2: tfsm = rtfsm1-Mealy_union rtfsm2;
given Q be Element of the_reduction_of tfsm, q1, q2 being Element of Q such
that
A3: q1 in the carrier of rtfsm1 & q2 in the carrier of rtfsm1 and
A4: q1 <> q2;
consider tfsm1 be finite non empty Mealy-FSM over IAlph, OAlph such that
A5: rtfsm1, the_reduction_of tfsm1-are_isomorphic by Th47;
set tfsm1r = the_reduction_of tfsm1;
consider Tf being Function of the carrier of rtfsm1, the carrier of tfsm1r
such that
A6: Tf is bijective and
Tf.the InitS of rtfsm1 = the InitS of tfsm1r and
A7: for q being State of rtfsm1, s being Element of IAlph holds Tf.((the
Tran of rtfsm1).(q, s)) = (the Tran of tfsm1r).(Tf.q, s) & (the OFun of rtfsm1)
.(q,s) = (the OFun of tfsm1r).(Tf.q, s) by A5;
A8: dom Tf = the carrier of rtfsm1 by FUNCT_2:def 1;
then
A9: Tf.q1 <> Tf.q2 by A3,A4,A6,FUNCT_1:def 4;
rng Tf=the carrier of tfsm1r by A6,FUNCT_2:def 3;
then reconsider Tq1 = Tf.q1, Tq2 = Tf.q2 as Element of tfsm1r by A3,A8,
FUNCT_1:def 3;
the carrier of tfsm = (the carrier of rtfsm1) \/ (the carrier of rtfsm2
) by A2,Def24;
then reconsider q1, q2 as Element of tfsm by A3,XBOOLE_0:def 3;
reconsider q19 = q1, q29 = q2 as Element of rtfsm1 by A3;
not Tq1, Tq2 -are_equivalent by A9,Th45;
then
A10: not q19,q29-are_equivalent by A7,Th44;
set rtfsm = the_reduction_of tfsm;
A11: final_states_partition tfsm is final by Def15;
A12: the carrier of rtfsm = final_states_partition tfsm by Def18;
then reconsider Q as Subset of tfsm by TARSKI:def 3;
q1,q2-are_equivalent by A11,A12;
hence contradiction by A1,A2,A10,Th57;
end;
theorem Th60:
tfsm = CRtfsm1-Mealy_union CRtfsm2 implies for Q being State of
the_reduction_of tfsm holds not ex q1, q2 being Element of Q st q1 in the
carrier of CRtfsm2 & q2 in the carrier of CRtfsm2 & q1 <> q2
proof
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
set rtfsm = the_reduction_of tfsm;
consider tfsm2 be finite non empty Mealy-FSM over IAlph, OAlph such that
A1: rtfsm2, the_reduction_of tfsm2-are_isomorphic by Th47;
set tfsm2r = the_reduction_of tfsm2;
consider Tf being Function of the carrier of rtfsm2, the carrier of tfsm2r
such that
A2: Tf is bijective and
Tf.the InitS of rtfsm2 = the InitS of tfsm2r and
A3: for q being State of rtfsm2, s being Element of IAlph holds Tf.((the
Tran of rtfsm2).(q, s)) = (the Tran of tfsm2r).(Tf.q, s) & (the OFun of rtfsm2)
.(q,s) = (the OFun of tfsm2r).(Tf.q, s) by A1;
assume
A4: tfsm = rtfsm1-Mealy_union rtfsm2;
then
A5: the carrier of tfsm = (the carrier of rtfsm1) \/ (the carrier of rtfsm2
) by Def24;
given Q be Element of the_reduction_of tfsm, q1, q2 being Element of Q such
that
A6: q1 in the carrier of rtfsm2 and
A7: q2 in the carrier of rtfsm2 and
A8: q1 <> q2;
A9: dom Tf = the carrier of rtfsm2 by FUNCT_2:def 1;
then
A10: Tf.q1 <> Tf.q2 by A6,A7,A8,A2,FUNCT_1:def 4;
rng Tf=the carrier of tfsm2r by A2,FUNCT_2:def 3;
then reconsider Tq1 = Tf.q1, Tq2 = Tf.q2 as Element of tfsm2r by A6,A7,A9,
FUNCT_1:def 3;
reconsider q2 as Element of tfsm by A7,A5,XBOOLE_0:def 3;
reconsider q29 = q2 as Element of rtfsm2 by A7;
reconsider q1 as Element of tfsm by A6,A5,XBOOLE_0:def 3;
reconsider q19 = q1 as Element of rtfsm2 by A6;
not Tq1, Tq2 -are_equivalent by A10,Th45;
then
A11: not q19,q29-are_equivalent by A3,Th44;
A12: the carrier of rtfsm = final_states_partition tfsm by Def18;
then reconsider Q as Subset of tfsm by TARSKI:def 3;
A13: final_states_partition tfsm is final by Def15;
q1,q2-are_equivalent by A13,A12;
hence contradiction by A4,A11,Th58;
end;
theorem Th61:
the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,
CRtfsm2-are_equivalent & tfsm = CRtfsm1-Mealy_union CRtfsm2 implies for Q being
State of the_reduction_of tfsm ex q1, q2 being Element of Q st q1 in the
carrier of CRtfsm1 & q2 in the carrier of CRtfsm2 & for q being Element of Q
holds q = q1 or q = q2
proof
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume that
A1: (the carrier of rtfsm1) misses (the carrier of rtfsm2) and
A2: rtfsm1, rtfsm2-are_equivalent and
A3: tfsm = rtfsm1-Mealy_union rtfsm2;
set ISrtfsm2 = the InitS of rtfsm2;
set ISrtfsm1 = the InitS of rtfsm1;
A4: (the carrier of rtfsm1) /\ (the carrier of rtfsm2) = {} by A1;
set Stfsm = the carrier of tfsm;
set Srtfsm2 = the carrier of rtfsm2;
set Srtfsm1 = the carrier of rtfsm1;
set rtfsm = the_reduction_of tfsm;
set Srtfsm = the carrier of rtfsm;
assume not thesis;
then consider Q be Element of the_reduction_of tfsm such that
A5: for q1, q2 being Element of Q holds not q1 in the carrier of rtfsm1
or not q2 in the carrier of rtfsm2 or not for q being Element of Q holds q = q1
or q = q2;
A6: Srtfsm = final_states_partition tfsm by Def18;
then reconsider Q as Subset of Stfsm by TARSKI:def 3;
union final_states_partition tfsm = Stfsm by EQREL_1:def 4
.= Srtfsm1 \/ Srtfsm2 by A3,Def24;
then
A7: Q c= Srtfsm1 \/ Srtfsm2 by A6,ZFMISC_1:74;
Q in Srtfsm;
then
A8: Q in final_states_partition tfsm by Def18;
then
A9: Q <> {};
then consider q being Element of Stfsm such that
A10: q in Q by SUBSET_1:4;
per cases by A10,A7,XBOOLE_0:def 3;
suppose
A11: q in Srtfsm1;
set Q9 = Q \ {q};
A12: now
A13: Q9 c= Q by XBOOLE_1:36;
reconsider Q as Subset of Stfsm;
assume
A14: Q9 <> {};
reconsider Q9 as Subset of Stfsm;
consider x being Element of Stfsm such that
A15: x in Q9 by A14,SUBSET_1:4;
A16: Q9 c= Srtfsm1 \/ Srtfsm2 by A7,A13;
per cases by A15,A16,XBOOLE_0:def 3;
suppose
A17: x in Srtfsm1;
reconsider x as Element of Q by A15,XBOOLE_0:def 5;
reconsider q as Element of Q by A10;
not q in Srtfsm1 or not x in Srtfsm1 or q = x by A1,A3,Th59;
hence contradiction by A11,A15,A17,ZFMISC_1:56;
end;
suppose
A18: x in Srtfsm2;
set Q99 = Q9 \ {x};
A19: now
A20: Q99 c= Q9 by XBOOLE_1:36;
reconsider Q9 as Subset of Stfsm;
assume
A21: Q99 <> {};
reconsider Q99 as Subset of Stfsm;
consider y being Element of Stfsm such that
A22: y in Q99 by A21,SUBSET_1:4;
A23: Q99 c= Srtfsm1 \/ Srtfsm2 by A16,A20;
per cases by A22,A23,XBOOLE_0:def 3;
suppose
A24: y in Srtfsm1;
reconsider q as Element of Q by A10;
A25: y in Q9 by A22,ZFMISC_1:56;
then reconsider y as Element of Q by ZFMISC_1:56;
not q in Srtfsm1 or not y in Srtfsm1 or q = y by A1,A3,Th59;
hence contradiction by A11,A24,A25,ZFMISC_1:56;
end;
suppose
A26: y in Srtfsm2;
reconsider x as Element of Q by A15,ZFMISC_1:56;
y in Q9 by A22,ZFMISC_1:56;
then reconsider y as Element of Q by ZFMISC_1:56;
not x in Srtfsm2 or not y in Srtfsm2 or x = y by A3,Th60;
hence contradiction by A18,A22,A26,ZFMISC_1:56;
end;
end;
now
assume
A27: Q99 = {};
A28: for z being Element of Q holds z = q or z = x
proof
given z being Element of Q such that
A29: z <> q and
A30: z <> x;
z in Q9 by A9,A29,ZFMISC_1:56;
hence contradiction by A27,A30,ZFMISC_1:56;
end;
reconsider x as Element of Q by A15,ZFMISC_1:56;
reconsider q as Element of Q by A10;
not q in Srtfsm1 or not x in Srtfsm2 or ex z being Element of Q
st z <> q & z <> x by A5;
hence contradiction by A11,A18,A28;
end;
hence contradiction by A19;
end;
end;
now
reconsider q as Element of Srtfsm1 by A11;
q is accessible by Def22;
then consider w be FinSequence of IAlph such that
A31: ISrtfsm1, w-leads_to q;
set adl = ISrtfsm2 leads_to_under w;
A32: now
reconsider q as Element of Stfsm;
assume
A33: not adl in Q;
reconsider q1 = q as Element of Srtfsm1;
adl in Srtfsm1 \/ Srtfsm2 by XBOOLE_0:def 3;
then reconsider adl as Element of Stfsm by A3,Def24;
A34: not ex Y being Element of Srtfsm st q in Y & adl in Y
proof
reconsider Q as Subset of Stfsm;
assume not thesis;
then consider Y be Element of Srtfsm such that
A35: q in Y and
A36: adl in Y;
reconsider Y as Subset of Stfsm by A6,TARSKI:def 3;
Y in Srtfsm;
then Y in final_states_partition tfsm by Def18;
then Y misses Q by A8,A33,A36,EQREL_1:def 4;
hence contradiction by A10,A35,XBOOLE_0:3;
end;
reconsider adl2 = adl as Element of Srtfsm2;
final_states_partition tfsm is final by Def15;
then not q, adl-are_equivalent by A6,A34;
then consider dseq being FinSequence of IAlph such that
A37: (q,dseq)-response <> (adl,dseq)-response;
(q,dseq)-response = (q1,dseq)-response by A1,A3,Th53;
then
A38: (q1,dseq)-response <> (adl2,dseq)-response by A3,A37,Th55;
ISrtfsm2, w -leads_to adl2 by Def5;
then (ISrtfsm1,w^dseq)-response <> (ISrtfsm2,w^dseq)-response by A31
,A38,Th12;
hence contradiction by A2;
end;
assume
A39: Q9 = {};
now
assume
A40: adl in Q;
adl <> q by A4,XBOOLE_0:def 4;
hence contradiction by A39,A40,ZFMISC_1:56;
end;
hence contradiction by A32;
end;
hence contradiction by A12;
end;
suppose
A41: q in Srtfsm2;
set Q9 = Q \ {q};
A42: now
A43: Q9 c= Q by XBOOLE_1:36;
reconsider Q as Subset of Stfsm;
assume
A44: Q9 <> {};
reconsider Q9 as Subset of Stfsm;
consider x being Element of Stfsm such that
A45: x in Q9 by A44,SUBSET_1:4;
A46: Q9 c= Srtfsm1 \/ Srtfsm2 by A7,A43;
per cases by A45,A46,XBOOLE_0:def 3;
suppose
A47: x in Srtfsm1;
set Q99 = Q9 \ {x};
A48: now
A49: Q99 c= Q9 by XBOOLE_1:36;
reconsider Q9 as Subset of Stfsm;
assume
A50: Q99 <> {};
reconsider Q99 as Subset of Stfsm;
consider y being Element of Stfsm such that
A51: y in Q99 by A50,SUBSET_1:4;
A52: Q99 c= Srtfsm1 \/ Srtfsm2 by A46,A49;
per cases by A51,A52,XBOOLE_0:def 3;
suppose
A53: y in Srtfsm1;
reconsider x as Element of Q by A45,ZFMISC_1:56;
y in Q9 by A51,ZFMISC_1:56;
then reconsider y as Element of Q by ZFMISC_1:56;
not x in Srtfsm1 or not y in Srtfsm1 or x = y by A1,A3,Th59;
hence contradiction by A47,A51,A53,ZFMISC_1:56;
end;
suppose
A54: y in Srtfsm2;
reconsider q as Element of Q by A10;
A55: y in Q9 by A51,ZFMISC_1:56;
then reconsider y as Element of Q by ZFMISC_1:56;
not q in Srtfsm2 or not y in Srtfsm2 or q = y by A3,Th60;
hence contradiction by A41,A54,A55,ZFMISC_1:56;
end;
end;
now
assume
A56: Q99 = {};
A57: for z being Element of Q holds z = q or z = x
proof
given z being Element of Q such that
A58: z <> q and
A59: z <> x;
z in Q9 by A9,A58,ZFMISC_1:56;
hence contradiction by A56,A59,ZFMISC_1:56;
end;
reconsider x as Element of Q by A45,ZFMISC_1:56;
reconsider q as Element of Q by A10;
not x in Srtfsm1 or not q in Srtfsm2 or ex z being Element of
Q st z <> x & z <> q by A5;
hence contradiction by A41,A47,A57;
end;
hence contradiction by A48;
end;
suppose
A60: x in Srtfsm2;
reconsider x as Element of Q by A45,XBOOLE_0:def 5;
reconsider q as Element of Q by A10;
not q in Srtfsm2 or not x in Srtfsm2 or q = x by A3,Th60;
hence contradiction by A41,A45,A60,ZFMISC_1:56;
end;
end;
now
reconsider q as Element of Srtfsm2 by A41;
q is accessible by Def22;
then consider w be FinSequence of IAlph such that
A61: ISrtfsm2, w-leads_to q;
set adl = ISrtfsm1 leads_to_under w;
A62: now
reconsider q as Element of Stfsm;
assume
A63: not adl in Q;
reconsider q1 = q as Element of Srtfsm2;
adl in Srtfsm1 \/ Srtfsm2 by XBOOLE_0:def 3;
then reconsider adl as Element of Stfsm by A3,Def24;
A64: not ex Y being Element of Srtfsm st q in Y & adl in Y
proof
assume not thesis;
then consider Y be Element of Srtfsm such that
A65: q in Y and
A66: adl in Y;
reconsider Y as Subset of Stfsm by A6,TARSKI:def 3;
Y in Srtfsm;
then Y in final_states_partition tfsm by Def18;
then Y misses Q by A8,A63,A66,EQREL_1:def 4;
hence contradiction by A10,A65,XBOOLE_0:3;
end;
reconsider adl2 = adl as Element of Srtfsm1;
final_states_partition tfsm is final by Def15;
then not q, adl-are_equivalent by A6,A64;
then consider dseq being FinSequence of IAlph such that
A67: (q,dseq)-response <> (adl,dseq)-response;
(q,dseq)-response = (q1,dseq)-response by A3,Th55;
then
A68: (q1,dseq)-response <> (adl2,dseq)-response by A1,A3,A67,Th53;
ISrtfsm1, w -leads_to adl2 by Def5;
then (ISrtfsm2,w^dseq)-response <> (ISrtfsm1,w^dseq)-response by A61
,A68,Th12;
hence contradiction by A2;
end;
assume
A69: Q9 = {};
now
assume
A70: adl in Q;
adl <> q by A1,XBOOLE_0:3;
hence contradiction by A69,A70,ZFMISC_1:56;
end;
hence contradiction by A62;
end;
hence contradiction by A42;
end;
end;
begin :: The minimization theorem
theorem Th62:
for tfsm1, tfsm2 being finite non empty Mealy-FSM over IAlph,
OAlph ex fsm1, fsm2 being finite non empty Mealy-FSM over IAlph, OAlph st the
carrier of fsm1 misses the carrier of fsm2 & fsm1, tfsm1-are_isomorphic & fsm2,
tfsm2-are_isomorphic
proof
deffunc F(object) = $1`2;
set z = 0, zz = 1, A = {z}, B = {zz};
let tfsm1, tfsm2 be finite non empty Mealy-FSM over IAlph, OAlph;
set Stfsm1 = the carrier of tfsm1, Tr1 = the Tran of tfsm1;
set Of1 = the OFun of tfsm1, Stfsm2 = the carrier of tfsm2;
set Tr2 = the Tran of tfsm2, Of2 = the OFun of tfsm2;
set Sfsm1 = [:{0}, Stfsm1:], Sfsm2 = [:{1}, Stfsm2:];
deffunc F(Element of Sfsm1, Element of IAlph) = [ $1`1, Tr1.[$1`2,$2] ];
consider T1 be Function of [: Sfsm1, IAlph :], Sfsm1 such that
A1: for q being Element of Sfsm1, s being Element of IAlph holds T1.(q,s
) = F(q,s) from BINOP_1:sch 4;
reconsider I2 = [ 1, the InitS of tfsm2 ] as Element of Sfsm2 by ZFMISC_1:105
;
reconsider sSfsm2 = [: B, Stfsm2 :] as finite non empty set;
reconsider I1 = [ 0, the InitS of tfsm1 ] as Element of Sfsm1 by ZFMISC_1:105
;
set sSfsm1 = [: A, Stfsm1 :];
deffunc F(Element of Sfsm1, Element of IAlph) = Of1.[$1`2, $2];
consider O1 be Function of [: Sfsm1, IAlph :], OAlph such that
A2: for q being Element of Sfsm1, s being Element of IAlph holds O1.(q,s
) = F(q,s) from BINOP_1:sch 4;
reconsider sI2 = I2 as Element of sSfsm2;
set sI1 = I1;
reconsider sO1 = O1 as Function of [: sSfsm1, IAlph :], OAlph;
reconsider sT1 = T1 as Function of [: sSfsm1, IAlph :], sSfsm1;
deffunc F(Element of Sfsm2, Element of IAlph) = [ $1`1, Tr2.[$1`2,$2] ];
consider T2 be Function of [: Sfsm2, IAlph :], Sfsm2 such that
A3: for q being Element of Sfsm2, s being Element of IAlph holds T2.(q,s
) = F(q,s) from BINOP_1:sch 4;
reconsider sT2 = T2 as Function of [: sSfsm2, IAlph :], sSfsm2;
take fsm1 = Mealy-FSM (# sSfsm1, sT1, sO1, sI1 #);
deffunc F(Element of Sfsm2, Element of IAlph) = Of2.[$1`2,$2];
consider O2 be Function of [: Sfsm2, IAlph :], OAlph such that
A4: for q being Element of Sfsm2, s being Element of IAlph holds O2.(q,s
) = F(q,s) from BINOP_1:sch 4;
A5: A misses B by ZFMISC_1:11;
reconsider sO2 = O2 as Function of [: sSfsm2, IAlph :], OAlph;
take fsm2 = Mealy-FSM (# sSfsm2, sT2, sO2, sI2 #);
Sfsm1 /\ Sfsm2 = [: A /\ B, Stfsm1 /\ Stfsm2 :] by ZFMISC_1:100
.= [: {}, Stfsm1 /\ Stfsm2 :] by A5
.= {} by ZFMISC_1:90;
hence (the carrier of fsm1) /\ (the carrier of fsm2) = {};
thus fsm1, tfsm1-are_isomorphic
proof
deffunc F(object) = $1`2;
consider Tf1 being Function such that
A6: dom Tf1 = the carrier of fsm1 & for q being object st q in the
carrier of fsm1 holds Tf1.q = F(q) from FUNCT_1:sch 3;
A7: rng Tf1 = Stfsm1
proof
assume
A8: not rng Tf1 = Stfsm1;
per cases by A8;
suppose
not rng Tf1 c= Stfsm1;
then consider q being object such that
A9: q in rng Tf1 and
A10: not q in Stfsm1;
consider x be object such that
A11: x in dom Tf1 and
A12: q = Tf1.x by A9,FUNCT_1:def 3;
reconsider x2 = x`2 as Element of Stfsm1 by A6,A11,MCART_1:10;
x2 in Stfsm1;
hence contradiction by A6,A10,A11,A12;
end;
suppose
not Stfsm1 c= rng Tf1;
then consider x being object such that
A13: x in Stfsm1 and
A14: not x in rng Tf1;
0 in {0} by TARSKI:def 1;
then [0,x] in sSfsm1 by A13,ZFMISC_1:87;
then Tf1.[0,x] in rng Tf1 & Tf1.[0,x]=[0,x]`2 by A6,FUNCT_1:def 3;
hence contradiction by A14;
end;
end;
then reconsider
Tf1s = Tf1 as Function of the carrier of fsm1, the carrier of
tfsm1 by A6,FUNCT_2:1;
take Tf1s;
now
let x1, x2 be object;
assume that
A15: x1 in dom Tf1 and
A16: x2 in dom Tf1 and
A17: Tf1.x1 = Tf1.x2;
A18: Tf1.x1 = x1`2 & Tf1.x2 = x2`2 by A6,A15,A16;
x1`1 in A by A6,A15,MCART_1:10;
then
A19: x1`1 = 0 by TARSKI:def 1;
A20: x2`1 in A by A6,A16,MCART_1:10;
x1 = [x1`1, x1`2] & x2 = [x2`1,x2`2] by A6,A15,A16,MCART_1:21;
hence x1 = x2 by A17,A18,A20,A19,TARSKI:def 1;
end;
then Tf1s is one-to-one onto by A7,FUNCT_1:def 4,FUNCT_2:def 3;
hence Tf1s is bijective;
thus Tf1s.the InitS of fsm1 = sI1`2 by A6
.= the InitS of tfsm1;
now
let q be State of fsm1, s be Element of IAlph;
reconsider q1 = q`2 as Element of Stfsm1 by MCART_1:10;
reconsider Tq1 = Tr1.[q1, s] as Element of Stfsm1;
q`1 in A by MCART_1:10;
then
A21: [q`1,Tq1] in [: A, Stfsm1 :] by ZFMISC_1:87;
thus Tf1s.((the Tran of fsm1).(q, s)) = Tf1s.(q`1, Tr1.(q`2, s)) by A1
.= [q`1, Tr1.[q`2, s]]`2 by A6,A21
.= Tr1.[q`2, s]
.= (the Tran of tfsm1).[Tf1s.q, s] by A6;
thus (the OFun of fsm1).(q,s) = Of1.(q`2, s) by A2
.= (the OFun of tfsm1).(Tf1s.q, s) by A6;
end;
hence thesis;
end;
consider Tf1 being Function such that
A22: dom Tf1 = the carrier of fsm2 & for q being object st q in the carrier
of fsm2 holds Tf1.q = F(q) from FUNCT_1:sch 3;
A23: rng Tf1 = Stfsm2
proof
assume
A24: not rng Tf1 = Stfsm2;
per cases by A24;
suppose
not rng Tf1 c= Stfsm2;
then consider q being object such that
A25: q in rng Tf1 and
A26: not q in Stfsm2;
consider x be object such that
A27: x in dom Tf1 and
A28: q = Tf1.x by A25,FUNCT_1:def 3;
reconsider x2 = x`2 as Element of Stfsm2 by A22,A27,MCART_1:10;
x2 in Stfsm2;
hence contradiction by A22,A26,A27,A28;
end;
suppose
not Stfsm2 c= rng Tf1;
then consider x being object such that
A29: x in Stfsm2 and
A30: not x in rng Tf1;
1 in {1} by TARSKI:def 1;
then [1,x] in sSfsm2 by A29,ZFMISC_1:87;
then Tf1.[1,x] in rng Tf1 & Tf1.[1,x] = [1,x]`2 by A22,FUNCT_1:def 3;
hence contradiction by A30;
end;
end;
then reconsider
Tf1s = Tf1 as Function of the carrier of fsm2, the carrier of
tfsm2 by A22,FUNCT_2:1;
take Tf1s;
now
let x1, x2 be object;
assume that
A31: x1 in dom Tf1 and
A32: x2 in dom Tf1 and
A33: Tf1.x1 = Tf1.x2;
A34: Tf1.x1 = x1`2 & Tf1.x2 = x2`2 by A22,A31,A32;
x1`1 in B by A22,A31,MCART_1:10;
then
A35: x1`1 = 1 by TARSKI:def 1;
A36: x2`1 in B by A22,A32,MCART_1:10;
x1 = [x1`1, x1`2] & x2 = [x2`1,x2`2] by A22,A31,A32,MCART_1:21;
hence x1 = x2 by A33,A34,A36,A35,TARSKI:def 1;
end;
then Tf1s is one-to-one onto by A23,FUNCT_1:def 4,FUNCT_2:def 3;
hence Tf1s is bijective;
thus Tf1s.the InitS of fsm2 = sI2`2 by A22
.= the InitS of tfsm2;
now
let q be State of fsm2, s be Element of IAlph;
reconsider q1 = q`2 as Element of Stfsm2 by MCART_1:10;
set Tq1 = Tr2.[q1, s];
q`1 in B by MCART_1:10;
then
A37: [q`1,Tq1] in [: B, Stfsm2 :] by ZFMISC_1:87;
thus Tf1s.((the Tran of fsm2).(q, s)) = Tf1s.(q`1, Tr2.(q`2, s)) by A3
.= [q`1, Tr2.[q`2, s]]`2 by A22,A37
.= Tr2.[q`2, s]
.= (the Tran of tfsm2).[Tf1s.q, s] by A22;
thus (the OFun of fsm2).(q,s) = Of2.(q`2, s) by A4
.= (the OFun of tfsm2).[Tf1s.q, s] by A22;
end;
hence thesis;
end;
theorem Th63:
tfsm1, tfsm2-are_isomorphic implies tfsm1, tfsm2-are_equivalent
proof
assume tfsm1, tfsm2-are_isomorphic;
then consider Tf such that
Tf is bijective and
A1: Tf.the InitS of tfsm1 = the InitS of tfsm2 and
A2: for q being Element of tfsm1, s being Element of IAlph holds Tf.((
the Tran of tfsm1).(q, s)) = (the Tran of tfsm2).(Tf.q, s) & (the OFun of tfsm1
).(q,s) = (the OFun of tfsm2).(Tf.q, s);
now
let w1 be FinSequence of IAlph;
set rw1 = (the InitS of tfsm1,w1)-response;
set rw2 = (the InitS of tfsm2, w1)-response;
set aw1 = (the InitS of tfsm1,w1)-admissible;
set aw2 = (the InitS of tfsm2,w1)-admissible;
A3: for k being Nat st 1<=k & k<= len w1 +1 holds Tf.(aw1.k) = aw2.k
proof
defpred P[Nat] means 1 <= $1 & $1 <= len w1 + 1 implies Tf.(
aw1.$1) = aw2.$1;
A4: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A5: 1 <= k & k <= len w1 + 1 implies Tf.(aw1.k) = aw2.k;
assume that
1 <= (k+1) and
A6: (k+1) <= len w1 + 1;
A7: 0 = k or 0 < k & 0+1 = 1;
per cases by A7,NAT_1:13;
suppose
A8: 0 = k;
hence Tf.(aw1.(k+1)) = the InitS of tfsm2 by A1,Def2
.= aw2.(k+1) by A8,Def2;
end;
suppose
A9: 1 <= k;
A10: len w1 <= len w1 + 1 by NAT_1:11;
A11: k <= len w1 by A6,XREAL_1:6;
then consider
w1k be Element of IAlph, qk, qk1 be Element of tfsm1 such
that
A12: w1k= w1.k & qk = aw1.k and
A13: qk1 = aw1.(k+1) & w1k-succ_of qk = qk1 by A9,Def2;
consider w2k be Element of IAlph, q2k, q2k1 be Element of tfsm2 such
that
A14: w2k= w1.k & q2k = aw2.k and
A15: q2k1 = aw2.(k+1) & w2k-succ_of q2k = q2k1 by A9,A11,Def2;
thus Tf.(aw1.(k+1)) = Tf.((the Tran of tfsm1).(qk, w1k)) by A13
.= (the Tran of tfsm2).(q2k, w2k) by A2,A5,A9,A11,A12,A14,A10,
XXREAL_0:2
.= aw2.(k+1) by A15;
end;
end;
A16: P[0];
thus for i being Nat holds P[i] from NAT_1:sch 2 (A16, A4);
end;
A17: now
let k be Nat;
assume that
A18: 1 <= k and
A19: k <= len rw1;
k <= len w1 by A19,Def6;
then
A20: k in dom w1 by A18,FINSEQ_3:25;
then
A21: w1.k is Element of IAlph by FINSEQ_2:11;
k in Seg len w1 by A20,FINSEQ_1:def 3;
then k in Seg (len w1 + 1) by FINSEQ_2:8;
then k in Seg len aw1 by Def2;
then
A22: k in dom aw1 by FINSEQ_1:def 3;
then
A23: 1 <= k by FINSEQ_3:25;
k <= len aw1 by A22,FINSEQ_3:25;
then
A24: k <= len w1 + 1 by Def2;
A25: aw1.k is Element of tfsm1 by A22,FINSEQ_2:11;
thus rw2.k = (the OFun of tfsm2).[aw2.k, w1.k] by A20,Def6
.= (the OFun of tfsm2).(Tf.(aw1.k), w1.k) by A3,A23,A24
.= (the OFun of tfsm1).(aw1.k, w1.k) by A2,A25,A21
.= rw1.k by A20,Def6;
end;
len rw1 = len w1 by Def6
.= len rw2 by Def6;
hence rw1 = rw2 by A17,FINSEQ_1:14;
end;
hence thesis;
end;
theorem Th64:
the carrier of CRtfsm1 misses the carrier of CRtfsm2 & CRtfsm1,
CRtfsm2-are_equivalent implies CRtfsm1, CRtfsm2-are_isomorphic
proof
set rtfsm1 = CRtfsm1;
set rtfsm2 = CRtfsm2;
assume that
A1: (the carrier of rtfsm1) misses (the carrier of rtfsm2) and
A2: rtfsm1, rtfsm2-are_equivalent;
set Srtfsm2 = the carrier of rtfsm2;
set Srtfsm1 = the carrier of rtfsm1;
set UN = rtfsm1-Mealy_union rtfsm2;
set RUN = the_reduction_of UN;
set SRUN = the carrier of RUN;
defpred P[object, object] means
ex part being Element of SRUN st $1 in part & $2 in part \ { $1 };
A3: SRUN = final_states_partition UN by Def18;
A4: for x being object st x in Srtfsm1 ex y being object st P[x,y]
proof
let x be object;
set xs = { x };
A5: union SRUN= the carrier of UN by A3,EQREL_1:def 4;
assume
A6: x in Srtfsm1;
then x in Srtfsm1 \/ Srtfsm2 by XBOOLE_0:def 3;
then x in the carrier of UN by Def24;
then consider part being set such that
A7: x in part and
A8: part in SRUN by A5,TARSKI:def 4;
reconsider part as Element of SRUN by A8;
consider p, y be Element of part such that
p in Srtfsm1 and
A9: y in Srtfsm2 and
for z being Element of part holds z = p or z = y by A1,A2,Th61;
set IT = y;
take IT;
x <> y by A1,A6,A9,XBOOLE_0:3;
then y in part \ xs by A7,ZFMISC_1:56;
hence thesis by A7;
end;
consider f being Function such that
A10: dom f = Srtfsm1 & for x being object st x in Srtfsm1 holds P[x,f.x]
from CLASSES1:sch 1 (A4 );
now
assume
A11: not rng f c= Srtfsm2 or not Srtfsm2 c= rng f;
per cases by A11;
suppose
not rng f c= Srtfsm2;
then consider y1 being object such that
A12: y1 in rng f and
A13: not y1 in Srtfsm2;
consider x1 being object such that
A14: x1 in Srtfsm1 and
A15: y1 = f.x1 by A10,A12,FUNCT_1:def 3;
consider part1 be Element of SRUN such that
A16: x1 in part1 and
A17: f.x1 in part1 \ { x1 } by A10,A14;
A18: now
assume
A19: y1 in Srtfsm1;
y1 <> x1 by A15,A17,ZFMISC_1:56;
hence contradiction by A1,A14,A15,A16,A17,A19,Th59;
end;
part1 is Subset of UN by A3,TARSKI:def 3;
then
A20: part1 is Subset of Srtfsm1 \/ Srtfsm2 by Def24;
y1 in part1 by A15,A17;
hence contradiction by A13,A20,A18,XBOOLE_0:def 3;
end;
suppose
A21: not Srtfsm2 c= rng f;
A22: union SRUN = the carrier of UN by A3,EQREL_1:def 4;
consider y1 being object such that
A23: y1 in Srtfsm2 and
A24: not y1 in rng f by A21;
y1 in Srtfsm1 \/ Srtfsm2 by A23,XBOOLE_0:def 3;
then y1 in the carrier of UN by Def24;
then consider Z being set such that
A25: y1 in Z and
A26: Z in SRUN by A22,TARSKI:def 4;
reconsider Z as Element of SRUN by A26;
A27: Z is Subset of UN by A3,TARSKI:def 3;
consider q1, q2 being Element of Z such that
A28: q1 in Srtfsm1 and
q2 in Srtfsm2 and
for q being Element of Z holds q = q1 or q = q2 by A1,A2,Th61;
consider F being Element of SRUN such that
A29: q1 in F and
A30: f.q1 in F \ {q1} by A10,A28;
F is Subset of UN 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
A33: now
assume
A34: f.q1 in Srtfsm1;
f.q1 <> q1 by A30,ZFMISC_1:56;
hence contradiction by A1,A28,A29,A30,A34,Th59;
end;
Z is Subset of Srtfsm1 \/ Srtfsm2 by A27,Def24;
then
A35: f.q1 in Srtfsm1 or f.q1 in Srtfsm2 by A25,A29,A31,A32,XBOOLE_0:3,def 3;
assume y1 <> f.q1;
hence contradiction by A23,A25,A29,A30,A31,A35,A33,Th60,XBOOLE_0:3;
end;
hence contradiction by A10,A24,A28,FUNCT_1:def 3;
end;
end;
then
A36: rng f = Srtfsm2;
A37: now
let x1, x2 be object;
assume that
A38: x1 in dom f and
A39: x2 in dom f and
A40: f.x1 = f.x2;
consider part1 be Element of SRUN such that
A41: x1 in part1 & f.x1 in part1 \ { x1 } by A10,A38;
consider part2 be Element of SRUN such that
A42: x2 in part2 & f.x2 in part2 \ { x2 } by A10,A39;
assume
A43: x1 <> x2;
part1 is Subset of UN & part2 is Subset of UN 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;
end;
reconsider f as Function of Srtfsm1, Srtfsm2 by A10,A36,FUNCT_2:1;
A44: f.the InitS of rtfsm1 = the InitS of rtfsm2
proof
consider part being Element of SRUN such that
A45: the InitS of rtfsm1 in part & f.the InitS of rtfsm1 in part \ {
the InitS of rtfsm1 } by A10;
consider Q being Element of SRUN such that
A46: the InitS of rtfsm1 in Q & the InitS of rtfsm2 in Q and
Q = the InitS of RUN by A1,A2,Th56;
assume
A47: f.the InitS of rtfsm1 <> the InitS of rtfsm2;
Q is Subset of UN & part is Subset of UN by A3,TARSKI:def 3;
then Q = part or Q misses part by A3,EQREL_1:def 4;
hence contradiction by A47,A46,A45,Th60,XBOOLE_0:3;
end;
A48: for q being State of rtfsm1, s being Element of IAlph holds f.((the
Tran of rtfsm1).(q, s)) = (the Tran of rtfsm2).(f.q, s) & (the OFun of rtfsm1).
(q,s) = (the OFun of rtfsm2).(f.q, s)
proof
let q be State of rtfsm1, s be Element of IAlph;
set q1 = (the Tran of rtfsm1).[q,s], fq = f.q;
set q2 = (the Tran of rtfsm2).[fq,s];
A49: dom (the Tran of rtfsm2) = [: Srtfsm2,IAlph :] by FUNCT_2:def 1;
A50: the carrier of UN = Srtfsm1 \/ Srtfsm2 by Def24;
then reconsider q9 = q as Element of UN by XBOOLE_0:def 3;
f.q in rng f by A10,FUNCT_1:def 3;
then reconsider fq9 = f.q9 as Element of UN by A50,XBOOLE_0:def 3;
set qu = (the Tran of UN).[q9,s], qfu = (the Tran of UN).[fq9,s];
A51: qfu = ((the Tran of rtfsm1)+*(the Tran of rtfsm2)).[fq9,s] by Def24
.= q2 by A49,FUNCT_4:13;
consider XX be Element of SRUN such that
A52: q1 in XX & f.q1 in XX \ { q1 } by A10;
A53: final_states_partition UN is final by Def15;
ex part be Element of SRUN st q in part & f.q in part \ { q } by A10;
then
A54: q9, fq9-are_equivalent by A3,A53;
then qu,qfu-are_equivalent by Th19;
then consider X being Element of SRUN such that
A55: qu in X & qfu in X by A3,A53;
A56: (the carrier of rtfsm1) /\ (the carrier of rtfsm2) = {} by A1;
A57: dom (the Tran of rtfsm1) = [: Srtfsm1,IAlph :] by FUNCT_2:def 1;
then dom (the Tran of rtfsm1) /\ dom (the Tran of rtfsm2) = [: Srtfsm1,
IAlph :] /\ [: Srtfsm2,IAlph :] by FUNCT_2:def 1
.= [: {} ,IAlph :] by A56,ZFMISC_1:99
.= {} by ZFMISC_1:90;
then
A58: dom (the Tran of rtfsm1) misses dom (the Tran of rtfsm2);
A59: qu = ((the Tran of rtfsm1)+*(the Tran of rtfsm2)).[q9,s] by Def24
.=q1 by A57,A58,FUNCT_4:16;
A60: X is Subset of UN by A3,TARSKI:def 3;
now
XX is Subset of UN by A3,TARSKI:def 3;
then
A61: X = XX or X misses XX by A3,A60,EQREL_1:def 4;
assume f.q1 <> q2;
hence contradiction by A55,A59,A51,A52,A61,Th60,XBOOLE_0:3;
end;
hence f.((the Tran of rtfsm1).(q, s)) = (the Tran of rtfsm2).(f.q, s);
A62: dom (the OFun of rtfsm2) = [: Srtfsm2,IAlph :] by FUNCT_2:def 1;
A63: dom (the OFun of rtfsm1) = [: Srtfsm1,IAlph :] by FUNCT_2:def 1;
then dom (the OFun of rtfsm1) /\ dom (the OFun of rtfsm2) = [: Srtfsm1 /\
Srtfsm2, IAlph :] by A62,ZFMISC_1:99
.= {} by A56,ZFMISC_1:90;
then dom (the OFun of rtfsm1) misses dom (the OFun of rtfsm2);
hence (the OFun of rtfsm1).(q,s) = ((the OFun of rtfsm1) +* (the OFun of
rtfsm2)).[q,s] by A63,FUNCT_4:16
.= (the OFun of UN).[q9,s] by Def24
.= (the OFun of UN).[fq9,s] by A54,Th19
.= ((the OFun of rtfsm1) +* (the OFun of rtfsm2)).[f.q,s] by Def24
.= (the OFun of rtfsm2).(f.q, s) by A62,FUNCT_4:13;
end;
f is one-to-one onto by A37,A36,FUNCT_1:def 4,FUNCT_2:def 3;
hence thesis by A44,A48;
end;
theorem Th65:
Ctfsm1, Ctfsm2-are_equivalent implies the_reduction_of Ctfsm1,
the_reduction_of Ctfsm2-are_isomorphic
proof
assume
A1: Ctfsm1, Ctfsm2-are_equivalent;
set rtfsm2 = the_reduction_of Ctfsm2;
set rtfsm1 = the_reduction_of Ctfsm1;
consider fsm1, fsm2 being finite non empty Mealy-FSM over IAlph, OAlph such
that
A2: (the carrier of fsm1) misses (the carrier of fsm2) and
A3: fsm1,rtfsm1-are_isomorphic and
A4: fsm2,rtfsm2-are_isomorphic by Th62;
A5: rtfsm1,Ctfsm1-are_equivalent by Th41;
set Srtfsm1 = the carrier of rtfsm1, Srtfsm2 = the carrier of rtfsm2;
set ISrtfsm1= the InitS of rtfsm1, ISrtfsm2= the InitS of rtfsm2;
set Sfsm1 = the carrier of fsm1, Sfsm2 = the carrier of fsm2;
set ISfsm1= the InitS of fsm1, ISfsm2= the InitS of fsm2;
A6: rtfsm2,Ctfsm2-are_equivalent by Th41;
fsm2,rtfsm2-are_equivalent by A4,Th63;
then
A7: fsm2,Ctfsm2-are_equivalent by A6,Th15;
A8: fsm1 is connected
proof
assume not fsm1 is connected;
then consider q1 being Element of Sfsm1 such that
A9: not q1 is accessible;
consider Tf being Function of the carrier of fsm1, Srtfsm1 such that
A10: Tf is bijective and
A11: Tf.the InitS of fsm1 = ISrtfsm1 & for q being State of fsm1, s
being Element of IAlph holds Tf.((the Tran of fsm1).(q, s)) = (the Tran of
rtfsm1).(Tf.q, s) & (the OFun of fsm1).(q, s) = (the OFun of rtfsm1).(Tf.q, s)
by A3;
A12: dom Tf = Sfsm1 by FUNCT_2:def 1;
set q = Tf.q1;
q is accessible by Def22;
then consider w being FinSequence of IAlph such that
A13: ISrtfsm1,w-leads_to q;
A14: 1 <= len w + 1 by NAT_1:11;
then
Tf.((ISfsm1,w)-admissible.(len w + 1)) = (ISrtfsm1,w)-admissible.(len
w + 1) by A11,Th43;
then
A15: Tf".(Tf.((ISfsm1,w)-admissible.(len w + 1))) = Tf".q by A13;
len (ISfsm1,w)-admissible = len w + 1 by Def2;
then len w + 1 in Seg (len (ISfsm1,w)-admissible) by A14,FINSEQ_1:1;
then len w + 1 in dom (ISfsm1,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 (ISfsm1,w)-admissible.(len w + 1) = Tf".(Tf.q1) by A10,A15,FUNCT_1:34
.= q1 by A10,A12,FUNCT_1:34;
then ISfsm1,w-leads_to q1;
hence contradiction by A9;
end;
A16: fsm2 is connected
proof
assume not fsm2 is connected;
then consider q1 being Element of Sfsm2 such that
A17: not q1 is accessible;
consider Tf being Function of Sfsm2, Srtfsm2 such that
A18: Tf is bijective and
A19: Tf.ISfsm2 = ISrtfsm2 & for q being State of fsm2, s being Element
of IAlph holds Tf.((the Tran of fsm2).(q, s)) = (the Tran of rtfsm2).(Tf.q, s)
& (the OFun of fsm2).(q, s) = (the OFun of rtfsm2).(Tf.q, s) by A4;
A20: dom Tf = Sfsm2 by FUNCT_2:def 1;
set q = Tf.q1;
q is accessible by Def22;
then consider w being FinSequence of IAlph such that
A21: ISrtfsm2,w-leads_to q;
A22: 1 <= len w + 1 by NAT_1:11;
then
Tf.((ISfsm2,w)-admissible.(len w + 1)) = (ISrtfsm2,w)-admissible.(len
w + 1) by A19,Th43;
then
A23: Tf".(Tf.((ISfsm2,w)-admissible.(len w + 1))) = Tf".q by A21;
len (ISfsm2,w)-admissible = len w + 1 by Def2;
then len w + 1 in Seg (len (ISfsm2,w)-admissible) by A22,FINSEQ_1:1;
then len w + 1 in dom (ISfsm2,w)-admissible by FINSEQ_1:def 3;
then (ISfsm2,w)-admissible.(len w + 1) in dom Tf by A20,FINSEQ_2:11;
then (ISfsm2,w)-admissible.(len w + 1) = Tf".(Tf.q1) by A18,A23,FUNCT_1:34
.= q1 by A18,A20,FUNCT_1:34;
then ISfsm2,w-leads_to q1;
hence contradiction by A17;
end;
fsm1,rtfsm1-are_equivalent by A3,Th63;
then fsm1,Ctfsm1-are_equivalent by A5,Th15;
then
A24: fsm1,Ctfsm2-are_equivalent by A1,Th15;
reconsider fsm1, fsm2 as reduced finite non empty Mealy-FSM over IAlph,
OAlph by A3,A4,Th47;
fsm1, fsm2-are_isomorphic by A2,A8,A16,A7,A24,Th15,Th64;
then fsm1,rtfsm2-are_isomorphic by A4,Th42;
hence thesis by A3,Th42;
end;
::$N Myhill-Nerode theorem
theorem
for M1, M2 being connected reduced finite non empty Mealy-FSM over
IAlph, OAlph holds M1, M2-are_isomorphic iff M1, M2-are_equivalent
proof
let M1, M2 be connected reduced finite non empty Mealy-FSM over IAlph,
OAlph;
thus M1, M2-are_isomorphic implies M1, M2-are_equivalent by Th63;
A1: M2, the_reduction_of M2-are_isomorphic by Th46;
assume M1, M2-are_equivalent;
then
A2: the_reduction_of M1, the_reduction_of M2-are_isomorphic by Th65;
M1, the_reduction_of M1-are_isomorphic by Th46;
then M1, the_reduction_of M2-are_isomorphic by A2,Th42;
hence thesis by A1,Th42;
end;