let PTN be Petri_net; 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; for t being transition of PTN holds
( t is_firable_at M0 iff <*t*> is_firable_at M0 )
let t be transition of PTN; ( t is_firable_at M0 iff <*t*> is_firable_at M0 )
hereby ( <*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 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;
( 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 )
;
( <*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;
verum end; assume
t is_firable_at M0
;
<*t*> is_firable_at M0then 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;
verum
end;
assume
<*t*> is_firable_at M0
; t is_firable_at M0
hence
t is_firable_at M0
by FINSEQ_4:16; verum