let IAlph, OAlph be non empty set ; for w1, w2 being FinSequence of IAlph
for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q1t, q2t being State of tfsm st q1t,w1 -leads_to q2t holds
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
let w1, w2 be FinSequence of IAlph; for tfsm being non empty Mealy-FSM over IAlph,OAlph
for q1t, q2t being State of tfsm st q1t,w1 -leads_to q2t holds
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
let tfsm be non empty Mealy-FSM over IAlph,OAlph; for q1t, q2t being State of tfsm st q1t,w1 -leads_to q2t holds
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
let q1t, q2t be State of tfsm; ( q1t,w1 -leads_to q2t implies (q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response) )
set q1w1 = (q1t,w1) -response ;
set q2w2 = (q2t,w2) -response ;
set q1w1w2 = (q1t,(w1 ^ w2)) -response ;
set Dq1w1w2a = Del (((q1t,w1) -admissible),((len w1) + 1));
set OF = the OFun of tfsm;
assume A1:
q1t,w1 -leads_to q2t
; (q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
A2:
now for k being Nat st 1 <= k & k <= len ((q1t,(w1 ^ w2)) -response) holds
((q1t,(w1 ^ w2)) -response) . k = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . k
dom ((q1t,w1) -admissible) = Seg (len ((q1t,w1) -admissible))
by FINSEQ_1:def 3;
then
dom ((q1t,w1) -admissible) = Seg ((len w1) + 1)
by Def2;
then
(len w1) + 1
in dom ((q1t,w1) -admissible)
by FINSEQ_1:3;
then consider m being
Nat such that A3:
len ((q1t,w1) -admissible) = m + 1
and A4:
len (Del (((q1t,w1) -admissible),((len w1) + 1))) = m
by FINSEQ_3:104;
A5:
m + 1
= (len w1) + 1
by A3, Def2;
A6:
len ((q1t,w1) -response) = len w1
by Def6;
let k be
Nat;
( 1 <= k & k <= len ((q1t,(w1 ^ w2)) -response) implies ((q1t,(w1 ^ w2)) -response) . b1 = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b1 )assume that A7:
1
<= k
and A8:
k <= len ((q1t,(w1 ^ w2)) -response)
;
((q1t,(w1 ^ w2)) -response) . b1 = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b1per cases
( ( 1 <= k & k <= len ((q1t,w1) -response) ) or ( (len ((q1t,w1) -response)) + 1 <= k & k <= len ((q1t,(w1 ^ w2)) -response) ) )
by A7, A8, NAT_1:13;
suppose A9:
( 1
<= k &
k <= len ((q1t,w1) -response) )
;
((q1t,(w1 ^ w2)) -response) . b1 = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b1then A10:
k <= len w1
by Def6;
then A11:
k in dom w1
by A9, FINSEQ_3:25;
A12:
k in dom (Del (((q1t,w1) -admissible),((len w1) + 1)))
by A4, A5, A9, A10, FINSEQ_3:25;
A13:
k < (len w1) + 1
by A10, NAT_1:13;
A14:
k in dom ((q1t,w1) -response)
by A9, FINSEQ_3:25;
k <= len (w1 ^ w2)
by A8, Def6;
then
k in dom (w1 ^ w2)
by A7, FINSEQ_3:25;
hence ((q1t,(w1 ^ w2)) -response) . k =
the
OFun of
tfsm . [(((q1t,(w1 ^ w2)) -admissible) . k),((w1 ^ w2) . k)]
by Def6
.=
the
OFun of
tfsm . [(((Del (((q1t,w1) -admissible),((len w1) + 1))) ^ ((q2t,w2) -admissible)) . k),((w1 ^ w2) . k)]
by A1, Th8
.=
the
OFun of
tfsm . [((Del (((q1t,w1) -admissible),((len w1) + 1))) . k),((w1 ^ w2) . k)]
by A12, FINSEQ_1:def 7
.=
the
OFun of
tfsm . [((Del (((q1t,w1) -admissible),((len w1) + 1))) . k),(w1 . k)]
by A11, FINSEQ_1:def 7
.=
the
OFun of
tfsm . [(((q1t,w1) -admissible) . k),(w1 . k)]
by A13, FINSEQ_3:110
.=
((q1t,w1) -response) . k
by A11, Def6
.=
(((q1t,w1) -response) ^ ((q2t,w2) -response)) . k
by A14, FINSEQ_1:def 7
;
verum end; suppose A15:
(
(len ((q1t,w1) -response)) + 1
<= k &
k <= len ((q1t,(w1 ^ w2)) -response) )
;
((q1t,(w1 ^ w2)) -response) . b1 = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . b1then A16:
((len ((q1t,w1) -response)) + 1) - (len ((q1t,w1) -response)) <= k - (len ((q1t,w1) -response))
by XREAL_1:9;
then reconsider p =
k - (len ((q1t,w1) -response)) as
Element of
NAT by INT_1:3;
A17:
len ((q1t,(w1 ^ w2)) -response) =
len (w1 ^ w2)
by Def6
.=
(len w1) + (len w2)
by FINSEQ_1:22
;
then
k <= (len ((q1t,w1) -response)) + (len w2)
by A15, Def6;
then
k - (len ((q1t,w1) -response)) <= ((len ((q1t,w1) -response)) + (len w2)) - (len ((q1t,w1) -response))
by XREAL_1:9;
then A18:
p in dom w2
by A16, FINSEQ_3:25;
A19:
(len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + 1
<= k
by A4, A5, A15, Def6;
A20:
(len w1) + 1
<= k
by A15, Def6;
A21:
len ((q1t,(w1 ^ w2)) -response) =
len (w1 ^ w2)
by Def6
.=
(len w1) + (len w2)
by FINSEQ_1:22
.=
(len ((q1t,w1) -response)) + (len w2)
by Def6
.=
(len ((q1t,w1) -response)) + (len ((q2t,w2) -response))
by Def6
;
then A22:
(((q1t,w1) -response) ^ ((q2t,w2) -response)) . k =
((q2t,w2) -response) . p
by A15, FINSEQ_1:23
.=
the
OFun of
tfsm . [(((q2t,w2) -admissible) . p),(w2 . p)]
by A18, Def6
.=
the
OFun of
tfsm . [(((q2t,w2) -admissible) . (k - (len w1))),(w2 . (k - (len ((q1t,w1) -response))))]
by Def6
.=
the
OFun of
tfsm . [(((q2t,w2) -admissible) . (k - (len w1))),(w2 . (k - (len w1)))]
by Def6
;
len w2 <= (len w2) + 1
by NAT_1:11;
then A23:
(len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + (len w2) <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + ((len w2) + 1)
by XREAL_1:6;
k <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + (len w2)
by A4, A5, A6, A15, A21, Def6;
then
k <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + ((len w2) + 1)
by A23, XXREAL_0:2;
then A24:
k <= (len (Del (((q1t,w1) -admissible),((len w1) + 1)))) + (len ((q2t,w2) -admissible))
by Def2;
k <= len (w1 ^ w2)
by A8, Def6;
then
k in dom (w1 ^ w2)
by A7, FINSEQ_3:25;
then ((q1t,(w1 ^ w2)) -response) . k =
the
OFun of
tfsm . [(((q1t,(w1 ^ w2)) -admissible) . k),((w1 ^ w2) . k)]
by Def6
.=
the
OFun of
tfsm . [(((Del (((q1t,w1) -admissible),((len w1) + 1))) ^ ((q2t,w2) -admissible)) . k),((w1 ^ w2) . k)]
by A1, Th8
.=
the
OFun of
tfsm . [(((q2t,w2) -admissible) . (k - (len (Del (((q1t,w1) -admissible),((len w1) + 1)))))),((w1 ^ w2) . k)]
by A19, A24, FINSEQ_1:23
.=
the
OFun of
tfsm . [(((q2t,w2) -admissible) . (k - (len w1))),(w2 . (k - (len w1)))]
by A4, A5, A15, A17, A20, FINSEQ_1:23
;
hence
((q1t,(w1 ^ w2)) -response) . k = (((q1t,w1) -response) ^ ((q2t,w2) -response)) . k
by A22;
verum end; end;
len ((q1t,(w1 ^ w2)) -response) =
len (w1 ^ w2)
by Def6
.=
(len w1) + (len w2)
by FINSEQ_1:22
.=
(len ((q1t,w1) -response)) + (len w2)
by Def6
.=
(len ((q1t,w1) -response)) + (len ((q2t,w2) -response))
by Def6
.=
len (((q1t,w1) -response) ^ ((q2t,w2) -response))
by FINSEQ_1:22
;
hence
(q1t,(w1 ^ w2)) -response = ((q1t,w1) -response) ^ ((q2t,w2) -response)
by A2, FINSEQ_1:14; verum