let P be set ; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ; :: thesis: fire t2,(fire t1,m) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
A2: Pre t1 c= (Pre t1) + (Pre t2) by Th16;
then A3: Pre t1 c= m by A1, Th14;
then A4: fire t1,m = (m - (Pre t1)) + (Post t1) by Def8;
A5: Pre t2 = ((Pre t2) + (Pre t1)) - (Pre t1) by Th19;
A6: ((Pre t1) + (Pre t2)) - (Pre t1) c= m - (Pre t1) by A1, A2, Th20;
m - (Pre t1) c= (m - (Pre t1)) + (Post t1) by Th16;
then Pre t2 c= fire t1,m by A4, A5, A6, Th14;
hence fire t2,(fire t1,m) = ((fire t1,m) - (Pre t2)) + (Post t2) by Def8
.= (((m - (Pre t1)) + (Post t1)) - (Pre t2)) + (Post t2) by A3, Def8
.= (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2) by A1, A2, A5, Th20, Th21 ;
:: thesis: verum