[MUSIC] Okay, so we are now at a point where the worst-case production time of a given production has been coupled to the worst-case consumption time of the same number of tokens, plus the execution time of the actor. But, actually want to do one step back and I want to continue from. This part of the formula. And now the next thing, if you remember my sketch of the proof is that we have to look at the eager scheduling. Now, eager scheduling was really a dragon of a formula. In week two, I explained it already. I'm just going to do a small recap eager scheduling means that at any point of execution, so at any point of execution the U in this case. There exists a point, a buffer B. And a consumption arrow that leads into it. And for that buffer, you know that at every earlier point at least, that buffer was completely emptied. What does that mean? Well, that means that the total number of consumptions. Is bigger than the total number of productions into the buffer, plus the initial number of tokens in the buffer. And we've also seen that completely empty to was a bit imprecise. What we really want to say, is that you could not have consumed more than what you actually consumed which means that any additional consumption would make sure that you would go over the number of tokens that was in that buffer. Now, for data flow graphs, we can actually simplify this formula and make it into a bit of a smaller drag in. The first thing is that an actor actually, it's a single rate data flow graph, which means that only one token is consumed at a time. And it means that this part and this part can be simplified a bit because you do not have to add up over all the arrows that can zoom from this buffer, you only have to pick one arrow. So, you only can write 1 there. And the same thing is, because it's a data flow graph, you know that there is only one incoming and one outgoing arrow. You do not have to add up over all the other arrows either. Which means that these sums are also a bit redundant. Because you can only pick one of them. And if you look at the smaller than sign. If one number is smaller than another number, and we're talking natural numbers here, and so one number's smaller than another number plus one. That's the same as saying that it's smaller than or equal, and forgetting about the plus 1, right? And if we do that, then we get this formula and I will have to remove my scribbles again, there it comes. [SOUND] We get this formula which makes life a little bit simpler. The crux of the formula is still that we can find a B such that for every earlier point a buffer it or this condition holds. How do we fill that in, in our estimate of the worst-case production time? Well, we fill that in here. You can see it coming up. This is what was already there. And this is the new part. And it says the number of consumptions at point v and there is this cv here you can see that indicating that the choice of c and the choice of b actually this should be a b thing as well the choice of b are dependent on v the number of consumptions is larger than b v, than the tokens at the input, and for any earlier point this condition holds. Now, we're going to play around with this condition a bit because of course you can also you do a plus iota b here, and you can also do a minus iota b on the other side, and we know that this cv is also smaller than this n, so we can take that condition smaller than n here. Then we can remove some of the other remarks. So, pay attention and maybe try to do this on paper for yourselves. And you can get to this. So, now we have the iota b to the other side, and we have used the condition that it's smaller than n. And we have a nice formula like this. Now, the next step. Is a bit tricky. We're going to look at sigma-t here and we're going to use the continuity again. And I'm going to give you the whole derivation in one go. [COUGH] Using the continuity of time, we know that every lower value than sigma-t, so then this occurs before the point of execution v. So, within the context. So, if you can fill in this here, which means that you can also fill in this. It's the supremum of all the time at all earlier points of execution, so the time at point v is the same as the supremum of all times of earlier points, which, because we know that at earlier points this condition holds means that it's the same as the supremum where we've plugged in that condition. Which means that it is smaller than the supremum where you actually removed the condition that the point should be earlier. Cause now we're just taking a supremum over a weaker condition. And that one you could recognize is actually the worst case execution time, or the worst case production time of the previous excerpt that was connected to the buffer bv. Then of course you have this one step which is basically a one step logical step from the proof sketch. If you know that it's equal to the production time at this earlier point then you can also say it's smaller than doing this for all previous vectors. Because the maximum overdose will also only make the estimate bigger. And that means that finally, we've ended up with the formula that we were looking for. Now, this formula we are going to continue with, and now we are going to look at the whole graph. We're going to take a whole graph and do multiple steps, because this formula describes basically how you go one step back in the graph. You start at some point and you look at one previous point in the graph. You trace back over one actor and one buffer. But, if you now make a whole pass through the graph, then you can do even more useful things with this formula.