let IAlph be non empty set ; 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; 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; 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; ( q1,w1 -leads_to q2 implies (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));
A1:
len ((q1,w1) -admissible) = (len w1) + 1
by Def2;
( len ((q1,w1) -admissible) = (len w1) + 1 & dom ((q1,w1) -admissible) = Seg (len ((q1,w1) -admissible)) )
by Def2, FINSEQ_1:def 3;
then
(len w1) + 1 in dom ((q1,w1) -admissible)
by FINSEQ_1:5;
then A2:
ex m being Nat st
( len ((q1,w1) -admissible) = m + 1 & len (Del (((q1,w1) -admissible),((len w1) + 1))) = m )
by FINSEQ_3:113;
A3: 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 A2, A1
.=
(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
;
assume A4:
q1,w1 -leads_to q2
; (q1,(w1 ^ w2)) -admissible = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)
now let k be
Nat;
( 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 A5:
( 1
<= k &
k <= len ((q1,(w1 ^ w2)) -admissible) )
;
((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 A5, NAT_1:13;
suppose A6:
( 1
<= k &
k <= len w1 )
;
((q1,(w1 ^ w2)) -admissible) . b1 = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . b1then A7:
k < (len w1) + 1
by NAT_1:13;
A8:
k in dom (Del (((q1,w1) -admissible),((len w1) + 1)))
by A2, A1, A6, FINSEQ_3:27;
k in NAT
by ORDINAL1:def 13;
hence ((q1,(w1 ^ w2)) -admissible) . k =
((q1,w1) -admissible) . k
by A6, Th20
.=
(Del (((q1,w1) -admissible),((len w1) + 1))) . k
by A7, FINSEQ_3:119
.=
((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . k
by A8, FINSEQ_1:def 7
;
verum end; suppose A10:
(
(len w1) + 1
<= k &
k <= len ((q1,(w1 ^ w2)) -admissible) )
;
((q1,(w1 ^ w2)) -admissible) . b1 = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . b1then
k <= (len (Del (((q1,w1) -admissible),((len w1) + 1)))) + (len ((q2,w2) -admissible))
by A3, FINSEQ_1:35;
then A11:
((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . k = ((q2,w2) -admissible) . (k - (len w1))
by A2, A1, A10, FINSEQ_1:36;
((len w1) + 1) - (len w1) <= k - (len w1)
by A10, 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
k <= ((len w1) + (len w2)) + 1
by A10, FINSEQ_1:35;
then
k <= (len w1) + ((len w2) + 1)
;
then A13:
i <= (len w2) + 1
by A12, XREAL_1:8;
1
<= i
by A10, A12, XREAL_1:8;
hence
((q1,(w1 ^ w2)) -admissible) . k = ((Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)) . k
by A4, A12, A13, A11, Th22;
verum end; end;
hence
(q1,(w1 ^ w2)) -admissible = (Del (((q1,w1) -admissible),((len w1) + 1))) ^ ((q2,w2) -admissible)
by A3, FINSEQ_1:18; verum