00:01
Time in. Detroit Excellence. My best. I know what that means.

00:37
So what he was just like black lady said from the south and she said, like, her song was like, I know that baby bless you before I hope you have a good break and give me a hard one.

01:07
Like go back to your goals.

01:14
My sometimes, I have to be a few minutes away because I'm in space and it's starting to medium and conditioning.

01:35
So, if you feel like,

01:53
Results.

02:21
There is yeah, exactly.

02:36
All right, things. You should hear that In this book.

02:51
Seems as if improvement. As if there's still a few people who are not getting enough help. And if you if you start working on the homework on Tuesday and I happen to have a dinner, when I come to gradually because I'm tired, kind of. So, I didn't understand that.

03:18
So today, no lecture, which is going to play, I mean, just to understand things better. And I think it's very important for you to think about your homework transgressions because you know I might see things up but you know don't always know if you're actually internalizing right now or they're just consulted, he says to take you.

03:41
So if I take it out. So, so what I'm going to do, going to start back. If specification is some people think I do trouble understand market and some people are actually trying to improve such clearly was stated that. So we'll go back to specification and talk a little bit about it.

04:05
Give you an opportunity to ask questions. Then we're going to look at an exercise where I'm keeping your solution. I'm giving you a specification. And then I have to prove that the solution actually needs a specification. And so after that, we're going to take some trigger problem and try to provide just, we can get a sense of the direction.

04:33
And then we're going to go back to the same apply and see how this diff specific. So what I'm giving you is really kind of this basic think. So if you actually going to do these specifications, what system just going to and I wanted to promise to see how you have to really adapt right on the end of specifications.

05:04
So I told you before that basically have the most, the most common way to specify a program is need

05:25
Mixed.

05:35
And here are cyber if you're supposed to basically just copy this. And then release basically say you need people is defined as first. So sometimes we can what we're doing proofs and so on we say need maybe But the thing is it's what we're doing here is basically I mean I let you code the program so you have a kind of a dot understanding of what the program does but and then I then ask you to write the specification.

06:14
I mean at the most don't level here this one. So, so basically and the normal circumstances and basically like a specification and you give it to someone else and say coding and then he has to deliver a program that matters specification. And then I go to someone else as I say proven.

06:41
So it takes this thing the code and checks it out and that's rewards. So that is my money and do it. So some of you for instance, basically sending me well saying doesn't mean you know, I don't know what it means because you know, I don't know what it was a program that you had before and worried about a specification.

07:04
So these are really specific ideas because some organizing, so, basically, you need it tells us what the what a visual conditions are drug. Providing the program and post these wonderful desired outcome of approach. So you could say is true and basically, you're telling me, I don't care what you need from conditions.

07:34
You you are using your business but give me this give me post. So you could have said true and then post it was very important for the post have no observation of our posts. Number one, is that, In English already for talk about what for stays.

08:00
By having an equilibrium means that the two regions are distinct, they have to represent labels, and if two cells are in the same region, must have the same level. So really suggest to you, there is an economy here with relationship there. So you have to basically take that and convert it into the into an expression.

08:19
This is what you can expect The planet. So once you know this is unity, this is unique. This is nothing to do with. This is logic, this can be done by anybody that has never thought of you anymore, okay. So you think if you careful about that, the other thing is important to understand is that this is all larger towards all the math, it's available.

08:49
So for instance, in when we were like 19 programs, we know that, we have no recursion. So that sentences we just kind of write in that we normally like to write because it just can't do in front available to us Now in when we are in math in Massachusetts really good.

09:13
So if you want to use a version for one of the formats of that, it's fine. We are not. We're not doing problem. So here, what you can use with any implies, you've been over here, we can just for we can expand, we can use for all. We can use that exists and we can also define functions that there's marketing fine.

09:39
You can use in any way. Anyway. We want, No, but you should not be doing. We should not be using here. If of, in this notation because we use activities in statements for God, yes, there is a. If in logic, let's say any of B at any means being implied, say so we already know about so if we start using it in, so in this statement we must have getting and then start making games.

10:22
So, don't notice. And for even on in logic, we have x. So again we're going to meet to use. This is notation of just purity to a and now the expression said to be on top of the state of the program. So basically, so you when you specify the, we got assuming this state.

10:50
So you know, for instance, hell is a set of legs with a label to make this, right? I mean, I can't even talk this expectations. I'd like to because L that has the one thing that is up. So in that sense, you know, we are using something of a program that the answer is for.

11:21
Now, some people made a mistake and saying something like, stable unless, but unless people activate them relationships, if they don't have different definitions, you cannot combine them like that. So, and this is one thing in value. The one thing that's on So you can't say in value and age to be makes no sense, okay?

11:45
They really have problems. Imagining. Okay. Now in some situations and mentioned last time, it may be the case that we noted is a as a trend making program, we wanted Indian and if we do that, we can basically, we can say in it fixed point and then let's say this one implies.

12:14
So it's a different way to specify. So this we said, okay, we started this patient. You have to generate this and once you generate the gold display. That's what this sense here. Basically says, you're starting a nation configuration and make sure you reach a love. You don't even spell it out.

12:37
This fixed point on, that problem, whatever program, we write that to fix one, four, eight. And you journey the first point by basically putting equal instead of colonial and then you say 6.35 sports, we know that six point estate. That's the definition of the fixed point. It doesn't change.

12:55
So, in the fixed point, he twice a design result. You know that but at this, you know, to you can use this only if, you know, if any system is a program stud remaining and insisting that there is a fixed and then it was okay. So, any questions?

13:21
Let's move the solution that I gave you a list. Talk about it. Let's see. Radiation is another thing. So So that's your assignment. So some of the next question is to the program. Are you going to program that you want specification? And it is correct. So focus your mind today on that.

13:46
How are the approaches. So we have a program teaching.

13:59
Here. We have seen on.

14:14
Color.

14:32
So you can invent your own, your own types as long as that is that obvious for their input explains. Okay, so in this case color it just makes any narration. Okay. Well labeled this this is fairly unclear.

14:59
But we can define what it would want.

15:08
Always. So we have here. I'm copying. Exactly.

15:39
Dream. The people's and one is, I And if you

15:59
Very and then we close. Thank you. So, what is the saying? Basically that we have two two lights three. I just happen to write an IJ. Thank you, probably the easiest way. You know, that's why. Okay so they don't know range. Then the same region it. The distance is at most one and the either in the direction and there are central, which is much, many of the effects.

16:36
Now, some of you have a different visual requirement, that the two nodes are not the same. And in some situation, it makes sense that they have on the same and sometimes sufficient doesn't exist. It sounds actually. There are some assignments whereby if you have many requirements, they're not the same.

16:57
Then you actually get in the run itself, think that's not a good thing. For instance, and the maximum label around me and in and we use that maximum labor around me and to make an assignment. But if you excluded me and I had the maximum label, he got the wrong reason trying to be very different.

17:21
Most of some of you use minimum and initialize L to 0 when he finally zero you take the minimum the results here. The last thing is that we're gonna, So if you find same region that

17:47
And we initially,

17:55
Products are J.

18:05
James think, No. So what I did here is to conduct the coordinates of the, So that means that in my definition of labeled how it has to explain the label is appeared compared now, and they had to be using the one who had here. So why doesn't really do this?

18:38
What does this and his transition to for me?

18:47
Every number of the beginning. So I sort of across the problem by any idea. Some of you initialize it where LIJ is high times m plus j. So basically again you come up with an immediately number that was unique across entire grade. Let's find this but I can't exactly it was real.

19:18
The initial zero, then you are obliged to assign labels in the program as part of the sunset. So you see that sometimes, you know you can move naturally and an assignment In some problems. Something really weird happens. You can do the science. They need to section the already. Before it's post.

19:48
I will not accept her from working outside. Don't do that. Okay, but it's still perfectly valid. Okay. You would you know, there's so this information is equal to an equational program, your basically providing equations. So you make all the way, all the regions labels. Now we can't do it here because anytime you when you because so if you wanted to do that you need to have that.

20:19
Okay? So using initializes zero. And then we have to have an assignment. Which says if I'm not zero, then assign me a new link. And then so the number of people basically what they do, they did they had a counter. See. So there are two solutions to approaches that people do.

20:40
One was data cloud, and every time you assign the label, it's like a ticket deal. Anytime the signal level of disability, you encounter the country by one. It's not a label improvement, that's all others. Basically define the max of the entire maintenance and computing. What's the largest number so far?

21:02
And then, when you define the label assign the largest number plus one, the same thing the difference is that, you know, when you do max essentially, you are creating a tribal powerful implicit computation in the definition of always we want to do have a counter and we implemented by the character that's more pragmatic.

21:30
You know, more implementary closer to for real implementation because that matches have to be implemented at some pressure. So somebody has to really write a code for their max. And so, it's that. Remember, we can't talk about performance at. We can only talk about the formulas, we give an architecture, so you don't have any architecture.

21:53
Any of these solutions are not good, okay? But we also develop a taste of what is nicer and what is better than what's? Another teacher wants to be completed. So, by doing this, we basically, we stated that everything was usually every regulatory state. So now we're just have to make sure that we don't mess it up basically.

22:27
1980 Q1 JPQ. And okay, I'm going to go Now. My dream called equal. Minimum have my okay. Now, if same baby,

23:06
Something like that. All right, so notice about using minimum. There is not going to afford that is because I'm not, I have nothing to the right to see if his time if you are really signing to zero and they will have zeroes in the way that it is maximum to always, push it up for you which sends out In my case, have a title.

23:41
I don't have that problem so I can always compare to another boyfriend. Give the smaller of the, of the two Now. Some people. And he's one person made it over the trick in doing the code where if you have two cells next with other neighbors and these are of their might initialize, they need help to be initialized with the same.

24:04
Same more value. Well, that sounds interesting. First of all you don't need to do two, Don't complicate a code and do two things at the same time. I mean, which are the one and the accomplish the same thing. But there's thing is that in that particular program, if you have a cell, which is isolated single part of a single cell that program will never label itself.

24:30
So now you have two cells like that in two different places, those would stay unable. So you never leave each post, okay? So you see how you have definition to details and what? Okay questions. Yes. Yeah, I'm Jesus. IJ the first way. Compare a little PQ. Okay, so there's something called lexicographical order that we should not form mathematics.

25:10
And basically, if I compare versus work from us to, this is smaller than that because the first element is smaller. But if there are, those are same Forest Elementary compared the second one is the same like numbers. Okay? So yeah, so somebody actually had to send me an email about his physical expert, graphical order and he has a questions.

25:41
So is very important solution, okay? That is variety of solutions, but in principle, we have to come to the same system, we have to label, you know, three issues the same labels and then propagate the labels across the cells and that's all the same vapor is used to be able to do that propagation and not at the same level here doesn't say that they have the two cells that could be distinct because minimum a and a is still a.

26:13
So doesn't make any difference so that's why that is required.

26:24
Okay. So in terms of the specification, most of the time sophistication, becomes elegant and clean, you can have good motivation. So I had a post office that developed a very complex specification for one whole router and they managed to get it all over one page, one page supported by five pages of definitions.

26:57
So no having that authorization can simplify so that these are an example of how you invent locations that are very useful to you. So I invented, I mean the only way of x which basically says x is between. I mean, x is in this range one morning and then So I mean, then I basically said x to both y which is basically that in the same region so just use all my developer locations as a video copy.

27:37
Send me because this same region is defined. And you guys did that you use same region from the program in the spot. Okay. Yeah. You shouldn't do that because the program. I didn't expect that I because if I plant the program I had no idea what it means. So, you need to be find everything.

28:04
So basically, this is the same neighbors in the same region, okay? And then I development is equal.

28:21
So God might as extremely the trust and reflexive transit closure of raw. So that means that basically if two scenes are in the same regions, they are designated by that. So the way we find that basically is something like X or O paper, that is a disease that makes it all the and see why that means that texture.

28:55
He said he cursive relationship, which you can write with them. In this section. Here, you need to write it in there. You can use it here but you cover it in the so now you can have this. You know you need my latest is Hello. Thanks Uncle right. That's okay.

29:25
Then in my post as LFX we call. Hello. I eat and only if text. No. So if that is the same region distance, then this thing will be jumped, your master, the same level in this handsome label. You must see in this image didn't put a video on a very clear, very simple form.

29:56
No, let's go back to to your assignment. So things many, many of you have basically used as a initialization equals 0 and you used as let's say the counter equal 1. Okay. So first of all, when you're dealing with a program, if you want to find out what the initial conditions are, you just take the elite section and the place all the boxes and so on, and you're done.

30:34
So it's a mechanic that transformation, you know, between the two. Now, the problem here we don't have the need program So usually like what they need. So me like this L equals 0 that imposes on me, do obligation to generate the length, because you give me no labels when I wrote here physical X.

31:02
I already established all the labels to be made particular given this. Then I'm applying the coder to make sure that I send you the labels The vision. Number two of course is doing any between S equal 1. It's not relevant to the specification of the program is specific to your curve.

31:28
It is your mechanism for creating the ticket giveaway. But it's not rather you see s doesn't show up in the first condition at all the first condition talks about whether you are same labor or the same reason. This doesn't exist in the first condition. So SCC another so throughout the tendency to just calculate automatically should, you know, inhibited and this should not be included in the even though it's in real, they need of your program should not be included in the, you need from the specification.

32:06
Because now you're closing distance to between something that doesn't profit is not relevant.

32:17
One more thing.

32:22
This is a list whenever you guys. Remember this point, whatever is whatever you write certifications, you do not drink because mothers and she was safe. And sure says find abstainment which guarantees that you move from this to that. The program doesn't exist. How can you find a statement or the program doesn't exist?

32:52
You're forcing you to code in a certain style, which is not just to constrain. So you should never use and feel in the specifications. Please use in the clues. But never in this, we need to use leads to because our problem questions.

33:18
Okay, so your job is through this program for you, which is great for this. And that's your specification. There you start is a good labeling.

33:34
Peace rotation is only from using the always section. But is that an is notation? Oh sorry, sorry. Sorry, so what? Yeah. But in a science is where people operate. That's only one place where you can use an info becomes regard on the same or another thing that some of you have had a problem with.

34:07
It's you'd have a statement, one part of the bar staying too. If God like the statement one might be, he's a salesman table. I mean there's a label to sell with certain counter and income in the count in the same. Step this eve applies only to this s to the second step that looks like this one.

34:34
So you need to really make sure that you caught the G on the other one on the other side as well. Also, if you have something not like this, you cannot use an if there. No, we don't have that motivation. So those are two two elephants. And one, there's another error.

34:56
That is more subtle. And when you have per box, some very relaxed, okay? There's some statement, some of you put in here, predicates which sometimes I feel Santa's apples depending on the color. The state of the program that changes a number of statements in the program. You cannot do that.

35:27
You have to make sure that this always result in a constant number of statements So you can so you can't write a program work. If case, even you choose a even statements in the case are which is a case statement there. Okay. So, let's write that.

36:03
Okay, towards 0 of Camel. So this is crazy and now see the two statements. Yes, this end. Okay. What please? So cake can change. So when K is equal to this divisible by 0, we get this statement but in case now no longer be 2 by 0, we get no same.

36:44
So you're changing the number of statements. You can put it as a condition here. If case evil because it doesn't change its Did we do that or not? And great.

37:11
Continents, but it changes after you release it, no color space is saying never changes the labels of the world, okay? And so that is. Okay, and the other questions.

37:35
So this is a very subtle, It's very easy to make them. And, and what I mean, I tried to catch it every time you did, but I may have made something.

37:53
As a question about the specification, if we were using like program Sylvia, please, okay. The drone is same. It's labeled energy across the region. So, same region is really this. This is the same region, it's absolutely exactly. This life is not that and you read the tries to close five.

38:31
People have any to statements. If they are in the same region, they could be farther far from each other. But you down the same region. Must have the same label. You got indifferent agents, one simp, a wonder one of the homework assignments. Did something very clever which was to the computer, all the all the members of the region.

38:54
So basically do a set of everybody in that that has a the color. Let's see. And that correct?

39:20
I don't think I've

39:25
And asking that you cannot use the set of relation because you can start you will need. You are instead of all the regions in that stair of the United region to the same level that you know requirement. This is just defining the set of the set of nodes instead of cells which are in the same region and you can define a set

39:58
I think I missed that because to define that set you needed to use recursion. Yeah, I need, I think that the solution and the first color, I see the become you are the us to do that one at a time. So yeah. So that was I I did not bring.

40:19
I mean, I did not find that is wrong but just definitely wrong. They already said, what is wrong? So we said, hey, have any final set. You need to have you can't use. You cannot use imprisonment. So the seventh have to be you know, the union of all the elements which are already in the set, you have to have the neighbors in the name of the neighborhood and that's it, that would be impression.

40:59
Now, you don't have enough knowledge at this point to prove this program. So,

41:14
So we need to feel a little bit of your when your skills or going a program for you.

41:30
Okay. So, that's

41:38
Let's take a trigger. Yes. Can you say again point? We cannot use ensure in specification. She sure says find a statement and unique statement which is going to make the transition from peak to kill, what you don't have any statements because you have no code. Oh, so if you try to say that, I mean I can't because I don't you don't have a program to point.

42:06
Oh, it's too specific to the program. And there is also an example of of a unit program that says ensure is not a property of the united robot, but I cannot understand. Facebook please. Correct. So I think that's a good exercise for everybody. So basically, the the case is something like this x called equal 0 If x greater than 0 blocks, That's starting from zero, If x is smaller than and basically, what what saying is that you have

43:17
So x different from 0 ensures. Thanks for equal to z. That's that's a problem with you trying to solve right? Because okay so the issues are following, you know, the problem issues you have to select a statement, the guarantees that's going to make the transition, okay? So let's say I choose this thing.

43:44
I put my finger on this and I and is my hand. That is my finger. Okay, so I put my finger right Now. What happens if x is actually smaller than than 0. Oh, if I execute this statement, it's not going to happen. Oh the statement has regarding 3, the transitions going to take place.

44:09
So it is a leads to and we approve this list to support school by this junction, my cases. So you basically say x greater than 0 and assures x equals to 0 x smaller than 0 and shows x equal to 0. And since these are two all the cases, you can combine them and then you can say anything different from 0 leads to particular.

44:48
So this is an disjunction rule for the needs and that's up to you for blood. So you see intuitively looks like well should be right but it's not okay. You see the x is greater than 0. I can pull to the statement. Is this one? Because it's more than zero.

45:09
So then when I combined it to and comply to the concise, that makes me act different than zero which will focus. And so we just need to only once edit any ones statements, to make sure the data for to make sure that.

45:41
But you have to choose one and other statements might do it before this time and diselected but that's the statement that you choose. It's your guarantee. The worst case is anything else? Eventually he has to choose me and if you chooses me that the transition experts,

46:05
So if I modified a program, I changed the program into one statement and insurance. Oh and I put if x. So then the insure property is correct. Yeah, then remember you can prove a list too by putting an insurance So improve insurance and therefore you conclude the list. Oh,

46:42
So let's take a pretty simple program. So,

46:55
Okay, so we have a another a which is greater than zero and what we're going to do we are going to we're going to have the specification here so we need and a is defined from 1 to n and then we're going to extend it from 85 and 0.

47:21
You're going to add in one more variable there, but when I say, age, big and zero, it's right, they say is not expected. So, we need basically says, Define is a 0, equals 0 and

47:44
All right.

47:49
And,

47:55
So different friends. And so ever made here's the an yeah, I experimented with zero, this is greater than zero and this that's English. Okay? No, because it's going to be the same. You need these proposed posters table, suppose is defined as A 0, rather than 0 and

48:47
So in this case, we basically are saying that we start with a being no zero and this is 0 and they end up with this being called zero and a being zero, right? So all specifically this is greater than 0, and this is all

49:14
So could you write the program to do that? Of course, you have to do it just set 80 to three and eight from one to n to zero and you're done. Okay, so sometimes just getting the Indian post is not sufficient. I mean, maybe it gives people too much freedom, that is important.

49:36
That's already people operate and apparently, right, this is better than, you know, and the other one. And this is equal to and below that is greater than zero.

49:53
And like I said, I can write a program set this to three and since it's all of that to zero and then, okay. So specifications. No I'm not always limited to to post doing them or sometimes they have additional constraints. So for instance, I can introduce a new guardian, which says that five zero

50:38
So, this is now constraining what we do a little bit more, right? Because we're basically said, you have to have needs to pause, posting stable, but you also have to satisfy this environment. There's an additional. So what one of the things that you're going to discover? And that's what I'm drawings are.

51:01
So important is that in Guardians actually culture. You're thinking about the algorithm, so really the imposed they reflect on strengths and how you are to improcess processes. Okay, so you can see now that we need to maintain constant that some of the array. So when when we end up here, we do end up with zero here.

51:32
But if we started here with this Disney pass, now we have to end up here. And then being asked because you're single and has to be missing it true. So when initially is true, a 0 is 0 and this has to be equal to this so that the sum of all the elements in the ray and what we reach first, they behind it.

51:57
Still has to be true. So this doesn't count. So only at zero contributes to salvation. So, so s and h is yes. So being very experienced just part of this specification. So we can spend the specification one more. One more step. You want to see this specifications can get, can get very interesting and some of them don't even have an even closed.

52:26
So you know, and I'm building knowledge here to gradually be to do an elevator, you know, and everybody's on faction program and other things. But when they're here, so we made a small step here, which there isn't it? This is imposed here for two reasons. Why is not to fix down intuitive.

52:49
It says it's specifications are not limited to. You need them closed, we start with animals, but they can be more complex. Number one, the other thing is that the fact that in guidance are created. So when you're going to try to prove anything about your regional labor program, the first thing you better start thinking is variance, that's going to help you solve the problem, okay?

53:11
So, and spec.

53:18
So you're saying if you're not here, it's great and got him.

53:28
Is not that, it's not a problem, How's it? The only problem is properties have, at least they guardian is a safety property. It just says that whatever state your name. This has to be true but doesn't tell it if you have to get to any signing particle. The only thing it tells is, if you have to get somethings, it's a fact that we're going to

53:52
Needed to use the first and from and now in addition to that, we have a new guardian as that's our the way we think. But this is the only thing that forces you that I can thrive if we don't have that a program that does nothing. It's a perfectly good program.

54:15
Let's say, but by the private property forces you to do something force of the towers, okay? So yes. So the statement between, I mean, there are for example, there are three statements in a specification and between then we have ended three pros that you have to do. Oh, so it's there any there's a difference between?

54:52
Yeah, I have. I have sold all my apples and I still have to sell. That's a hand between two logical sayings. And I prove this, and I prove that oh, you don't use an end between also, there's no end. Oh, that's three obligations. Oh, okay. Like you guys feel letters from the judge and the first letter says, do this.

55:18
The second letter says, is that they are not. Oh we decided so we use a satisfiability really rather than you know they have true or false. Oh we prove them correct enough. Okay, I just and I sleep like photography, okay? So my small groups because the next kind of congregation to each other and thing for the three minutes of voice, what a program might, how would you write a program together?

56:05
In the first, first person come to the board. Tell me what you got here.

56:29
So we have a zero and paid for one. So we basically kind of combine the naming to one single day. Also a, the capital, A stands for one to or okay. Oh, zero is zero. The others around zero 0 is greater than 0. The other side of equal to 0 4, and you need to maintain the sum const.

57:10
You sure.

57:47
The words.

57:55
Yes, so can I use the shift? Where to start to do this. Oh, just give me a solution. So his proposal is. So then so then what we have here?

58:23
You.

58:30
Page, zero one right out of the box.

58:39
Was wrong.

58:46
My smaller than hey what's my name? Okay. Have i plus one. Okay, thank you very much and you said end to zero right? Or something matter. What do you mean you have to set a event with zero? Oh yes, or something zero.

59:15
So here when you're one statement and feed zeros from the right and send them up, shift them and something like right. Okay, init. Yeah, we need to put the initial name and initially for some coffee from here.

59:39
Whatever. Okay. We don't have anything to understand.

59:47
Okay, don't have this solution. Does that mean it has a solutions? Right. I can, I can basically randomly choose two elements and sometimes a little

1:00:03
I could do that, but I could choose another element. And somebody did A directly and 0 it has been sensible, right? So, the main ways to skew again. But now, let's let's think about proofs. Okay, so, one of the first things we should do, we are you need? It's from there.

1:00:30
Okay, so free we need to check. This is valid poster. So initially we said as is equal to, right? And then we assume that, you know, the guide police. So there's no improvement. First question isn't, as if we should recall, And yes, initial calls because zero and this synop.

1:01:04
So we show them guardians points. Okay, so now we want the assuming value towards and round to prove the statements every state. We only have one every statement to those indirect. So we we need to look at things. Here is basically the way we are ways that the first element here is adequate zero.

1:01:31
And on the other elements, she left and changed. So now, we have a zero battery 10, plus one more value, and the rest of the values are still there. So the total sum is still as we can do a formal mechanical truth but you don't need to do that just add you informally.

1:01:50
Okay, make sure that your language is precise. Okay. So,

1:02:00
So I think so we can just Now. Let's let's look at first supposed to say Well of course state of means that that a zero is known zero and equal zero, right? That's so basically the statement a 0, doesn't change and the rest of the start doesn't change because there should be zeros and we are adding a zero to a zero, so nothing changes.

1:02:32
So first, this table invited is preserved so it might look like we're at home free probably at all must what what is what we that we haven't told you. I'm being through the needs function but what started that? What another was not done. So AI is a zero. So this is so let's say zero one, two, three, four.

1:03:08
This is 0 and this have all greater than 0 7. 16 99 44. That's what he said, first, AC or zero, and there is the pregnancy here. So in this case, it seems about the array of ai larger than one incident. And it doesn't say anything about the content and done things, you know what it is, right?

1:03:44
The companies they are in love already 100%. So it didn't say anything about the content in the context in the RA. No. It's basically since there are plastic numbers. It doesn't witch number. But of course. Remember, it says everything is positive. Yeah, everything is possible. It's just one example.

1:04:12
We don't care about the numbers have but everything is positive and this is zero. So sorry the initial function that suppose statements in the initial part. So it was said the everything in that part to meet the system. The politics. This is an assumption. We are given this. Yeah, we are told assume that this is okay and then use it noticing that I think that it's important to understand has has been defined in terms of being a socialist state.

1:04:50
So as by in English, we say the test is a sum of values in the array. A once again, and then since and 0 is 0, when we have 0 to it is still service. This is still yes, believe don't have like if we wrote an algorithm that we have made that the negative numbers into the array.

1:05:19
Would, it's still big value. It was good boy. Yes. But but would affect possibly the proof. I'm giving advice good to make the proof easy for you. Thank you but it starts out as positive. Both those are stated but somehow you write an algorithm that makes some numbers named as I can.

1:05:46
I can do. I can write another reason which

1:05:55
Keep your, if you are known zero, I have two cells which among zero I can add to one the number in the recommend. The other one by saying number and they got into or the kind of crazy and kind of more difficult to prove. So, we just need the initial state in for the program.

1:06:16
And then we waited, excuse, we don't care about the initial steps, because it doesn't, we may stay there for may not. So we just important improving in life. Yeah, we cannot prove you guys. If you don't have any of that, The enjoyment name garden industries. Yeah, I got it.

1:06:41
Okay, So when we close this, in Guardian for this program, we need as an initially true. And we said, since that's was a sum of each element by different by definition in English, when we add the zero, which is zero, the total time is tellers. So initially this former is true, then we assume that the formula is true and we look here, so we can look at the rate here.

1:07:17
You know that one of these zeros here at the end and this is right. So then when it was a shift, this element, it's added there and everybody else gets moved gets moved over and changed to the zero. So if we skip this element, everybody else in this donation, is concerned and this element goes into a.

1:07:49
So when we added to the, to the current value of A, the inviting is still preserved. But remember we assume that invariant is true, and then we analyze the statement to show that if this actually continues to be true. After laser canist, That's the way we prove that guy to have it.

1:08:10
Can you surgeons how to improve stable in this case? Yes. Okay, so the force, it's this has been like this. So, there's some number here and everybody else is there.

1:08:35
From my city to this statement. This zero is added to the A doesn't change the state of A zero shift left as a change, the state of zeroes. So it's the same state or so, clearly this terminal over changes across. So the same amount of return to the state That's ice state.

1:09:04
Okay, so we basically say assume that cost is true. Again, that's the way you have to in the language. They please assume post is true or now show that cannot be validated. Well, I don't understand here which randomly comes values, then obviously, then the poster being done also, the first sentence this assumed post is through.

1:09:32
Simplest is true and showed that it cannot become false. Oh, that's it. So anybody's clear must work. That's so fun. What is missing from the proof community and leads to we never put the leads. Okay, so the question on the board day is how do we prove at least and this is a part of this problem.

1:10:01
And so when you have P to few the way, I mean that number of ways to prove it one is improved. That is an issue you're done because proven ensures and leads to follow through there. Well it's not going to happen in the choice. It's trying to get from a need to to end because you know, there are many, many steps.

1:10:33
So that's more going to work. And as a possibilities like we then if you form with the disjunction would provide a couple of cases and then combine the cases we get at least Well this is not the case here either. So what happens is that the third way is to do transitivity if you're starting to stay P you don't understand.

1:10:57
R we take from the state Q so that's transitivity therefore from P. You get to kill, but you see that's kind of when you have a small number of steps. Six number of steps, he goes to one state and then the next thing they're done, that's simplifies and have as many as in one.

1:11:17
But, I mean, it's but only have a program that that is running generally, the number one wife. So, what you need to do is go to this induction.

1:11:31
So how do you prove simple induction? What we do we introduce what something called a valium function.

1:11:55
To some domain. So basically assigns a number to the store. This state is worth $10,000 for this state is words, five buildings or this state is worth 10 miles of real estate and just we just map the state of the program to some domain. No, there are some typically what what you do here is you use natural numbers?

1:12:29
So improve your rewards. This is telling us I'm so far away from the world, that's not. So to begin to be a good function with metric. So, these metric

1:12:46
You must be.

1:12:51
Well, What does he mean? It's my father, and this domain there is a problem, So is to get closer and closer and closer and close on the close and close and closer. You can't go beyond it. There's a part of it so natural numbers has a metric. And the domain for this, for the very function are very nice because they have a zero so it's about a family.

1:13:23
We're gonna stop there. Integers are not good because the engineers go to minus infinity. So, one found it means that you have a we start here and there's a bar that we can't go beyond the body. Okay? So the what you're going to do it, basically, you're going to show that if this metric people came, but sometimes you keep natural numbers.

1:13:57
The smaller than cake.

1:14:03
For. How you?

1:14:13
So, what's what's happening here? You're proving that you're on the middle of execution. You are some state, the computer number. I'm sure that if you no matter what number you're computed, these statement which is going to decrease the number When I get a state which what the number is smaller.

1:14:40
So you should. You should improve this piece. Then we can conclude.

1:14:50
When Justin?

1:14:55
You know, international basically says, you're reducing from one to the next minute. Right. So if you just prove this at once for an arbitrary state beauty symmetric, then you can conclude the heat type, okay? Needs to.

1:15:20
Because it just could be the metric is well founded, I'm go below zero. So no matter what you are, we're going to decrease it. Decrease it difficulty decreases but you can't decreasing it basis. There's a stopping point, so that's a way so that don't improve progress by induction. You introduce another and then to show that the magic decreases and then when the metric is zero, symmetric equals zero.

1:15:53
We actually imply your force by definition of the. So even if there are many part main part of the pattern, to infuse, the energy zero, which one you want to Now many different ways here. You just have to choose your metrics, so, you know that and then the other, you know, the other singer so fast that it's only, but you choose a Mexican each other.

1:16:31
So then the question here for you is, what is a good metric for this for this program?

1:16:44
The amount of zeros in the array would be nice. Yeah. But the problem is that the amount of genos increases, so you need something. So we have non-zero just now three, so we can you can. It is the the number from let's call it either. Here is number of one hero.

1:17:15
With one this one and that I mean the bottom I mean if you find that domain is being bought and at once they're fine, okay? But so number of zeros and as far as element, so if we assume that there's someone in the program we want to show that now the metric decreases.

1:17:40
So, what you want to show is that you time, okay? It's through the smaller than more than three or three.

1:17:59
Show to show this how you can,

1:18:13
And you know program but yeah we talking about is the finance state or infinite states which in case.

1:18:33
So everybody something else. Just come the number of zeros and in the real way and we can write that came right.

1:18:54
Of plus I like that zero high.

1:19:06
And people 0.

1:19:19
So it is like her, so it's like that heuristic. So you, so they're getting through your

1:19:28
So in the shorter than completely, you know,

1:19:39
No, everybody is. And that's another part of definition from now on. We know that, we know that he died, somebody came and I need to prove that it leads to having more less being less engaged or maybe even

1:20:12
Because one step of our, these labels alone great there, or yeah, idea. The last two is one leader and see this one. So one is why pregnant and because A is going to be positive talking with a whole entire. I'm trying to control. Okay? I continue to be just from in one and I wanted it just

1:20:55
Okay, so I do prove this

1:21:00
You improve it with an insurance. You could probably. So insurance means that with the statement, God is an everybody wants family to do that here. So, it's really gonna show that but I'll be proved that insurance.

1:21:25
Here's the subject is going to come up in this conversation. So basically they really okay and this is this is a formula. Okay? 30 months, simple. That's on one wonder has some stuff besides it, all right? And so this is a so this is a metric. So basically says that equal to k.

1:21:58
So we're saying this sum is equal to k. These two thinking minister and probably in that case, you may want this cake to be greater than 0 already of the

1:22:22
How to think about how you prove that.

1:22:29
So you said is an issue. So, there's a statement which takes us from whatever we write to either. Now remember eating this for me, okay?

1:22:42
We came about the initial section, you know, you can't talk about any. So so basically say each other it's important to play with zero straight one.

1:23:01
It was an issue but it seems that they had the equal to the number of the AI equal to zero even here space here. Yeah, we need to count to the number of the AR, which it will be coming there, and it didn't compel that because the equity is equal to zero.

1:23:24
And in the number of the AI equals yellow, the number would that you are including you have to prove this, okay, this is a statement. Yes, conveys me. That this is true. You about executing and go from here to here In English Comprising events, true.

1:23:56
What do you mean? Just not sure. Because the have one, one decrease is more than because here, but have you specifically decreased by one we've taken the proof?

1:24:27
So you know what is true? You got five zeros. It basically disclaimer. According to this property, you should cut down to four zeros. Sorry. Yes, portable. The five months ago and the executive statement you get down to four one. How do you argue that? That statement doesn't from the Ace of N equals 0 on the end for the from the ace of angle 0 on the answer.

1:24:58
We see it. Well, if and he's already 0 and you put a 0 into it,

1:25:10
Present degrees. Remember here for, you know, some how it is. So, this is supposed to be nothing right here.

1:25:29
For the five cells which are not zero except for not a zero execute this panel. And according this property is true, you're going to go down to four cells which are not

1:25:46
Statement, you know exactly what it does. You know, the property for the second part of the statement makes it

1:26:04
Make one left, nine zero. Okay, so you'll impression is correct, what happens? Is that there's like this. Okay. So, these are all wheels, because I won't lose those. And when you do a shift and you can 7 ones, this is unsealed. So it's you know, one day so that would be yes.

1:26:32
If both AI is equal to zero, then when you die, yeah, it doesn't matter because of

1:26:45
In Hawaii. So if there are seven numbers here and the take one of them away, this is going to be six numbers. I'm being data is all them are real and then you decorate. So, zero, the metric is zero. We're done. We don't need to worry about that case because 0 cannot increase, but you need units to close that.

1:27:14
Okay. I was assuming that this is true. Okay. You have more than one at least one around, right? This is what it says. The number of non-zero element is greater than zero. Therefore it's at least one. Yeah, right. Okay. Basically the statement, if you get the number down by one and she argues that that happens in this statement.

1:27:40
Because you know, this last zero here moves over there and so reduces a number of, okay. But it doesn't have enough information from the statement to be able to like make it at that time. That's about one happens. If there is a number here, we become more zero.

1:28:15
See, you know how the program does you cannot prove how you learn by the program? Does you need to prove by you, looking at the former? And at this statement in this and I have to tell this property. So you do not have enough information to be able to prove this because it's possible that a zero becomes yes, this moves over there, it is by one, but in a zero.

1:28:43
Because three, how do I know that 01 comes with the only AI to impose first, time to AI plus 1 because the people AI plus 1 is 0. Yes, we need to. So in this part here, you can prove this for these guys that becomes 0. Yeah. But you cannot prove that the number of number of non-zeroes is decreased because I can, I'm gonna do the following.

1:29:18
I'm gonna add a seven here and think of seven hours. Okay. But hold on When you're all the time, the last one is zero 15 left and like where would that sound? So you, you know, so when you're pulling it based on technological and the only way you can actually, so what you really want to prove with the form?

1:29:52
Let's go back.

1:29:59
So, these are the ones here in the 7 8. You said this year. So what you want to prove is that When is 0 moves there, everything else is still good. And therefore you know, before the Elf is still not there and therefore the number of the medical. But the only way to prove that is to use, basically his knowledge of the on the curve and the way to use that knowledge is being producing invariable.

1:30:34
And basically there's any value which says there is a number of some locations. Let's say alpha where everything from left to the alpha is positive and everything right to the alpha is zero. So we probably introducing that. Now, we take this in value and then stick it in here.

1:31:03
So now, you know, that everything is here zero and another thing is non-zero, the only change with spectacular is one zero. Is this the removing over there? Nothing else can do anything because it's a value. So by using the invarium and this formula and the statement no unit should respect how to add an invalid, which reflects what this, what he's saying.

1:31:34
I mean, why in this case we're going to you have different right? Prove that initially if this came his end and to ensure that everything is experimented by as always, okay? And can venture capital city. So it proves become a little more. I mean and not as you have to avoid the tendency to use what, you know, about the program to you need anything to focus and say, okay well I'm given if this and that because, you know, you different, this one here.

1:32:27
Cannot depend on measure values. Only way you can make it depend on your surface. If you feel something validated, we don't have been guided because of English events, you can have negative numbers that could change things. We become more assigned line. ETA is definitely Mario or just it's just one at a time.

1:32:58
Like the only body of every another, they got into a very important program. So you have to prove that every statement in this case we have only one statement. Yeah because I find you can boxes, you have to take one of them improve it that it doesn't bother them guys.

1:33:14
So sure that these are is true. The only use they need to put down and then you are seriously and it looks 10. And by statement by statement by 10, most of them don't don't do anything, they graduate. So there's one problem some will make some changes to the state and then traveling you have shortly.

1:33:34
They garden is not.

1:33:38
See how things can get. But quite complex, even for the trivia program. Like this that you fully understand. Of inner assignment. When I believe from opening value to come up with the right values and then come up with a red method and show that they decreases and make sure that whenever you decreases you after you use the code that is given to you.

1:34:07
And and you can see why why is traffic is we've had no defining acceleration in order for people just once they know, they make it about easier. All right, let's think about it.

1:34:46
Really.

1:35:22
Proof. But then the

1:35:36
About you. So that one of us, you basically what you got us, okay? So we're helpful now, you're given close education and the program and I appreciate the program.

1:35:59
Prove to the program to satisfy the

1:36:09
What? Yeah, you're gonna have gonna answer them in that case, okay? But just make that nothing. So you're going to have to respect, and then you don't have to guid proven guidance first to

1:36:59
Did you find interviews for more likely putting on the gas right here? Which is you? Come with just wait, players. Yeah, really help you. So, once I got really very

1:37:32
Video. Yeah. Yeah.

1:37:47
Got more than

1:37:52
From the maybe they came out like, basically, like okay, okay.

1:38:18
Very well you basically I think I should say everything that is smaller than the one. Okay, so it's positive. So, we take us to 10 using a zero. Yeah. So here, so, So they're still available, That's the statement separations.

1:38:59
Also, I haven't told you about that.

1:39:20
You made it all get on which move zero that doesn't change. It's and that was changed. That's good reason for you. It's probably got to do that for being revealed.

1:39:43
Just three people without That's funny, you guys somewhere else so that way. Okay. So you yeah, doesn't go solo with that something more.

1:40:51
But there influence going, What would you like?

1:41:13
You know that?

1:41:25
15.

1:41:38
I think God forgot about my dreams.

1:41:47
I don't know.

1:41:56
This is dropping. I'm over here. We continue that we should have about that video. I'm not this person again. This makes it sound. I brought 17 and

1:42:32
It was really great. We also got our current password says that.

1:42:40
There more like it.

1:42:46
No graduating.

1:42:58
Yeah. No, I have no reason to attach it.

1:43:33
Yeah, that's

1:43:43
Perfect.

1:44:54
I was just. And,

1:45:05
Goodness.

1:45:26
Deal with.

1:45:33
Love. Yeah.

1:46:02
Okay. Cameras, right? So we have that ready, which is the great with themselves that diverse the women and then I would add a m which is use for marketing to keep track of which cells have been included. So they can then be. So we have a definition for neighbor so that means everybody else has that.

1:46:34
Removing one wonder why we have the negotiation of accounting for me. How many cells are around the neighborhood. The definition for verse the mention of death. Okay. And then we have because this is same. So this way if you have a knife cell and the border, you can pick up the board because your border and another self in a different colony than it.

1:47:19
Don't that clear?

1:47:27
Here, when are you done with walking? The colony is when for everything that is more, you have a neighbor that ever is market as well. That's so you want to let me know when there is, you know, has some true values. But doesn't satisfy that property. Means it just took opinion to that colony.

1:48:02
When the property students.

1:48:10
So initially.

1:48:16
Family.

1:48:20
There's nothing wrong. So now for the size section, we have three cases. First of all, we need to find the initials and initial cell divide and as we are live cell because it's not like this normally finding colony. So basically,

1:48:44
Dogs that I change. Okay, I'm gonna stick the and let's give the range for AMJ. Everybody knows what the range is once or okay. And I think forming of true here.

1:49:07
Between. Basically says, if nothing is marked anywhere and you picked up a cell which is alive market, this becomes false, that becomes no longer true. So this is not going to happen again until you reset the matrix system, right? Then the next thing, what you're going to do is start building the column so Jake the Q again.

1:49:46
I'm going to skip the range that my J people through in.

1:49:59
And you hand simple.

1:50:15
So you set it through, if you have a neighbor that is mark the market, if you have enabled, it is more and the more in the and

1:50:30
Question. Now, you may be setting the marketing. Again, we're gonna have to listen and not what about now. I could check the NIJ sports but doesn't make any difference is simply communication. And I need to do the update, So,

1:51:00
Corn.

1:51:07
Perfect. I'm gonna be tricky this time and just make sure that you're vigilant. So, this is part of our find Jay corn and, and

1:51:31
And that's really good business. Also, we need master should be ready. I could do that as well.

1:51:49
Information. No, notice of this change matters, sometime the truth. Something. Therefore but there's only one statement to panel, but so the one steak, so all of us have this one set, sometimes that's nothing. Somebody does something so I can use it in there. If this was box here, I could not use this because used to change the number of statements that are true and the number of seven character generated.

1:52:23
So, that violates its legal. And then, what do I do, though? GIJ points of true.

1:52:47
Be there.

1:52:54
Okay.

1:53:01
Now, it's an interesting thing here that another MIJs through here and MIJ multify. So I might be touching those cells. I mean, I turned the mass on those cells which are actually true. I could take this one out into a parallel and I mean, but then I had to make sure it's under the same same thing.

1:53:30
So I want to, I won't do it that way. I'll have to do it here. Pamphlet and with understanding that this for the first time first time and here m equal to force. Yeah. Just every cell is okay. It doesn't make sure and the second one that's the two squares but the second assignment.

1:54:02
So if there isn't still this is small. The front. Yeah. That's you first or just once we are not going the box That's a blast outside of this. Oh, that's inside. Okay. Okay. So that's a very clean, very elegant way to decide, but having that I having death and birth rules already building here and there really does account.

1:54:35
Then you know, you don't have to worry when you look at the code, you know, that it's greater than these very small and that you check it once here and you're done. This impossible is I'm not that we do it once and then everything is good girl mode. So this is a foundation on that which addressed express, which is we have exactly, you are bad and heavy justice.

1:55:12
So I just I just put the condition there and I created both. So he said a spelling about here would have the truth longer and possibly more like it in my arrow had bruised once here and then I used it in the in the coke later on. So this definition is always helped me out.

1:55:33
Is he can't never fall off in the if this is the address to do this neighbors, you know, not enjoying the protein. Level was here to say just the same color, maybe the industrial code and some qualities of, okay? So you're saying you're just breaking it up to avoid confusion and reaction just okay.

1:55:58
This is one study that happens. Then objects only those cells which are more has been in being part of the human reset. And then we decided so we can start all one here. So the system could choose a statement where GIJ is false, nothing happened, which is because I want another one rather than another one.

1:56:25
And then eventually we're going to find them. And now your proofs here that have to prove that a seeds was created. The way you've kind of processed is proof, is that initially? Then eventually, that leads to a seed at least one it's seated as it don't do anything. And because every point on the way live is, at every point on the grid, as we selected, let's assume that this particular point is alive.

1:57:09
It's got ideal eventually the systems which is another one before. That's why we're done sooner, but it's gotta give it to this point. There was a therefore it's a it's a man ensures for that. That we use. We see that.

1:57:32
Volunteers.

1:57:38
Okay. So the first statement in the, a size session, the capital and equals false, you mean the? Oh okay. And can you say again what does the mask ready does? I mean, why there is two double colored? So, basically, what I can say is that if I have

1:58:28
True. Sounds. So, if I pick a cell that is in the colony and I pick up one of his names, this neighbor is also Mark has been the colon. It's not my plan. What time is it working? Since his, for all cells means for any fair that they choose any better of the neighbors I choose, if one of them is marked.

1:58:57
The neighbor is also all. So that's why we're back. There's nothing else to buy. It's kind of the no opposite of this nice. There's nothing else more.

1:59:17
It is not, it is not the case that there is a cell which should be part of the colony and is not mine tensily. That's a way of thinking about the positive way is basically if I have a neighbor and I'm like, and it's in the colony, it should be one, too.

1:59:35
That's true for everybody in the and hot finds the operator before. And TQ freedom means, okay, these

1:59:58
Well, sorry.

2:00:09
Right. Also, same colony. And this. Oh, so that's end. Oh, I see.

2:00:25
All right, So let's say that we want to, I will try to improve this forever. Let's say that we want to write the specifications or what is going on with you. Okay. Another rules because the verse you have to have so many to be born. You have something to die, right?

2:00:52
You know those rules okay? So that they intended the problem, okay? How do you specify? What's going?

2:01:03
Is there a post condition? You know, is there a fixed point? No idea? Because no more than yourself the release of configuration is undefined. So you say g to have any many configuration at once, so don't have anything to explain and I have a post, what in the world we have.

2:01:37
Appropriate. Nobody that you're going to write the code. I want to specify what should be like. And instead of programming I mean I want specify what I should do. What you should be writing for the two things that we can ask the program to do for recipe. That we would say that write a program in unity and satisfy the following specification.

2:02:08
And I have to do the specification. Now, this is a game if you don't play by the rules of the game invited him through games, right? So basically we know that we can we can ask make sure that you play by the rules on the game. So that will be a you know everybody if you make a move has to be a legally but that doesn't require that.

2:02:35
It's a safety problem. It doesn't require the game to touch and play anything. The computer could just sit there not doing anything. And obviously every move that it does, is it does nothing is real. So, we also want to force it to, but it's not always a move it to be made.

2:02:56
So we have the basically say if there is a move to be made then you better move for. Those are the two things that we want to specify. So now I'm going to show you how sophisticated come together this.

2:03:16
And like, God gives you that you can go to the top 10 department, of course has departments in the country. Pick up five random faculty from that department and they won't be able to do this degrees. So special, really, we look at this problem in India. All right, so you are really going inside quite many and that doesn't mean that you can go to other professors and don't have to go to a top 10 departments people anywhere in the in the department.

2:03:48
And a professional trying to find a problem diagonals. Some, you know, the same thing We had we have specialized normally and I'm trying to share it with you my specializ.

2:04:06
And by the way, while this program is this game, I mean it's used as an example, many, in many places. I've never seen a form of specification. So Mary was to be able to Christmas. So we need to start thinking about the motivation. So addressing I'm going to do now.

2:04:35
Obviously you try different things and then you discover that you need to communication and then you present it as, you know, by the way, I'm such a genius. I you know I saw this notation from the beginning and now look how things are simple. There's another way for us, that doesn't, you know, there's not a way like this and in Arabic, people think through and do a thousand different things.

2:04:59
And then once you find the solution that they present and having that way, that's what they're trying to help present in their. So remember we had come.

2:05:13
That was counting a number of live cells around you. So I'm going to extend the definition to another parameter in x For x is a arbitrary in my environment. It's not Jesus specifically, it's anything. So if you give me the x, I can go to account or I j on that particular way and you're going to see why I need this.

2:05:41
So, I'm going to also deter it.

2:05:47
In x that

2:05:55
It's like G becomes all parameters.

2:06:01
Then I will not get interested. I didn't have something called revolving.

2:06:14
Trying to be fine because we didn't have it all in our program. So, it's basically going to be

2:06:39
The basically, we said that a converse could take place and I for the best contact place that self could evoke would change, right? Because that's what the one program works. It is a implementation. No, Once you have this, then we can have evolving.

2:07:06
Thanks, which means there is an IG people and that here and I'm not sure if I use the order. And So basically, now it's telling me that in this configuration, this configuration could change, The reason I could change is because the birth or test could take place.

2:07:46
We have seen quality.

2:07:55
Can in tanks that's just extending to ads. We have same start the previous time, the transit plot because this is all mathematics. So, you can find them.

2:08:20
The basically says that IJPQ and in the same colony but one of the neighbors. And okay so what this one is definition is to help us out. The first thing is that we cannot get any fixed point. Evolution takes place only there is some possibility of change. So, basically, we want to say, if the evolution would happen in and then, if you evolve, you better, follow the rules of the game, those are kind of the rules from on.

2:09:11
This.

2:09:21
By the way, in the lecture notes that I sent you that to proceeds, I suggested to study those because I'd help you with myself. What is the meaning of the star?

2:09:36
So, if you have any age to be being relationship and seeing rights to be a relates to B, and to be able to see the effects of other people. So maybe they Probably. So what you want to specify is that you if there is the possibility, there is on one another verse possible in better heavens.

2:10:09
And this is a totally different way that we have specific settings. So, where is the power 10?

2:10:27
This.

2:10:36
So basically says that if Jason some configuration government is simply to use before like x equal to K, except now Ghana is a big big. Sorry it's a constant university financial. So if we had an exchange of configuration, which and God according to God, which can be wrong, eventually, Jesus going to be different from.

2:11:05
Therefore the practice will take place. No, they've put just destroy everything and you know flip beats or something like that and that's still progress. So that's not. You need you should be following the rules. So basically we have validated. So this is the progress property, but I need to have a safety property which makes you an available in syndrome.

2:11:27
It just says do something. So here from unless All I enjoy. So,

2:11:53
Different.

2:12:00
By J in place, right by okay.

2:12:14
Not employees.

2:12:35
So basically it says it even, two configurations are different, whatever, there was a change, it changes according to the rules. So if so this is different from those configurations and current the new configurations different from all, but it's true. Therefore, in the world was false, there was an empty cell in the world and now it's true.

2:13:04
And in the previous world, it should have been a verse that the placement and even as well around this falls. And it's different for the previous and the previous world must have been true. And they're going to previous world, which should have been a death of signed to that same.

2:13:29
Two lines of code. My friends for this specific age two lines.

2:13:38
So you have all those definitions? Yeah. No, Well actually the important thing is purchasing this therapy to think about all the current and all state is coming to many logics is not. I mean, it's not something that I just embedded here. So in many larger external logarithms, for instance there's a and a prime or let's say a is a current state and they prime in the previous state so they don't have to.

2:14:10
So this way, they don't have to say G in Montgomery morning when they want any part of the previous day. They said you pride to say JP different from G and so he's not there. I mean, it's not something I just said it's such a common user and larger, but I think they the key ingredients here is it.

2:14:31
You know, we came now, we have to rely on the current for the relationship between the current and the next thing public. Any other questions? What? I put. I have a question for you, too. Yes, so there's my last question here. So there's no internet or was for. There's no need something.

2:14:57
We don't really want to. I mean those doesn't exist. Final celebrate. Some of you were writing this video. Just a definition for them specification and then you have to provide the code okay? Which is full of his rules. It's possible to have no balls. There is not, anybody don't know.

2:15:24
And we kind of characterize it, we just don't know what we want to get. We want to came to follow the rules. We don't know what the game is going to produce. I've gotta look at the board. There's somebody in the game. That's okay. And so that's that's an interesting part, but there's an alternate interesting question that you should be asking, okay, I'm not asking me.

2:15:55
I'm gonna ask you. Yeah, So if not on this, we use here. Let's so it's the only time we can use all of this. No, no. You get this on this and many situations, but this is basically a relation between to stay with that. So, so that's basically forces these changes to happen.

2:16:19
Nice and simple. Okay, so you wrote you out to your vaginal again, right? Which one of the people that I'm satisfied is,

2:16:53
Three. Hold on. The whole satisfied is property, but what if I wanted to write a program of a particular kind? See the specification is not strong enough to force you into one particular solution invested in any changes that can make the board have to be. According to the rules, they foreseeable tennis and one at a time then doesn't tell you.

2:17:20
So we need to have additional specifications. So here for himself we can do right? Something like me from on this.

2:18:02
Everybody knows what this means. There is a single to the single high inject so that basic corresponds to a beginner. The very one at a time. So the difference between this configuration that most configuration is only one cell. So there's a single place where that difference know that other places have not been changed to make it make a progress.

2:18:36
It may follow the rules, but it doesn't work. Now, let's say that we want to also say the whole thing.

2:18:50
For all IJ.

2:19:17
Everything that could change has changed. So that's a synchronous synchronous update of the entire group, somebody would say, well come into that corner. That's also if I move take care of it numbers.

2:19:45
And these are ING.

2:20:05
So, basically that it says, there is one cell that has been

2:20:15
Okay, In that case, everybody else are from the same combination of. So basically the stuff here and say for all of you,

2:21:02
So now what this tells us to tell us that we I don't get scared because you're not going to see things as complicated this and takes a look. There's a lot of So to do this. So basically there is one cell which is different pen. Any other cell that is different.

2:21:27
Wanted me the same colony with that said, and that means that we only want.

2:21:38
So it gets interesting. All right, anybody homework about what you talk today.

2:22:03
Right? So keep keep your mind very sharp and clear. Don't make a sound and remember, you don't have to prove that or triples because they have to argue why that by looking and make sure that you don't sleep in the argument. You know, seems assumptions that are not there.

2:22:23
Everyone, usually some driving this music.

2:22:34
Okay.

2:22:50
Right now.

2:23:05
Yeah.

2:23:27
Yeah. So I haven't really been here. If I have no, we are. Oh yeah. Okay, control from one thing. We see people. No, he's not the one. That's my truth. That people are trying to speak Chinese for this teacher and that different versions of So influence. And I didn't rules.

2:24:22
So they have basically it's a hypothesis. So is this part of the project starting fundamental, Which part of this is part of the group system and social table. But I mean, there's also the same thing that helps few, Well, we can type hypothesis. And So basically they successfully want further just important through this and there's one way to get this.

2:25:05
New space without any additional work to do so busy like children. So this is a statement about affect. Yeah. So it's not able to, I can go over there, you can use it, you don't have to do anything just use. So just use this, don't worry about that. We as well as guilty also.

2:25:35
That's the meaning of the knowledge. The notation impressed. Also, for some that's also the show.

2:25:54
The problems. And that's making the way. We are and the fourth kind of person believed the size definition of family. But then what was important to you. Here is, These are the rules. Okay, So if you want to use these rules, something else We let you go the question mark.

2:26:33
There's no reason why.

2:26:39
So there is no and hope you.

2:26:53
Don't know if that we would think that then help. What did this? What do you do? If why do you need this? Well I mean, what are we what could we use it? You want?

2:27:19
Yes, This is a way to by showing the space grow. The program is going to be graphically. What we need we need to post like because it is one of the reasons zero in that you show that being zero prices and also you said invariance, whatever statement. That is the safety.

2:27:52
So for our program, no problem, I feel like this can be invariant.

2:28:06
But it doesn't, That's it. The food.

2:28:19
The memo's agents. Very simple problems with the regions and how this change, probably the same stay the same or if you can value just to reduce or forever. Yes. So what is an inundra example of anxiety is that in this cell. So let's, let's assume the patient has a, an example of what he got into the digital C.

2:28:52
Only the most region one. No wonder what the program does. Because I've changed regions that's an event but we just come up with one statement one can became multiple designers depending what they could improve, right, right. They've got a interview capture the way you think about the program or the program does.

2:29:18
So point, answer the program does not change the regions. That's going to be very important because the product changes attention. There's no to see how that's when you need to insert a new value in which protects this from the show that that's just because you look at the, you need to take a photo of the food.

2:29:49
So, it's important for the nature of our change, things that you just said.

2:30:16
What's going to be producing?

2:30:22
Learn about.