let IAlph, OAlph be non empty set ; for s being Element of IAlph
for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
(qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)
let s be Element of IAlph; for w being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
(qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)
let w be FinSequence of IAlph; for tfsm being non empty Mealy-FSM over IAlph,OAlph
for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
(qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)
let tfsm be non empty Mealy-FSM over IAlph,OAlph; for qa, qa9 being State of tfsm st qa9 = the Tran of tfsm . [qa,s] holds
(qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)
let qa, qa9 be State of tfsm; ( qa9 = the Tran of tfsm . [qa,s] implies (qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response) )
set OF = the OFun of tfsm;
set asresp = the OFun of tfsm . [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]
; (qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)
now ( len ((qa,(<*s*> ^ w)) -response) = 1 + (len w) & len (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) = 1 + (len w) & ( for j being Nat st j in dom ((qa,(<*s*> ^ w)) -response) holds
((qa,(<*s*> ^ w)) -response) . j = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . j ) )thus
len ((qa,(<*s*> ^ w)) -response) = 1
+ (len w)
by A1, Def6;
( len (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) = 1 + (len w) & ( for j being Nat st j in dom ((qa,(<*s*> ^ w)) -response) holds
((qa,(<*s*> ^ w)) -response) . b2 = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . b2 ) )then A3:
dom ((qa,(<*s*> ^ w)) -response) = Seg (1 + (len w))
by FINSEQ_1:def 3;
thus A4:
len (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) =
(len <*( the OFun of tfsm . [qa,s])*>) + (len ((qa9,w) -response))
by FINSEQ_1:22
.=
1
+ (len ((qa9,w) -response))
by FINSEQ_1:40
.=
1
+ (len w)
by Def6
;
for j being Nat st j in dom ((qa,(<*s*> ^ w)) -response) holds
((qa,(<*s*> ^ w)) -response) . b2 = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . b2let j be
Nat;
( j in dom ((qa,(<*s*> ^ w)) -response) implies ((qa,(<*s*> ^ w)) -response) . b1 = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . b1 )assume A5:
j in dom ((qa,(<*s*> ^ w)) -response)
;
((qa,(<*s*> ^ w)) -response) . b1 = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . b1then 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
( j = 1 or j > 1 )
by A6, XXREAL_0:1;
suppose A9:
j = 1
;
((qa,(<*s*> ^ w)) -response) . b1 = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . b1thus ((qa,(<*s*> ^ w)) -response) . j =
the
OFun of
tfsm . [(((qa,(<*s*> ^ w)) -admissible) . j),((<*s*> ^ w) . j)]
by A8, Def6
.=
the
OFun of
tfsm . [qa,((<*s*> ^ w) . j)]
by A9, Def2
.=
the
OFun of
tfsm . [qa,s]
by A9, FINSEQ_1:41
.=
(<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . j
by A9, FINSEQ_1:41
;
verum end; suppose A10:
j > 1
;
((qa,(<*s*> ^ w)) -response) . b1 = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . b1then 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 <*( the OFun of tfsm . [qa,s])*> = 1
by FINSEQ_1:40;
then (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . j =
((qa9,w) -response) . i
by A4, A7, A10, A11, FINSEQ_1:24
.=
the
OFun of
tfsm . [(((qa9,w) -admissible) . i),(w . i)]
by A16, Def6
.=
the
OFun of
tfsm . [(((qa9,w) -admissible) . i),((<*s*> ^ w) . (i + 1))]
by A16, FINSEQ_3:103
.=
the
OFun of
tfsm . [(((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 = (<*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)) . j
;
verum end; end;
hence
(qa,(<*s*> ^ w)) -response = <*( the OFun of tfsm . [qa,s])*> ^ ((qa9,w) -response)
by FINSEQ_2:9; verum