let PTN be Petri_net; :: thesis: for M0 being marking of PTN
for t being transition of PTN holds
( t is_firable_at M0 iff <*t*> is_firable_at M0 )
let M0 be marking of PTN; :: thesis: for t being transition of PTN holds
( t is_firable_at M0 iff <*t*> is_firable_at M0 )
let t be transition of PTN; :: thesis: ( t is_firable_at M0 iff <*t*> is_firable_at M0 )

hereby :: thesis: ( <*t*> is_firable_at M0 implies t is_firable_at 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 Nat st i < len <*t*> & i > 0 holds
( <*t*> /. (i + 1) is_firable_at <*(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 Nat; :: thesis: ( i < len <*t*> & i > 0 implies ( <*t*> /. (i + 1) is_firable_at <*(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_at <*(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_at <*(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_at M0 ; :: thesis: <*t*> is_firable_at M0
then A4: <*t*> /. 1 is_firable_at 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_at M0 by A4, A1, A2; :: thesis: verum

end;

assume <*t*> is_firable_at M0 ; :: thesis: t is_firable_at M0
hence t is_firable_at M0 by FINSEQ_4:16; :: thesis: verum