let IAlph, OAlph be non empty set ; :: thesis: for w1, w2 being FinSequence of IAlph
for tfsm being non empty Mealy-FSM of 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; :: thesis: for tfsm being non empty Mealy-FSM of 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 of IAlph,OAlph; :: thesis: 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; :: thesis: ( q1t,w1 -leads_to q2t implies q1t,(w1 ^ w2) -response = (q1t,w1 -response ) ^ (q2t,w2 -response ) )
assume A1:
q1t,w1 -leads_to q2t
; :: thesis: 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;
A2: len (q1t,(w1 ^ w2) -response ) =
len (w1 ^ w2)
by Def6
.=
(len w1) + (len w2)
by FINSEQ_1:35
.=
(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:35
;
now let k be
Nat;
:: thesis: ( 1 <= k & k <= len (q1t,(w1 ^ w2) -response ) implies (q1t,(w1 ^ w2) -response ) . b1 = ((q1t,w1 -response ) ^ (q2t,w2 -response )) . b1 )assume A3:
( 1
<= k &
k <= len (q1t,(w1 ^ w2) -response ) )
;
:: thesis: (q1t,(w1 ^ w2) -response ) . b1 = ((q1t,w1 -response ) ^ (q2t,w2 -response )) . b1A4:
k in NAT
by ORDINAL1:def 13;
A5:
len (q1t,w1 -admissible ) = (len w1) + 1
by Def2;
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:5;
then consider m being
Nat such that A6:
(
len (q1t,w1 -admissible ) = m + 1 &
len (Del (q1t,w1 -admissible ),((len w1) + 1)) = m )
by FINSEQ_3:113;
A7:
m + 1
= (len w1) + 1
by A6, Def2;
A8:
len (q1t,w1 -response ) = len w1
by Def6;
per cases
( ( 1 <= k & k <= len (q1t,w1 -response ) ) or ( (len (q1t,w1 -response )) + 1 <= k & k <= len (q1t,(w1 ^ w2) -response ) ) )
by A3, NAT_1:13;
suppose A9:
( 1
<= k &
k <= len (q1t,w1 -response ) )
;
:: thesis: (q1t,(w1 ^ w2) -response ) . b1 = ((q1t,w1 -response ) ^ (q2t,w2 -response )) . b1then A10:
( 1
<= k &
k <= len w1 )
by Def6;
then A11:
k in dom w1
by FINSEQ_3:27;
( 1
<= k &
k <= len (w1 ^ w2) )
by A3, Def6;
then A12:
k in dom (w1 ^ w2)
by FINSEQ_3:27;
A13:
k in dom (q1t,w1 -response )
by A9, FINSEQ_3:27;
A14:
( 1
<= k &
k < (len w1) + 1 )
by A10, NAT_1:13;
A15:
k in dom (Del (q1t,w1 -admissible ),((len w1) + 1))
by A6, A7, A10, FINSEQ_3:27;
thus (q1t,(w1 ^ w2) -response ) . k =
the
OFun of
tfsm . [((q1t,(w1 ^ w2) -admissible ) . k),((w1 ^ w2) . k)]
by A12, Def6
.=
the
OFun of
tfsm . [(((Del (q1t,w1 -admissible ),((len w1) + 1)) ^ (q2t,w2 -admissible )) . k),((w1 ^ w2) . k)]
by A1, Th23
.=
the
OFun of
tfsm . [((Del (q1t,w1 -admissible ),((len w1) + 1)) . k),((w1 ^ w2) . k)]
by A15, 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 A4, A5, A14, FINSEQ_3:119
.=
(q1t,w1 -response ) . k
by A11, Def6
.=
((q1t,w1 -response ) ^ (q2t,w2 -response )) . k
by A13, FINSEQ_1:def 7
;
:: thesis: verum end; suppose A16:
(
(len (q1t,w1 -response )) + 1
<= k &
k <= len (q1t,(w1 ^ w2) -response ) )
;
:: thesis: (q1t,(w1 ^ w2) -response ) . b1 = ((q1t,w1 -response ) ^ (q2t,w2 -response )) . b1
( 1
<= k &
k <= len (w1 ^ w2) )
by A3, Def6;
then A17:
k in dom (w1 ^ w2)
by FINSEQ_3:27;
A18:
len (q1t,(w1 ^ w2) -response ) =
len (w1 ^ w2)
by Def6
.=
(len w1) + (len w2)
by FINSEQ_1:35
.=
(len (q1t,w1 -response )) + (len w2)
by Def6
.=
(len (q1t,w1 -response )) + (len (q2t,w2 -response ))
by Def6
;
then A19:
k <= (len (Del (q1t,w1 -admissible ),((len w1) + 1))) + (len w2)
by A6, A7, A8, A16, Def6;
len w2 <= (len w2) + 1
by NAT_1:11;
then
(len (Del (q1t,w1 -admissible ),((len w1) + 1))) + (len w2) <= (len (Del (q1t,w1 -admissible ),((len w1) + 1))) + ((len w2) + 1)
by XREAL_1:8;
then
k <= (len (Del (q1t,w1 -admissible ),((len w1) + 1))) + ((len w2) + 1)
by A19, XXREAL_0:2;
then A20:
(
(len (Del (q1t,w1 -admissible ),((len w1) + 1))) + 1
<= k &
k <= (len (Del (q1t,w1 -admissible ),((len w1) + 1))) + (len (q2t,w2 -admissible )) )
by A6, A7, A16, Def2, Def6;
A21:
len (q1t,(w1 ^ w2) -response ) =
len (w1 ^ w2)
by Def6
.=
(len w1) + (len w2)
by FINSEQ_1:35
;
then A22:
(
(len w1) + 1
<= k &
k <= (len w1) + (len w2) )
by A16, Def6;
A23:
(q1t,(w1 ^ w2) -response ) . k =
the
OFun of
tfsm . [((q1t,(w1 ^ w2) -admissible ) . k),((w1 ^ w2) . k)]
by A17, Def6
.=
the
OFun of
tfsm . [(((Del (q1t,w1 -admissible ),((len w1) + 1)) ^ (q2t,w2 -admissible )) . k),((w1 ^ w2) . k)]
by A1, Th23
.=
the
OFun of
tfsm . [((q2t,w2 -admissible ) . (k - (len (Del (q1t,w1 -admissible ),((len w1) + 1))))),((w1 ^ w2) . k)]
by A20, FINSEQ_1:36
.=
the
OFun of
tfsm . [((q2t,w2 -admissible ) . (k - (len w1))),(w2 . (k - (len w1)))]
by A6, A7, A22, FINSEQ_1:36
;
A24:
((len (q1t,w1 -response )) + 1) - (len (q1t,w1 -response )) <= k - (len (q1t,w1 -response ))
by A16, XREAL_1:11;
then reconsider p =
k - (len (q1t,w1 -response )) as
Element of
NAT by INT_1:16;
k <= (len (q1t,w1 -response )) + (len w2)
by A16, A21, Def6;
then
k - (len (q1t,w1 -response )) <= ((len (q1t,w1 -response )) + (len w2)) - (len (q1t,w1 -response ))
by XREAL_1:11;
then A25:
p in dom w2
by A24, FINSEQ_3:27;
((q1t,w1 -response ) ^ (q2t,w2 -response )) . k =
(q2t,w2 -response ) . p
by A16, A18, FINSEQ_1:36
.=
the
OFun of
tfsm . [((q2t,w2 -admissible ) . p),(w2 . p)]
by A25, 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
;
hence
(q1t,(w1 ^ w2) -response ) . k = ((q1t,w1 -response ) ^ (q2t,w2 -response )) . k
by A23;
:: thesis: verum end;
hence
q1t,(w1 ^ w2) -response = (q1t,w1 -response ) ^ (q2t,w2 -response )
by A2, FINSEQ_1:18; :: thesis: verum