As usual, when you start the talk, you start thanking the organizers for inviting you and for organizing so nice a meeting, and I do it soon. Thank you. But I also thank you particularly for the schedule, since during the first two talks this morning, I was happy to see that they were, they mentioned actually they were on the transducers, there were greater dopimeter, there were monadic second-order logic and more or less complicated, sorry, fragments of some logic and there were a lot of carriage traces and of course words. And if you pay attention, then you will find all these popping up in my talk as well, but only in more or less in passing, but all the theory I'm going to explain. This somehow based on the findings of that kind. So I'm going to speak about the theory of the subword order. So just to remind all of us, U is the subword of V, the U resides from V by dropping some of the letters and then we write this less than or equal sign and the other way around V is a super word of U. Here are some examples, V square A V square is the subword of this word that they won't read since you can from that word drop the crossed out letters and you end up with the left one. And then any word is a subword of itself, you just do not drop anything and the empty word if you drop everything is the subword of everything, so of every word, so it's the least word. And why should we talk about this subword foundation? Well, it has some relevance. It has been used in terms of writing since it's a special form of flexibility path or to prove some termination properties or you can use it in the verification of loss of channel systems and the life. And I would be surprised if you would not have heard about that. Here's just the basic, the first levels of the subword order. I already mentioned that the empty word is the very least one and then you have two words that delta Vg is binary age. Then you have two on the second level and on the third level and that's what I wanted to stress here. You have, for instance, AB and that's above A and above B but the same holds for BA, so you do not have the letters despite the fact that any two words have a common upper bound. Actually every finite set of words has a common upper bound but it's not the letters, it's not the semi-letters. What is known is that it's a well-called order and that's the basic for its use in verification. Well-called order means in particular you do not have infinite anti-chains but they can be out very long. Just look at any level, of course two words of the same length cannot be subword of each other and you have out very many words of the same length. Just choose the length large enough. Now the general question I'm asking what classes of properties are decidable about subword order? And as usual as very often when I did talks this means I consider the relational structure and this relational structure has the universe set of all words over a fixed alphabet A. I have the binary subword relation in the structure and then I have the constant for each and every word. So formulas can refer to particular words. And I also have regular predicates, universal predicates. You can say there is a word X in the language, this and that language, such that blah, blah, blah. So universe, binary subword relation, infinitely many constants and regular predicates, all regular predicates. And then I want to make statements about this structure and of course I consider first order logic. I have the ability to say X is a subword of Y where X and Y both can be variables or constants, they can both be constants and it can be mixed. I can say X belongs to K, then I have Boolean combinations and you can extend the list as usual and I have existential and universal quantification over single elements. So it's classical first order logic about this structure. But as it turns out, first order logic is far too powerful. I have to restrict it and therefore I'm now defining some fragments and then later some extensions. So couple of logics here on the right-hand side. First, sigma 1 as usual, the existential fragment, all the formulas in prenext normal form that only use the existential quantifier. Sigma 2, prenext normal form, couple of existential quantifiers followed by a couple of universal quantifiers and that's it. Then I introduce the logic fo plus mod. Here I add another type of quantifiers that allows me to say there's an even number of nodes having this and that property. Well, even with just the simplest example, p modulo q and p and q are constants there, natural numbers. I also introduce fo k, where k is a natural number and this is all of first order logic but you only have the variables x1 to xk. You cannot use more variables and this makes it very hard to say there are k plus 1 many nodes with this and that property. In some situations this is possible but these are only very, very special situations. For instance, on a linear order, that's all clear. You can do that with two fingers pointing at the nodes but in general you can't. So we lose quite a lot by restricting the quantifiers to, sorry, the variables to just k many. That can be reused but we only have these names and to make up for this loss of expressivity we add another quantifier, a threshold counting quantifier. I allow to say there are at least n many nodes with one property. So you only need one variable but it will be instantiated say n times and the same property will be checked for all of them. The list isn't finished yet. We have c plus mod q, a k, sorry, and now you know the recipe. We have k variable names. We have threshold counting quantifiers. That's why we have the c here and we have modulo counting quantifiers. That's why we call it mod k. So sigma 1, sigma 2, the usual quantifier alternation fragments f o plus mod, bounded number of variables, threshold counting quantifiers and then mixtures of all this. What is known? So first result, the sigma 1 theory of the partial order alone is decidable. So I drop the constants. The formula cannot mention the constants. It cannot mention the regular predicates. It's just the partial order. So this is admittedly a weak result. Karantyka and Schnabelang showed that the fo2 theory is decidable even in the presence of regular predicates. So two variable names. You can alternate quantifiers as you wish but you have only two names. These are the positive results and then despite looking weak it turns out that they are close to undecidability since here sigma 1 theory of the order alone was decidable but if you allow constants in your formulas you get undecidability and constants, of course, are a special case of regular predicates. Just use regular languages. So this is undecidable and if you go from sigma 1 to sigma 2 the order alone gives an undecidable theory. So this is really kind of the maximal thing you can hope for and here fo2 theory, two variable names is decidable if you allow a third one you get undecidability even without any called as syntactic sugar constants and regular predicates. So the subword order that we are all more or less familiar with has complicated properties. It's complicated to determine these properties. What we tried to do with Georg Setscher and we succeeded to some extent was to investigate what happens if we restrict the universe. We do not allow all the words but only the words from one particular language. And of course let's make it trivial. No, not as trivial as the finite language but say a language that's just a chain. One letter iterated. Then you have the natural numbers and it's not trivial but we all know what's happening. So if we have a more complicated language what is happening then and I will present two constructing results and two generalizations of these four. And I could ask now where you expect a generalization and where you expect a contrasting result. I'll make this clear in the talk. So let's first consider the theory of a language with a separate order and all regular predicates. Then our result, our basic result is the following. If the language L is context-free and bounded. And bounded means a couple of copies of W1 and then a couple of copies of W2, etc. for a fixed sequence of k words. So such a context-free language. In that case the strongest logic I considered here the FO plus mod theory, sorry, becomes decidable. And the proof strategy is as follows. We will do an first order interpretation in Pressburger arithmetic. So we will translate the formula talking about this sub-word order into a formula talking about the tuples of natural numbers and using addition only. And phrase differently, what I need is a function that associates a word with every k-tuple of natural numbers such that at least all the words from the language can appear that way, belong to the image of this function g. And not only this but in addition I need formulas that express a property of a tuple of natural numbers which property shall this be, the property that the image under g belongs to the language k for every regular language k. And sorry, also for the language L. And then of course we also need the corresponding result a formula in Pressburger arithmetic with three tablets of variables expressing that the images are sub-words of each other. Now we need these formulas, not really, since we know that definable in Pressburger arithmetic is the same as semilinear. What we need is that certain sets are semilinear namely if you take the function g and take the pre-image of the language k then this shall be a semilinear set and the same shall hold for the sub-word order. If you have this then you get decidability. Now there's essentially only one idea for a function g in this context. You take a k-tuple of natural numbers and this gives you the powers of w1, 2, etc. that will result in the word. So I couldn't make up any other idea. I'm sorry, we will also need a couple of other functions here. First an alphabet that has k elements, gamma 1 to gamma k and then a monorethromomorphism that maps from gamma star to A star and it takes the letter gamma i and maps this to the word wi up here. So it's in a sense very similar to this mapping but now from one free monoid to the other. And then the parix monorethromomorphism that counts the number of occurrences of a letter and we need it on gamma star. So here we have the functions again. That's A star. Here we have the k-tuples of natural numbers. Then we have the gamma star and while here is g that maps m to w1 to the m1, etc. We have here the mapping f that maps gamma i to wi monorethromomorphism. Here we have an identity. This is not a monoid, just a language. And here we will use the parix image. And that's why the answer is not immediately clear to me since we do not use the parix image there but at a very different position. It doesn't matter. It might still be possible. Now the first thing I wanted to prove that if k is context free then the pre-image of k energy is effectively a semi-linear and here is essentially the proof k lives in A star and it's context free. If it's context free there and here we have a monorethromomorphism then its pre-image called k1 here is effectively context free. Now here I have the identity and of course if I want to move k1 here I will take the intersection and therefore it's important that this language is regular and we all know intersection of regular and context free language is context free and that's k2. And now I can apply the parix image and get that psi of k2 is effectively semi-linear and what I did was I moved k on this way over here. And having done that I checked that this is precisely the set I was interested in. This is precisely G inverse of k, the pre-image of k and we are done. This is for each and every context free language. Now we wanted to have a similar property for the subword order. Subword order doesn't live in A star but in A star squared. So we have to square each and every object in this diagram and then the claim is more or less the same. If you start with the subword order here and you move it back here you get an effectively semi-linear set and why is that the case? You start here again and you are used that the subword order is rational. If this is rational then its pre-image under a homomorphism is rational the same here with, yeah, intersection with a rational relation wouldn't work but this is not only a rational relation it's a direct product of two regular languages and therefore you can do this intersection here and then you use Peric image and you get a rational or in other words semi-linear set up there and therefore and then you prove that this is really what you wanted to have. So essentially the same proof but two dimensional. So what we get is for any words w1 to k and any context-free language that's bounded the fo plus mod theory with regular predicates is decidable and not only decidable but even in elementary time and the proof is as follows the two claims that I just sketched provide an first-order interpretation of the structure we are interested in in the natural numbers with addition and that allows you to translate any fo plus mod formula that talks about L into an fo plus mod formula that talks about the natural numbers and this is a dangerous moment since we all, I guess most of you remember in presbygary arithmetic I can easily say a number is even by just saying there is something such as doubling it gives the original one but that's not the mod we use here. The mod we use here is there's an even number of witnesses for some property. It's a completely different concept so this is extremely difficult. No, it's not. And we were able to prove together with Peter Habermehl that also this fo plus mod theory is decidable and the complexity doesn't increase so it's the same complexity as for presbygary arithmetic. This was the first result. We have the results on A star and here we had the undecidability for small fragments of first-order logic and if the language is extremely nice, bounded and context free then you can even add the regular predicates you can even add modular count and quantifiers and get decidability. Clearly, it is out that I would classify as construct, construct. Is it the case that you're saying that to push out a few, let's look at the actual numbers but you're saying that the specific kinds of fo plus mod sentences that you're getting under the information that you have is that specific sub-theory of the fo plus mod theory of number plus plus plus plus is that decidable? But what about the general fo plus mod theory of number plus? What about fo plus mod theory of mass number respect to the mass? Natural number respect addition? Yeah, that's precisely what I... No, it's decidable in general. So it was the result completely independent. We didn't know anything about a separate order at that time. Which is not quite true but we didn't think about it at that moment. Now, in the next couple of slides, I'm going to generalize this result here where I will consider an arbitrary regular language for a star. So the sigma one theory of a language L under separate order, the theorem as I said, if L is regular, then the sigma one theory is... of the order alone is decidable. And the proof idea, we distinguish two cases. The language L could be bounded. Regular and bounded, well, then it's context free and bounded, then the whole first order theory is decidable, even with modular... So this is done. The second case, language is not bounded, but still is actually long. Then I only want to decide the first order theory. Sorry, the extension theory. So I have a statement of the form. There are five nodes that are ordered like this. Or like that, or like that. That's the formula. And of course, this junction can be taken out, so all you need is to be able to check whether a particular finite partial order embeds into the... order at hand. That's all that's needed to be decided. And in order to prove it, we had to find some results that we didn't find in literature. And the first one is if L is regular, then there are words W, Z, V and X. They are non-empty. V and Z have the same length. And W, Z, V, star, X is a subset of L. Actually, this is a moment... Yeah. Where I have to tell you something, it just occurs to me. Some 15, 20 years ago or so, I worked together with him, who shall not be named in this occasion. And I learned a lot from this cooperation. And one thing, and I'm telling it my students regularly, one thing I learned was first make a proof that's important, and then go over it again and think about the names of variables. The first things should be small letters, and then there should increase. Never say, let N be a natural number, then there is a natural number M, since that's before it in the alphabet. So there are words X, U, V and W. U and V have the same length. And X, U, V, star, Y is a subset of L. And this is not new. This is known now that I have deciphered it. And the word U, V is primitive. So it says every finite automaton, deterministic finite automaton has a state with two loops, distinct loops, and if you go through both of them, then you get a primitive word. Okay, that's one thing. And why do we need this primitive loop? So let N be large enough. P is some natural number, your favorite one.  If you do so, then you have a certain embedding of partial orders. This is the P-dimensional cube, the 0, 1 vectors of length, and ordered component-wise, P-dimensional cube. And this here is the subword order. And what is the language? You have P copies of N copies of U, V of the primitive word. So a primitive word copied a lot. And you prefixes either with epsilon or with V. Of course, epsilon stands for 0, V stands for 1. And since you have P many 0s and 1s, you repeat this word P times.  What is complicated is the other way around. That if you take two vectors and map them in the obvious way, then you do not map incomparable ones to comparable ones. And that's where we need primitivity and we also need that many iterations here. And the whole proof is purely word combinatoric. And we learned today that the combinatorics on words are sometimes too complicated. You shouldn't go into the details there. At least I use this as an excuse. Now, this language here, ordered by a subword order, embeds trivially into L since any of the words here belongs to UV star and you prefixes with X and you suffixes with Y. And this is, of course, an embedding. So that's clear. And now all finite partial orders embed into L. I only embedded the P-dimensional cube, but just a second. But of course, if you now come across finite partial orders with P elements, say, then you can embed it into the cube and the cube into the language. And that's the end of the proof. Anka. Maybe I missed something, but L is on one letter. So we have to get this unary. If the alphabet is unary, yes, that's a case I missed out. But if L is unary. Sorry, if the alphabet is unary. Then it's not true that you find the A. Yeah. But the result still holds since the partial order, regular infinite language is the national number. You are right. I should have at some point said that an alphabet is at least two elements. Yeah, right. Yeah, you are right. But Anka was stressing this. So the theory is correct and the case distinction has to be taken with care. Now, if L is regular, then the sigma one theory of this language L is decidable since you can decide whether a given partial or finite partial order embeds. Actually, every does. Now, the sigma one theory of a language together with constants. I go back. Looks like this. A star, subword and constants. And in general with the whole universe, it's undecidable. And I don't know how to generalize that. So let's consider very particular languages. Let L be regular with the following property. If you have a pumpable word, so x, u star, v, y is a subset of L. If you have a loop in the automaton, then this loop contains each and every letter. Every loop in the automaton contains every letter. That's the property. And then we can prove that the sigma one theory is decidable. Of course, this is not true for a star since you have just one state and you loop with very short loops. But if L is nice, then you get decidability. And the proof idea is very similar to the previous one. If you make a case distinction, either L is bounded or it's not bounded. Well, we have settled that case once forever. Constants can be considered as single irregular languages. So that's okay. Now what if L is not bounded, then we need some technical results. The first one is any sigma one sentence. Any existential sentence is equivalent over this structure to a disjunction over a block of existential quantifiers, conjunction, and then some statements that xi is above wi and psi doesn't contain quantifiers or constants. There is one type of many of atomic formulas missing, namely x is below w. We can only say x is above w in these formulas. And that's the main thing here. We have here only statements x is a supervert of w and it's also not allowed to negate them or not necessarily, let's put it that way. And this normal form only works under this severe restriction on the language. It doesn't hold in general. Having proved this, we show that if p is a finite partial order and w any word, then this partial order embeds into our partial order above w. And that means take w to be the concatenation of all the words wi, then you find p above them and of course this means that all the nodes of the image of p are above wi. So that's all you have to do. And again, also in this second step, you need the particular property of the regular language. It doesn't hold in general for all languages. Now here, if the universe is all words, then this Sigma 1 theory with constants is undecidable. If it is a regular language with, we call it frequent letters, then since, well, whenever you see an a, then in a finite distance you will see another a or you are close to the end of the word. Then if you have such a regular language, the theory becomes a decidable. There's one cell still empty. The fo2 theory with regular predicates is decidable. I want to generalize this and I have no hope to add a new variable since that would give undecidability. I even consider c plus mod. So I have these fancy quantifiers, but only two variable names. So variables x and y, all the quantifiers I ever mentioned in this talk, threshold counting and modular counting. And then the theorem says that the c plus mod 2 theory with regular predicates has effective quantifier elimination. So first remark, so far the new results were always talking about some language L here. Now I'm going to the general case again, but that's not really a restriction since you could just restrict every quantifier to the language L. If L is regular, then that's a predicate and therefore you could also put here any regular language. So to make it simple, we use the full universe. And effective quantifier elimination just says you can rewrite each and every formula into an equivalent one that doesn't have any quantifiers. Unfortunately, this quantifier elimination procedure is non-elementary, but it immediately gives decidability. If you have a quantifier free formula, then it mentions only constants and of course you can decide whether this word is a subword of that word. So you get decidability, but it's not particularly fast. Proof idea, well quantifier elimination as usual by structural induction over the formula and there's not much to be said if you have a disjunction or an atomic formula. The crucial step is if you have a formula that starts with a quantifier and I use this Q here since I have these fancy quantifiers and psi is a Boolean combination. And here it is important that we have only two variables, X and Y, so psi mentions at most X and Y and therefore you can only have the formulas X below Y, Y below X. X is in the regular language or Y is in the regular language. These are the only four types that can appear in the Boolean combination. So we have this formula phi, let's go back one slide. It was a quantifier followed by a Boolean combination. Now this is phi and the quantifier can count there are at least five elements that are red or blue is the same as saying there are two red and three blue or one red and four blue, etc. That's what I mean by basic arithmetic. The Morgan laws, there's no need to explain that and what you get is phi is effectively equivalent to a Boolean combination of formulas X belongs to K or there is a certain number of elements of K that are proper sub words of Y proper sub words of Y or incomparable with Y. So you are down to these four cases. And then you look into the literature on you recall the literature on regular languages, recall K is regular and you immediately remember that for any regular language K the set of all proper sub words is effectively regular. Just take the automaton and play around with it a bit. And the same holds for super words and if you want to do not want to explain it like take the automaton and play around with it but if you want to sound more scientific then you say the reason is that the sub word relation, the proper sub word relation is a rational reduction and you have the image of K under this rational relation. But then we hear this settles the second and third case and the fourth one is incomparability. Well rational relations are not closed under negation, complementation, and not closed under intersection. So you really have to think about it for a moment or two or you look into the paper by Karen Decaun and Schnigelin and they will explain to you why also incomparability under the sub word relation is a rational relation. The basic idea is that, well the first fear is that you have to check two properties at the same time. The first one is not a sub word of the second and vice versa. But the basic idea is that if X is shorter than Y then Y cannot be a sub word of X and that helps a lot and essentially is the basis for this result. Okay, this settles the case if Q here is the existential quantifier. So then we have upward, downward closure and incomparability set. But now what about counting things? There are at least two super words. And here the theory of weighted automata comes in handy and with weighted automata you can do threshold counting just take natural numbers with addition and multiplication and to have a finite semi-ring cut it off at the threshold. Plus one. But in order to use it we need that the sub word order is not only rational since rational you could have two paths but it's even unambiguously rational. You can produce a transducer that has only one accepting run for a pair of word and sub word and the same holds for the incomparability relation. And then you plug it all together and you get the result and therefore the formula phi that we started with quantifier followed by some Boolean combination is effectively equivalent to some formula X in K for a certain regular language K that you can compute. And this finishes the quantifier elimination. The FO theory, FO2 theory of A star with regular predicates is decidable and the same holds with all the possible counting quantifiers. I can talk about complexity. It is not, well if you recall the proof I sketched here the center was every partial order embeds anyway. So all you need given the sigma one sentence all you need to verify is whether there is a finite partial order having this property and the size is this number of variables. And so it's an NP you just guess a finite partial order of the right side and you check. That is also NP complete is not far more difficult. Yeah. This was despite the fact the proof being more complicated at the end it's again every finite partial order embeds sufficiently often. This was the very first result reduction to Pressburger arithmetic which is elementary and therefore this proof is elementary and the proof with quantifier elimination I sketched. Yeah of course I transformed the formula into that's disjunctive normal form whenever you do that you get a non elementary bounds but we don't know a lower bound. So the fo2 theory with regular predicates seems to be non elementary what if you restrict to constants to variable names and constants and suffered order of course. And there's a result published this year by Karen DeKar in general that says well actually it appears in the journal version a couple of years older every fo2 formula is effectively equivalent to some quantifier free formula we already saw this but now you can bound the length of the constants and the constants get well at most doubly exponential sounds terrible but it isn't we started with non elementary. So you do the quantifier elimination and you end up with short constants. Double exponential constants means you have doubly exponential many elementary quantifiers sorry atomic formulas you have four-fold exponential many the formula can have four-fold exponential sounds and this is only if you take care of how to write it it could also explode even more if you are not careful in doing the elimination. So anyway how do we get these short ones? We do again a quantifier elimination but now we do not have regular predicates but we have the constants that we can use and the basic thing is if you have a threshold quantifier with quantifier psi quantifier free and constants of length say at most n then you can build an equivalent quantifier free formula with constants of length polynomial in n. So the quantifier elimination when you have constants but not regular predicates every step gives a polynomial increase of the length of the constants. Now the formula psi yeah to explain it a bit more so the formula psi here this one that is a Boolean combination is a Boolean combination of formulas x below y y below x x below w or the other way around where the word w has length below n and the same with y these are the possible atomic formulas in psi now let's try to get rid of some of them first one a formula of the form x is the subword of w w is a constant that can be expressed as there is some subword, this junction there are only finitely many anyway subwords of w and x is one of them yeah now x is the same as v is not allowed in our logic so we have to get rid of this formula again what we do is we say v is a subword of x and no longer word is a subword of x that means it's the same as saying x has the same length as v and therefore it equals a stupid question, why do you know what it is that is going to write v subword of x and x subword of v since then you have this formula again so we introduced it we introduced formulas x equals v in particular for v equals w so we have x equals w and now you propose to replace it by x below w and w below x we could have saved a lot of time okay, this allows us to get rid of these two atomic formulas there's no expression about super words but only about subwords constants, yeah now again the Morgan laws basic arithmetic, so the usual machinery the formula that exists at least T many y satisfying psi is can be written as a Boolean combination of formulas of the form w is a subword of x and there are at least as many words that are proper subwords super words of x and you have a Boolean combination of statements of w is below x sorry, w is below y that's all that's left and the w's here all have lengths at most n now I want to get rid of this and what I do there is I take a set of short words w and I consider the set of all those words whose that all have a subword from w every word of capital w is a subword of x and x doesn't have other short subwords and short meaning at most n this is a language and since w capital w is finite it's a regular language and it allows us again some usual messaging of formulas to get rid of the Boolean combinations and just say y belongs to Lw and the same up here w is a subword of x this junction of formulas x belongs to Lw is this any better? yes, it is since Karen Deca and Chanel Belang showed you can read their results as follows let w be such a set of finite words the following languages are quantifier-free definable with constants of length n to the 2a and without formulas of the form x is a subword of w they are not interesting anyway this is the set of all words that have some superword in Lw some subword and some incomparable word we already knew these languages are regular but here the result is stronger they are not only regular but they are definable in terms of existing and non-existing subwords and such a language is called piecewise testable and the language that Lw defined was defined by saying these words are subwords and these are not so they are also piecewise testable and the two authors used the theory of piecewise testable languages and extended it considerably and then got this result in their paper you will not read find this theorem stated like this but in the language of logic it is precisely this now this is the existential quantifier but we also have the threshold counting quantifier and this is the work I am doing together with my student Schwartz essentially the same result holds for the threshold counting quantifier the only difference is that the threshold here it of course has some influence on the length of the constants and they grow moderately now what you get is every C2 formula with constants is equivalent to some quantifier free formula with constants of double exponential length and without atomic formulas of the form X is a subword of W then you look again into this very nice paper and you see a result that I find surprising fix your favorite M and then take a word W and you want to make it short without changing the set of subwords of length at most M if M is too say and you have three consecutive A's in your word then you can safely drop one you make it short so can we do this in general? recall that there are A to the M many words of length at most M so if at all then I would have hope to shorten it to A to the M but they did it the other way around they showed that every word has a subword of length polynomial in M that has the very same subwords of length at most M so without losing any subword of length M you can shorten the word up to length M polynomial in M okay? and then let phi of X just one free variable be a quantifier free formula with constants of length at most M the set of witnesses for phi can be accepted by some DFA of size to the M to the constant so any such formula has a small automaton now this M of course comes from this theorem it was doubly exponential so what they get is the C2 and what we also get is the C2 theory can be decided in three-fold exponential space and if you are more careful then you see there's this uniform in A you just build the automaton and you always squeeze it and you are a bit careful anyway it works in three-fold exponential space optimal but we can even do a bit better let's go back so I go back to theorems we know that we can build a quantifier free formula with short constants and we know that every word has a small subword short subword of the same and then the theory by Ferranter and Rakov tells us that well if you have encountered a quantifier there exists a word X and what's coming behind it says this X has some relation to Y and it's a super word of something or not then you can also use a short word as witness therefore we can restrict quantification to words of doubly exponential length if you have one witness you also find a shorter one you're not in the counting part it also works for the counting and this is then the result the C2 theory with constants can be decided in doubly exponential space so we save one exponent by not building the automaton but restricting the quantification to more or less short words and this is just to see that it's really a contrasting result sigma one theory of AB star with constants is undecidable here we have only two variables so it's completely different if we have three variables we have undecidability and if we have regular predicates then we only know a non-elementary procedure I talked about complexity we have here this non-elementary complexity and what's new now is that the F02 or the C2 theory is decided in elementary space how much, well I know everybody every speaker has to ask how much time do I have doubly exponential, no I can't talk clearly it's as much as the others let me just show off with a final result allow me to do that I won't talk about the proof I haven't prepared anyway and actually I promised to mention traces so allow me to keep my promise mother cabbage traces there's an obvious definition of what a sub-trace is there's an obvious question which of these positive results transferred to mother cabbage traces and I'm only talking about the decidability of the C2 theory with regular predicates M is the set of all mother cabbage traces here and, well, there are some reasons for optimism first, well, many results on words generalize to traces and if you want to look up some of them you look into this book we have a good understanding of what a regular set of traces is that's particularly important here since we have regular predicates and we should be better understand them well and if we have this counting quantifier then we also need some counting and recall I used weighted automaton so we would also need, if for words we would also need them for mother cabbage traces and also this exists we understand that pretty well so it's clear that it works now there's this other ingredient in the proof of rational relations subword order is a rational relation and you can define what rationality is what rational relation between trace monoids is but it doesn't preserve regularity or recognizability forget about it it's a very good reason to be pessimistic anyway, what can we do and here's the idea for the solution instead of regular languages and rational relations what I use is internal logical descriptions and interpretations so all the time I'm talking about logic but I'm talking about external properties this trace is a sub-trace of that one and now I'm considering, as Anker did a trace as a graph and I'm talking about the internal structure of the graph as we do with monadic Saint-Dollar logic in other words we translate external formulas we talk about a sub-trace order and two internal ones for monadic Saint-Dollar logic they talk about the nodes in a graph in a trace and the theory is from a C2 formula with one free variable one can construct an MSO formula such that for all traces we have to following the set of traces with regular predicates satisfies the external property so the trace T has this and that property with respect to its sub and super traces if and only if internally it has the property psi okay and since given such a formula psi we can decide whether there's a trace T having we get that the C2 theory of the sub-trace order with regular predicates is decidable as well I better finish since I haven't prepared more what's open is well we have a very particular form of regular language frequent letters such that the sigma one theory with constants gets decidable and we have a very nice regular language a star where it's undecidable it's I have no clue where the border is between decidability and undecidability not even an idea where to look yeah we do have a non-elementary upper bound for the complexity of the C plus mod 2 theory with regular predicates with constants it was simple with regular predicates we don't simply don't know and I transferred one result from the word case to my search cases and as you saw on my tables there are a couple of more and if you don't remember them then here is the table again thank you very much thank you


Hello, I'm Jack Herrick, and my life's mission is to give every single person on the planet a free, practical education. So I'm doing that via a project called WikiHow. And for those who've been in WikiHow, who've never been in WikiHow, it's a how-to website which publishes hundreds of thousands of guides with simple step-by-step instructions on how to do pretty much anything. So to prepare for today, I read this article on how to give a speech. You probably can't read from the back, but it basically says that public speaking is more scary than death. But if I follow the ten steps, I would survive. So if after five minutes I'm still here, you'll know WikiHow works. So 13 years ago, fellow EHF fellow Josh Hanna and I had a problem. We wanted to start WikiHow and we wanted to focus the company entirely on global impact, more than profit. And because we were not going to focus the company on profit, we couldn't successfully raise venture capital money, which is the normal kind of Silicon Valley model of starting a business. Meanwhile, all of our competitors took the opposite strategy, and they raised gobs of money. In fact, there was 15 different companies that each raised more than $10 million each. Collectively, these 15 companies raised an astounding $1 billion. We had zero dollars. And I got to admit, it looked like we were not going to make it. But fast forward 13 years later, take those same 15 companies, chart them by audience size that we're now number three on this list of 15. So how is this Cinderella story even possible? Well, it turns out we had four values that made our success possible. And in the time I've spent in New Zealand, I've discovered that Kiwis share these values and Kiwi businesses, many Kiwi businesses also share these values. So I love to talk to you about them. Number one is purpose. WikiHow's purpose is really all about global impact. That is clear in every decision we make at the company. And let me give you a few examples of that. Number one is all of our software is open source software. You can take all the software we've built over 13 years, download it, use it yourself, start your own company, start your own WikiHow competitor, whatever you want to do with it. Two, all of our content is Creative Commons license content. Three, we've translated WikiHow into 17 different languages, including many languages that we knew would never create a profit. And four, we've also figured out ways to distribute WikiHow to the millions of people around the world who cannot afford internet access. WikiHow value number two, people. So when you run, it turns out all employees want to work for a company that has a noble purpose. And as a result, WikiHow has been lucky enough to track the very best talent in Silicon Valley. I've started four companies, and this one, without any funding, has the best team of any of the companies I've ever worked with. I'd like to point out one other thing about our team. WikiHow, sorry, EHF fellow Tracy Chow has done some amazing work pointing out, showing to the world that Silicon Valley is incredibly unequal in terms of gender balance. WikiHow has, on the other hand, a gender balance team. WikiHow value number three, perseverance. Our goal has always been to educate every single person on the planet and to take as long as it takes to do that. So we think we're pretty much going to be here forever. As a result, we make very long-term decisions. And it shouldn't be a surprise that when you make long-term decisions, they tend to pay off in the long term. So an example of a decision is thinking about our stewardship of this planet. Ten years ago, WikiHow became the largest website to become an entirely carbon neutral company. And I'm proud to say we're still doing that. And many, many other web publishers have since followed that. Value number four, paced growth. We reject the idea of growth at all costs.  And I'm happy to say that most of them have ended up pretty much just going home. So 13 years in, WikiHow now serves 200 million people a month. We're very, very proud of that. But we're also very aware of the fact that we're still leaving 97% of the planet unserved. With the time I'm going to spend in New Zealand, I'm going to reinvest in the four values I talked about and hope that together we can find a way to serve the remaining 97%. Thank you.


So, good morning everyone. My name is Jitain Prachapathy, I am an architect and I am faculty from Academy of Architecture. I am going to talk about context sensitive approach to sustainable building design. So, we will be talking about context, the approach to sustainable building design and why sensitive or how sensitive. Now, the sustainable design is with respect to or with reference to architecture. The contents of this lecture include the need for sustainable design and context based approach. This will be followed by case studies to illustrate the approach and the intent is to encourage students and professionals to design better. If you see in this slide, there is a old saying which says that we have not inherited the world from our forefathers, but have borrowed it from our children. So, we did to protect the environment so that our future generations can be taken care of and we cannot keep on utilizing or consuming resources at the rate at which we are doing. This professor Monika Jain, she so put it well that we are actually consuming a lot of resources is not it and the resources are actually finite in nature. So, we need to now be more sustainable, we need to conserve our resources and this can be done by adopting sustainable building techniques. So, judicious planning can provide a better environment, prosperity and good health. Vernacular architecture or traditional architecture evolved in response to environment, economy, social and technological context. This resulted in a regional flavor or language of architecture. Nature architecture evolved based on the context, whereas present day architecture is largely influenced by air conditioning and artificial lighting. This has been driven by the industrial revolution. What has happened is that now we no longer depend on nature or the context there is a disconnect with nature is not it. We do not need to design our buildings based on the climate where it is located, based on the technologies available, social needs. You find the same type of building being built everywhere all over the world because we have access to good technology. So, what is sustainable design? Can we learn from vernacular architecture and adopt it in today's context? Then we will link with tradition to and link it to our requirements today. Our requirements have changed from before, our comfort standards have enhanced, our needs have increased. So, we need to link the two together and what we can do is we can create a new and unique identity in our architecture or our building design. So, here we see a building by architect Ashok Lal and see what is done is he is used an innovative shading technique is also used photovoltaic solar panels over the roof over the courtyard. And it looks nice, so sustainable architecture can use past experience, but in a new manner and you can become innovative and it can look nice also. So, what we can do is we can create a new and unique identity by marrying the old traditions with the new technology that is available with us. This is a very nice definition of sustainable design by the Rocky Mountain Institute. I will not go into it because Professor Jain has already talked in depth about the need for sustainable development. But what we can do is you see the first picture here that is what she was talking about urban there is a rapid need for urban development and we are falling short we have nice high rises which are surrounded by urban squalor it is called slums, isn't it? So, can we make something which looks nice, beautiful and it is environmentally conscious also that is the goal. So, that was the context and now how can we approach the problem, what is the approach? This is what we do or we follow we do the preliminary analysis which includes studying the climate, the microclimate, what Professor Jain elaborated on, we study the site conditions and also the comfort requirements. Would a person comfortable in Europe or America feel the same level of comfort if he comes down to Mumbai or to Rajasthan, no no it is very different they will not be comfortable here. Similarly, if we go to Europe we will not feel comfortable, we will feel cold there ok. So, we need to know the comfort requirements also. Then we try to adopt passive solar architecture, passive solar architecture is using natural means to attain comfort and to reduce energy conservation. It is how do you use the sunlight, the wind, the materials, your design itself to achieve comfort ok. Typically, it uses these are the things that you can use landscaping, orientation of the building, building envelope like Professor Jain said, the materials you can change, techniques these are advanced techniques, simple techniques are shading, color etcetera. Advanced techniques like radiant cooling, passive down roughed evaporative cooling, chrome walls, induced ventilation etcetera they can also be employed ok. We look at daylighting also, because daylighting is free in India is not it sunlight is free and abundantly available, so we should use that. All this can be you know you can analyze all this by using softwares called simulation softwares which Professor Naik will be talking about in the next lecture ok. What this software do is they help in designing better, they can help you to evaluate two different hypothesis or building. The next step is to integrate alternative technologies into the building or site design. This include renewable energy, it includes water and waste management, it includes building management systems, low cost or embodied energy of materials also. Lastly, what one can do is you can validate your design is not it. Once it is built you can go and measure it. Before it is built you can go for a peer review, even after it is built you can send it to papers or get it reviewed by in journals ok. And lastly you can do a post occupancy evaluation. What is post occupancy evaluation? You go to the building after it is built and you go and ask the people who are using it. Is it now working as per your requirements? Any building that is built is built for the users is not it? Buildings are built for the users, so you should make sure that they are happy. This slide shows the type of analysis that can be done ok. This is a hand based tool called the bio climatic chart which you can use to analyze the climate and also find out the comfort requirements in a particular region ok. The next picture is a chart generated by a software called climate consultant. It analyzes the climate and it can give you various passive techniques which will help you to achieve comfort in a given area ok, in a given climate. This is developed by the University of California Los Angeles software is climate consultant free of cost you can use it download it and use. You can then analyze the micro climate. What are the conditions at site? Does it have trees which can help to shade, where is the wind coming from, how is the sun moving in the sky? You can orient your buildings accordingly, take advantage of topography of the site, self shading. So, many things can be done if you could do the micro climatic analysis ok. Lastly, the next picture is zoning where you can you know zoning helps you to integrate your other aspects of environment with your the functional aspects of your building and site zoning helps in that ok. For example, do you want to give pedestrian access only to your site or do you want vehicular access throughout the site? How does it help or not help? If you have vehicular access throughout the site, it will add to the pollution is not it. If you restrict vehicular access, you are reducing pollution. So, you can work on certain things like that ok zoning helps to do that. This is how you the building envelope or the building form can evolve by using this techniques ok. You can start out with a T and then you say ok this is working fine, but can there be a different arrangement and in the end you get something like this ok which looks at the wind pattern as well as the sunlight ok orientation. You can look at low cost or alternative construction technologies also. What happens if you use another type of material? For example, instead of concrete brick is cheaper or is instead of brick you can find soil stabilized mud blocks are cheaper ok. So, you can look at that and typically you can get about 15 to 20 percent saving by using different types of materials. This shows how renewable energy is incorporated in the site, rooftop, solar streetlights, rainfall harvesting, biogas plant. So many things are there which can help to make your site more sustainable ok. You can take advantage of simulation software like radiance to do the daylight analysis of a particular room. You can find out whether the light is enough or less, whether there are glare conditions what can you do to improve it. Can you change the color that means the reflectivity of the walls? Can you change the type of glass in the room? Can you add a light shelf to increase the depth of the day lighting ok. Many things are you can use. These are the passive technologies that can be adopted. You have cross ventilation, you have courtyard effect which acts as a heat sink, you have filler slabs, you have ventilated roofs, you have light shells here is not it. You can incorporate rainwater harvesting in your section of the building also ok. Now, we used all these technologies in a building which was built in a very backward area of India in a place called Bikan Gau and this was used in a school ok. The school was low cost, I will just show you the picture of that. So, this were actually the we have done this analysis for a particular building ok and that building is this ok. This is the education park at Bikan Gau in Madhya Pradesh in a very backward area of India very poor it experiences about 16 to 18 hours of load shedding a day. So, we had two things first of all we could not go for air conditioning not possible because load shedding is not it and in a very poor area charity based project. So, we could not make it a high 5 building also is not it. So, that was the context can you use air conditioning in that area in a rural area no. Can you make it can you use very very expensive material there no because the resources were not available is not it. This building was built by local contractors at a cheaper rate than conventional buildings in that area and also on time this building was built in 9 months ok. It is probably the first zero energy building in India in school ok in school campus planning. So, what you see here is the solar panels on top of the roof you see the light shelf you see windows that promote light that promote ventilation as well as provide glare free daylight you see the walls they are not plastered to save money ok. And what you see that is that although it is sustainable it is low cost it is in a rural area built by local people still it looks nice no. So, sustainable architecture or design or context based design should not be looked as you know you should not get scared by it, but you should think that is it is an opportunity to design better is not it. So, we will go to the next part which is now in urban context ok. This was for a rural context no air conditioning, but suppose someone some client comes to you and says oh I want to make a corporate office in Mumbai which is fully air conditioned I want to project a corporate image would you say no no I just do sustainable design. So, I will not do your work you cannot do that no. So, you will take up the project and you say ok let me see how I can optimize the building then ok and then you go ahead. So, typically as a professor Jane said because of air conditioning being widely available technological progress that we have now we have buildings which are built like this all over the world. The same type of building you will find lot of glass no shading devices irrespective of climate you will find this type of buildings all over the world. What happens to such type of buildings? You have to make them air conditioned it is 100 percent requirement.  So, it has to be then 100 percent air conditioned and there is a big impact on your energy builds ok. We did a small study sometime back a few years back in fact with Professor Dayak and we found that such a some similar buildings like this their energy requirement is so huge it can run into lakhs of rupees ok. So, what you can do is you can start by adopting very very small simple technologies which will not cost much ok. Things like orientation things like color things like your chajas ok shading devices that you can incorporate into the building and it will still give you a lot of significant improvement it will optimize your building ok. We did some simulation studies by using this simple techniques how much can you save just by using simple things which can be done in any building you can save typically about 16 to 20 percent of your cooling loads huge impact consider 15 to 20 percent of say 30 lakhs a month it is a huge saving ok. So, we use simulation simulation software for that ok. In this we used software called transys Professor Dayak helped in that. This shows some more results that can be obtained from simulation you can do a parametric analysis it is what if analysis what which type of glass is based which type of wall is based which type of color is based what happens if you use shading or no shading. You can do that type of analysis you can get results say the monthly cooling loads you can find out during which period your maximum energy requirement is you can do that. You can also find out from which part of your building most of the heat is coming from is it from the internal gains is it from the light and people are inside or is it coming from the building envelope. So, this is a building that we designed based on the context based on simulation and this is what we came up with this is a IT building in Mumbai and we were targeting it for lead gold ok. We used the lead guidelines to achieve a sustainable design here. This building won a national award in 2008 IAD awards we were the first runners up. Now if you see in this building you see large terraces right they help to shade the glass and the wall area. You see that it is not all glass you see this vertical things this verticals they are vertical shading devices they are called fins ok. They help to reduce the heat gain from a particular direction so these are shading devices the terraces are horizontal shading devices the fins are vertical shading devices. Glass area is reduced the type of glass is different we used reflective coated glass we reduced the size of the glass we used it only where it was necessary. We used a lot of local stone called malage stone available in Bombay ok. So what happens is that you optimize the building you can optimize the energy requirements by up to 50 percent by adopting passive solar architecture by using simulation ok. Now here also you find that even for a air conditioned building in a rural in a urban environment you can still have a good looking building is not it. So once again you can can you say that sustainable building design does not impose restrictions on the freedom to design it looks good it is functional and it is energy and resource efficient also. So can we conclude that it can be adopted in any place in India or anywhere. So again to sum up with the salient features are what of sustainable building design salient features are passive solar architecture, energy and resource efficient technologies Some tools that you can use are lead and grieha these are guidelines for achieving sustainable design you can go to the website you can download these guidelines they are free of cost go through them and use them in your design. You can use simulation to optimize your design and it is actually very good simulation professor and I will show you. So we use it a lot now. So this slide shows you know this is a passive no not passive this is a renewable photovoltaic panel which is used in the school at Bikkengaum. These are the filler slabs low cost you see it is not plastered we have removed the amount of concrete also. So we reduce the cost by about 20 percent in the slab there and see it is unfinished but still it looks nice. After doing the daylight studies in a software called radiance this is the type of daylighting that you can achieve in the this is in the school this is in one of the halls. So you see it becomes nice it feels comfortable there is no glare the whole room is lit so one should adopt these technologies. What are the benefits for students or young professionals who are going into the profession? You attract discerning clients you know clients are attracted to this type of work now because there is a awareness in everyone that sustainable architecture is required isn't it. So if you are geared towards doing all this type of work you will get better projects isn't it you will get to do more demanding more challenging and better projects. They are aesthetically pleasing green design you can promote corporate and social responsibility through your design and because you are being resource efficient you are being energy efficient you are also maximizing the profits for your clients. So it is a win-win solution for all. So the conclusions that can be made from this presentation is sustainable design is the need of the hour and it has many benefits it should be taken as an opportunity to design better isn't it. Everyone can make a dabba and make it functional isn't it but the challenge here is to also make it look nice also and be rooted in the context of the place where it is being designed. We can learn from vernacular architecture or traditional methods of design for implementing in today's context the context has changed today isn't it we have better access to technology our aspirations have changed so we can take the we can learn from the past but apply it in a new context. We can harness nature and technology to create a new and unique identity we should not look towards the old and try to replicate that only lot of people you know they try to they are hung up about vernacular architecture and they want to do that only today but that may not be the requirement today because our needs have changed isn't it try to what you call it try to develop a new language of architecture isn't it try to develop a new vernacular okay so and of course we have also talked about the expected savings and some issues regarding sustainable building design okay. Now if one wants to go further in this then these are the references that you can look at there are many books and guidelines available there are many organizations and websites these are a few of the scientists and architects working in India in sustainable design and then there are tools tools are available for doing sustainable design you can quantify your design find out which design is better how you can optimize your design that tools like the bio climatic chart you just need to do a Xerox and work on it climate consultant from UCLA website you can download it use it free of cost eQuest is a simulation software for doing thermal analysis again free of cost okay earlier it used to be available for lakhs of rupees okay now it is free of cost you can do your thermal analysis radiance is for doing daylighting again free of cost it does high end it can do what do you call it it can give you rendered images like 3d studio max also okay so it is worth investigating this software also there is another software software like eQuest called energy plus ecotech is there this is a commercial software by AutoCAD ESPR is a software developed by University of Strathclyde in Europe again a very very good software very robust but you need to spend time we use eQuest so I'd like to thank Professor Jane NME ICT Academy of Architecture IIT Bombay Solar Decathlon Education Park initial Shetty consultants okay and especially the organizers of this workshop for giving me the opportunity to present this lecture thank you


Respect can be one of the most important aspects of a relationship, whether it's respecting yourself or others. As defined by Oxford Languages, respect is defined as due regard for the feelings, wishes, rites or traditions of others. If you often feel like you're being used, taken advantage of, ignored or taken less seriously, you may feel like you're not getting any respect these days. Want to know how to command respect like others do? If so, keep watching for six psychologically proven ways to get more respect. Look him dead in the eye. Do you look everywhere but into the eyes of the person you're talking to? Holding someone's gaze is a key way to convey mutual respect. According to psychologist Dr Erin Itoff, looking someone in the eye shows them that you think they are important. In addition, researchers at the University of British Columbia found that eye contact can make you more resistant to tactics of persuasion and influence. This means that you're more likely to stand your own ground rather than fall under the influence of others. The next time you talk with somebody, try to give them some eye contact as they speak. You might feel an increased sense of closeness that will command yourself some respect. Perfection, objection. To command respect, you might think that you need to hide any of your weaknesses or flaws as much as possible and put on a facade. After all, what else can make you seem less worthy of respect and praise than making a mistake? But the reality is often quite the opposite. In 1966, Harvard psychologist Elliot Aronson discovered the Pratfall Effect. This type of bias showed that the people considered superior by others tended to be more likeable or attractive when showing weakness. In one of Aronson's experiments, this weakness took the form of an everyday blunder, such as spilling coffee over oneself. This small mistake humanised people who seemed to be superior, like managers, teachers or parents and thus made them more likeable. Let's be honest. Who doesn't love a good blooper reel at the end of a show or movie? It's kind of nice to know perfect people mess up too, right? Dress to impress. Let's say you're on a first date with somebody at a nice restaurant. Your date comes in and they're wearing a t-shirt, jeans and aunt's bathed. Does this seem like a good first impression to you? What would you think of your date if they came groomed, well-dressed, bathed and put together instead? Probably seems a lot more likeable, right? These are first impressions. They are almost always the first indicator of whether you're like or be liked by someone. While natural looks are out of your control, the way you dress isn't. How you dress can give you the opportunity to change other's impressions of you. Clothes can also be a way to boost confidence and a manner of self-expression that can help you command respect. According to researcher Kim Johnson of the University of Minnesota, our behavior in respect to other people is influenced by the person's dress and the meaning we associate with that dress. While most make the mistake of dressing to blend in with others to avoid being judged, try dressing in a way that makes you stand out with your personal charm. This may include choosing a unique style, wearing clothes that accentuate the beauty of your body's heart and dressing in a way that makes you feel more self-confident. So, if you want to command more respect, try dressing in a way that you think would do so. But don't forget to still be you. Respond, don't react. Have you ever seen a news headline and got immediately angry? Everyone has had a strong feeling before. However, this can be something that causes people to not respect you. According to Mayo Clinic, those who can maintain personal composure during times of stress or excitement are able to be more assertive and often more respected and likable. Being assertive can help boost self-esteem and earn the respect of others. Asserting yourself means upping your confidence and standing your ground without being too aggressive or emotional. Overwhelming feelings can obstruct conflict resolution. Showing others that you're able to be firm and confident while being calm can garner respect. If you're too aggressive, you might seem like a bully that ignores the needs of others and is self-righteous. You don't want to be someone explosive like Bakugo from My Hero Academia, which can get in the way of problem-solving.  Do you know someone who talks on and on and on? When you finally get the chance to speak, do they interrupt you to talk about themselves or ignore what you say and divert the topic back to them? Would you respect someone who doesn't give you respect? Probably not. To create mutual respect, the thoughts and opinions of everybody should be acknowledged. In many circumstances, people often do not concentrate on what is being said. They just listen just to listen. According to the Professor of Cross-Cultural Management in the University of Berlin, Dr. Marie Therese-Clairs, keeping an open mind and listening deeply is a sign of respect. Doing so can make others feel that they and their beliefs are valued and well thought of, which can cause them to reciprocate the respect and attention. You can show you're an active listener by paraphrasing and validating their words or asking relevant questions, which will make them feel heard and understood. Remember that commanding respect always involves giving respect to others too. Sometimes you'll meet some people who simply are unwilling to reciprocate respect, no matter the circumstance. We cannot change others or their actions. In those cases, it might be best to limit how much you're with these types of people. Remember, respect should always be a mutual thing between two people.   We hope you can use some of these tricks to help you command respect in your life. As always, please subscribe to us for more videos like this. Thanks for watching, Psych2Goes!


Hi, I'm Dee Stevenson. I'd like to share an entire case with you. This is a Fempto case. This is a fairly soft nucleus. And I use a, in this particular case, I use a pattern, a particular Fempto pattern. I make a side port incision with an MVR blade. One thing I've learned, and I learned this from residents, is I mark my dime, I mark the metal blade that I use with a purple marker. So you can see on the video, you can see on the video actually that I have marked my side port incision. I don't know about any of you, but when we're learning, and even when we've had great experience, a lot of times I can't find my side port incision. So this is very helpful.  So I kinda do a dimpled-down technique where I make sure that there's no adherence anywhere on the capsule, so I don't have any tags. Usually, there's free-floating and they're easy to do, but I'm kind of a creature of habit and I'm kind of a safety person. So then I hydro-desect and hydro-delineate with a very little bit of power or pressure because you wanna release all the gas bubbles because you don't wanna have a posterior capsule rupture due to this. Now I use the Stolaris and it is, again, a small tip, 1.8. It goes through. So what I'm doing is I put viscoelastic in first. So now I have, the pattern has cross hairs, if you will, or a Maltese cross, cross hairs with little cubes. So what I do is I actually go in with a second instrument and I do a little bit of a divide and conquer here where I go make a groove and then I'm gonna crack it and then I'm gonna rotate it and I'm gonna do the same thing again. So I make four quadrants out of this. And I kind of like to be a little safe with these little cubes and you can determine what kind of pattern you use. I don't use this cube pattern as much anymore, but this was the beginning of my Fempto career when I first started using this. So it was an easy one to do. However, you wanna make sure that those small little cubes don't bounce around on the endothelium and bother the endothelium. So you just kind of follow through. So what I've done now is I've gotten half of it out. So now I'm rotating it with my second instrument and I'm cracking it again and I'm allowing the the cortical material, I mean the nuclear material to come to my port. So I've cracked it now and I'm rotating it for the last crack and now I'm going to do, I put it in a foot position too. So I'm gonna aspirate all those quadrants and some of the epinuclear rim comes along with that. So this is a very controlled setting with a small incision like I said, a 1.8 incision for my FACO incision and then the side port incision is made with an MVR blade. So you have, the Stalars is very nice machine because it keeps a nice stable chamber. I don't have a lot of egress of fluid coming out so it's very stable. Now this is taking the epimembrane or epi nuclear shell out with a FACO tip. You don't have to do it with that. You can do it with your IA, which is a little safer. Now this is a silicone tipped IA and I kind of strip it and start and kind of pull things tangentially towards the center to pull it out. Sometimes I start superiorly sub-incisional because that's kind of the hardest to get out but with FACO, with Femto, it's a little, the cortex is a little different. So I do it in a circumferential fashion and I can actually lay this silicone tip on the capsule itself and it really, really causes little damage or anything, it has a silicone tip before the metal is in the IA so that it's very safe if it does suck up some posterior capsule, it will not tear it. So again, now I'm going for the sub-incisional cortex which comes out quite nicely. And again, I polish all capsules because I think that it's important to have, I don't like doing capsulatomies once you have a, you know, the yag capsules, once you have a retinal detachment from one, you're very, I'd like to not have to do it. So I polish very nicely so the lens does, the bag doesn't contract or doesn't have fibrosis. Now I'm opening the wound to 2.2 with a metal blade and I'm gonna use the Invista lens. Now the Invista lens is a hydrophobic acrylic lens. It opens fairly slowly so you have time to be able to insert it into the eye then make sure both the trailing haptic is in the bag and then I warm my viscoelastic to allow it to open and I rotate it into the bag and make sure it's very well centered. Now I'm a Aura user, Aura with Verify Plus and the lens opens slowly so if you're a person that does or if you end up using Aura, if you're a person that does or you have to wait for the lens to open and the visco, warm viscoelastic helps it open better. This is a beautiful lens. Again, aspheric, centers just beautifully, has vaulted haptics so very little capsular fibrosis occurs. I'm Dee Stevenson, thank you for watching. I hope you learned something.