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 q11 being State of tfsm1
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 & q11 = q holds
q11,w -response = q,w -response
let w be FinSequence of IAlph; :: thesis: for tfsm1, tfsm2 being non empty Mealy-FSM of IAlph,OAlph
for q11 being State of tfsm1
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 & q11 = q holds
q11,w -response = q,w -response
let tfsm1, tfsm2 be non empty Mealy-FSM of IAlph,OAlph; :: thesis: for q11 being State of tfsm1
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 & q11 = q holds
q11,w -response = q,w -response
let q11 be State of tfsm1; :: 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 & q11 = q holds
q11,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 & q11 = q holds
q11,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 & q11 = q implies q11,w -response = q,w -response )
set q1 = q11;
assume A1:
( tfsm = tfsm1 -Mealy_union tfsm2 & the carrier of tfsm1 misses the carrier of tfsm2 & q11 = q )
; :: thesis: q11,w -response = q,w -response
set res = q,w -response ;
set res1 = q11,w -response ;
set ad1 = q11,w -admissible ;
A2: len (q11,w -response ) =
len w
by Def6
.=
len (q,w -response )
by Def6
;
A3:
len (q11,w -response ) = len w
by Def6;
now let k be
Nat;
:: thesis: ( 1 <= k & k <= len (q11,w -response ) implies (q11,w -response ) . k = (q,w -response ) . k )assume
( 1
<= k &
k <= len (q11,w -response ) )
;
:: thesis: (q11,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 (q11,w -admissible ))
by Def2;
then A6:
k in dom (q11,w -admissible )
by FINSEQ_1:def 3;
A7:
dom the
OFun of
tfsm2 = [:the carrier of tfsm2,IAlph:]
by FUNCT_2:def 1;
A8:
(q11,w -admissible ) . k in the
carrier of
tfsm1
by A6, FINSEQ_2:13;
w . k in IAlph
by A5, FINSEQ_2:13;
then A9:
[((q11,w -admissible ) . k),(w . k)] in [:the carrier of tfsm1,IAlph:]
by A8, ZFMISC_1:106;
[:the carrier of tfsm1,IAlph:] misses [:the carrier of tfsm2,IAlph:]
by A1, ZFMISC_1:127;
then A10:
not
[((q11,w -admissible ) . k),(w . k)] in [:the carrier of tfsm2,IAlph:]
by A9, XBOOLE_0:3;
(q11,w -response ) . k =
the
OFun of
tfsm1 . [((q11,w -admissible ) . k),(w . k)]
by A5, Def6
.=
(the OFun of tfsm1 +* the OFun of tfsm2) . [((q11,w -admissible ) . k),(w . k)]
by A7, A10, FUNCT_4:12
.=
(the OFun of tfsm1 +* the OFun of tfsm2) . [((q,w -admissible ) . k),(w . k)]
by A1, Th71
.=
the
OFun of
tfsm . [((q,w -admissible ) . k),(w . k)]
by A1, Def24
.=
(q,w -response ) . k
by A5, Def6
;
hence
(q11,w -response ) . k = (q,w -response ) . k
;
:: thesis: verum end;
hence
q11,w -response = q,w -response
by A2, FINSEQ_1:18; :: thesis: verum