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 )

set M = <*(Firing (<*t*> /. 1),M0)*>;
A1: <*(Firing (<*t*> /. 1),M0)*> /. 1 = Firing (<*t*> /. 1),M0 by FINSEQ_4:25;

A2: now

A3: len <*t*> = 0 + 1 by FINSEQ_1:56;
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 ( 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) )
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 A3, NAT_1:13; :: thesis: verum

end;

assume t is_firable_on M0 ; :: thesis: <*t*> is_firable_on M0
then A4: <*t*> /. 1 is_firable_on M0 by FINSEQ_4:25;
len <*t*> = 1 by FINSEQ_1:56
.= len <*(Firing (<*t*> /. 1),M0)*> by FINSEQ_1:56 ;
hence <*t*> is_firable_on M0 by A4, A1, A2, Def4; :: thesis: verum

end;

assume <*t*> is_firable_on M0 ; :: thesis: t is_firable_on M0
then ex M being FinSequence of Bool_marks_of PTN st
( len <*t*> = len M & <*t*> /. 1 is_firable_on M0 & 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;
hence t is_firable_on M0 by FINSEQ_4:25; :: thesis: verum