let IAlph, OAlph be non empty set ; for w being FinSequence of IAlph
for tfsm, rtfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm
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
let w be FinSequence of IAlph; for tfsm, rtfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm
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
let tfsm, rtfsm be non empty finite Mealy-FSM over IAlph,OAlph; for q being State of tfsm
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
let q be State of tfsm; 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
let qr be State of rtfsm; ( rtfsm = the_reduction_of tfsm & q in qr implies for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k )
set TR = the Tran of tfsm;
assume that
A1:
rtfsm = the_reduction_of tfsm
and
A2:
q in qr
; for k being Nat st k in Seg ((len w) + 1) holds
((q,w) -admissible) . k in ((qr,w) -admissible) . k
defpred S1[ Nat] means ( $1 in Seg ((len w) + 1) implies ((q,w) -admissible) . $1 in ((qr,w) -admissible) . $1 );
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
(
k in Seg ((len w) + 1) implies
((q,w) -admissible) . k in ((qr,w) -admissible) . k )
;
S1[k + 1]
assume A5:
k + 1
in Seg ((len w) + 1)
;
((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1)
A6:
(
k = 0 or (
0 < k &
0 + 1
= 1 ) )
;
per cases
( k = 0 or 1 <= k )
by A6, NAT_1:13;
suppose A8:
1
<= k
;
((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1)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
the
Tran of
tfsm . (
q1i,
w1i)
in the
Tran of
rtfsm . (
q2i,
w2i)
by A1, A4, A8, A11, A13, Def18, FINSEQ_1:1;
hence
((q,w) -admissible) . (k + 1) in ((qr,w) -admissible) . (k + 1)
by A12, A14;
verum end; end;
end;
A15:
S1[ 0 ]
by FINSEQ_1:1;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A15, A3); verum