00:41
And you also have a career exformer because it's to go, the answer is like a ball Omega. It's India.

01:04
Never was enough.

03:11
Rolling through.

03:16
I forgot to read the to let the child the right character description and figure out. But here, my whole question is just to help for the best.

03:39
Okay.

04:24
That yeah, that's the word I got.

04:45
Effective.

04:56
Because that's it, the bad. He's like,

05:05
Of years ago. There's like, really think it's irritating because I do not understand this much. If you say, oh, I'll be magical to see if story. I don't know what that means.

05:20
Number to YouTube.

05:39
Thank you for the defense. Like I was gonna make it one one. Oh yeah, my grandpa is going to church many people and

06:06
Patients. Yeah. Not necess every time. We have it.

06:18
That is, I just submit a picture of necklace, with of these photoshop middle fingers and just like a little different race. So if you compare like I was busy this week, it's a coastal part of Africa.

06:43
Retracted retracted across or just like, what I was trying. I want to get it. I was trying to see what like you know just like I want to be missed your hatch collision. So, they're thinking like the four most likely would be, like, figure 1999 Honda 101 now, I think one more, one, two, three, four.

07:08
Oh, that's a good one. Four. Three. Two one, I don't think boiling three corners obviously is one, two, three, four more music players. Okay, I must say, I think I think that six quite rare, because I think that's a pretty bold. The full choice would not be my and it was not.

07:34
You've got your first voice in your last possibilities. Don't think I was there probably last like 9 1.

08:02
That you're going to go back here.

08:08
I wish you could jump forward, amusions false out. Some really amazing factors at that number, but I'm not married. I can pull up pictures of Google, but yes, it is over there.

08:25
It's also a cool number. So it's like a mathematical. Interesting number for some reason occupational proof by contradiction member.

09:07
Once again help security device look like what's the highest number of computers ever reached for any lab analysis or anything like that number we've ever really free. Just support the problem one. I assume that we do that.

09:24
What people became friends and we totally wanted to calculate above this new group of Africans in the country with other

09:54
And,

10:08
Because it was,

10:24
I'm really.

10:39
Anyway, all right. Okay, so normally when well first of all, congratulations and the homework of of other people that experience the job. But the bottom line, you have trouble because

11:01
That's all available people have submitted questions and partial drafts and I responded to that and it's on. So, there are also been so remember that

11:19
It's not just about, you know, kind of giving the grade. I mean, we don't interact. I mean, in some sense, if you're not doing well on the homework, you're going to learn more because when I ask questions and you're going to learn from those questions. So that's part of the reason why the homeless are, you know, a little bit more confident and like it was really much bigger yourself.

11:44
And but you know so those questions answered and then you know there's subtle subtle issues. Like if you run example, many of you use something like fire. The bar icon ID and not part of the part of the condition and it works. It is, by the way, she doesn't work.

12:12
If it's if it's robots because the power body is one statement and the statement can contract and expand contract and expand can even do nothing. They still want statement. We have part of the bar when done is true, this statement disappears and most famous. Generally obviously women have also found is true but you know n squared statement but in terms we cannot statements so that you can see this with you know with fairness assumption that eventually every statement is selected.

12:55
Well if you don't have any if the standards come and grow you cannot have them. Guaranteed that are selected and you get back, probably some fundamental things. But you know, you make a mistake, then we talk about it and then you understand it. So there's several things like that that you have to make, you know, earlier you make more kind of different kind of mistakes.

13:19
Like, you know, we used bracket in perhaps IJ. I cannot do that. Okay, time. And then, and then I can see. I enjoyed being declared as integers, but Angie, I'm not very able to, I'm John the Quando, so he don't be clear. Seems which, I'm not really, they're not part of the same that does not patient to help you build yourself.

13:54
So, you know, simple and some of those arrows and the beginning that you're making the beginning because disappeared, and the difference between marks and no guards. Also kind of is a beautiful. Another example there was a you have a statement for instance you have you know and current equals 0 maybe by feel that one.

14:25
As if you don't even know it's not, we have to have this joint conditions are every case. When has a handle that you used to do at the beginning, was you have your singing brackets. And then you have the key. This is true but you can't handle. You can have a God but it does apply to an entire concept.

14:50
It hasn't been a God so you can say this statement, the x equal conical, equal 1, if something but you can't apply that. If to everybody outside the brackets is it, that notation doesn't allow us to. So whenever they still occasionally, find. Is that even if themselves what? He's then mean inside the order section, the noise section is definitions.

15:19
You know you another sign of statements. No another.

15:30
You have I mean, the way we use it and I think is the God on a statement. We've already the God. And the God is false. This demo doesn't forget if it's true. Anything understand No enlightening and predicate logic if then take a form of event exists. But it's means that there's different things that implication and intentionally.

16:00
We don't permit using that form of formal level. Your empirical logic inside always section because you get confused and between the assignments statements and endolog. One last thing, make sure that the operator is consistent with the gun. They have a plus you know we expect to have an integer, there will be flow but we are really but if you have an end it has to be a logical expression.

16:33
You can use a one there but yes, but can we assume that zero is false wise, true? Well you could but I think that, you know it once you learn to do things right? You can start. Oh shortcut but don't do that. Oh so first, I mean you really want you don't want to then that lead to another mistake somewhere else.

16:57
Oh another financing is that. Yeah. So questioning very, very stood question is something an email and said okay? And if you have plus, there are some number of things but the range is empty. So you're not summing anything. So you say, plus I to J, you know, they're all true, whatever.

17:31
You know what? But if there are no elements, what do you return and for all those concepts, you return the user element. So for plus the difference is zero. So the range is empty, 0 from multiplication, the unit element is 1. So your as you turn one, if you do union them you need element.

18:00
It's empty set because you know, they said A union empty set is to A, that's a whole unit. Element is for the operation. So I have to be. So you so that is very very very nice to observe that. Okay, so my main good progress, get more help for those of you that haven't you know post systematic started early a small questions and incrementally built build your solution you know.

18:28
In some cases actually gave a least of, you know, do this first second, third fourth, to help to help move over long. I not only would talk about the solution first, but I haven't done enough social today, because we're gonna do exercises next week, and, we'll begin the solution next week and we're gonna do something else.

18:49
Actually, awesome. We're gonna go beyond giving the solution asking very, very interesting questions about if you actually wanted to specify formally the problem. How would you do it? And I show you those.

19:07
So today we're going to talk about the proof logic basically you know and location that you're going to use for proof and specifications. No, I want to make sure this understands this is not a theoretical computer science class. The fact that you're using mathematical notation doesn't make you a irritation.

19:30
Okay. Professor default is being theory, okay. If you're doing complexity, you know, the possibilities are, that's real, okay? But we are not doing that basically, using a traffic on location. Two express, properties of programs. So that's the weeks we focused on motivation. So hopefully we've been enough progress. So we don't make as many mistakes on a patient and the future.

20:05
Now we're going to something much more difficult, much more. We're looking at the look of the product. This is new to you is difficult. It's difficult for having this particular notation when we want to become here to load around the computer scientists. So they will have to stumble initially said, oh, you mean this?

20:29
I mean that. Okay. But I mean, so but we need to use a simple motion that you can work with and I told you it's not there for a logic. We're going to have to, when I move slowly, that sounds subtle. The rest is basically exercising things and taking them a little bit level.

21:09
Now, the book itself goes into great little depths on theory about proof, that's things like that. I'm going to trying to keep you that you can use them in different settings. So at some later point of time, we're going to take another beta That's specifying and show how this motion can use on a practical problem.

21:40
I mean, we use that elevator in our either so opportunity in class, okay? But we don't matter. It's specified. Particularly formally. And these comfortable capital looks like elevator going through the roof into this image of the body. So anyways, so this is

22:01
Of legs, but it's fun. We need to understand these concepts.

22:12
I'm not going to push you to use have an informed techniques to the, in the minutiae level. So we're going to talk about proven statement properties of statements, right? But I'm not going to ask you to actually do the mechanics of proving the problem instead. Right. We're gonna want to get higher level, but when you do understand the concepts and then you have to start learning how to apply them.

22:43
Okay. So today is programming.

22:57
One. So please ask questions as you know, as you as you encounter with difficulty because everything is meant. I also should point out this whether your program is logic and these are moving on that is because we are working with state-based model and we freedom from working with these model we will be using projects.

23:20
We So, because of different approach to understanding about products. So there's be some presents wherever program, So they say the program people. So the question is, what what does it mean? What does the semantics of the program be in the moral system that we are? Employed Basically the function on face and when it gives us is the set of infinite sequences can be presented execution of this problem.

24:02
Please accept remember our products answer infinity. So every time you break a branch make a decision, you start a new sequence. So, you know, really take all these segments. They have, they had a set and that's one way to characterize. What the program the meaning of the program there.

24:27
You know particular execution. Let's say r and belong to set, so the r is not only equipped one, specifically is equ. And what is our world in the set of prayers as 0? L 0 S 1, L 1, S 2 L 2. Exactly. So this in the state images of your program state, What is a program state for us the state of the Simon of values debate?

25:11
So, in general, the program state in computer science is the code. If it's modifiable most of the time, the code is not multip. So that's not what the state The program counter, which tells us what statement is going to ex and the memory, that's our state. I remember, you know, in computer science In our case program content, doesn't matter.

25:38
So we code is fixed. So there's no part of our state anymore. It's a constant program counted disappears. Because when we're running six, emotions, everything is concurrent. So the so basically the exit of the operating system chooses, you know, the schedule it chooses, which statement next. So you can't say, we are now at this time and we're going to use the next one, whatever the schedule executes.

26:05
So and then, So that's our stage, the state of the memory is ready, all the variables. That's why we're going to be clear. I am J which I've used as first construction because I'm not part of this thing before And then this is a statement.

26:26
So we label the statements called ML1 to whatever. So basically what this says is that I wasn't staggered as one I execute this statement and one. And now, the next step is going to be as to the schedule to the standard L2 next level here. And this is the termination.

26:55
If I give you as I and I give you have time into one particular thing as our last one, can give you more than one. Because we forced on our systems of We are using the Now I have mentioned in my or maybe not so weapon formation together, He said the unity.

27:21
Basically, they made a decision that they, you think you want to make a proof easier later on papers came out and showed that you can extend the tools very easily to know that the viscous. So we we can write now unit is something address all and because x plus 1 because the termination depending on the access, you get them you value, but you could actually write something about x colon econ.

27:49
X plus 1 or line 7 y, minus 3. And we can still prove 75 days which is another technical choice. It chooses, more of the other side, We have not allowed to do that in this class and they don't use it in the talk but people have been under players on it and show them.

28:12
Yes, there's not that difficult to, to change the proof logic to extend into that, but like I said, this is completely different. So the next thing. Now, a couple of those aerations, I mean and of course we can use some notation like, for instance art that state are either safe in the eyes, the state, in the eyes there and arrived at labeled eye.

28:46
That they know is a label of a statement that activity, the eyes step In the. I'm telling you this because in you're going to see this used, I'm going to to be more important, just but we have notification to be able to refer to an execution. And so, for example, stepping, which is apparent, I speak to label.

29:10
Now another thing that I want to to mention so so concept that I think that we need to couldn't, this is the the destiny. Is we assume that everything that our systems weekly fair,

29:37
So you know, in any relative execution, if you choose a statement, you choose to study calculated three, you should see Elton speaking executive and influentable. Which means that when you start eventually, our producer is executed. And then if you added any point of the execution, what album you see was executed, it must be that later for then we could write that formula down in string, but they but there's something more important that social, with, as a weak reference, We can only talk about fairness.

30:19
When we, we cannot talk about fairness only to find that sequences. That's why the programs are defined as a set of human sequences, not as a set of, you could define it as a set of financing, you know, first 20 steps. But one step on this is Amazon, but if you do that, you cannot have a square as because if I only, so if I say I'm going to, I'm going to have lunch with you something and it's now, moon and Saturday.

30:59
And we haven't had lunch. I mean, and we stop because it's a final sequence, right? It's not kind of. I mean, there's nothing to say that well maybe I could have had in the future, it's just we start the sequence to them. We start communicating the extension email to her, so that's why you have to have infinitesis.

31:23
So they tell me, six elements, we prepare nebulizing and infinite sequence. Every statement is integrated in infants and number of times and that's why we don't have variable numbers things. So if you have two statements, A and B, and you create a, and then you create B to destroy a different start and everything in the tool, they don't exist the same time, the scheduler we honest shoes, avoid the statement when it's available so so you can't say that, you know the schedule is unfair so you know you have so and be you know, that two statements and they they come and go so here aids here and then these here and eggs here.

32:21
So the basically the schedule is as well. I chose A was what developed since he was not available in number of times. Then the schedule of basically is no obligation. So, that's all we keep in the number of statements takes. So there are always there and always available Now.

32:43
You have a god donate they have opening system, they discovered and say, only choose this statement when the God is false, and if the ground is false and even this them and never does anything, it's always selected. So, you have to be careful about those kind of situations when you like to know?

33:08
Sure. No, not coming over days.

33:16
We do nothing. That's a classroom. And of course we have water here.

33:33
Okay, So so those are the two important concepts. Now, I want to ask one more one, one thing, Just, again from clarification if we create this ingredient, sequences type in some status 0. So, every time. So let's become statements, they crash out, right? That's okay. Thanks. And I think put you and worth all of that.

34:21
I have to bring my race around Anyway, so your intuition might be that we start in this state and then we graduate and every can be passed to the teeth when one of the efficiencies. But remember that then you don't start in one single initial state, they can be many initial.

34:52
When you say, you have a vertical X and we declare as being integer range, 0 to 10, you got 10 emissions, things. If you don't initialize so we can have our training but that's the integer.

35:17
I have an increase number of stocking states, so I took that in mind, it's not once one state is going to be possible. And if the number of initial states because our program, we wanted to work no matter what day you should stay like any questions for for I want to make sure what's a statement.

35:41
A statement is one of the most famous in the science section. You know, we have statements. Yes of separated by box. Oh, so statement is the one that's come with the colony equal and well it could be just a statement next going, equal. Why x I'm going to call y, which just one statement, or we could have it quantified, you know, it says have a box and I between one and end, you know, column and some statements.

36:17
So this statement has to have current equal, common equality? Yes. Oh colony itself when you express a signing of values to variables and that's diamond, that's an assignment which is used in statements. Oh, but you can have big statements that have many parts. They have part of them done.

36:38
They don't want them when you're parallel, they don't want steak. Oh, and when you have box then you get this many statements as you want. So you have a box so you have lost high, the one.

36:59
5 to 10. And then we have something right here by colony or something you've got. Now, end statements in your program and this number of statements has to be fixed, cannot value.

37:21
That's why this range here always has to be something that is fixed. Oh, so if you have high comma j from one to end then it kind of n squares statements. If I got, i j l from one to n with an accusations and that's totally fine but has to be fixed.

37:39
Oh, you have a ballot bar. It's only one statement and the size of it can vary. So can have many substigments or not, very melt That doesn't matter. But when you have box, you have to have this ranges to be determined to be fixed and very big, but has to

38:05
Any other questions? Perfect. So only making progress in our programs by assigning values So the assignments statements is really fundamental to everything we are doing.

38:34
And you know, the general expression is excommunicable to some variable maybe multiple variables and which is all about 11, you know our assignment for this value expressions. And always remember, this expression can have a guard. And the only executed, those statements, those portions of the statement forms about is true and then we evaluate all the power, don't expressions, the current state, then we make it all the silence.

39:08
So generally, the next thing. So there's no possibility of interference to do something funny, like, saying next colony. Because the white plus 1 in part of God next.

39:29
So now you're assigning two different values to the same variable and the same in the same statement and that is the legal. So you are not allowed to assign the same variable, you know, different. Now, they make an exception, if you got anti, even though you have two assignments, which keep the content expressions, but if you can guarantee that the value is always the same, then it's okay.

39:55
I never got anything that the value is always how well I can I can get x or equal.

40:15
Yeah, sure. Why square. This square. But someone in the program I have that. I'm human. Why is horizontal? So it doesn't look like that. It probably be there head rules because they're giving two values to x and the same statement. But because I know that y is the apol is the same So try not to do things like that and then all 45 of them don't turn off.

40:50
Okay, so we have this standards so you know if I make it fuller it has a target to it. God is including okay. And like I said, makes that doesn't have to be one variable the monthly variables, and then we have multiple expressions. So, this is kind of generic for all these.

41:12
So then the question becomes what can by the way? This is nothing to do with concurrency, right. This was already existing special programming so we're not on a new territory where an ancient, so the question didn't because, okay. So what what can we prove about the statement? I mean, if you're going to prove things about the programs, you have to put something about the individual savings, to be able to draw bigger computers.

41:45
So, what we can do is basically properties of this form

41:55
So the one is not only single number basically what he said. It says that you start mistake which satisfies property and you execute this statement, you can end up in the state where Q is exercise. Now is maybe true or maybe false if you're able to prove it then it's true.

42:20
I mean hope we don't really I should say we're gonna use. This is true. This is false. But on proofs. That's not, it's stupid. I mean we should be really using that lineup. It just easier for us, The properties are hold or doesn't hold. So it's not really because true, and false and specific, you know what it means and large, you know, property holidays normally believe that improvement can approve it.

42:49
I can cover that content. So, this is only thing that we can food and that has been known for decades and the question then becomes how how to improve social. So, you can choose a piano cube. And then I can do the truth, and I can tell, yes, or no.

43:11
It also doesn't know. Okay. So it's not like you know, the P and the Q come with the statement. It's anything you want to the statement, any modifying x, and you may have some properties about the universe. Fine. You know, I just approved. You know, the statement doesn't, it's not relevant to, that doesn't change the problem.

43:35
So the way you improve this, the way a very simple formula which is called their Sanibachis,

43:51
Basically, do we have to move that p into us Q x expression.

44:03
So what businesses are? So what it does is we have this this condition, if you want to prove has really used it through these logical proof not if this is pure magic, doesn't matter what the symbols mean here? When we talk about it and it's pure logic, please and predicate, implications allow you to cooperation through the predicate modified in some way notice.

44:30
Also that this is a mechanical transformation which means that I can take a first grader, can't change the rule and can do the translation. Well, you take the people from here and you move it there. You take the two from there and move it here. Take this and then move it there.

44:51
Take excellent. Put it there, people whose greater can do this? Any computer can do it. So I'm not going to ask you to prove this kind of sex. It just looks at the eyeball and formal and say yes true or no. It's okay. So what does it you what this says?

45:17
Every place you see replace it by the expression. Again, this is a first grader can do that. If I say every single see a letter, a in red, replace it by letter, B in green, the first greater can do them. So, computer can do this mechanic and really just have to use logic and their friends, mental gods.

45:46
Attentions, that can prove things and give them a special. It is to reform. So we wanted to say that this property called by basically showing that this expression you see whole specific, okay? Like I said we're gonna wait our hands but that's pretty good. Remember. Okay, so let's make an example.

46:10
So we have for instance, then x comment. Come over. Follow me. You don't know why the person that is a statement. The same is current. It has stretched two small expressions. And to variables If already expressions and assign the balance of the variables. Okay. Now, we can prove any properties we want, but here is an example of a property.

46:37
You can say, why is it called a k?

46:42
When I was this statement, x is greater than minus 3. And y is equal to 9 couple of visions not in the Mr. Product. The assignments thing when I started, it's a pretty good. This is going to be true or false. This is the predator true or false. The end.

47:03
All application of other existentials universal, only logic. So these are credit logical credits. Now notice that there is this. Funny thing. Kidding. What does K come from?

47:25
There's no came, you know, the expression. So what we're really saying was, when it's put a k like this, and a symbol that is not present, in is not one of the states. Part of the state is not a very good by okay, you're probably not program. So, when you put a symbol in this outside of the scope of the basically assume that is a constant that is universally qualified.

47:54
So we really were implying that we're saying for all K, I have to prove that this is true for. All right, so you got to make sure I want you to close as we don't confront you as between this University quantified values and the valuables of the. So it's a moment in.

48:21
What K is y is equal to k. All right? So now let's be the first grader that follows. What so what is their name of gay in these? Okay. Yeah. What is the yes or no, it's just amazing. It just

48:45
So it's implicitly quantified from not everybody. Okay. So now, let's calculate the first layer and the first grade are basically installed to follow this rules. So, the first rule is that it's copy, copy P. Here is y cochlear, right? Okay. You cut it then it says put an implication of them.

49:11
Verification number then it says quite EQ. Okay, so here's Q x - 3 and y equals equal to and probably x. They will know we have a maximum y. So I have to copy them both, make some money, I'll be the expression only have two expressions 0 y, plus 1.

49:38
So, now you do the computer because true or false? Now there's no patience says replace evidence of x is 0 instead of y, which is my transformer again. It's mechanical posting y equal to k. X x is replaced by zero and minus 3. And y is equal to my Wi-Fi password.

50:12
So this is true for this. So basically a one implies, why?

50:33
To do something. Yeah, something don't get you wanted to believe in that.

50:45
Okay, so now again, y equal to k.

50:53
So my plus one with them. Thank you. So if y is 3 for is going to answer. So, this is

51:12
From the other one, The property of this statement, then.

51:22
But remember for about a dissolved mechanical computer can do it, you're not going to be asked to read them. You better just eyeball it and say yeah this and use it in the rest of the proof questions ever.

51:42
And so we know you is returning my three resources. So what? Why is that not? Because this is true and true and anything. It's anything. So if not, it's true, another question. So the P is the great condition and it is called correct these for the precondition and is called the process, okay?

52:12
Yeah, pretty impulse condition so we can only do properties of same and in terms of free and false conditions,

52:32
You can train these together. You can see comfortable, but but it is a lot of problems.

52:47
I'm going to come first So one problem with them that we kind of lost our in this example. So I completed everything is three but that's a little bit of complexity here. So, one problem is not just about actually conditioning. So, if you have bad expressions, like

53:15
Is 0. If these, you know,

53:24
Feel them. You are. If the feel that you

53:38
So, how do you deal with substitution? Because it's not as simple as you had in here that begin to take care of the condition. So what really happens is, you know, we already have the expression, thanks expression.

54:00
That things present. We have human eggs expression. We need to transform it differently because you need to take into consideration of all the gods. So really going to happen is that it's going to have d 0 implies Q x 0 x.

54:32
So basically what this says has Thank you. God and does a substitution like this for, which is before, this is not you but put the guide as a condition info. So when B0 is through this has to be very and then you have to combine all this God. So, you know, to the implies Q x V.

55:13
So basically what you're doing now, breaking the problem to cases, improving each case server. So let's assume that B 0 is 2. So we made that assumption and then using application. Can we change cube? So we still the same is before? Yeah, b. Implies that an expression, but guess how much to be that this is be implies cube?

55:48
So now I have to combine the precondition with the card because only if the card is true, this is one of the executive. These false you're going to be needing. Can you impact and have to prove these for all the darks? It's not perfect and modern understanding that the relation for the issues really command them with a.

56:14
Okay? So let's make an example here. Accordingly for one.

56:25
Impacts has greater than 0. X is equal to 0. If x is a minus. So you see that we have serious assignments. If possible values based on the guards and that is actually where I'm going to sing the properties through momentum, which path to two, No matter which God was true.

56:49
The property still holds. So that's why see we're saying that, you know, we have to prove we have to prove provide the card and price the result but we have to do this for every condition and believe from the 0 or the 1, the 2bm. And we also have to use this equation where we're basically all the data form.

57:23
So you also have to add here.

57:32
0 is false, and

57:42
In price Q. So what does it mean? So this is an M.

57:51
So you see the energy substitutions here? Subsequent.

58:01
Because there doesn't occur because nothing is happening. So pleased. I mean, so cute remains cute, the very none of the variables. I'm notified. So it's the same sustainable. The same predicate. So when you have multiple cases like this, you need to break it down with the subcases including the situation.

58:25
Where does not. So what is that if you have places that have. So let's encourage three cases that cover all the possibilities. I'm headed back. This is going to be false because it's never the case that don't we have false, XXX is a great present 0 smaller than 0 or equal to so these can never be false.

58:53
So base basically is automatically hold. So you don't have to worry about it anymore. You just have to take care of the other cases. So, this one from again, it's mechanical it does break into cases and you screw everything separately and all it feels is just the combination of it.

59:13
You know, frequentation implies Garden of Life. And it's just not very stable. How if you want to do something, it's not straightforward.

59:35
Then think about if you're assignments.

59:42
And the word is different in US and every single done here.

59:56
I have no idea. I'm what is more complicated in the assignment? Then what you got here? There's what did you use? What would our variables? Right. There's nothing about the races. They're all single variables. So what in the world do we do? When I have a race? Well, we can have all that too.

1:00:28
So, we integration notation

1:00:33
So everything so far is been very mechanical very well and raise it, a little more comfort, we have to introduce anyone. And and these are very useful in place.

1:00:50
You semicolon problem or

1:01:02
So what this notations is, basically a transformer, he takes one array him, He turns towards a different degree. It's like a function. So if you have a formula, then array, just integers and plus, minus a zero and we apply a function called negative positive. We get a new array in which all the numbers are now first, That's easy to think about.

1:01:28
It's the same thing. So what basically says that I get the mere is qualified. It's still an array, it looks exactly like egg. You know what respects, except in the eyes location. The value is different. So basically we have a here, okay? Repeat the eyes location. And here we have B for a graph.

1:02:02
This location was 23, this

1:02:09
It is when he finds a way to give us a new rate, which is same as old one, except for that one location. And that's a very, very useful notation to have for all kind of reasons in all kind of situations to be able to to express reasoning quickly.

1:02:30
So this is really expressing the facts of taking a supply to you, but the answer is a function and that that allows not to refer to genetic functions as it been to that specific assignment questions. How do you do? Exp interesting. Yes, I you whatever so you can you can even quantify.

1:03:06
So I even I say I what I even if you want to end then do the old to know, whatever values you government events, okay? So you can, it's very generic. It's very, very easy to explain. Okay. So, All right, so now we there isn't really anything positions rotations because we like to deal with assignments of values to arrays.

1:03:38
Yes. So I can be a topological model for dimension a race. I can be a number of indices on the range and can have a range of all of them can never break. So I see the same. I mean say that you use before or basically you know what's like you can use that inside there, it's an ongoing trade between.

1:04:08
These are that the value is corresponding guys. So that's using one statement to change the values at the same time. Yeah, it's a function, basically takes the memory of currency to the next thing in one single step. It's a, it's a pure metap, it's not flattened and it's talking about you, you can do anything you want.

1:04:33
I can't swap by this, but in this case, all I'm doing is assigning. I'm keeping an example of how you, but I'm getting an example of how we can refer to the impact of AI.

1:04:52
So we because now I can talk about the new array of the AA. And we say, is this that I think most that's a problem So we don't want to do We're going to use this notation to put through some properties. So we're going to have a statement here.

1:05:17
Part of the bar. All right, we can join in.

1:05:29
Okay.

1:05:34
Okay. And,

1:05:41
How many statements do I have? And what one El bar, once he help us in one single store, was let me happen in here. What have you really doing this? We're similar. Yes, exactly. So if you take zero something am and you put it into a zero. And if you take n and played 0 to put in, So basically, we need to just stop the record.

1:06:19
So now let's say that we have some property that we want to achieve after their swap. So basically that says that for all J satisfied change between one and okay, we have AOG, it's more than okay, plus

1:06:58
Now, what is this formula? We got is a difference, okay? Right. Okay, so this is a so this is our predicate q. All right, so now we what we want to do. We want really want to to ask a question. What should have been true before in order to get this result again?

1:07:31
So basically, you know what should have been true before is Q or X is replaced by expression. But now X is not an X. It's an array, so it's getting smaller. It's more exactly the more best here. So what we're going to be using, example, is saying same approach, so we're going to take Q and whatever uses of air will be facing by corresponding for responding and corresponding expression, right?

1:08:06
So, let's go meet them here. So, this is still

1:08:17
So I'm copying $2. And I'm going to substitute the valuables with expression. So for OJ, there's no problem calling, no problem. Zero is one implementing JS. No problem pain. Well, but they was changed. A became. A prime social is a prime. So but what is what is a Why did we pranked Well project?

1:09:00
Remember this notation okay; zero?

1:09:23
Okay.

1:09:28
And,

1:09:36
So this is the same old array in which square inches of pi. I replace it with pain and manifest so that so I got a new arena or so this is a prime. Yeah, but I moved it. Really fun.

1:10:07
Then smaller then.

1:10:22
I need to do the same thing. Same already okay;. I component.

1:10:36
Okay. Same thing, a and that is right. So listen, this annoying prime is the same problem. Same. No change. All right, but now I need Jake Messer.

1:11:03
And that.

1:11:08
Becomes.

1:11:15
Any. So you see how the expression will make a silent array of multiple services for substitute in. So now once we have this then we can work the normal way. So or like J, you know,

1:11:46
So I only copied this. Now, this says, I wanted J7

1:11:55
So what did J7?

1:12:03
Well, I make I equal to j, right? Because I get aids and everything. Think I wanted the third element and make y equals 3 and I get paid and minus 8 correct. So this is okay and minus drink and it's more of them. And here I wanted J plus one of them.

1:12:35
So I make pi doesn't give us one because that's about an interesting and I know it doesn't the rest of. So basically it's a of n, minus j plus 1.

1:13:00
So this annual array, where the ice element is this the J7? It's same thing but the judgment of life question. This that question. But why J is not zero and

1:13:25
We are interested in comparing an AJ to a new plus one. So we need to compute a new aid. A prime trade compared currency to other companies. Now, it's quantified for OJ of your only. We need to be able to make you compute those contents.

1:13:50
So, once I get that, we can play with it and right here, I did 10. Hey.

1:14:13
So, can you write for all parallel bar? And I'm not sure I mean I want to make sure I understand what the for all operator mean This visit for every day. Yes, In this rain, this is true. So it's that equal to parallel bar. And statement. It's logic for all the problems.

1:14:50
Yes. So for all means that for every value of J is that range. The balancing is true. Is passion is true. What this says is that for every now and for every day, the js are the many smaller than the next one. Oh, that's one. So, and every sort.

1:15:18
Oh, So now we certainly. So, we got here and managing minus one when you factor that might achieve finance or why? Because you do the same way and then they can change. We can change the range and basically say for all J three or small and three and have a colon

1:16:03
Okay, form of it. Okay, they minus 1 see. I basically replaced see and minus j. I just replaces this change.

1:16:23
This changes on the range of the quantifier and give it some exactly the same problem. So that means that originally, the range should have been sorted in.

1:16:44
Is not in order to be and then results. Why we don't have the great condition. Well, we've got basically computed, the computed test. Yeah. And we're just very interested in computing. This, We're not interested in classical entry.

1:17:13
So basically truly drives this so computer. So in order to have, if we swap the array and and the order should have been reversed in the original is in the sending order, should they be sending order a visually and that's something completed. So that so it matches our integration and anyway so and we have now the mechanics just one second.

1:17:46
I'm not going to ask you to do this. Subsequ to understand that can be done. I want to understand the transportations available in anything sure this mechanics but they get computers can be there for us because now the risk is that you are going to tell me that. You know, if there was in order to get it in a sending descending order, it should have been an ascending order with it.

1:18:16
You allow for repetition, and this doesn't allow for reparation so you can make charge error judgments because you actually didn't draw the formula through. But I trusted enough, I'm thinking in, you know, avoid those kind of animals. So yes, we are prone to error because we are being informal tools, and that part.

1:18:36
So when you tell me that these property holds for this statement, I'll take it for granted. It's how did you move from the the last two ones? Sure. Well, so, I took and minus J and remaining of. So, when J0 qualifies to be n and when James and others must be zero to just, I mean, I I use the same j so we can see there's the same formula, but you can, I can replace J, is any variable in a quantifier and doesn't change it?

1:19:18
Any sending it to mention that equivalent between a minus j and alpha 1 basically, yeah, just what I said, you know, I'm going this one, the and then contend to receive five inspections.

1:19:40
So like I said, don't take some rice because you may decide that. And hold on top of here. In fact what. Okay but I don't need you to to answer all those mechanics. No level mechanical, you know what? I learned more and then machines can do and care. By, you know, I will name property to begin.

1:20:07
So now we know how to prove things about assignments, that for No, there are certain things that we can prove about products.

1:20:35
So we're interested in the summer stage because our programs consist of asylum centers. So in fact, you know we we're really interested in the statements of a particular program about the science community job. So basically, you know things, this is about seven.

1:21:02
So that's available to us at the bottom of, okay? And do that because we just use a stem. And from our program to go to this mechanism and improve that experiment, does whatever it the property of the stem holds. Okay, that was a general properties that you can if you have a social event, this is moving process of things.

1:21:32
So, for instance and improve see

1:21:47
What is PSQ means. If you're starting them in a standard phase 2 P, few. That's what that's for now means. And we have a mechanism to prove his goals a lot, but that is true.

1:22:19
To the set of all states. So the clear that defensive instrument is unless you have an exception of some sort okay division by 0 or something like that. So the smaller statements fit 50 divided by 0 is like the sustainment doesn't finish and our statements are assumed to be executed, you know, atomic singles, that, okay?

1:22:42
So if I resume a single step, what you can at least change the very values in the in the memory true says, and then care what the data sign. So this is always proven and seven more interesting.

1:23:13
You can do this again. You can start getting false. False means there's no valid state, but it doesn't have nobody stay down program. Has all its data valid states and some of the values to remember, memory names to values. So that so you can start in the state of Illinois doesn't exist, you could end up anywhere you want.

1:23:40
So, that's not that particularly, I mean, it's important to know this to things to understand what this format means, but there's nothing to use from the truth. You know the most proofs okay because you're basically saying I'm standing in non-existent state. How can you stop an on? Definitely don't know.

1:24:03
And this is logically consistent to work with all the formulas. Now, more interesting thing is we have something called inference rules.

1:24:20
And inference memory is saying rule that you can apply. You can prove somethings and because you prove them, you can conclude other things, whatever. Okay. So it makes this positive, you can conclude that x from the x equal 1 is also. So, here's an example of an inspirational

1:24:56
This part is called the hypothesis.

1:25:04
And this part is called, conclusion.

1:25:09
So if I were able to do this proof of this property, then you can computers. So basically, I'm saying that there's another you assume that you started in a state fee, basically this technical ass and test in false. Well, means that you are outside of the program bombs. Then clearly, you could not have started this in being.

1:25:35
So, that's a way to show that, you know, people could not be true.

1:25:44
I'm taking rules. So you prove this and then you come from this online, okay? And other influence, really? For instance, might be something like SQ color.

1:26:08
No before that. So this is an influence. But before I let it conclusion, wonder is happening here standard as we decided to stay satisfied with. Remember, staying here, notice there is a comma there. Some of you use comma instead of n, which was illegal. Okay, this car basically says, you need to do this to proofs independently improve days and improve that if you put them both separately, then we can draw some conclusions in the here.

1:26:52
It is P. And yes, comm, your prime cover PR.

1:27:11
Few more different again, the karma here is not a man, but basically said you can go through separate, conclusions use the one that you need is basically says that if you are studying them in a, in the intersection of PMB prime. So remember from P, you can go into Q.

1:27:36
We have been brought and intersectional the two. Be fine to pray is to die. So if you started this intersection, you end up in this inter. And who are we seeing you again?

1:28:06
Before we take a break, and another property important. So, to deeper on your price to cover,

1:28:22
Can comma, right? Good. Take pride.

1:28:36
So, you may want to prove this but maybe very difficult. So then you prove something else where people are invited to be and Q in Brazil. Probably, so then you can conclude that from people. I'm

1:29:00
So you, so if people have implies P and speaks here inside the people, few prime price, Q, you pride inside. So, if you put the to fuel,

1:29:26
Then.

1:29:44
Deep frying in place in Q. Nice. So, if you throw that move from D to Q enormously, you're gonna move into

1:30:04
No, an interesting observation and we start rules for us to

1:30:19
How we have a problem and they have programmed their statements as so for instance we can write something like this, like the following as Okay, next next greater than or equal to

1:30:47
What does it say? This is what every statement that I have in the program is somebody K. The only thing that can happen is okay, chemical small. They can also use existential. And so, I did it makes it more, okay, Pass Texas.

1:31:21
So that specifics as there is a statement. I'm just wearing laundry increase because this doesn't guide me increasing, just gonna choose it. You cannot increase This. Increase can achieve that you can that somebody is going to increase it. So what's really happening here, which is really quite interesting and they're shopping is that if you know how to think about assignments, there properties of a service account, and you use universal and existential partifiers improvising.

1:32:05
This is called the safety property because doesn't guarantee the dancing is going to happen. But in the streets, what you can do, that's all the products probably which basically says something is going to happen. So what guys and what is that I do is that in principle. We can stop the course semester here.

1:32:28
Brother, go home and get a name now. However, people that did proofs like this. And that is this and something. When there really is that, if you have one of these sequences, these talks about what the statement can do. And that signals, you know, you obviously,

1:32:58
People trust like this. And then notice that simply the customers of the proof. Well, you've been there from programming so they said well this is just too low level. So thankful problems. Can we take these to the level of and what people do next after they were afraid to basically?

1:33:22
I'm gonna see how people can think more abstractly about haven't been. So you see one of the problems here when you can think about all the students which is excellent for fruits. And I just proved something that probably ever followed a lot of programs. You know, we had to look over the statement what they do, but if I want to specify a program and say I want the program that does this, I don't know what the statements are.

1:33:53
So I need a language. That is independent of the specific statement of the monastery and that's what we're going to do.

1:34:06
56 minute break. Maybe you are the graduate of the break or 10. Then go over there. I'm going to bring that sandwiches and beer.

1:34:35
Turned out for what the filter. Okay, he from key that really was her second notification, I have. Yeah, so you don't move from state to state this understands in which people these are not the same 6 and this takes us. Like a subset of The movement is from P.

1:35:31
A value is necessary more program, but in other people around all of the subject of

1:35:59
It could be of this, so you're not moving between these two. So, instead of staying this is smaller than that.

1:36:18
Yeah, I could prove that. I think all the state the state that is in so but people friends inside of you. So, if you have a statement, you can write all together. Yeah. Okay. But because I'm cubed then automatically, right? Because Q is morning. So, that's So we might become one or and female people want to take the subject.

1:37:05
And this is and we see a implant.

1:37:17
So when P is on this group P has been, but there's nothing to do with the stimulation because

1:37:55
Google. My pleasure is this very good? Is that combining all which can. So that's why I asked you all this because to all this family member that we have. Yes. So is this that terrible part? No part build things. Yes. Always like cement. Yes, We build a house from our house.

1:38:29
Oh, now we have the house and we ask this is house, where the blue and nothing to just all or all the doors open. Oh, all of the windows open. Oh so when we build it doesn't matter to get by the state outside. So so I think I said as long as I mean the tell me one and this kind of thing, but is applies to every value here.

1:39:13
This has to be true from, basically, increasingly says, I between zero and n. And this is the B of I smaller than k. Oh, I forgive plus one. We take every value of high and check it against of what I put 0 to change this. When I equal 1, which is this, what?

1:39:43
I could help and all of them have to be true or they're. Sorry, for all. It's the same as hope. Oh, yes. So there's not even no difference that exists in the center of and for all the sand and also this through is actually incredible. All of the same thing of it's so apply and to all this expressions in the same thing as saying all these expressions are true or best feels but but that is what

1:40:36
Organization.

1:40:48
Right.

1:41:10
Getting horrible program.

1:41:26
Goodbye.

1:41:31
Or by the Olympics. So what we want to do next is basically move away from all this long level and our very previous work to something that is. So, we're really looking at coming up communist service.

1:41:54
Don't feel like so to do that, we're going to have a sample program here. So okay, so I'm gonna make some assumptions. The summer program is complaining to sequences and checks it out, the same set of them. So we assume that for the same as the FMG. So you see that, that is 0.

1:42:24
So the ignition elements are always the same. The last elements I'll also the same. Why do we do this? This constant and is because So we see the environment over And then F, it's have in the hospital and always treated them to one before.

1:43:05
And then whatever. I for the line.

1:43:22
Jewelry.

1:43:34
So if I have this door race clients might three, basically says, the first element, I always the same comes here. So the last element that are the same as square and this element is always greater than 24. This are some some conspiracy to just put another way to pick up pharmacy.

1:44:03
Okay, accusing later on white that. And at this point, just thank you for. That's what it means first and last of the same. And the last is about the same as

1:44:18
So now the program, the program is basically going to look at the storage and going to compare it. So one of the things to be seven and all the other one is one, three, four seven. This equivalent is a set of three, seven. Have more sleep for seven years to settle.

1:44:47
I've got the hand, he's this, if we have this seven seven sermon. Then these two sets are the same and comparative to sequences whether or not this from percentage. So program is called compared.

1:45:15
And we declare,

1:45:26
We're not a very FMG because SNG are constants outside of the program. We use it but it's important that this is initially.

1:45:46
You know, so it's going to be and then the sign we have three statements therapist is one that are there's two customers. So we made this payments on that before we go back and then I gotta have it. So the first one says view or an equal u plus 1 him you is more than him and half of you is recorded of.

1:46:29
So basically what it says that you starts here, and if it's in a situation where like this that are the same, it just moves over there, ignore what evangelist, so to move to the middle and stop the provided.

1:47:01
The same thing happens as being. It looks like that early which be has to be smaller than, and to show you.

1:47:18
Have anymore. And then the last element, basically, this room D. Those are the last one if you is more than n and v is more than 10. And okay, no cross. One is equal to G for. So this takes care of situation where like this, this is doing, this is me to have funding to stream.

1:48:03
And the next level is the same, and then we can possible over until the next element is different. They can move and the program starts portable patient. Okay, so we're going to use this as a to illustrate. Yes, that is j. G of q and in the vertical object, not checker or algorithm.

1:48:34
Yeah, I only have three from different. All right, so now we are really interested in using this as a playground and very interesting. So, so the very first assertion is the unless problem.

1:49:05
So, basically what it says, it says that people are in a state.

1:49:16
But in some state ERP.

1:49:22
You can stay in P forever or you can move to he comes with anything else. It's a first thing. It doesn't candidate need to do get you. So it just basically says, you can stay identifiable won't move to you, right? And this has to be problem in the program and to show that the program actually satisfies our own programs properties of programs.

1:49:53
So, the formula I said it's for OS. So basically says, from all the statements where the standard ass is in the program, B of we can prove and not queue as P or Q. Can conclude. That's So capital of generations. First of all, this is the safety. Program seconds of incomparency that took other problems.

1:50:38
Safety. Alignments Safety says you know representing Rome in particular, you could do nothing for the rest of your life. Conversely. Found anything wrong. Okay. A lot of men says, we're gonna do something. She's normally anything wrong, but you're gonna do something. When you combine the two, you're gonna make progress in the collection test.

1:51:04
So this is safe. You basically does not require the program to do anything. It just says that if that's make a change, you can only go from field. Yes. So this unless is outside of the program itself like this is a problem. Okay, so we have a program fee and it will show that this satisfy this problem and the low will show this.

1:51:30
We'd have to look at every statement and pee and prove this relationship with what I just. And the way we're going to prove that is by eyeballing, you're not gonna have to do any discussification. But notice, first of all that to prove this property, you look at statements and we take each statement that satisfy the problem.

1:52:01
So some statements might give you a big or no 72k that's all fine and but the way to prove it is from the text of that program you look at every statement that text understanding and you show that that property is true for every one of them. Three proposed things, you are able to compute that.

1:52:30
Then you have again improve from the text of the program. You do not start thinking of. Well, if I want to this task around that cast and at that task, we get there. But if we starting with this initial value, it's on, no, no, no, no, you can't do that.

1:52:51
What are you doing? Is look, you say this are the property and you look at the very statement, that's the satisfy. Yes, no, yes, no, yes, no. That's the only thing you can do, that's the power. You don't have to think about the execution sequences, he just drew properties of the program.

1:53:09
He was out everything about the exhibition system directly from the program. Text of each other. No, the interesting thing is that what will be on the skill that a lot of interesting properties that come from about. So for instance you can say, stable Well the the same thing as programming P unless

1:53:46
Want to stable three meets means that even the program. Gets into this paper piece through. It's going to stay there forever. Can't get out of it. Now can be very large space so it can move through all that space, right? That property. Would once you get it, there's no guarantee that you get there by even there.

1:54:11
So most of the time basically what always going to prove it is going to say, okay, let me assume that in state P. I pick up this statement. Do I get out of state?

1:54:26
The case positive that is changed, okay to negative. No that and this apparent some statement. Only 24k. So the proof is really does nothing, okay? No, another property use is constant.

1:54:57
So this property is a very stable, It's very, very important constantly basically. It says stable P. Then stable.

1:55:20
That's kind of weird, isn't it?

1:55:25
It's a man is not an Lord. It's a man. They have to prove us, people whose promise, But the community of things that if you get into pain, you stay between beforeever to get into those being to not be forever. But initially, the reason we p what is not, right?

1:55:49
The composite truth. So we start with P, then you stay people. Every time you're not be mistake, you stay not people there.

1:56:05
And then we can all use this because it's very easy. It may easy to, I mean, United States. So, you may think it's kind of

1:56:22
But we'll get some example. Let's just go to the high level. That doesn't come back together. Now you're not going to use concentrated offers at the following. I'm going to use for that word, everybody. Never embarrassed people that basically says, to table have image

1:56:55
So in the Guardian is a property that is true forever. That is to initially import a statement. Property is a truly probably that you did create support of sort of another rule but in the guidance as you initially started with this being true and you kind of continue to do forever.

1:57:19
Notice that here is a place where we actually do. They need to look at the anchorization values to prove our basic on the other part of these stable. And unless we did not care about initialization and nothing really initial values. We get in the property. In this thing. Here we factoring the initial guide.

1:57:42
So when you practice from an invalid, we have two obligations, You have to prove that most women breaks it and you have to prove that initial history. No statement breaks in basically basically says free aspects. Any statement that executed still? If you started peekers gives you that, this is really, I don't care what system you're going to build.

1:58:17
I don't think you're ever going to use but in Africa, notation from the rest of your life. You need understand this because this is fundamental to thinking about programs and it came out of came out of signature programming. How do we prove that the loop does something see, statements, decided to stay using the statement and again, another state group makeup on looping.

1:58:49
So the the only solutions are improving a look, is to come up as a looking variant and prove that the movement pays it in value. And then you combine the anxiety into the terminating condition and that gives you the post condition clean, guardian plus termination condition on the loop gives the concentration.

1:59:11
That's what we do in sequence of order. The interesting thing about it, the invariant it's also that it's a really, it's an abstract expression of thinking about the problem when you do, the only one, look at the group. And look at the invariant, it really tells you what the algorithm you had in your because evaluated specific to the algorithm that you find for using that indemnity.

1:59:42
So guys are going to be extremely, extremely important.

1:59:54
They are saying that the important I am. Sorry, guidance. Is that if you have any guidance fee that, the same thing is true. So what you needed when you needed some place you can have invariant because someone's. So let's say something.

2:00:23
Business. Let's look at an inference at to P, unless you cover in value. Not.

2:00:42
And we can computers from this type of

2:00:48
Probably how do we reason about? How do we improve? Okay, I do like this. Well, okay. We have our rescue man but you're having very not queue so it's not crazy. Guardian Man. Then basically, you can hide it anywhere. So you can basically have up here on the SQ and block you, who am I?

2:01:14
Who is false, so that gives you pee unless polls, which is exactly state. You see how you use, and you take advantage of the variance in, you know, to augment predicates because I was through bring them. Okay, let's say some other examples.

2:01:42
This was an example of how we use. This kind of what is coming back in substitution theorem in developing some. Now, let's actually do some proofs about problems because that's what we're going to have to do and exercise. If you ever get it constant and repent and said,

2:02:16
It's a true think of that program, in true enough.

2:02:24
And these are sides of the ring to constant.

2:02:32
Think about the full price that they have the same and seven months. So let's say that the peace group that means that Andy's bigger than seven like it's 14 is going to be working forever or not. Look at the code. Yes, five important forever. I've never seen him Now.

2:03:00
Let's take a look. Now, if you've been in is smaller than 73,

2:03:10
Is going to be true forever. Yes, but again don't change. So you see kind of don't really associate necessarily constant number and equal five is being constant. I mean, even problems that have been through both the particle and

2:03:36
Constant have three because of G. Kind of reasoning that may be true or maybe false when we're changing F and I'm not genuine change. So if it's true, is remains true forever. It's all inexpensive.

2:04:04
New contains.

2:04:09
You old enough.

2:04:29
No. But as I said, if you have some value k in gonna stain that I came forever or getting bigger, not some other, it's not gonna do this to get big. If you notice there's no statement that decreases you so if you is equals some value is it doesn't change 20 degrees.

2:04:56
So the properties and you see, I need to do it standard myself. So stay my teach can only increase. Okay properties. True statement is doesn't concept problem then attach you trivially true. Yes. Only increases you so. Yes to get through again. I have to look at every statement substance of knowing part of you so that they kind of they got another something back.

2:05:29
And then if they have an impact area, to be honest, and increase the technology. So, we determine that statement was true. No, you can tested every state. It doesn't want and we cannot decrease it. They want to. That's the fact that three cannot. Okay, So therefore you see the not queue is imply because greater than cades same is not Q.

2:06:08
So you know, okay, so you're taking all the statements to these girls. They want is a time, okay? Separate. And you check that this property is satisfied for each other.

2:06:27
Stable, you

2:06:47
So, it has to be.

2:06:52
Against here, is that here for

2:07:03
But notice what's what the condition is actually these to think you come equal. There's nothing wrong with change that, so you assume that you is really good. When and now you check it statement, it's easy to end with this modified your end, you know because of this product now because doesn't attach you now because of this guy and just using the property code and then you test the statement against the person

2:07:46
So, maybe the property USA looking. Can he cannot enter and I'll break that because only way to break is because my minus 1 and none of them. Decrease, what we go to. And plus 1 is not of them. Change. You can, if you are going to regular that's only

2:08:13
Okay.

2:08:19
I'm going to slow it because it's an old process. So you need to, you know, to kind of so that same guardian.

2:08:41
And between 0 and then true or not.

2:08:53
Group true helping. Improve it. Well initially viewing beer zero. So we know today, start offering zero and we've seen that, they can't decorate it. Anybody gardens and that is close.

2:09:15
And so 31.

2:09:24
To equal. And we can only the baby.

2:09:39
First of all, stock is initial condition. Is it true?

2:09:47
My.

2:09:52
Because apples falls. So this is false and this is false, believe it or not, those thoughts. And then we, then we assume that it's an ideal voice. And and then there was a question. I didn't think and when we do end nothing here, you cannot change in any department.

2:10:22
Not only statements about,

2:10:30
So your is equal to b.

2:10:42
Questions. So this is the level that we try to start by. Thank you.

2:10:52
You and they're going to use this formulas to specify what the program should do in a respondent approved program.

2:11:04
So, as I mentioned on this, it's a safety property. Well basically one do anything wrong.

2:11:20
The first progress somebody that could begin.

2:11:36
The progress already because it's going to require something perhaps and what ensures that they can see,

2:11:54
Progress will be made because there is a statement. It's going to take you from people to and it's a life respect. So you're gonna have to prove that there's a stand. Then we very solid something. Very subtle about proving insurance, you need to pick the statement and say this is my statement and I'll take a finger Eve the opening system chooses this statement.

2:12:26
I'm guaranteed that I'm going to establish Q so you can establish Q by in some situations using this statement and subsequently to themselves statements. That superpresent there's not an ensures and I'm sure it's a guarantee by. Once they choose that statement and you wait two dot brain system, select it and then you're going to dedicate into cube.

2:12:52
Now you might get there faster because all the statements can also do but that's a guarantee. That's what I usually let.

2:13:11
So, let me put that to

2:13:22
Unless,

2:13:27
And there's this thing with this some of that as invad, I've had B and not here as

2:13:45
If you're improving, if you can produce two things insurance,

2:13:56
So you see here. So this is a product safety property which can visit you need the same P or move for Q. That's on the options that we had because if you don't have that guard theme then you could go into our that's a lot. And there is a statement which is planted in the selected is going to be from my pto.

2:14:21
But this is all 27 of the program, they can be understandlands but this is a guarantee people and the scheduler avoids. Any statement that the patrimony P2Q eventually is required to select this statement and you're going to get the result of the job.

2:14:44
So, let's take some properties.

2:15:03
You people k, make sure you greater than

2:15:23
You need to produce things. Need to prove that this from view equal to K are there is breaker already proved that, right? And I have to prove, there's a statement which accomplishes this

2:15:44
By the property, hold them.

2:16:01
So, if there is statement that will increment currently implement,

2:16:09
No, right? No, there's no standard idea and for this condition is false to build out of the grave, and this condition is false, you doesn't increase. So, I can't point to a statement that current case

2:16:31
Woman.

2:16:36
Improvement. So, let's assume that the two areas are actually the same, okay, that is somebody.

2:16:52
And to the case.

2:17:01
You.

2:17:11
There are identical arrays.

2:17:28
The trick is that you need to point in a statement.

2:17:35
Is going to?

2:17:43
Clearly, door two is only.

2:17:51
Instead of performance. Let's say and doesn't.

2:18:07
Wells. What what happens? If where the situation is 3? 3 in the identical, right? And so, you're staying sweet decreases. If also.

2:18:50
So, it's possible that you is here and which is existence.

2:19:01
And,

2:19:06
So statement three would not one equipment,

2:19:18
The same thing as they were born this state.

2:19:28
So you see there isn't that? So he's a very the same. No because they you can move the two pointers are not synchronously. Moving and moving a series feels like F1 went off a couple of times before I could almost select a couple of times before. So you see that's a difficulty.

2:19:52
Much enjoy the various. So actually if I'm learning later on, if you don't lose insurance and specification of programs because I'm sure it's like a statement and if you don't have the program, you can pay for they can't use and everything. So this property in some sense is true play.

2:20:15
When things are equal, how you are going to increment you but in some states you are going to use one statement. Another state is going to use another statement. So it's important issues. It's very simple and it's very easy.

2:20:33
Okay, so let's take another property.

2:20:48
Each customer general. And basically, the way we're writing is she I don't have like that or I decided

2:21:15
So what this says about, okay, if you are in a state or peace,

2:21:23
We gonna empty the later times. We're gonna get in the state of Houston. I don't know how you're gonna. Hello. I don't know how to get, but I got into gonna give it. If I start with an array, that is not zeros. I've got to be the eventually run into a were everything is here.

2:21:45
That's but it's going to take a lot of steps or maybe we can run step depending on the property. So, these two is really what, what is going to use is to be using specificated. This is another powerful progress condition that is to them, the couple of ways to prove the sometimes so it's not like the other properties were we just look at the statements and, you know, we need to do some other mechanisms so we can move shorts you and then can come through.

2:22:34
So, by definition, and you can get that into one step eventually in one step and you'll get there one step in the same thing. And eventually Another possibility is that CP needs to q and few things to our. Then you can conclude the field. Next this time, you think?

2:23:10
So if you're not going to hear the p takes you to Q here. Think I'm going to do the two things into our here and clearly you're going to get into work.

2:23:26
And now, sometimes we do to find out because thanks many steps to get there. So we do an induction tools, show that it's good. Because every step again a little bit closer to another closer to another, and that's a little

2:23:48
Another way to do it, producer of destruction.

2:24:03
And this is very terrible. Can be harder to understand. That's right, it's one more. And then targeting isn't always the, basically, the formula circle. That is a disjuncture.

2:24:22
New Johnson is all the breaking into cases. So basically say for all M and belonging to some W from space, only we prove Makes perfect. Then we can conclude that the reason them.

2:25:05
So but still perspective that makes session. The W has only three six elements. So the basically and one It's not the states in which peace to and we prove that in each case, that's conventional need to keep

2:25:36
Then, we can conclude that 181 of this. State is true, can be accomplished. There is, there is more mistakes. He said then we're gonna get. So if you put that in general from any one of them, you can actually begin to cube. Then you only have to prove that one of them exists.

2:26:02
I mean, you can conclude the problem, the developer of them exists you can get and this is really proving it right next.

2:26:14
No, think we, if we use these two, for instance of the two UND people 0-0. These two will be, if I when we miserably 0 or the latest point it reached on a very and but that, that is going to involve leads to properties to show how we make the progress, and then electronate that, you cannot go beyond these, you know, be zero because the arrays are different in that different

2:27:02
Oh,

2:27:09
Questions.

2:27:14
For excuses. So I'm not sure if I hear you wrong, but when you say progress property, okay? Is that equivalent to life needs property? Like it's a lot least to the lightness property. So unless is a safety property and leads to his enlightenment requires progress. The lightness of privates are the same thing.

2:27:40
Oh life needs and progress is awesome. That's it. Okay. So what you're I don't think we have positive workers in this part.

2:28:21
So in the for more number two, once you have you have a shoe place. So she's registered this as we.

2:28:38
So this is a zero.

2:28:43
And we don't let's mean to happen in the mother. She's so basically it does it moves elements from from, right? So there's one. Every step is going to be a synchronous register these most of the next. This was the next. This is a business to hear and so on.

2:29:08
Now, working on. So also going to do is actually and 0 is not going to draw, the data is going to start it down. And it comes in basically we're going to push on the data to the left and it's going to fix zeros. So in every step data, most one step closer to a zero and a zero is I can optimize.

2:29:37
So the code for the program is called shift and sound, It's in a is given. So what what you need to do is that a number of the 10 properties that, you know, maybe true, or maybe not true about the problem. So you have to take these property so you will get your program into the program and then you'll these properties.

2:30:07
Number one to the same numbering, copy the property and then explain. Why is it true or not? If it holds them up first, we say halls or two you can use trifolds. True discoveries through this properties force. That the first thing you say, and then you explain why?

2:30:30
Okay, so that's it's already to do that. Just each property. Any other questions. Any questions?

2:30:52
So that properties all of this custom stable ensures, and

2:31:02
Right. Then have no questions. I can get back the venture and we may need to, to go back over these. We have a couple of minutes. So the information is about stopping and then we can maybe go back over. Where you thinking next?

2:31:26
Yeah.

2:31:30
Okay, I think you don't have to worry. Definitely we're gonna use reductions on God. So the principle is going to be that we are going to develop a metric of how far we are from the target. And then we're going to prove that with the eventually the metric decreases.

2:31:58
Several times decreases. Will eventually get the doctor? Not only that I've been going to proof a former proof of why these proof makes sense based on the general induction history. So it's gonna be interesting. Okay, then also I wanted to talk about

2:32:27
Reason. Because it's a state in which the program no longer changes. That's everything throws. Once we get that to that. So, we usually have FP of forever that state we don't always change. So it's used for termination, so she's already, our executions are different. If we seek place point means that we have finished as a world and then the computer should be smart enough to stop.

2:33:10
Now, the interesting thing about fixing dinner and this is, you know, because of systems at the charity of fixed point. That's very, very important but they just think about 6.8 unity, is it actually fixed point is mechanical. So, a fixed point. For all as. So, I can pass the P and S is

2:33:52
So what this says that for every statement, which is valuables assignment expression, how long is payments, The fixed point is protects the collection.

2:34:10
That's amazing. You know what it means? It means that whatever you see a box, if you guys think it's an end and whatever is equal and equal to and you gotta fix one again. What does that mean machine computer? He just had a little script and can do the computer fixed Now.

2:34:35
Not, I mean a couple of wishes, The not having program has sexual So for reasons we have a program which is k for an equal k plus 1. Intriguingly it says if we're running forever unique and many key, whatever. Right now, if you apply the rule here, basically, this becomes a okay, plus one and this is false, so there's no six pack.

2:35:12
Another interesting thing is that they may be more than on display. So you have x 1 x is equal to 0 box and it's going to access equal to 0.

2:35:38
If it doesn't just cross statement, you can have one. And if you don't think in the second statement first because you get it too. So you can have problem with this one. An interesting to see that what happened from the head conditionals. So,

2:36:05
For instance, we can have k for an equal k plus 1. If okay, smaller than that.

2:36:18
So according to supporting to our rules, not only have to, we replace the colon equal, y equal. But we also have to do is if and the way that he is converted is by implication. So basically, where we ignore. Okay. Smaller than 10. Some twice. Okay, you application. So you see there, if it comes this indication,

2:36:55
My, what I was here is smaller than slice. What is this?

2:37:08
Internological expression is a true false homes. So it came from the main place for us and this must, of course. So if this is false, the inverse magnitude, the universe of case, one of the head is what thing, right?

2:37:37
So what that says, basically two things. So notice that we are having incrementing. So in I know that you are intuition says, I am an increment commander I stop at a right because of this code but you forgot is that also depends on the definition values. So if you stop low you stop at 10, but if you start high, you never increment.

2:38:16
So that's why the fixed point is not equal to when it's greater than or equal to that. That's a good start at, you know, and and being the kind of initially greater than and nothing happens, but the English Facebook. So, the important sense is that one fixed point is used in place of termination to the fixed point.

2:38:42
Can be computed, syntactically ingenuity. You don't have to depend each others and then we can use it to fix point to deal with situations where we want the program capture, okay? To the three exercises.

2:39:33
Training.

2:39:43
Only. So, this thing So that I couldn't replace or you can only go home to the market area. So that's kind of here. So basically, thank you.

2:40:22
Okay, you want to time? Probably is really clear? Yes, ever here.

2:40:42
All you is equal to.

2:40:51
That is believe in. Yeah. Okay. Okay, the past. Yeah.