00:00
It up right here. This is a wonder one copy of what I have in this event and what the will never work. What about it will? Never work. I saw him for the data is just like but not early, like skeleton is a stuff when we go away off into the medical inspector, there's a time stop and a lot of moving parties and I want a person to notice things.

00:34
So it's not like everything is like we could database everything. Generally the same shape. Sometimes I do it. Like this, This one is exposure. This is also this one. Everything is unique, everything special and it sounds special way. Like all they want to go to search system, like, get a full text search and send it to way.

00:58
I don't know how they want to. Yeah, get a link to it. Very all. I take it because I just put in a dry that always works. Yeah, to now, I don't know. The brakes. The part of conflict that gives me is there so much energy, and then also, it'll always like, go inside, like, the projects are not great to deal with.

01:23
And honestly, they're usually pretty big and relatively complex. So it's not like, like, it'll be like, oh, yeah. This project's deal and do these four readings. All right. That's like I don't have time number what it was but it was like do these readings turned in the homework and something else.

01:42
It was sweet. I don't know how you I don't and I feel like I have some dispensers. Go on, you've seen less and less students feel comfortable answering questions because we can't do all these readings. We've done and she hurts that this is super specific on a few points.

01:59
I was like, this is really what you're asking out of this quiz. You said to check that we didn't really. I didn't know if I needed to like, take notes and like, review them. Well, I guess I don't like you. Oh, my guess is because of one of the correct trigger, guys.

02:16
Well actually use the online version because I know I was like, if there was multiple choice for one that didn't have multiple choices. Like, yeah, that was pretty unfair. I was like, well, I didn't have the personality so I thought I didn't want to take it online. I didn't realize they were agreeing.

02:33
We had a giant advantage of giant, it's astronomical. Yeah, the first question of myself as well. As far as I said, there's too many, there's too many powers of ice to remember, I built 428 unlike. Well if you had them one time, we also saying that it generates a solution on the first default wasn't a solution to find other me, integer all white squares are all less squares.

03:00
Well, so that's why the one guy was kind of annoying because some solution is an answer. See, but I don't think, I think in the first few months expanding presuming, I really wouldn't return. So no white or all black unless that's just the only 50% of the would do that.

03:16
They just weren't correct. Yeah, I don't know. Well, that was the problem. The majority of the genetic algorithms don't return and applicable answer out of majority, I think most do the most aren't more strong periodic. Most not sure. I feel like they remember reading that they're reading regardless. There was so much reading it doesn't.

03:37
I don't know what I remember. I think.

03:46
Have to get out in that little bit of pressure.

04:09
Don't you don't have anything? Yeah, I would like not that.

04:45
Employment.

05:19
Or the program transfers processor transmission. I think one was everybody good. We still want to give them people, So anything that everybody had to do, what the measure of the problem was about. Now, one of the things that we have to give you money and if you are given, you know, anybody like that and got to be variables, I mean, you're not experiencing use that.

05:50
I mean, that's why they were given that. I mean you can solve the problem by basically you know having P&Q in some type of value and stopping the matrix. You know, in the, in the always, it's making sure this is, it would be done, but there's not enough, have a solution.

06:11
So, getting mine that have looked. I mean use what is given and conducive stuff using common sense and on your produce solution? So they had to matrix and this is one here.

06:34
And basically that what the guidance said that was facing beloved and left of peace. It's transposed and everything above. And right of cube is transported. Now, we're not in the matrix is not transportation. So we have to find initial values from PMQ. That make, basically allow the matrix to be entrepreneurs by having the range empty.

07:08
So if you if you basically have feed of the one here and three program,

07:19
Basically in variance as anything below and left of P, it's transpose. Well, there's nothing low and left, So that's fine. Every single bump and rifle cube is transmitted. And now so what we need to do now is figure out how we're going to transpose the idol in the matrix to to get the result to that couple of strategies one strategy is the basically increment p and q increment p and recommend Q several.

07:55
So basically, you can have a statement that they speak would be plus one. And when he passed that and transpose, just all the session. And now the easier paste and then you can do the same thing just Q. So, you

08:29
And now Q. Well, within careful about it is that when you're doing this, to make sure that the range is correct because the range is not correct. If you extend into here, your transpose seems back. So you only want to try supposed to say that they'd love each other.

08:50
I think people doing this Now, and as a special case, you can fix Q and just move feet, have one of the homework, does that what we can fix P and just move key. But since P and Q are both given to you really, it's a more appropriate level solution than move.

09:18
Now, there's another possibilities that you need them together. So in that case,

09:40
It transpose all of those cells in the single as a single step. Again, you have to make sure that they stop, you know, something you don't get into the situation of reversing the transportation authority. Now there is a little problem with this approach which is, it depends on what happens different.

10:11
So you can get into situations. Is it very end here? But a peace here accused there and what I'm doing. So basically on incredibly big and implementing Q. So, humans here and P moves there. So now Peter is greater than Q. So that it's a violation of the invariant.

10:39
So you need to basically separate the two cases, is it even on earth? If the matrix, if n is odd, this situation cannot occur. Because what would happen is that you have a patent like this,

11:01
And when you do the next step, they're both here, but if it's even then you get a decisions and then you're not careful, you can sleep over. So you have two options. I mean, basically have to the end of the handle of two cases. And so, what some people did, they basically allowed to pee to increment but then Q, they tested Q.

11:31
And they did not determine Q in the same. I mean there is artists on any questions about kind of the nature of the problem. So my in my solution basically, oh, when I think that the number of you made the mistaken that corrected it not only made a mistake but basically writing inside the code the i34 a 300 he does not exist in our program.

12:10
You can use A in the proof to refer to like A B, the initial values of B. But it's not he's not, you know, you can't refrigerate later on only way to refrigerate because somehow you initialize a second matrix and you kept the old one to the initial values in one and use another one for work and you spend of never have So that is inside of the decoding.

12:43
So and obviously that people I think northeast but just to the emphasizing. So we're stopping these to values and if you look at the indices, you're going to realize that, you know, if you instantiate it, you're going to swap Ij and then they also spawn its called JI and company swap the gloves.

13:11
So in some though, what the statement does he does swaps in both directions, but there's the same values. So when you have a parallel bar, if you're scientist the same variable, the same value is legal. So if you have a parallel bar here in the same text colonical 3, and that is called an equal to plus 1.

13:40
They both are sleep and that's considered legal. Now, if you plus 1, so this becomes any. So even though we have, we are swapping in multiple places that the value system here. The result is the same where just swapping once that any questions on that?

14:25
So let's apply in my solution. I basically to carotene view separately.

14:38
This is clean and look good.

15:22
That's the key. And then the cube is the same In much easier to understand that. In some of the formulas you guys know who were. I mean, I really had to scratch my hand to figure out what this is doing right or wrong. So, it is important, the way you write, Okay?

15:41
So this is making me clear that you are traveling from P to cube that entire bracket. And if you look at the texture, that's exactly what you're doing. Because so as much easier to just think about it. And, and the reason about,

16:04
Okay, no. A lot of proof we have, I mean we have they need least support that seller. So the way I I approved it is number one or something guardian. And basically says,

16:32
The PNQ has stayed with us, staying within the matrix because I, you're gonna have to use adapt that can go in at some point. When please, you go to keep those thing. Is that? This is not a way to think about the problem that makes it clearer in terms of guidance.

16:56
Look at this area. Hisp is cute or the t equals t plus 1 part when does that do that first every single index in the ray? So it's just so be. It's kind of, I mean, he's fixed and we implement one of our Everybody gets transposed, and figured. So, it's exactly exactly.

17:31
Moving from here to there. And from there, little bit of scripture, there's something interesting about it. Notice this area. What's true about the area?

17:52
The same as A. And what's true about this other area is a transcript so it's another way to kind of present things cleaner in terms of what they happening without waiting. So basically what happens is that we have all over J.

18:20
10 and what please? Hi. Okay, here. So, the t-shirt equals a pi and everything got in for all IG. Right. J q be

19:03
So basically this exercise anything between P and Q is converted. Everything outside the area. It is transmosed. It's simpler cleaner to think about it. And you know and of course we have to prove the team variance and initially they're true because everything is not inverted, we're going to end is nothing worth it and there's nothing outside.

19:34
So initially all of them contain this is missionary true because we initialize it to one and then somebody made a mistake and initializing to to to and and minus one. So that was all falling on and that's referred to from Guardian. Basically we look at the statement and we can see that feed has moved above 1 and part of that move all these cells.

20:13
I mean, I'm transferred, so that so that will not transpose before in the region. Now become transposed, In terms of? Yeah, leads to It's interesting that. I mean, some of you have not really looked at the fact that you need to show that when the metric is zero, he implies.

20:44
So so basically you have, you know again the simplest metric is really Q1 speed, that's is bonded by because of this invariant here is bounded by zero below and then when pmq are equal, then there's nothing in between them except for itself and BI from that equal. Because if I get, I entering equal and that's, and that means that they were on the way, swipe.

21:34
So that's that's okay. And then based on this one everybody that's everybody else's. It is served transpose. So you have to basically show that new people. Okay, these two and then you

22:07
Okay, and then you have to show that movie called zero implies close. Now they were to shove, that is a really cool to zero complies to people and compute. So the interesting part and then people think of Q, we could provide a disadvantage. Then we've got we've got post.

22:32
So so there's nothing more to three program. We have people cute and valued two.

22:58
Pain.

23:07
So the two interesting things to prove his progress, you only look at the fact that just I don't imagine being independent, The rest of us starting to

23:29
So this only piece that is important, including the price and that makes us think easier. So all of you that this decreases. We have two statements and you know, they're not we're not equal. So therefore, this is exactly and therefore peace. It's more.

24:03
So that's one of the questions You PNQ were critical to fully progress. And to prove the progress, you do not have to worry about the fact that the matrix was being converted over to prove the process. And so the people confusion then we use it on the values to show the forces and often the case that the invariants are paying seems together and only need to show progress on one on one thing.

24:36
So even if you want to do it not dramatically formally. It's very easy to show that people are equal to plus one actually answered about the headings of assignment with streaming but it's much complicated to be able to transposition. So this one of the vision,

25:10
It's the benefit of your posts if you show that again here, if you show the PMQ is table,

25:30
Then you can say it's table equal and in value. And and that used to that implies statement for being too long over there because yeah. Yeah, listening. So, that's a way to approach the ability, much much easier and other than I'd be from this understanding. So, improve this. I mean, you simply find that what they did.

26:07
I simply write the ingredients. I simplify the code. I did a progressive strictly on the P&Q with learning anything else. Then I using Guardians to prove that people can advise the post and that was to build your post. Again, I use the stability of being compute. I've been guarding split using implication and it's not.

26:39
So you don't always have to do in directly. I mean you use a color. What you need to use it. To look what you don't always have to to use a code if you come up with a knife that I'd be right. Also notice that being variant is really defining the way you think about this solution crisis.

27:01
It was involved in the forces us to only to this kind of solutions bruising and rules out as a social questions.

27:35
That even odd problems. Very easy to to because you are playing it, the proven formally. So you do not run into the situation where you use together, that the consumption of even on. Okay. Spring break, and obviously, there's nothing to do next week. So the next home office is due to this and so we're gonna let our shift to some.

28:08
I mean, it's kind of weird today because you're gonna do sense. Something I'm gonna shift Monday action but impractical great engineering focus on the other direction. That was very clear. So we kind of go over the places. So the problem that you are getting is an assignment is ready, it's very practical problem.

28:31
So you are home or six, you have to develop this interview, specification for an electronic brake system. So you want this electron break to be safe. So, your company accepted the contract to develop the software and the electronic emergency parking, right? I'm obviously breaking two typical microprocessors which are obviously development that they are just treating to ensure $40 and after response to driver presses and releases a colorful control.

29:09
And So it's a button here. Just touch it and there's a remover collared on it. Like Alex the driver president to control the engagement of emergency.

29:35
So if your neighbor if you you can go the internet and you can see people and you stupid things at 80 miles analogy pulling, you know what happened? They died. So, clearly these company was once know, quality product there, that is safe. So, even though the user may press that, you know, So the first step in developing the electronic brake software is to specify the requirements for the entire system.

30:09
Actually, the contract requires on the software to the approval. Correct. Besides you I lost to develop a formal specification of electronic brake system. Keeping mind usability and the safety of the drug. This is really based on a real and a real consulting experience. I have the company hadn't signed the contract.

30:33
They're gonna have this emergency brake for, you know, some high-end car, like the sport, and that they would prove the system, they know the code and they do nothing about verification. So they didn't name basically, you know, they call the intro when a pickle was supposed to prove it, but there's no way for more government for us.

30:59
I'm making them 10,000 lives. What they should have done, is to bring the controls structure into. Once, in the module, it used to profile as they controller. And then under the assumptions about the rest of the system, like for instance, that you gave the right, velocity information, or whatever else.

31:20
And there those assumptions. Then control the behaves, quite pleasing for them. And I don't know what happened to the contract in the end particular season. So anyway, so what is available to you? Well, first of all, you have to think about the brake, the abstract level, The blanket is a state, and so the state of the grade is going to be important in the specific.

31:51
Well, the specifications would wrote in both variables. Those are really the state of the program. This is not a program really, with this moment is a specification for the system, so we enter. So we need to come up with an abstract state of the system and then look at the properties for how this understands thing can change or may not be a lot of change.

32:16
So that was a description of the abstract state of the system, including events, like press release department and data state of the grade instead of the field because of important. So you need to make one of decisions about applying the emergency brake information that you No you cannot solve this problem.

32:42
By saying, I think you, you do not think you, you think, right human eye. The only properties that you think of what you want to break to do or not to do it when I name it. And once you die, you do that, then you start looking at how you actually translate your English language properties into associations of our business system.

33:14
So you know, he guidance can be used for those integrity. Unless can you use the constraint transitions? These two can use the force by response and

33:33
Two things is that you're gonna come up with crazy things that I'm not gonna make sense in terms of formalization, and that's okay. We work, we work through. Here's gonna get feedback on. And the other thing is that you have to try to keep it simple. So, for instance, many of you because my physics and high school in college, you want a single continuous variable, okay?

34:03
So the speed of the car is between 0 and 260 miles an hour, I know you're looking at that generation and deceleration, you know, got no. So looking physics. Make deals. Do not deal with discreetly. So it's the highest high speed on low speed, only stops and things like that.

34:29
Break it up into kind of finite number of conditions. What it needs to be high. Speed doesn't really matter to us. And the reform only by the end of singles or let's say composer now, right? Okay. But what else is just specification, you know? Because that definition that constanted brackets.

34:52
It can be changing back later on the things. So not just continuous the results, try not to rely on time. And finally,

35:08
It's very bad of your code to. I mean, that's real time systems where timing is important for them, for more systems. You know, do not invoke hard. Think of, you know, options events, think of state. And also remember that this is normal that, the government model is very much focused on thinking about states.

35:37
So, you have available invariant on this list, but you may not need them, depends on. And now this thing is done.

36:07
Something questions, you didn't talk about the two macro processors in our system. Do we need to clear about? Well, I told you that was just a very the processor. Whether you have one processor, 10 processor or a hundred, the specification should be. So if you send sending the signal, the express the button, then two micro processors needed to respond.

36:43
Yeah, but your designing. Now, what I do the specifications, I'm not designing. We want to say, what is the behavior of the button. So when I press a button, you know what states I'd rather than and like I should be allowed to do.

37:12
The office vacation, a reasonable specification can be done, five nights a year. I mean, almost financially depending how complicated they are. So, but make sure you try to write a sentence in, put a one property. One send us an image property to

37:38
But before you do all of this, you talk about the abstract, what is important in your decision processes. If the altitude at which the vehicle is running, it's important that you have to have that information the locations important and you have to have that information. If it's not important, that's not part of the system, 20% of what it's needed in YouTube in order for you to make that.

38:03
So for the system, the software to make the registration, they need the velocity of their power, that's your duration. We need the time of day, whatever. Okay. Rule out says that you don't need but make sure that anything that is needed is that I assume that the if the brake process is fully engaged with the power, you know they are force single because mechanical kind of brake basically four strings to go to the four wheels and they bring the, you know, the brakes on the, on the drum.

38:46
So that the implementing the foot brake, which is basically on the side of the drum, and then this would be additional. So it doesn't does a plus pressure. It don't stay out of the visual time keeps in simple. You don't need to use all the funding. All the mechanisms that they have available is only the start with the technologically, as an engineer, think everything to me at first, it is not important logic, how you find system to work, and then you turn into someone, a specialist and formal specification and will transfer

39:39
The questions.

39:44
Tried.

39:50
Okay. So, what I would like to do next is to review another properties that

40:04
Touch with move magic that might show up in some work later on. So this, I'm not saying that you need to be are going to be tested on and not seem to be going to need to

40:23
The memories. But those are very basic questions that I'm going to do a book or something In the middle of the school. The proceed answer, the most specification. Well, I knew whatever. There's something that's always going to tell me because I forget ensures cannot be used in insurance can only produce improves of a program because we have statements that can be and ensure the transition and that's specification.

40:56
You don't have the code so you don't know what statements are there. So you never use insurance. You may use leads to or you can use idea until basically combinations. And okay, so the only situation is what you're going to need to refocus some of these properties. And the way the way to do it is the basically handouts and the summary says, apparently, the easiest one is a property.

41:26
I see, oh my God, I can't remember. I don't even sounded that com hundreds and thousands and really literally hund from that people can use and that but you know, you go to the matter. To the he says progressive progress. Properties being used here. That means you just go open it up and look at the form.

41:55
Okay, so so this standard things that we you can actually working. In this business you need to use a regular basis. We only touch on them because you don't use them as seriously other people working in the same as they say, but primarily for credit to the banks. So, So, what we want to do today is basically look at the number of keywords and

42:29
And if you depend on how much time we have this, we have that we may take some things actually try from some crews. So, you can see that if we don't have the time to leave the proof just to get familiar for the spread of pros around. I don't know if that's So we have another different property.

42:53
I mean, that would be fun. My pretty good. Remember that? Unless these two invalid, stable constant, these are all predicated nations and a pretty good size that they relate to predicates. So they are not really basic logic but rather than relationship between us that's what the human they do.

43:16
So, we have, unless

43:32
So it's called something called a different city.

43:42
It's basic recipe, unless

43:49
But remember that the definition of, unless is that the same people ever? Who are you moved to the next day?

44:03
Part of the same view, whatever purpose in the next state can also give you the speed. So that's why I pee on SP you know, nice makes sense and not not always very useful but it's true When other properties antidepress.

44:33
So if I stay here, can stay there forever. Or who can move to the state of the right? Well, they're only the universe. If you think about PM or three the universe is in providing, mistakes PMOP so you can move real estate.

44:52
Consequence weekly.

45:08
Is Q.

45:13
The logic of.

45:21
So yeah, the excuse says that because the same thing, whatever moved to Q but if you move to Q again a few

45:33
Two in price are which means that whatever his heart into subset of Q? So excuse to, why is all the truth. So I guess to be smaller than the scope of kids. So, if you move into, Into Q&Q requests. It's like, it doesn't matter.

46:11
Some queuing. So this is cute. So if you get into Q exercise,

46:30
From Junction.

46:37
So you have a theme on this shoe and deep pride and this, right? That a couple of things that that you can do and imposement junction.

46:58
And basically everything. Okay. And crime.

47:11
Appears your price or deprived more information. So basically is allowed to remove something to cure both true and impair those permissions. So, it's possible that you move to two. And the more secure and being primes will change. Well, obviously the cube and the preparing is still there, You take all the combinations and that shows you all the possibilities of transition and become legally.

47:59
We can also do these junctions of PO run and that's

48:12
And he brought or not to cry through travel and if you do PMT5, you don't always find it still to those pictures. And so for example, it's possible that you get computed time but possibly the only one of them is true and then you can get into surprise and please build up be changed and you can get into to the constable of.

48:53
So you see that, you know the I mean because it you know uses on everyday basis they can come up with this format just like that. Cancellation. So, I don't want to spend the time going through God. Tell us so consolation.

49:34
Basically says on this few and few, unless this for this

49:58
So we know there's a few, we can always train people. This allows the first 10, people don't realize the same, but you move from people to. It's also allows you to move from, you could get into God.

50:22
So that's exactly right. So basically that's exactly what to say. These are going to stay in. People are, you can.

50:43
Again, I'm not going to go through all of them. It's videos but just some things that are important.

50:59
We have reflexivity here, too.

51:06
And assurance.

51:12
One special case of insurance is implied since being implies P then be

51:24
Consequence. We can.

51:33
Be and first two, and one shot.

51:53
What is remember that I think and talk about it before. That color is not a man. Another logical name. He's a man in the sense that you're probably this and you have proven, that is not the logical. So if you know that some people are going to have they are going to get into the Q and Q implies R.

52:23
Then obviously, we're going to get a book. So that's what it and whatability.

52:38
The first.

52:47
He appears as false and people not because personals where the legal effect we can't be in any of those program state. I mean that ignoring their division by 0%,

53:09
Conjunction.

53:22
Kind of human and befriend in short. Okay. Pride. They have been deprived. Sure, be and refresh for the prime.

53:47
Two or few and two friends. Okay, so from P amazing field. Make it look cute from people. I'm gonna try and keep them looking for Christ. Both PMP primer through where I got to go to prime.

54:14
Can feed my state, the same for a female.

54:22
Trying to build.

54:27
And parts of business preference for true. And then means that we have not really made the temperature prime and so it's possible that people have made the foundation huge and get implying

54:49
Has been made.

54:58
Basically said that interest.

55:04
Or part ensures you. Or, and that's when you useful because I want to clean other international predicate there.

55:43
You pat.

55:48
Through the pain plus Q, then you can conclude that V impossible.

56:01
Prove that he leaves before.

56:11
Okay. Now.

56:17
Are always like the ones with the same name anymore, or yeah, that similar, but therefore for different problem for different scope. So referencing about this because 17 or insur and then the possibility of impossibility of insurance. So, before the seventh time the same man because I really think kind of property, but pretty No.

56:46
Okay. So together sense, kind of these are, it doesn't properties. And, you know, that's like I said, that happens with properties like this. And when you're working on everything basis because really keep up, we kind of need to know the money improves or going to some form of derivation.

57:13
And it's not really to be honest, is not as skilled as this class. Usually means this class is introducing this to this set of skills. Quite is not particular, is doing is using the one basic part of the temporal logic for the actual now. Three. So, I saw these things but, and one properties of and now we need to slow down because these are properties that I've read about.

57:51
So, I'm very lazy this.

58:25
Okay, So we wanna please

58:40
Couple properties that actually critical and make an effort to believe in. First of all, is John this junction. I'm going to use a so to help you with enough because I don't know, Somebody wishing number. So, the first line from the three which is general is pass,

59:13
So we have a set said let's give it

59:24
And improve that for all.

59:31
Peace. Okay, things go.

59:41
Then it can come through the variation and said that and

59:55
Leads to and there isn't him, you know?

1:00:15
Okay, so I had this domain done. So let's three three times. So once all and w compute the PM Facebook, it's about properties that are. It depends on the values of the name. No. What to conclude is that before able to show that. If this is, if we are able to prove this, it's our proof obligation, then it's in conclude that the one value for region.

1:00:55
Peace seeing is true. That's what I need to that. There is a value of an inclusion. So notice here, we have BML QM under the same projects and tied to the same event but it's what all possible situations. So if in in all cases you move from P to Q and you find one case and it must be a case that the larger for people for the.

1:01:37
I mean there's one case that would follow from this. So that's that's very for why? Because you're gonna use this for case analysis, So you have three cases improve. Another also contact us. This is true. Then you can, then you can preserve the fact that if you are, if there is one that's true.

1:02:08
And the properties established and not. This is see the end little property here. There's nothing. So is this a property at the P? B is not a function of N in this property q. Got the q. It was another function of m. So now us to basically get rid of the end because it will be today's case.

1:02:38
And then we, if we show that you can get everything one of the steps, you know, that all this days that you could be in, you can go to one of the state. And these, the next one is going to be one of the other equations. That's an infinite rule.

1:02:56
It's an infinite rule. Another question is, if they're training them in the both ends. No. See this is another quantifier. Oh yeah, so this end is valid only here, okay, and this end is not even from here to here of this. And this end is one equality from here.

1:03:18
I can change the end here. Here. Take leave this and change this to m prime of changes and dollar fragment the meaning doesn't change. So this is when it's a this is proof essentially these two by conditions like three states. Remember, when you had problems? Because ensur, because in some state, you have to choose statement, one in some stage, you have to choose them too.

1:03:47
That's exactly the property that we're using. We showed that no matter which way we do, we are going to make it

1:04:13
For on the constellation.

1:04:26
So basically says that he leads to few of the can be leads to Christ, can converted please convinced to heal or so you see what's happening in the school cancellation because this allows us so this proof, it can Here for those cancellations. So, and part of the inflation is that in being, and they must go out.

1:05:11
Then we could have gotten into few firsts, and then we're going to go out. All right by still being peace here and but because it came to heart. So we and I got into the Q. So I'm going to have these are two or five. I know, I'm waiting my head.

1:05:33
There's not the way that matters, and there's another way to launch it, But that's kind of the level that we need to have a little bit of what this understanding of this formula has to be able to use them without actually going through support. That is, we have some time, I'll show you how to prove some of this formulas but these are decided important formulas and going to show up again in again.

1:06:03
And so it's remember the name of it and remember why it's useful, this is useful for you know privately show that no matter which state you're already going to make the progress. So, these are algebra places by cases. This allows you to make good term and the formula we will get to something that you need to get here has been

1:06:38
Progress.

1:06:49
Today, we don't receive this.

1:06:55
So this is a combination of properties, of progress and problems that involve say and then within something about, so P leads to Q and par.

1:07:15
So this is the progress property. The second part that says it's a few of that particular, eventually again interviewed They said that we're going R, don't replace you can go is people. But then you can conclude that if you are the team and are that leads to are for

1:07:44
So, so I still try this true because we have true, and obviously, you can eventually get into the queue, and possibly out of students, not artists, but true. So we get to an art for provide, you can make a transition to be. So, that's why you have one or

1:08:16
Skin number six. Number seven, induction.

1:08:35
If you want to use impact and basically using kind of thing. So program, and

1:08:56
And empty or better.

1:09:05
If you don't find it based on a function of this kind of stuff.

1:09:16
And smaller women for

1:09:27
Then it can improve.

1:09:43
So,

1:09:47
So basically what this is saying is that for all for any possible value of the metric that mentioned decreases or two becomes true if you become a student really equivalent to the metric. Cannot increase. Couldn't hit zero. Therefore post is established so safe. So I mean the you know kind of a more formal way and flying it is really going to show that the magic decreases.

1:10:27
We have this power here. Sometimes we use that ours used that metric was greater than zero degrees. This is my journal basically says that music decrease more to establish. Definitely not your music. So now we know that people then became concluded P.

1:10:57
So, this peace

1:11:13
That can use.

1:11:23
Okay. So these are properties. He was basically safety parts, so I see. You have progress, safety and computer projects, the first countries. Okay pattern. Okay, so we we can take a break now and I can do it. I mean, I

1:12:13
We could use after the break and we have an arm to do one proof. And then remember that. I'm going to, I'm gonna take a problem and practicing about performance justification about overhead system. So, like

1:12:46
520, You always take advantage of me.

1:13:48
Building.

1:13:53
Are really like the beyond fine right now. So they're cutting off like the other called the like the old ways or whatever they're called. So, so everyone has to turn that the little like, at the light instead of going to the yield thing and it added like 30 minutes to my trip.

1:14:12
Well, is no one can drive. Any actually was interesting to theirs. I was driving to. Actually more kind of unruly driver than ever before. I mean, people just jumping from one lady to another squeezing between two cars on. I mean, I always see some in a, you know, it's a half an hour trip.

1:14:42
I've already seen one two but because you serial near misses but here

1:14:57
But today was just crazy. I mean, I basically my name was going at 60 and I just stated my name right asleep. That's all crazy today. From this light, all the way up there between us. They're not the traffic in front is stopped. Anyway, so they're very overly understandable.

1:15:29
Who's beat up to slow down. Yeah.

1:15:37
Midterm season. Look at the roads.

1:15:45
Maybe single, where's it driving? Since the panda. I'm gonna be able to forgot how I am thinking. Like, we've always been mad at you. No, it looks always been sad but it feels worse. So this is like you were, you were normalized to it for a very, very long time and then you just didn't drive for a little while.

1:16:06
Yeah, it could be that. Well, you know, like if I go to South Africa for dinner, think the Chinese are not like to come back that same evening. I mean I stay all the night with friends is really nice drive through. Rudolph the five extra minutes, please and you don't want to go really like oriental and increase 25, you know, whatever, it's 25.

1:16:41
Yeah. So the question because no speed coming back happening.

1:16:54
Issue.

1:17:02
The facility question. Like, here it, I mean, this is just a contribution. That's a sign. Now how I use a number? Okay? So I use a number to show that the the method reasoning needs to be the great content. So actually you have more guys pounding from and then we have there.

1:18:07
We have proved yeah. That if you have this number then yeah we could also choose the metric. They give this sense of distance to the goal and 10 steps from the hand. So if I make it stay well, I wouldn't feel nice and understood because this doesn't go prove that, you know, we have to get in closer.

1:18:37
Yeah. Okay, I'm thinking

1:18:49
Here. And clicking the door, everything.

1:19:12
You're really fine. Anybody going someplace? It's been great and not going to anybody doing some Christmas. It's my bad. I'm going to do songs the second week industry. There's two weeks ago, Second weekends. Yeah, I'm going to bed tomorrow and my wife has a conference. So I'm just pass, We have double the conferences and most of my life are travel to conf wife, came with me.

1:19:56
What even when you never dropping that matching? I think. I'm not this week but I guess. Yeah, I saw that. I,

1:20:09
You know, the state is driving. But I wish they had the initial rules, which was in the future was six feet away and put pictures on. I thought it said that at first, and then they took it back and I mean, these classical feel bad, I mean, but there's 360 and enforcement in class that had for his parents, spread over twice, the size of this class community that you're having.

1:20:47
Well, I my wife bought me a speaker.

1:21:00
We have it. I don't have much conversations more, you know, if the speaker moved a little bit low then almost on. Didn't pick up the boys. Okay, so what they're gonna do now, again, you don't need to, I mean, you don't need to take notes. You just Watch this screen So the way we look at our lesson, one of the properties for our lives was.

1:21:35
So if you want, this is a really important thing. Something. So, let's sing have that's you

1:21:53
And the property says that we have P crime or this in few prime or required. Few, for all the combinations of Africa. It was move. You get that in front of the movie that one of them. So the question is, how do you prove? I mean, it's like an, it's commonly used and there's an example where the proof is directly from the definition, So it's very, very easily constructed.

1:22:38
So we know what, P on this field means and depend on SQL, So we can basically say paid my Q. Press promise, B or Q and we have pain. And so, if you pray, man, I'm not prepared as important. So this is first definition, definition of this. So as soon as these are true because as they are given to us, some other similar reasons in the proof, Okay, but that's okay.

1:23:22
Now I can combine it so we can basically take the left hand side to the right hand side. So basically, we have being and not and prepared.

1:23:47
Statement. Then we combine the other side. You on a cube.

1:24:04
And because this left hand side, Size and coldness site.

1:24:17
Okay, so so far it's all mechanical we're looking at definitions and just combined it with the know about this Now. But this is not what we need to, what we need to prove is this. So now,

1:24:42
From basically we now apply the definition here and we have the problem and this is P part unless not Q. So, now we have to do and not parentheses and in front

1:25:10
People and Q or the crime. Because, you know, it is beep and not give and understand. And then we have P4 Q.

1:25:35
Time or same thing. We about to go or not.

1:25:44
More parents.

1:25:58
So we call this inside the phone.

1:26:09
Well, if we are not here, the left hand, side implies left hand side. One, the writers like to improvise right inside and then I got out because there was a concept. So I've been implies I mean being like q and then already price W then we can make Google TW.

1:26:43
So, now, what we have to prove is basically left hand side inside.

1:26:59
So this is our left side here.

1:27:11
So, copy over.

1:27:19
And another

1:27:26
And,

1:27:46
Some of flies this.

1:27:58
Not.

1:28:16
Okay. So that's something you improve left inside, because coffee from there, right? Outside that I won the company from here, right changes. Now we have and now you have to apply them and not. So that means we get not t, and the prime and not the problem here and not the

1:29:09
Okay, So being happy.

1:29:19
So if he is through, then if they have water to try he promises him having a moment to and people they could not cure, or not surprised because we have this true that as a reminder. So we basically end up with having PNP prime and not confront and not Q.

1:29:51
Well, that's exact.

1:29:58
So that was one part of the Out of our prove that, right? And so I won implies right hand side. So, the right hand side, one is this.

1:30:29
PLS Q and

1:30:36
Right, we can do this to the community here. And then again P crime or p different or pride cube or here.

1:31:09
Prime Q and try. Looks exactly it. So sound approved, basically justice definitions and you just consequence can imply secure and then you know just all and only need to do this is a friendly you know sophisticated property approved a lot to be very equations.

1:31:56
That exercise in the glass nodes That's all in the past. So it doesn't automation. I just wanted to look at the thinking of how they build up. I think that time. So the precedence of between and this and latency called this junction so presidency. But the the yes, so well this unless all of them, oh, because oh, you can't have something for you sometimes.

1:32:45
Some of you used to be stable type of and unless something just left more videos, please.

1:33:38
Okay, so let's try now to make sure. So, it doesn't seem

1:33:51
P or Q.

1:34:05
So somebody else had proven it force so we can we assume that this is a melody and now just approved for showing the news to support our group process but it's a difference with somebody here that audio stuff. Now, what we need to prove is that

1:34:44
We need to prove P and sure few more time.

1:35:09
No improving this. Where allowing users? This has any transfer so you can always use any difference. Look at some is already.

1:35:21
So, here's the way we might run to the proof. First, let's say P and sure you that is

1:35:38
This page was here. So we assume that at all, then the ladies is formula and it's AP and Q for

1:35:57
Short is basically you just said t and true who is few or not Q. Would you still be across the pure my queue so we can for

1:36:26
For now, we have this property above So this which is after like that. So now we can do this concl, okay, P we think this is

1:37:00
Few more. Okay. So more car or the future?

1:37:16
Let's so we have this greatly investments here to go there. So this thing was there and we have to ensure that it's right here. You only have your car here.

1:37:45
More being queue. This is called an hour so that's that fact. There is QR.

1:38:17
And you want to but this is a cube fewer.

1:38:26
And then the heart. There I go. There. So really apply this formula to this and then what you get next is Not Q. Ensures few cars, because Q.

1:39:01
Few or you and P to the same as Q. The cube for P&Q. It is. So again for them to get a Q&A. So, there's an example of where we used, basically. Just influence, rules took care of Now.

1:39:37
The other proofs in the think about this problem, stop here. But one proof, it's actually the former appointment. That's very interesting because what we do the basically we use them ambitious let's start. Okay they start at least we get that idea. So there. So, there you go. We got two proofs that are important here inside.

1:40:08
Rise of the isbug induction. That is one of the, the proof on a different in the kind of induction the PhD probability. But then prove them, the induction is actually on the lens of the proof. So you need to break out the proof on the different assumptions. How many steps of what it took to get to this section of the?

1:40:37
So you have assumptions, right? If I promises if I promise is one the street and then the conclusion and that proof how long, how many steps it take. And and then based on that, you have to cover all the cases of different, a different group. So actually end up with having you know I think we prove this three different times intending on the what they're able to prove before.

1:41:18
Like for example the base case would be insured. He improved prove it from in one step. The next case would be trans activity or that needs. So that means that, you know that how to 10 steps, he is to prove this after that. He was perfect. Now I have to show that from 11 steps so you assume that is what provided intense types and then you combine them so that would work for 11 months and you have to do the same thing for this.

1:41:55
And it's very interesting. Conceptually the to think about inducted process, which is really, based on the number of steps. And if you need more improving things so far so I could you don't need to study the data, but do look at it just to see how to get the sense of.

1:42:18
But let's look at the least the industry. So, we had the adoption.

1:42:33
I'm doing shortage in the previous.

1:42:56
That's what we need to have. For the formula we're going to be using. But this actually passes another train though. They pass it to our large economy. Just the principal magnet induction. So that

1:43:29
Automatically induction. Looks like this for all and

1:43:39
And,

1:44:05
So we don't this in high school, you can prove that it is true for the assume that is true for 10 minus 1 and the prove that by being through 49 as one I can prove it to program then we'll show that it's true for all values of a right.

1:44:23
But that's a way of we're doing it. So the problem because other people here because this formula here just of this of this principle. So what you're going to do? Don't take any of them. I'm going to be find it as being P of M, these two, and they're going to find purebred.

1:44:59
To be pain and adjust the definitions. Choose the formula for this can be anything, right? And then this is defined, so

1:45:27
So now you take this program and we use this definition set. So now we have all them

1:45:48
All, and

1:45:55
Your batteries to. So this was for all them more than them, take a bed or pay when his piano is the kid. So we just substitute it. This amount to that. And and there promise few again here's M a of them that's really about. And if we are able to prove that then can conclude

1:46:37
Pee from him.

1:46:43
Which is basically a plan. It's happening here. Totally did for substitution for the definition of chose for a

1:46:57
So what we know how to prove is that given this become completed if that's the case and we perfect. So approved kind of goes like this.

1:47:32
So this is a premise by routers where it's outside. It's okay. So if you can do this for all and might be junction, maybe there is an end for. So, and then maybe

1:48:07
So just apply this junction here, then we'll play a little trick here. So cute.

1:48:21
And promise to because it's cure implies Q. That means ensures the experience of school 73 purely student. So now we apply these junction to these two, and we get, there is so we take this formula at this time. So this too, there is an end.

1:49:03
Okay. Now, here to turn out that the BLM

1:49:12
There is inside that and smaller than

1:49:27
Then some transitivity is a Q&A place for this. Is that part, please?

1:49:44
Now, this is to be shown that part of. And now we have been able to prove this provider here and the name of the prove that from this formula can get to this. Therefore this must be true.

1:50:10
So, that means

1:50:18
Pleasure.

1:50:24
For all of.

1:50:39
Has stopped with this over in carrying out this proof and therefore, you can take this program. That is true. So just pop it. This. Probably. Okay. Now, again, by these junctions, there is started about These compute. Well, those who can do that. Because Mondays Q does not depend on that to define the thing I can take out and I can rewrite this with the reason them.

1:51:20
But that p and and we plan.

1:51:28
And then I can be like this because PWM feet and there's an end and Q. It's always true. The metriculis of events. Again, I treat what we need to.

1:51:58
As more than

1:52:03
And he just tapped him. There's a page of her performance.

1:52:13
Kindly had the medical principle of induction to the

1:52:22
That's really questions. I remember, you don't know how this in order to the vision from this, PCM from this confession from death. That's another one attack.

1:52:47
Any questions and induction? We always do the investing step and plus one, we are not needing do not need to use and plus here. No. I mean, basically.

1:53:10
We just tend to show that the metric decreases can be like more than one.

1:53:53
The question.

1:54:09
Yeah, I hate changing all the more than a dozen blocks and it won't happen technology to have that good for you. Well, I would like to listen to and impressive good. If the devices is real. But unfortunately, the devices, I mean, at least if they had a system motivation because press apartments, they like sending that and he's that don't develop my feelings 10 years.

1:54:49
Well, my wife's got changes on the man who doesn't change time zones in Arizona. My God does not Another, my car has two. Clocks is a decent part and I don't know, and they're not tied to together think. And actually, we have to take, thank you. It's not the big man.

1:55:12
But everywhere in the first, the house a lot. I did some protocol corrupted changing, the tests pain and ignorance and a half. It's on protocol and I don't memorize it. I have to go to books. Oh yeah, you have to press twice this and then three times the other five times this and then you'll see a miracle happen.

1:55:35
All right, So I thought I wanted a, this would be an infinite difficult lecture and understand. So now there's no work and so I'm gonna give you a problem and how much was at least, remember the homework you have to come up with aspect and then the rules. So the problem that we have, it's probably coming from problem.

1:56:15
The system that was I should say that this system has been used as a standard test for specifies because specifications on less students. Don't kind of conference is, if you came up with new way of to do things, they don't say well why don't you show it to them on this like that?

1:56:41
For me, of course, 1 and and then the elevator has doors with open and close the floors and doors close, just open. And the, the floors, the buttons.

1:57:29
And another big,

1:57:41
And some other papers so far, one.

1:57:50
Outside or inside where they in the fire.

1:57:58
So You need to think about this problem. Think, what's important? It was a specifying paying public license. So get down to like 35 minutes to make some reasoning. Was, I'm targeted. So, you can use that this the project into

1:58:29
That was important. Open clothes. All right. Well which if that's actually something that's wrong. Yes. Google elevated moving or something.

1:59:17
Or with the previously elsewhere alignment number, That's enough bundles, for each other. Well, that's happened on button on this floor. It would be amazing and fireworks. This one.

1:59:42
We still here, we'll

1:59:47
What are those bottom buttons in the left? So normalized under one button because people usually press one and that's going to be elevator the two differences. Service. So, this is

2:00:11
But instead of that technology needs to be an op. Hold down request. Okay.

2:00:35
Going to be cutting them, this may be happening.

2:00:46
To the request comes from the cabinet.

2:01:01
And open the door long, and

2:01:07
I'm not the same about this state of and becomes a the time.

2:01:19
Population of the state. Because over one whether you're not ignored, Well forget about this information. No of that but it's more to create one. All right.

2:01:49
Again, kind of like, I think it Lego.

2:02:10
Calling the elevator. This is right. So,

2:02:27
Was.

2:02:31
Yeah, you're currently what are you?

2:02:39
Work. We should have some that's before, so it's a bargain right now. Like in the comment right here.

2:03:15
Don't know about. Okay, so what you're playing is now I'm two seconds. I mean, one is what we want. One of the properties that of the manufacturer. The other question is, what, how are you going to represent the state? So you can come through this problem because you just state doesn't belong to government as any map, actually, exactly.

2:04:12
You, I think exclusion of a little part will list location of going crazy. The stock is pos program. So I'm at for one another request here, just take it forward.

2:04:44
If there are questions you want, I just passed you right here, the whole receiver because you don't wait a little bit of reach location to bankruptcy. Locations, somewhere with you. The doors really the hardest thing about this thing. The cabinet. Is that how do you think about this paper?

2:05:17
You're going to learn. Yeah videos. Please up or down these rooms, which is the 24th of we don't have applications but across

2:05:59
And the macaroni.

2:06:10
Program. So we think, you know that we start

2:06:22
So this group here is basic pointing out, you just need variables to keep track of the various things in this mistake. So like where does no?

2:06:37
Doors. That's exactly what you did. Right existing the 1938. If not the question is with those second, just stay here become because every branch that comes with this. When you press something, Thank you for specifically. Okay, I'm gonna write on the board. You tell me what's what's stayed variables?

2:07:39
You have identify so far. So, let's start with the back there because it already done coming. So, you have to think about the cabinet part of the variables about it.

2:08:02
Standard openers, close the doors and door door, door standards.

2:08:12
And the third part is the boolean. Okay. Welcome. Before something open is. Okay, what else did you have?

2:08:31
And that was from one then, right? What else? But but the battery requests are really not community part of the kind of state of the artificial. The the customers or something like that. So, I'll put that separate. I guess it's important.

2:09:04
Okay, so what kind of unboxing me one through end? Okay, so many videos.

2:09:21
But is people defining like that. You basically says it's an only one in a town, all right? So it's in a sweet just set set subset to set my plan. Right.

2:09:47
Some of the okay. So basically, that's what we have another way to do this. Is we can have cabinet request k. That's bullied and pays people from one man. So we have one one for each. Okay. So anything else we need the cases moving. So,

2:10:22
And that's again, bullying everything and maybe maybe cleaner to make the other reason, but now just for this. Okay? And the warranty, actually.

2:10:41
Coming down.

2:10:45
Don't know.

2:10:50
That's just bringing reasonable.

2:10:56
Okay. Now, tell me in general, what do you want the elevators to? And it went properties. I will be interested. You are buying this elevator or you are asking somebody to manufacture people. Know what is so interesting? With our properties of people, we don't want them to move. The doors are open, okay?

2:11:20
So that's called a safety property from a more like community safety. But safety problems. So they are so we have to have a environment.

2:11:36
So what is safety requirement?

2:11:42
Whatever they are. Okay. What are the requirements? We coordination when someone asks before just like it should be a queue or some kind of stuck, but access implementation is we have service.

2:12:09
So about what instance, if I make a call or like the kind of elevator, they eventually come and serve as a call.

2:12:22
So if we assume that this is a reasonable representation of which is a call, but yeah, we were

2:12:42
We have sense door.

2:12:53
Right. And again, we can I guess that we can find it in terms of all doing very clear. But in that except for buttons, we also have your current example and flirting down called

2:13:21
Not potatoes different, right? Because you're like, you're requesting to go to that cabin cage, but you're calling from this database, there's a difference between number. However, okay. I'm not gonna say,

2:13:39
Is it when something integrity is?

2:13:49
Think of the top floor in the bottom top floor. Can you savor here then? But like, k, equals what I meant, that's really equal to them. So according to this representation, we could have how to prohibit it. Just not impressed but and all the way through mathematically, however you say that is not he left.

2:14:40
Well, I mean you can have the choices or you can see the length of in, okay, for adults. So I have close to from one to another one. Now goes both from to n to, okay, but there's another thing you can have, you can write any variant.

2:15:12
Okay, unless in. Yeah. So where we like to cook should never have that? Be true turn also down to be unifor in the representation but then we have a clean constraint that we expect and move by taking the button now because of the body. And basically requiring, that is never true how you implement.

2:15:46
It is never true. Even for the button there or maybe you just basically depress nothing happen. So, whatever, that's example of how you can expressification to important constraints with him, but God started other floor. Yeah. That's no Spanish. Okay. So, give me an example of safety, same thing. But wild cabins move, okay?

2:16:16
Well, the door cannot be opened and the doors. Not open if they're not at the floor, right? Okay. Yes. But they're always at the far, the ignorant? No, he's saying the circular doors. I'm having a presentation for 48 years. I have been, we're not moving and handbrake. So you have to be at the floor, have to be not moving and then you can, then you can have the door.

2:16:57
So that is not a maybe. So here is an example of how you can write on different specification. The elevators ever floor. Not moving. You run the doors to be open if you are even on the door of the opening guardian, if basically say head floor, not moving implies the robot.

2:17:24
Okay, so that's you know, that's an example. And either way to say that we can be on the floor and not moving. And then the door and the door doesn't feel, so the specification changes if you do that. But safety is going to have to go. A lot of ways the drawers not going through the stealing and not going through the ball.

2:17:52
Those wouldn't be kind of safety safety. What about service?

2:18:08
Turn on call from the floor and leads to elevator eventually being there for going that direction. Right? So so, basically, you could, well, listen to the other also have been very basically says, without being more or just making an application again, okay? And stop implies having

2:18:47
True capitalist Open.

2:18:53
Now, you said to start handling this and look at what it says about. It doesn't say.

2:19:14
Different doors might have these so that might not be very nice if you did. So, you could what he sounds and says, carrying door the problem. Even only if which God pull them back to relevation here.

2:19:58
So, we can say having our open and coming from

2:20:09
Okay, you've been on the

2:20:16
Floor.

2:20:24
Fourth. Okay, So then if we know that here. So the cabin door in the floor, I was only about location and because that's a kind of formulas that now. We suggested so I have an app called. Okay. Please do what whatever being there. Yeah. So, so coming for

2:21:17
Okay. Okay. So now what does that formula? I say and what doesn't say That maybe going down. So that's that's so many and maybe having the election.

2:21:45
Okay. For what even though the stuff it doesn't require it to stop. It just says, if I press a button to grow up, there are eventually going to be there but as it required to stop. So if we say doors open, since we have specified in the environment, but doors open the line, it's really well.

2:22:12
If you have this, they have to start. Yeah, so then we have the foundation to start and then if you combine this with that then you know the doors are open and inside now, fine. Okay, so let's say that we have now. A condition of basically says, if there's enough gold eventually, we get to the because that floor except right.

2:22:42
Good. So what happens? Now example,

2:22:56
Goes away. Turns out. There's the sounds like you should turning off how? There's nothing here to the other things. It's nothing here to prevent us from trying both. So, so you've got to specify the fly. It's an elevator that can get nasty, but it doesn't like certain apples. It just kind of turned off another.

2:23:21
So, plenty of specifications with Nothing, you can never know that, elevator is conservative, and it doesn't let it never turns off any lights specification laws that to have

2:23:39
Until you've been walk.

2:23:45
Well again, but I mean you can. So again, you have to decide do all that. I know it if you're going up and that there's a short below, you can leave it pressed if you want. And then, eventually universal services more. You can basically say, you know nothing's gonna happen You made President Obama from time to so you always have any also, no in that family request or second service academy because not just talking

2:24:26
And he for instance, you want to his opal to stay on and could actually good. You can use something called field until it's basically for these two and an unless

2:24:49
That's so it is until here instead of at least two, then they call. Can they call the state of the coil? Buttons is forced to stay on and see, you know, the formula I mean first of all you have to start thinking about what are the properties that you want from a system.

2:25:17
And then you have to cause them to look how you're going to formalize the system right before precipitation. And then you have to look at the form of precision analyzing. What is it saying? What it does and you always start using what our stock specific and then you can find it.

2:25:35
So you start with the specifications which says, eventually this is going to be but not, just like it doesn't say. It doesn't say that if I pass by and floor, I need to open the door. This is the eventually I'm going to get to it. So, I could basically think towards somebody place an alcoholic, and I this transcription of the line deliver and go 10 times, a hundred times up and down up, and never found and eventually stop.

2:26:10
There has to be after 100 days from so coming one kind of approach is to start abstractly and basically say, okay, the obligation is to eventually get them and then after that, you cannot promise these, you know, do you want, you know, minimum time. Something that happened. So then you can refine the specification.

2:26:44
Hopefully we can write a spec at the high level like eventually something is going to happen and then we can find that eventually into smaller steps. So you know that's that approaching you. You take that's not it's it's something we're not asking a lot from this. Elevator is very simpler later but here, you know the specifications require.

2:27:16
What is thinking to get? I have used it's going to point with your stitches over.

2:27:29
Okay, and I don't. Whatever It will. Eventually eventually move doesn't have to do it anytime soon or you and everyone would be lucky the stairs. It is just pressing the wheels. It goes before randomly Air Forces need to get out before. It'll move on.

2:28:21
Yeah, and Michael three months. I just have one of the

2:29:05
But if you are using box, then you have to because it will impact. Okay? Okay, that

2:29:33
The car will be no car and it's the long not emergency brake system.

2:29:49
Think of you don't know what to code. Oh okay. So I want to tell you what? How God for just talking about. So, someone was driving really fast, and then they just wanted to no one like this. Okay. So we have to think of old is like, I mean think of a real brain But that wanted to do it example.

2:30:22
One of the car is driving so fat but then the normal break doesn't do anything. So you have to I mean well yeah but you did it's a different way of. I mean, they maybe a different state of them, power break it whether you move, what you don't when maybe the base it fails,

2:30:47
Maybe because some cars but you can think of it when you press a button can hit multiple interpretations depending on the street. So maybe you are the 80 miles an hour and press the button it should just play music particularly 20 miles an hour impressive button, it should slow you gradually down and maybe if you're starting to raise apart television, the whole engage.

2:31:13
So you you're on a stop light vision. You don't know. No. You got when we so for the variable is the emergency is it's going to be on for all. Okay, so your choice, you can make it on and off, good. I don't really know how Are worms. And how much larger, how much of a reality we have to great is correct.

2:31:45
I don't know how. So, in real life, I mean we don't want to apply. I mean, if you stopped reply to break system, you'd want them to say high speed or low speed. If the driver side,

2:32:07
No. No. But you can use different government. Oh power. So, you break of the body supply, the different power. Okay, that makes and hear this flaw of or the same. So, I just want to make sure that we don't. No, Thank you. Can we still send you emails? Very cool.

2:32:42
It's great.

2:32:47
Choose traveling to choose Wednesdays through Tuesday. So, you know, afterwards there's going to be and have our programs together and then my computer doesn't mean that.

2:33:09
Wednesday.

2:33:37
Yeah. But today's time of the year and you're traveling. Yeah, but I mean, you know like then at the time I would answer them, I come around here. Restaurant is that. Thank you so much.

2:35:35
Nobody.