let IAlph, OAlph be non empty set ; for tfsm being non empty finite Mealy-FSM over IAlph,OAlph holds tfsm, the_reduction_of tfsm -are_equivalent
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; tfsm, the_reduction_of tfsm -are_equivalent
now for w1 being FinSequence of IAlph holds ( the InitS of tfsm,w1) -response = ( the InitS of (the_reduction_of tfsm),w1) -response 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 for k being Nat st 1 <= k & k <= len (( the InitS of tfsm,w1) -response) holds
(( the InitS of (the_reduction_of tfsm),w1) -response) . k = (( the InitS of tfsm,w1) -response) . klet 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:1;
then A6:
k in Seg ((len w1) + 1)
by FINSEQ_2:8;
then A7:
(( the InitS of tfsm,w1) -admissible) . k in (( the InitS of (the_reduction_of tfsm),w1) -admissible) . k
by A1, Th40;
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:11;
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: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 (( 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:14;
verum end;
hence
tfsm, the_reduction_of tfsm -are_equivalent
; verum