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 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 ;
:: thesis: verum