let PTN be Petri_net; :: 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:16;

A2: now :: thesis: for i being Element of NAT st i < len <*t*> & i > 0 holds
( <*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)) )

A3: len <*t*> = 0 + 1 by FINSEQ_1:39;
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:16;
len <*t*> = 1 by FINSEQ_1:39
.= len <*(Firing ((<*t*> /. 1),M0))*> by FINSEQ_1:39 ;
hence <*t*> is_firable_on M0 by A4, A1, A2; :: 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)) ) ) ) ;
hence t is_firable_on M0 by FINSEQ_4:16; :: thesis: verum