let PTN be PT_net_Str ; :: thesis: for M0 being Boolean_marking of PTN
for t being transition of PTN holds
( t is_firable_on M0 iff <*t*> is_firable_on M0 )
let M0 be Boolean_marking of PTN; :: thesis: for t being transition of PTN holds
( t is_firable_on M0 iff <*t*> is_firable_on M0 )
let t be transition of PTN; :: thesis: ( t is_firable_on M0 iff <*t*> is_firable_on M0 )
hereby :: thesis: ( <*t*> is_firable_on M0 implies t is_firable_on M0 )
assume A1:
t is_firable_on M0
;
:: thesis: <*t*> is_firable_on M0set M =
<*(Firing (<*t*> /. 1),M0)*>;
A2:
len <*t*> =
1
by FINSEQ_1:56
.=
len <*(Firing (<*t*> /. 1),M0)*>
by FINSEQ_1:56
;
A3:
<*t*> /. 1
is_firable_on M0
by A1, FINSEQ_4:25;
A4:
<*(Firing (<*t*> /. 1),M0)*> /. 1
= Firing (<*t*> /. 1),
M0
by FINSEQ_4:25;
now let i be
Element of
NAT ;
:: thesis: ( i < len <*t*> & i > 0 implies ( <*t*> /. (i + 1) is_firable_on <*(Firing (<*t*> /. 1),M0)*> /. i & <*(Firing (<*t*> /. 1),M0)*> /. (i + 1) = Firing (<*t*> /. (i + 1)),(<*(Firing (<*t*> /. 1),M0)*> /. i) ) )assume A5:
(
i < len <*t*> &
i > 0 )
;
:: thesis: ( <*t*> /. (i + 1) is_firable_on <*(Firing (<*t*> /. 1),M0)*> /. i & <*(Firing (<*t*> /. 1),M0)*> /. (i + 1) = Firing (<*t*> /. (i + 1)),(<*(Firing (<*t*> /. 1),M0)*> /. i) )
len <*t*> = 0 + 1
by FINSEQ_1:56;
hence
(
<*t*> /. (i + 1) is_firable_on <*(Firing (<*t*> /. 1),M0)*> /. i &
<*(Firing (<*t*> /. 1),M0)*> /. (i + 1) = Firing (<*t*> /. (i + 1)),
(<*(Firing (<*t*> /. 1),M0)*> /. i) )
by A5, NAT_1:13;
:: thesis: verum end; hence
<*t*> is_firable_on M0
by A2, A3, A4, Def4;
:: thesis: verum
end;
assume
<*t*> is_firable_on M0
; :: thesis: t is_firable_on M0
then consider M being FinSequence of Bool_marks_of PTN such that
len <*t*> = len M
and
A6:
<*t*> /. 1 is_firable_on M0
and
( M /. 1 = Firing (<*t*> /. 1),M0 & ( for i being Element of NAT st i < len <*t*> & i > 0 holds
( <*t*> /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing (<*t*> /. (i + 1)),(M /. i) ) ) )
by Def4;
thus
t is_firable_on M0
by A6, FINSEQ_4:25; :: thesis: verum