let PTN be Petri_net; for M0 being Boolean_marking of PTN
for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)
let M0 be Boolean_marking of PTN; for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)
let t be transition of PTN; Firing (t,M0) = Firing (<*t*>,M0)
set M = <*(Firing ((<*t*> /. 1),M0))*>;
A1:
( len <*t*> = 1 & <*t*> /. 1 = t )
by FINSEQ_1:39, FINSEQ_4:16;
A2:
<*(Firing ((<*t*> /. 1),M0))*> /. 1 = Firing ((<*t*> /. 1),M0)
by FINSEQ_4:16;
A3:
now for i being Nat st i < len <*t*> & i > 0 holds
<*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i))A4:
len <*t*> = 0 + 1
by FINSEQ_1:39;
let i be
Nat;
( i < len <*t*> & i > 0 implies <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) )assume
(
i < len <*t*> &
i > 0 )
;
<*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i))hence
<*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing (
(<*t*> /. (i + 1)),
(<*(Firing ((<*t*> /. 1),M0))*> /. i))
by A4, NAT_1:13;
verum end;
len <*t*> =
1
by FINSEQ_1:39
.=
len <*(Firing ((<*t*> /. 1),M0))*>
by FINSEQ_1:39
;
hence
Firing (t,M0) = Firing (<*t*>,M0)
by A1, A2, A3, Def5; verum