let IAlph, OAlph be non empty set ; for tfsm being non empty finite Mealy-FSM of IAlph,OAlph holds tfsm, the_reduction_of tfsm -are_equivalent
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; tfsm, the_reduction_of tfsm -are_equivalent
now set rtfsm =
the_reduction_of tfsm;
let w1 be
FinSequence of
IAlph;
the InitS of tfsm,w1 -response = the InitS of (the_reduction_of tfsm),w1 -response set ad1 = the
InitS of
tfsm,
w1 -admissible ;
set ad2 = the
InitS of
(the_reduction_of tfsm),
w1 -admissible ;
set r1 = the
InitS of
tfsm,
w1 -response ;
set r2 = the
InitS of
(the_reduction_of tfsm),
w1 -response ;
A1:
the
InitS of
tfsm in the
InitS of
(the_reduction_of tfsm)
by Def18;
A2:
now let k be
Nat;
( 1 <= k & k <= len (the InitS of tfsm,w1 -response ) implies (the InitS of (the_reduction_of tfsm),w1 -response ) . k = (the InitS of tfsm,w1 -response ) . k )assume that A3:
1
<= k
and A4:
k <= len (the InitS of tfsm,w1 -response )
;
(the InitS of (the_reduction_of tfsm),w1 -response ) . k = (the InitS of tfsm,w1 -response ) . k
k <= len w1
by A4, Def6;
then A5:
k in Seg (len w1)
by A3, FINSEQ_1:3;
then A6:
k in Seg ((len w1) + 1)
by FINSEQ_2:9;
then A7:
(the InitS of tfsm,w1 -admissible ) . k in (the InitS of (the_reduction_of tfsm),w1 -admissible ) . k
by A1, Th57;
k in Seg (len (the InitS of (the_reduction_of tfsm),w1 -admissible ))
by A6, Def2;
then
k in dom (the InitS of (the_reduction_of tfsm),w1 -admissible )
by FINSEQ_1:def 3;
then A8:
(the InitS of (the_reduction_of tfsm),w1 -admissible ) . k is
Element of
(the_reduction_of tfsm)
by FINSEQ_2:13;
k in Seg (len (the InitS of tfsm,w1 -admissible ))
by A6, Def2;
then
k in dom (the InitS of tfsm,w1 -admissible )
by FINSEQ_1:def 3;
then A9:
(the InitS of tfsm,w1 -admissible ) . k is
Element of
tfsm
by FINSEQ_2:13;
A10:
k in dom w1
by A5, FINSEQ_1:def 3;
then A11:
w1 . k is
Element of
IAlph
by FINSEQ_2:13;
thus (the InitS of (the_reduction_of tfsm),w1 -response ) . k =
the
OFun of
(the_reduction_of tfsm) . ((the InitS of (the_reduction_of tfsm),w1 -admissible ) . k),
(w1 . k)
by A10, Def6
.=
the
OFun of
tfsm . ((the InitS of tfsm,w1 -admissible ) . k),
(w1 . k)
by A9, A11, A8, A7, Def18
.=
(the InitS of tfsm,w1 -response ) . k
by A10, Def6
;
verum end; len (the InitS of tfsm,w1 -response ) =
len w1
by Def6
.=
len (the InitS of (the_reduction_of tfsm),w1 -response )
by Def6
;
hence
the
InitS of
tfsm,
w1 -response = the
InitS of
(the_reduction_of tfsm),
w1 -response
by A2, FINSEQ_1:18;
verum end;
hence
tfsm, the_reduction_of tfsm -are_equivalent
by Def9; verum