let IAlph, OAlph be non empty set ; for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let w be FinSequence of IAlph; for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph; for q11 being State of tfsm1
for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let q11 be State of tfsm1; for Tf being Function of the carrier of tfsm1, the carrier of tfsm2 st ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) holds
for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
let Tf be Function of the carrier of tfsm1, the carrier of tfsm2; ( ( for q being State of tfsm1
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s) ) implies for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k )
defpred S1[ 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
for s being Element of IAlph holds Tf . ( the Tran of tfsm1 . (q,s)) = the Tran of tfsm2 . ((Tf . q),s)
; for k being Nat st 1 <= k & k <= (len w) + 1 holds
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
( 1
<= k &
k <= (len w) + 1 implies
Tf . (((q11,w) -admissible) . k) = (((Tf . q11),w) -admissible) . k )
;
S1[k + 1]
assume that
1
<= k + 1
and A4:
k + 1
<= (len w) + 1
;
Tf . (((q11,w) -admissible) . (k + 1)) = (((Tf . q11),w) -admissible) . (k + 1)
A5:
(
k = 0 or (
0 < k &
0 + 1
= 1 ) )
;
per cases
( k = 0 or 1 <= k )
by A5, NAT_1:13;
suppose A7:
1
<= k
;
Tf . (((q11,w) -admissible) . (k + 1)) = (((Tf . q11),w) -admissible) . (k + 1)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
;
verum end;
end;
A14:
S1[ 0 ]
;
thus
for k being Nat holds S1[k]
from NAT_1:sch 2(A14, A2); verum