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) -admissible = (q,w) -admissible
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) -admissible = (q,w) -admissible
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) -admissible = (q,w) -admissible
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) -admissible = (q,w) -admissible
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) -admissible = (q,w) -admissible
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) -admissible = (q,w) -admissible )
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) -admissible = (q,w) -admissible
set ad1 = (q11,w) -admissible ;
set ad = (q,w) -admissible ;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len ((q11,w) -admissible) implies ((q11,w) -admissible) . $1 = ((q,w) -admissible) . $1 );
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
( 1
<= k &
k <= len ((q11,w) -admissible) implies
((q11,w) -admissible) . k = ((q,w) -admissible) . k )
;
S1[k + 1]
assume that
1
<= k + 1
and A6:
k + 1
<= len ((q11,w) -admissible)
;
((q11,w) -admissible) . (k + 1) = ((q,w) -admissible) . (k + 1)
A7:
(
k = 0 or (
0 < k &
0 + 1
= 1 ) )
;
per cases
( k = 0 or 1 <= k )
by A7, NAT_1:13;
suppose A9:
1
<= k
;
((q11,w) -admissible) . (k + 1) = ((q,w) -admissible) . (k + 1)
k + 1
<= (len w) + 1
by A6, Def2;
then A10:
k <= len w
by XREAL_1:6;
then consider w1k being
Element of
IAlph,
q1k,
q1k1 being
Element of
tfsm1 such that A11:
(
w1k = w . k &
q1k = ((q11,w) -admissible) . k )
and A12:
(
q1k1 = ((q11,w) -admissible) . (k + 1) &
w1k -succ_of q1k = q1k1 )
by A9, Def2;
A13:
ex
wk being
Element of
IAlph ex
qk,
qk1 being
Element of
tfsm st
(
wk = w . k &
qk = ((q,w) -admissible) . k &
qk1 = ((q,w) -admissible) . (k + 1) &
wk -succ_of qk = qk1 )
by A9, A10, Def2;
len w <= (len w) + 1
by NAT_1:11;
then A14:
k <= (len w) + 1
by A10, XXREAL_0:2;
[: the carrier of tfsm1,IAlph:] misses [: the carrier of tfsm2,IAlph:]
by A2, ZFMISC_1:104;
then
(
dom the
Tran of
tfsm2 = [: the carrier of tfsm2,IAlph:] & not
[q1k,w1k] in [: the carrier of tfsm2,IAlph:] )
by FUNCT_2:def 1, XBOOLE_0:3;
hence ((q11,w) -admissible) . (k + 1) =
( the Tran of tfsm1 +* the Tran of tfsm2) . [q1k,w1k]
by A12, FUNCT_4:11
.=
((q,w) -admissible) . (k + 1)
by A1, A5, A9, A11, A13, A14, Def2, Def24
;
verum end;
end;
A15:
S1[ 0 ]
;
A16:
for k being Nat holds S1[k]
from NAT_1:sch 2(A15, A4);
len ((q11,w) -admissible) =
(len w) + 1
by Def2
.=
len ((q,w) -admissible)
by Def2
;
hence
(q11,w) -admissible = (q,w) -admissible
by A16, FINSEQ_1:14; verum