Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

So, also ich korrigiere jetzt noch einmal die Beschreibung des Falles B1.

Also die Behandlung des Falles B1 war richtig und auch das Bild, was ich dazu gemalt hatte, war richtig.

Und auch die Formel, die ich dazu hingeschrieben hatte, gilt zwar in dem Fall, aber sie beschreibt den Fall nicht eindeutig.

So, diesen blöden Fall zu beschreiben ist jetzt in dieser Notation mit Kontexten, die wir uns hier gewählt haben, nicht so ganz einfach.

An der Stelle versteht man dann, warum viele andere Texte statt mit Kontexten mit Pfaden in einen Term hineinarbeiten.

Aber man kriegt es auch so hin. Ich mal die Situation nochmal an.

Wir hatten also hier unsere linke Seite von einer von zwei konkurrierenden Rewrite-Regeln.

So, darunter sitzt eine Substitution, Sigma 1,

die zum Beispiel auf eine Variable X angewendet wird, die also hier im Bild dreimal vorkommt, natürlich im Allgemeinen also 0 bis N-mal.

So, und hier drunter in dem Sigma 1 von X finden wir jetzt das L2 Sigma 2 wieder.

Und zwar sagen wir mal, hier unter dem dritten Vorkommen von X. Das ist jetzt das Blöde, dass das X mehrmals vorkommen kann.

Deswegen kann man das nicht besonders gut mit Substitutionen ausdrücken.

So, jetzt grenze ich da mal so ein paar Gebiete ab.

Das ist der Fall, wie er ist. Und es ist so jetzt sonnenklar, was die Situation ist.

Die Frage ist nur, wie schreibt man das auf, wenn man es nicht mit Bild machen will.

Hier haben wir zum Beispiel einen Kontext, wenn man so will. Das wäre ein Kontext, der hier ein Loch hätte.

Das Ding nenne ich jetzt mal, wie wollte ich es nennen, E.

Okay, und hier drunter sitzt jetzt ein weiterer Kontext, in dem das L1 Sigma 1 eingehängt ist.

Das ist jetzt dieses Blaueingerahmte. Das nennen wir mal C1 Strich. Der Gesamtkontext war C1.

Ne, C2 Strich, Entschuldigung. C2 Strich. Der Gesamtkontext hieß C2.

So, das heißt, mit diesem Bild vor Augen lautet also die korrekte formale Beschreibung dieses Falls.

Es existieren zwei Kontexte, E und C2 Strich. Hier sind sie hingemalt.

Und eine Variable X mit. So, wie kriegen wir da die restlichen Daten daraus wieder?

Also, das C2 ist gerade das Blaue und das Rote zusammen. So, nicht mit anderen Worten.

C2 ist C2 Strich eingesetzt, also der blaue Kontext C2 Strich eingesetzt in den roten Kontext E.

So, jetzt wollen wir außerdem noch sagen, dass wir das L1 hier finden.

Also, was wir eigentlich sagen wollen ist, L1 ist die obere Hälfte von diesem zusammengesetzten Kontext.

So, wie kriegen wir denn hier was mit L1? Das L1 selber, das kriegen wir nicht.

Also, wir schaffen es nicht, hier die beiden Dinger nur noch abzuschneiden. Dafür haben wir keine Operation.

Was wir tun können, ist, wir können hier das Sigma x wieder einsetzen.

Dann haben wir wieder etwas Vollständiges vom Format L1 zusammen, wo eben hier überall unter dem x dasselbe hängt, nämlich Sigma 2 von x.

Ne, Sigma 1 von x, Entschuldigung.

Vorher konnten wir das L1 hier gar nicht sehen, weil hier unter diesem x was anderes hing als unter dem x hier.

Nämlich hier so ein Kontext mit Loch drin.

Aber hier, wenn wir das Sigma 1 von x wieder einsetzen in E, dann kriegen wir eben L1 Sigma 1.

So, das ist die korrekte Beschreibung dieses Falles.

Ist so ein bisschen egal, weil der Beweis dann ja anschließend trotzdem per Bild erfolgt.

Ich wollte es nur einmal korrekt angeschrieben haben.

So, und jetzt wo wir es schonmal angemalt haben, ja dann noch einmal das, was letztes Mal in der Eile etwas kurz gekommen ist.

Der alternative Fall war, dass das also so aussieht, dass ich hier meinen Wedge der linken Seite, der einen Regel habe, L1 Sigma 1.

Und hier wieder das Fall B darunter, das L2 Sigma 2 wieder finde, aber nicht so weit darunter wie hier,

dass ich also tatsächlich schon in der Substitution lande mit dem Ding, sondern dass ich weiter oben sitze.

Ja, wie male ich das?

So, dass also hier das L1 sitzt, dass das L1 praktisch hier noch rein ragt in das L2.

Das ist die alternative Fall.

Hier steht, dass das L2 so weit unter L1 sitzt, dass es L1 selber gar nicht mehr stört.

Und hier ist der Fall, dass die beiden sich also echt überlappen.

So, das wäre also der Fall, den wir im Rahmen dieses Lämmer nicht mehr abhandeln, sondern der eben dann ein kritisches Paar darstellt.

Das hier liefert mir ein kritisches Paar und ich male einmal den Kontext hin, der dazu gehört.