let P be set ; for m being marking of P
for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds
fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
let m be marking of P; for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds
fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
let t1, t2 be transition of P; ( (Pre t1) + (Pre t2) c= m implies fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2) )
assume A1:
(Pre t1) + (Pre t2) c= m
; fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
A2:
Pre t1 c= (Pre t1) + (Pre t2)
by Th4;
then A3:
Pre t1 c= m
by A1, Th2;
then A4:
fire (t1,m) = (m - (Pre t1)) + (Post t1)
by Def7;
A5:
Pre t2 = ((Pre t2) + (Pre t1)) - (Pre t1)
by Th7;
A6:
((Pre t1) + (Pre t2)) - (Pre t1) c= m - (Pre t1)
by A1, A2, Th8;
m - (Pre t1) c= (m - (Pre t1)) + (Post t1)
by Th4;
then
Pre t2 c= fire (t1,m)
by A4, A5, A6, Th2;
hence fire (t2,(fire (t1,m))) =
((fire (t1,m)) - (Pre t2)) + (Post t2)
by Def7
.=
(((m - (Pre t1)) + (Post t1)) - (Pre t2)) + (Post t2)
by A3, Def7
.=
(((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
by A1, A2, A5, Th8, Th9
;
verum