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 tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
(q11,w) -response = (q,w) -response
let w be FinSequence of IAlph; for tfsm1, tfsm2 being non empty Mealy-FSM over IAlph,OAlph
for q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
(q11,w) -response = (q,w) -response
let tfsm1, tfsm2 be non empty Mealy-FSM over IAlph,OAlph; for q11 being State of tfsm1
for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
(q11,w) -response = (q,w) -response
let q11 be State of tfsm1; for tfsm being non empty finite Mealy-FSM over IAlph,OAlph
for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
(q11,w) -response = (q,w) -response
let tfsm be non empty finite Mealy-FSM over IAlph,OAlph; for q being State of tfsm st tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q holds
(q11,w) -response = (q,w) -response
let q be State of tfsm; ( tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q implies (q11,w) -response = (q,w) -response )
set q1 = q11;
assume that
A1:
tfsm = tfsm1 -Mealy_union tfsm2
and
A2:
the carrier of tfsm1 misses the carrier of tfsm2
and
A3:
q11 = q
; (q11,w) -response = (q,w) -response
set ad1 = (q11,w) -admissible ;
set res = (q,w) -response ;
set res1 = (q11,w) -response ;
A4:
len ((q11,w) -response) = len w
by Def6;
A5:
now for k being Nat st 1 <= k & k <= len ((q11,w) -response) holds
((q11,w) -response) . k = ((q,w) -response) . klet k be
Nat;
( 1 <= k & k <= len ((q11,w) -response) implies ((q11,w) -response) . k = ((q,w) -response) . k )A6:
[: the carrier of tfsm1,IAlph:] misses [: the carrier of tfsm2,IAlph:]
by A2, ZFMISC_1:104;
assume
( 1
<= k &
k <= len ((q11,w) -response) )
;
((q11,w) -response) . k = ((q,w) -response) . kthen A7:
k in Seg (len w)
by A4, FINSEQ_1:1;
then A8:
k in dom w
by FINSEQ_1:def 3;
k in Seg ((len w) + 1)
by A7, FINSEQ_2:8;
then
k in Seg (len ((q11,w) -admissible))
by Def2;
then
k in dom ((q11,w) -admissible)
by FINSEQ_1:def 3;
then A9:
((q11,w) -admissible) . k in the
carrier of
tfsm1
by FINSEQ_2:11;
w . k in IAlph
by A8, FINSEQ_2:11;
then
[(((q11,w) -admissible) . k),(w . k)] in [: the carrier of tfsm1,IAlph:]
by A9, ZFMISC_1:87;
then A10:
(
dom the
OFun of
tfsm2 = [: the carrier of tfsm2,IAlph:] & not
[(((q11,w) -admissible) . k),(w . k)] in [: the carrier of tfsm2,IAlph:] )
by A6, FUNCT_2:def 1, XBOOLE_0:3;
((q11,w) -response) . k =
the
OFun of
tfsm1 . [(((q11,w) -admissible) . k),(w . k)]
by A8, Def6
.=
( the OFun of tfsm1 +* the OFun of tfsm2) . [(((q11,w) -admissible) . k),(w . k)]
by A10, FUNCT_4:11
.=
( the OFun of tfsm1 +* the OFun of tfsm2) . [(((q,w) -admissible) . k),(w . k)]
by A1, A2, A3, Th52
.=
the
OFun of
tfsm . [(((q,w) -admissible) . k),(w . k)]
by A1, Def24
.=
((q,w) -response) . k
by A8, Def6
;
hence
((q11,w) -response) . k = ((q,w) -response) . k
;
verum end;
len ((q11,w) -response) =
len w
by Def6
.=
len ((q,w) -response)
by Def6
;
hence
(q11,w) -response = (q,w) -response
by A5, FINSEQ_1:14; verum