let IAlph, OAlph be non empty set ; :: thesis: for w being FinSequence of IAlph
for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q holds
q21,w -response = q,w -response
let w be FinSequence of IAlph; :: thesis: for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q holds
q21,w -response = q,w -response
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for q21 being State of tfsm2
for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q holds
q21,w -response = q,w -response
let q21 be State of tfsm2; :: thesis: for tfsm being non empty finite Mealy-FSM of IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q holds
q21,w -response = q,w -response
let tfsm be non empty finite Mealy-FSM of IAlph,OAlph; :: thesis: for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q holds
q21,w -response = q,w -response
let q be State of tfsm; :: thesis: ( tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q implies q21,w -response = q,w -response )
set q' = q21;
assume A1:
( tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q21 = q )
; :: thesis: q21,w -response = q,w -response
set res = q,w -response ;
set res' = q21,w -response ;
set ad' = q21,w -admissible ;
A2: len (q21,w -response ) =
len w
by Def6
.=
len (q,w -response )
by Def6
;
A3:
len (q21,w -response ) = len w
by Def6;
now let k be
Nat;
:: thesis: ( 1 <= k & k <= len (q21,w -response ) implies (q21,w -response ) . k = (q,w -response ) . k )assume
( 1
<= k &
k <= len (q21,w -response ) )
;
:: thesis: (q21,w -response ) . k = (q,w -response ) . kthen A4:
k in Seg (len w)
by A3, FINSEQ_1:3;
then A5:
k in dom w
by FINSEQ_1:def 3;
k in Seg ((len w) + 1)
by A4, FINSEQ_2:9;
then
k in Seg (len (q21,w -admissible ))
by Def2;
then A6:
k in dom (q21,w -admissible )
by FINSEQ_1:def 3;
A7:
dom the
OFun of
tfsm2 = [:the carrier of tfsm2,IAlph:]
by FUNCT_2:def 1;
A8:
w . k in IAlph
by A5, FINSEQ_2:13;
(q21,w -admissible ) . k in the
carrier of
tfsm2
by A6, FINSEQ_2:13;
then A9:
[((q21,w -admissible ) . k),(w . k)] in dom the
OFun of
tfsm2
by A7, A8, ZFMISC_1:106;
(q21,w -response ) . k =
the
OFun of
tfsm2 . [((q21,w -admissible ) . k),(w . k)]
by A5, Def6
.=
(the OFun of tfsm1 +* the OFun of tfsm2) . [((q21,w -admissible ) . k),(w . k)]
by A9, FUNCT_4:14
.=
(the OFun of tfsm1 +* the OFun of tfsm2) . [((q,w -admissible ) . k),(w . k)]
by A1, Th73
.=
the
OFun of
tfsm . [((q,w -admissible ) . k),(w . k)]
by A1, Def24
.=
(q,w -response ) . k
by A5, Def6
;
hence
(q21,w -response ) . k = (q,w -response ) . k
;
:: thesis: verum end;
hence
q21,w -response = q,w -response
by A2, FINSEQ_1:18; :: thesis: verum