let IAlph be non empty set ; :: thesis: for fsm being non empty FSM of IAlph
for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
q1,(w1 ^ w2) -admissible = (Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )
let fsm be non empty FSM of IAlph; :: thesis: for w1, w2 being FinSequence of IAlph
for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
q1,(w1 ^ w2) -admissible = (Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )
let w1, w2 be FinSequence of IAlph; :: thesis: for q1, q2 being State of fsm st q1,w1 -leads_to q2 holds
q1,(w1 ^ w2) -admissible = (Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )
let q1, q2 be State of fsm; :: thesis: ( q1,w1 -leads_to q2 implies q1,(w1 ^ w2) -admissible = (Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible ) )
assume A1:
q1,w1 -leads_to q2
; :: thesis: q1,(w1 ^ w2) -admissible = (Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )
set q1w = q1,(w1 ^ w2) -admissible ;
set q1w1 = q1,w1 -admissible ;
set q2w2 = q2,w2 -admissible ;
set Dw1 = Del (q1,w1 -admissible ),((len w1) + 1);
A2:
len (q1,w1 -admissible ) = (len w1) + 1
by Def2;
dom (q1,w1 -admissible ) = Seg (len (q1,w1 -admissible ))
by FINSEQ_1:def 3;
then
(len w1) + 1 in dom (q1,w1 -admissible )
by A2, FINSEQ_1:5;
then consider m being Nat such that
A3:
( len (q1,w1 -admissible ) = m + 1 & len (Del (q1,w1 -admissible ),((len w1) + 1)) = m )
by FINSEQ_3:113;
A4:
len (q1,w1 -admissible ) = (len w1) + 1
by Def2;
A5: len (q1,(w1 ^ w2) -admissible ) =
(len (w1 ^ w2)) + 1
by Def2
.=
((len w1) + (len w2)) + 1
by FINSEQ_1:35
.=
(len (Del (q1,w1 -admissible ),((len w1) + 1))) + ((len w2) + 1)
by A3, A4
.=
(len (Del (q1,w1 -admissible ),((len w1) + 1))) + (len (q2,w2 -admissible ))
by Def2
.=
len ((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible ))
by FINSEQ_1:35
;
now let k be
Nat;
:: thesis: ( 1 <= k & k <= len (q1,(w1 ^ w2) -admissible ) implies (q1,(w1 ^ w2) -admissible ) . b1 = ((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )) . b1 )assume A6:
( 1
<= k &
k <= len (q1,(w1 ^ w2) -admissible ) )
;
:: thesis: (q1,(w1 ^ w2) -admissible ) . b1 = ((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )) . b1per cases
( ( 1 <= k & k <= len w1 ) or ( (len w1) + 1 <= k & k <= len (q1,(w1 ^ w2) -admissible ) ) )
by A6, NAT_1:13;
suppose A7:
( 1
<= k &
k <= len w1 )
;
:: thesis: (q1,(w1 ^ w2) -admissible ) . b1 = ((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )) . b1then A8:
k in dom (Del (q1,w1 -admissible ),((len w1) + 1))
by A3, A4, FINSEQ_3:27;
A9:
k in NAT
by ORDINAL1:def 13;
A10:
( 1
<= k &
k < (len w1) + 1 )
by A7, NAT_1:13;
thus (q1,(w1 ^ w2) -admissible ) . k =
(q1,w1 -admissible ) . k
by A7, A9, Th20
.=
(Del (q1,w1 -admissible ),((len w1) + 1)) . k
by A4, A9, A10, FINSEQ_3:119
.=
((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )) . k
by A8, FINSEQ_1:def 7
;
:: thesis: verum end; suppose A11:
(
(len w1) + 1
<= k &
k <= len (q1,(w1 ^ w2) -admissible ) )
;
:: thesis: (q1,(w1 ^ w2) -admissible ) . b1 = ((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )) . b1then
((len w1) + 1) - (len w1) <= k - (len w1)
by XREAL_1:11;
then reconsider i =
k - (len w1) as
Element of
NAT by INT_1:16;
A12:
k = (len w1) + i
;
len (q1,(w1 ^ w2) -admissible ) = (len (w1 ^ w2)) + 1
by Def2;
then
(
(len w1) + 1
<= k &
k <= ((len w1) + (len w2)) + 1 )
by A11, FINSEQ_1:35;
then
(
(len w1) + 1
<= k &
k <= (len w1) + ((len w2) + 1) )
;
then A13:
( 1
<= i &
i <= (len w2) + 1 )
by A12, XREAL_1:8;
(
(len (Del (q1,w1 -admissible ),((len w1) + 1))) + 1
<= k &
k <= (len (Del (q1,w1 -admissible ),((len w1) + 1))) + (len (q2,w2 -admissible )) )
by A3, A5, A11, Def2, FINSEQ_1:35;
then
((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )) . k = (q2,w2 -admissible ) . (k - (len w1))
by A3, A4, FINSEQ_1:36;
hence
(q1,(w1 ^ w2) -admissible ) . k = ((Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )) . k
by A1, A12, A13, Th22;
:: thesis: verum end; end;
hence
q1,(w1 ^ w2) -admissible = (Del (q1,w1 -admissible ),((len w1) + 1)) ^ (q2,w2 -admissible )
by A5, FINSEQ_1:18; :: thesis: verum