let IAlph be non empty set ; :: thesis: for fsm being non empty FSM of IAlph
for w being FinSequence of IAlph
for q, q' being State of fsm holds
( (q,w -admissible ) . (len (q,w -admissible )) = q' iff q,w -leads_to q' )
let fsm be non empty FSM of IAlph; :: thesis: for w being FinSequence of IAlph
for q, q' being State of fsm holds
( (q,w -admissible ) . (len (q,w -admissible )) = q' iff q,w -leads_to q' )
let w be FinSequence of IAlph; :: thesis: for q, q' being State of fsm holds
( (q,w -admissible ) . (len (q,w -admissible )) = q' iff q,w -leads_to q' )
let q, q' be State of fsm; :: thesis: ( (q,w -admissible ) . (len (q,w -admissible )) = q' iff q,w -leads_to q' )
hereby :: thesis: ( q,w -leads_to q' implies (q,w -admissible ) . (len (q,w -admissible )) = q' )
set qs =
q,
w -admissible ;
assume A1:
(q,w -admissible ) . (len (q,w -admissible )) = q'
;
:: thesis: q,w -leads_to q'
(
(q,w -admissible ) . 1
= q &
len (q,w -admissible ) = (len w) + 1 & ( for
i being
Element of
NAT st 1
<= i &
i <= len w holds
ex
wi being
Element of
IAlph ex
qi,
qi1 being
State of
fsm st
(
wi = w . i &
qi = (q,w -admissible ) . i &
qi1 = (q,w -admissible ) . (i + 1) &
wi -succ_of qi = qi1 ) ) )
by Def2;
hence
q,
w -leads_to q'
by A1, Def3;
:: thesis: verum
end;
assume
q,w -leads_to q'
; :: thesis: (q,w -admissible ) . (len (q,w -admissible )) = q'
then
(q,w -admissible ) . ((len w) + 1) = q'
by Def3;
hence
(q,w -admissible ) . (len (q,w -admissible )) = q'
by Def2; :: thesis: verum