let IAlph be non empty set ; for fsm being non empty FSM over 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) . ((len w1) + 1) = q2
let fsm be non empty FSM over 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) . ((len w1) + 1) = q2
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) . ((len w1) + 1) = q2
let q1, q2 be State of fsm; ( q1,w1 -leads_to q2 implies ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2 )
assume A1:
q1,w1 -leads_to q2
; ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2
set q1w1 = (q1,w1) -admissible ;
set q1w = (q1,(w1 ^ w2)) -admissible ;
per cases
( len w1 = 0 or len w1 > 0 )
;
suppose A3:
len w1 > 0
;
((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) = q2
0 + 1
= 1
;
then A4:
1
<= len w1
by A3, NAT_1:13;
then consider w1k being
Element of
IAlph,
qw1k,
qw1k1 being
State of
fsm such that A5:
w1k = w1 . (len w1)
and A6:
qw1k = ((q1,w1) -admissible) . (len w1)
and A7:
qw1k1 = ((q1,w1) -admissible) . ((len w1) + 1)
and A8:
w1k -succ_of qw1k = qw1k1
by Def2;
len (w1 ^ w2) = (len w1) + (len w2)
by FINSEQ_1:22;
then
len w1 <= len (w1 ^ w2)
by NAT_1:12;
then consider wk being
Element of
IAlph,
qwk,
qwk1 being
State of
fsm such that A9:
wk = (w1 ^ w2) . (len w1)
and A10:
(
qwk = ((q1,(w1 ^ w2)) -admissible) . (len w1) &
qwk1 = ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) &
wk -succ_of qwk = qwk1 )
by A4, Def2;
len w1 in Seg (len w1)
by A3, FINSEQ_1:3;
then
len w1 in dom w1
by FINSEQ_1:def 3;
then
wk = w1k
by A9, A5, FINSEQ_1:def 7;
hence ((q1,(w1 ^ w2)) -admissible) . ((len w1) + 1) =
qw1k1
by A4, A10, A6, A8, Th5
.=
q2
by A1, A7
;
verum end;