Also, bei der ersten Aufgabe, das war ja nun beidseits irgendwie begründungsfrei, gut,

ich meine, begründungsfrei ist eine Sache, begründungsfrei ist falsch, ist eine zweite.

Was ist begründungsfrei und falsch?

Dass es begründungsfrei ist, sieht man mit losem Auge und dass es falsch ist, sieht man, wenn man es vergleicht und dann nochmal nachdenkt.

Okay. Ich dachte, ich hatte es noch nicht verstanden.

Der erste Schritt ist noch richtig, dafür den Punkt. Der zweite bleibt leider schon nicht mehr. Es ist noch nicht der Fixpunkt.

Noch nicht?

Ja, sieht man ja auch irgendwie mit losem Auge, weil die Dinger dann ja sonst alle wie Singular sein müssten, was sie erkennbar nicht sind.

Vielleicht haben wir die richtige Lüge. Vielleicht mit Begründung.

Ja, mündlich begründet sich das auch.

Mündlich begründet sich das. Aber kann es auch schriftlich begründet sein?

Ja, wenn man nicht vollständig alles durchgibt, kann man ja sagen, dass wir irgendwie rausfallen, die rausfallen.

Die Dinger bleiben in deinem...

Ich habe jetzt natürlich nicht mehr die ursprünglichen Fragen.

Den kriege ich wahrscheinlich sogar noch hin.

S hat einen A-Übergang nach S1 und dann S2.

S2 hat einen B-Übergang in sich selber.

Und dann hat S1, glaube ich, noch einen B-Übergang zu S3. Und das hat gar keinen Übergang mehr, wenn ich das im richtigen Kopf habe.

Ich kann aber gleich noch was machen.

S2 hat... Achso, nee, hörst du das schon auf?

Nee, da hört es auf. Da muss noch ein mehr gibt, der auf der rechten Seite.

Also T hat einen A-Übergang nach T2.

T1 hat dann einen Selbstübergang in sich selber mit B und einen B-Übergang in T2. Das hat keinen Übergang mehr, glaube ich.

Ja, das müssen wir wirklich natürlich bezeichnen, aber genau so einstunden, dass wir auf die Lüse und Match wieder so sind, wenn man die bringt.

Du schaust es dir gleich nach.

Ich schreibe einfach mal kurz alle Fahre hin und dann können wir die jetzt mal auskreuzen, wie nah das ergibt.

S...

Ja, stimmt so.

Das ist übrigens schon eine allerdings sehr sinnvolle Vereinfachung der Übergangsstellung, die dieses Mal in die Kommunierung aufleben würde.

Da steht Partition Refinement. Dann ist natürlich gemeint, dass das zusammen ein großes LTS sein soll, was wir da sehen.

Dann müssten da auch Paare wie S, S1 und so weiter betrachtet werden, nicht dass beide den Eingang jetzt weggelassen haben.

Das ist wohl dann auch schon ein Tick netter für die Aufgabenstellung. Das Entscheidende der Findig findet ja zwischen S und T statt.

Wir rechnen aber in Wirklichkeit nicht Partition Refinement, sondern wir rechnen iterativ die größte B-Simulation-Relation zwischen den beiden Dingern als getrennte LTS.

Bei B-Simulation hatten wir ja auch diese...

Genau, nicht das kann man bei B-Simulation ausmachen.

Das andere ist vielleicht doch ein bisschen sehr gut.

In der ersten Interaktion fallen jeweils schon mal die Paare weg.

Also S3 mit T und T1 fällt weg, weil die können jeweils was machen und der nicht.

Dann fallen die beiden weg, dann nehmen wir die Interaktion hin und entsprechend fallen die weg, weil ich hier dann T2 nichts machen kann, aber die anderen jeweils.

Gut, was ist noch weg gefallen? Es fällt noch der hier weg, und zwar weil S1 kann B machen, aber T nicht.

Und entsprechend fällt der hier weg, weil S kann A machen, aber T1 nicht.

Der hier fällt wahrscheinlich auch weg, weil... genau, zwei kann B machen und T kann nicht B machen.

Die anderen drei bleiben jeweils drin, weil S kann A Übergänge machen, T kann A Übergänge machen, das stimmt über einen.

S1, T1 können jeweils B Übergänge machen, S2, T1 können jeweils B Übergänge machen.

Gut.

S2, T2 können jeweils X machen.

Ach so, er kann auch.

Gut, im nächsten Schritt liegen jetzt diese beiden Parden hier raus.

Und zwar schauen wir uns dieses hier an.

S1, T1, da haben wir S1 macht einen B Übergang zu S3 und T1 macht einen zu sich selber und S3, T1 haben wir rausgeschmissen in den letzten.

Ja, warum sagt man das also? Was sagt man zuerst?

Wir sagen zuerst, wenn wir uns den Übergang von T1 zu sich selber anschauen, dann ist der Einzige, der dazu passt, der von S1 zu S3.

Und dann komme ich aber in ein Zustandspaar, was ich schon rausgeschmissen habe.

Genau.

So, und der hier fliegt auch raus.

Hier auch.

Der fliegt raus, weil S2, T1, weil S2, T2 nicht drin ist.

Genau.

T1, T2.

Genau, wenn ich T1, T2 mache, dann passt der Einzige dazu, der Hände ist zu sich selber und dann kommt wieder, dann verlasse ich wieder meine Relation.

Okay.

Und schließlich im dritten Schritt geht der hier raus, weil wenn ich mir den von T zu T1 anschaue,

dann habe ich da zwei mögliche Antworten darauf, aber beide Paare, wo ich hinkomme, sind jetzt im letzten Schritt gerade rausgeblieben.

S1, T1 und S2, T1.

Okay, und so haben wir jetzt gar nicht gesagt, aber der hier bleibt jeweils immer drin, weil da nichts passiert, da passiert nichts.

Genau, und nach der vierten Interaktion bleibt es gleich, das heißt, wir beenden den Algorithmus oder wir ausfügen den Algorithmus und dann wissen wir,

wie b7 oder so weiter und so fort ist.

Ja, vielleicht argumentieren wir nochmal, warum es leer bleibt, das ist klar, warum man bleibt.

Genau, also wir schauen an, für alle Übergänge, die S3 machen kann, gibt es einen passenden von T2, aber da gibt es keinen, also es passt.

Und umgekehrt auch.

Ja, okay, ich glaube, da waren existiert mit für alle Verwechselt.

Das ist der Fehler.

Ich glaube, ich habe mir da immer nur einen angeguckt und dafür geht es natürlich, aber man muss sich alle angucken,

wenn man findet, wenn jemand einslatt wird, dass es nicht geht.

Ja, es reicht nicht, dass man paarweise die besten Antworten hat.

Thor, Thor, Fehler, das habe ich nicht in der YouTube nachgedacht.

Jo, okay, das war das.

Und das war ja mehr so Warm-Up für die eigentliche Aufgabe von 2x2.

Hier nur eine wahnsinnig viele Teile ist der Teil, jetzt erfälle ich mich.

Aber alle zwei A hier links, da passt das glaube ich noch.

Ja, gut, das ist ja nichts tolle, eigentlich nur zu sagen, dass zu zeigen war, dass diese Relation,

also S0 ist T-Spiez und dann war das der Kursicht definiert, plus 1t, falls für alle,

was war das jetzt, für alle S,alpha, also alpha, Moment echt, und S Zustand,

mit S nach S', es ist hier ein T-Strich mit der Eigenschaft, T macht einen, also wenn es hier einen

alpha Übergang macht, macht die auch einen alpha Übergang nach T-Strich und es gilt S' und I in Relation zu T'.

Gut, dann glaube ich, die Zeige war, dass das Äquivalent ist zu Partition-Refinement nach I Schritten.

Und okay, das Partition-Refinement nach 0 Schritten ist alles sowieso zueinander Äquivalent,

das heißt, das passt und das hier ist eigentlich genau die Bedingung, die auch bei Partition-Refinement drin steht

und deswegen ist das Äquivalent. Also das ist nichts anderes als Partition-Refinement im Prinzip.

Also welches Beweisprinzip verwenden wir da? Induktion, Induktion, danke.

So, okay, das war also die 2a, die lag jetzt weiter, das ist schon klar, 2b war das mit der beschränkten B-Simulation.

Den Begriff der B-Simulation definieren, sodass das mit dem hier zusammenfällt.

Gut, das habe ich einfach nicht genau genug ausgeklärt. Ich kann sagen, was ich gemeint habe.

Genau, das ist doch mal interessant zu hören.

Ja, also, ich habe das so definiert, dass wenn man eine beschränkte B-Simulationsrelation genauso wie das da implementiert,

dass man sagt, okay, das ist das quasi die auf i beschränkte B-Simulation zwischen s und t.

Was bedeutet, dass sich der Zustand s und der Zustand t innerhalb von i Übergänge nicht anders verhalten können?

Also, dass das jedem, also wenn s, i Übergänge macht, um zu einem Endzustand zu kommen,

man kann t diese Übergänge auch machen, sodass die Endzustände zumindest mit dieser Unrelation zusammen gehen.

Das ist irgendwie nicht so schön, glaube ich. Das ist insbesondere keine Definition.

Na ja, man kann es.

Das ist eine Intuition vielleicht, aber man könnte es natürlich noch so sagen,

dann existiert B-Strich, das der den macht und das hier ist halt i-1.

Ja, das ist aber eine Wiederholung der Definition insgesamt. Ich soll es uns schöner definieren.

Also, das Ziel des Ganzen ist, dass wir hier sparen, dass wir uns die Chance geben,

nicht alles, was tatsächlich i Schritt B-Simular ist, auch in diese i Schritt Relation zu setzen,

sondern womöglich nur einen Ausschnitt davon, um eben zu kleinen B-Simulationen zu kommen.

Das ist dasselbe wie der Zweck einer normalen B-Simulation, nur eben für dieses i Schritt Ding.

Ja, also einmal hier vielleicht die Kassette-Simulationen davon.

Hier war noch etwas umgekehrt, aber das eigentliche, hoffe ich, Hausbild ist,

wir hatten ja diese Funktion f definiert, sodass die B-Simulation gerade die Postpix-Punkte von diesem App waren.

Dann heißt das hier gerade f von dem hier vielleicht das hier.

Also, ich spare mir dann die Funktion. Was ist denn so eine Funktion von f?

Also, ich weiß nicht genau, welche f das meint.

Kann ich nachschreiben und mal hinschreiben? Dann schreibe ich nachher mal hin.

Also f von s ist...

Partition-Refinement.

Ja, dieses f.

Okay, gut dann.

Ja, das ist im Ordnung.

Ja, und wir können jetzt sagen, eine Familie...

Ich habe es jetzt B-Simulation der Ordnung N genannt.

Das machen wir jetzt so weit jetzt.

Richtig oder genau falsch?

Ich glaube falsch.

Das würde ich so sagen.

Vor allem würde das ein Postpix-Punkt definieren.

Oh, ich habe es richtig gesagt.

Okay, dann nochmal.

Wir haben ri, f von ri, das heißt eben so in dem gleichen Schema wie hier.

Genau.

Und dann gilt das hier ist genau dann, wenn...

Dann beginne ich jetzt mal so als Liste.

Okay, ich verstehe es nicht ganz.

Also ich verstehe nicht ganz, was es bringt. Also ich weiß nicht. Wo ist der Unterschied zu der Aussage, die ich...

Der Punkt ist der, dass jetzt hier das R0 wesentlich kleiner sein kann als Q vor SQ.

Und dann dementsprechend alle anderen R's wesentlich kleiner sein können als Julie.

Weil wir hier nicht R0 weiter spezifizieren.

Also es sind sowieso nicht...

Das jeweils folgende ri ist durch ri-1 sowieso nicht vollständig spezifiziert.

Also selbst wenn wir mit R0 gleich Q kurz Q anfangen würden, was wir wahrscheinlich relativ scharflos tun können,

könnten wir immer noch dann anschließend weiter runterschreiben und sparen.

Weil wir immer nur verlangen, dass ri enthalten ist in f von ri-1.

Nicht, dass es gleich von ri-1 ist, wie wir das im Falle von TZT in PAK kennen.

Das heißt, wir können... Also da haben wir jetzt kein Beispiel drin, dass wir jetzt in ZQB das auch noch zum Ende.

Aber wir können, wenn wir Glück haben, hier sehr kleine, solche beschränkte B-Simulationen bauen.

Ja, das heißt, man kann es hier kleiner machen. Aber prinzipiell, das andere ist ja auch eine beschränkte B-Simulation.

Prinzipiell kommt nichts Neues dabei raus. Das ist wichtig.

Und anders als im Falle der normalen B-Simulation habe ich auch sogar eine anständige Definition von beschränkter B-Simularität,

die das Wort B-Simulation gar nicht verwendet.

Also ich den Begriff von normaler B-Simularität kaum anständig definiert kriege, ohne zu sagen, was eine B-Simulation ist.

Aber es ist eben im technischen Sinne, es ist hilfreich.

Also wenn ich jetzt anfange hier ein automatisches Tool zu bauen, das mir von einem wirklich sehr großen System zeigen soll, dass sie B-Simular sind,

dann werde ich in zweiter Falle wahrscheinlich sehr glücklich, wenn ich diese eigentlich einhalten kann.

Ja, nun, das ist jetzt also korrekt definiert und korrekt behauptet, man muss es dann natürlich beweisen.

Gut, die eine Richtung ist ziemlich einfach, nämlich diese hier.

Da können wir einfach sagen, wir setzen eher hier auf die jeweilige B-Simularitätsrelation und dann haut es alles hin.

Gut, jetzt in der anderen Richtung muss man ein bisschen Induktion machen.

Natürlich nach N.

Fall N gleich Null ist klar, warum ist der klar?

Linke Seite ist für alle x, y erfüllt, rechte Seite ist auch für alle x, y erfüllt.

Dann nehme ich einfach irgendeine Relation, die halt die beiden enthält.

Und das ist dann meine Familie von Relationen.

Das heißt, eine Induktionsschritt.

Und dann geben wir uns einfach zwei Punkte vor, die durch so eine B-Simulation der Ordnung N-Bris 1 in Beziehung gesetzt werden.

Und wir müssen jetzt zeigen, dass x und y in dieser N-Bris 1 B-Simularitätsrelation sind.

Das heißt,

wenn wir jetzt sowas gegeben haben, so ein x-Strich und ein Alpha-Übergang dahin, dann suchen wir gesuchtes irgendwie y-Strich mit,

sodass y einen Alpha-Übergang dahin macht.

Moment, jeweils mit.

Wir haben dieses Paar x, y, das liegt in Rn plus 1.

Das wiederum ist eine Teilmenge von F und Rn und daraus folgt, es gibt eben so ein y-Strich,

sodass x-Y-Strich zunächst mal in Rn liegt.

Und nach der Induktionsvoraussetzung ist dann eben auch x-Strich. Wie spricht man dieses Symbol am besten aus?

Natürlich, wenn y-Strich so ein B-Simularitätsrelation endet.

Das war jetzt natürlich nur der eine Teil. Wir müssen natürlich auch jeweils für Alpha-Übergänge von y Antworten von x ausfinden,

aber das geht völlig anders.

Damit folgt dann das x tilde n plus 1 y nach Definition von tilde n plus 1.

Ich glaube, dass man das so schön versteht, ist aber nicht der Aufgabenstellung.

Die Aufgabenstellung war nur, definieren Sie von jedes hier einen Begriff der B-Simulation, der das charakterisiert.

In dem Sinne, dass s tilde i t genau dann eine B-Simulation gibt. Mehr war ja nicht gefordert.

Rein formalistisch kann man jetzt natürlich sagen, dass ich sagen kann, eine tilde i ist die einzige B-Simulation bis s t tilde i.

Und dann wird die Behauptung trivial erweist. Das kann man natürlich rein formalistisch machen.

Ich hatte aber vorher erklärt, was das an sich wäre.

Und danach noch die Aufgabe, wo man die Fixpunkt-Charakterisierung...

Genau, die Fixpunkt-Charakterisierung hat hübsche Rückwirkungen auf diese Aufgabe.

Dann machen wir also noch die Fixpunkt-Charakterisierung als nächstes.

Das ist die...

C, C waren die Spiele, oder?

Ja, genau. Also noch mal eben noch ein G und dann anschließend C.

Okay.

Also dann...

definieren wir uns unsere Abbildung und sie geht von...

Genau.

Braucht das hier eigentlich M plus 1? Ah ja genau, braucht M plus 1.

Ich hab mir gedacht, ich hätte hier irgendwie so eine Definition eingebaut oder eine technische Definition.

Moment, aber das F-Vertrag kann in XM oder ist nur ein G?

Ach so, ja, ja, ja.

Und auch auf der Menge haben wir jetzt eine partierte Ordnung.

Das ist eben Komponentenweise Inklusion, die hatten wir jetzt am Dienstag auch schon.

Dann...

wenn ich jetzt Fn...

und so etwas habe, dann hat es ja N plus 1 Komponenten, die jetzt auch von 0 bis N indiziert sind.

Das heißt, ich sage einfach, was die jeweiligen Komponenten alles sind.

Und die 0te Komponente ist dann eben...

einfach nur das S0 wieder und die...

und so etwas.

Genau, jetzt habe ich einen ästhetischen Einwand gegen diese Definition. Sie ist, sobald ich es erkennen kann, technisch richtig, aber...

Okay.

Also wie oft verwende ich S1 zum Beispiel hier auf der rechten Seite?

S1.

Ja, einmal.

Einmal. Und S2?

Ja, auch einmal.

Und S0?

Ach so, zweimal.

Meiner Meinung nach wäre also eine etwas andere Definition natürlicher.

Das sieht man so jetzt schlecht. Man sieht es dann hier, wenn man es in Tupelschreibweise schreibt.

Und hier also S0 bis S1 bis Sn wird abgebildet auf...

Das würde ich da tun, natürlicherweise. Denn der LSL ist 0.

Was kommt natürlicherweise da?

Der ist 0?

Dann kommt es jetzt 2 mal. Ich würde ja den einen nach rechts, der LSL fällt raus, alles zwischen den Kreuzkugeln.

Gut, ja, wie dem auch sei. Also Klappen und Fixlöcher.

Dann kommt der Top von diesem Verband. Und dann ist S0 ohnehin...

Und nach der Definition ist dann eben die B-Simulation der Ordnung N genau die Postflitzpunkte von diesem LN.

Mit anderen Worten, wenn wir das einmal begriffen haben, wie sieht das dann aus mit dem Beweis D und D?

Da assim arkadaşlar.

...

...

Den muss man gar nicht mehr führen.

Wenn wir einmal gesehen haben.

Hier haben wir ein offensichtlich monotones Funktional auf meinem vollständigen Verband.

Dass das Ding da monoton ist, das sehen wir mit großen Augen.

Und ein Blick auf die Definition von so einer Bismulation der Tiefe N oder Bismulation der Ordnung N sagt uns,

eine Bismulation der Ordnung N ist genau ein Postflixpunkt von FN.

Dann gibt es eine größte Bismulation der Ordnung N, das sagt uns der Satz von

Ligman Stratarsky, und die ist gleichzeitig ein echter Fixpunkt.

Das ist eine weitere Aussage des Satzes von Ligman Stratarsky.

Wenn ich mir dann angucke, was es heißt, ein echter Fixpunkt von diesem Funktional zu sein,

das heißt gerade, dass man gleich Töden 0 ist.

Ein Fixpunkt von diesem Ding zu sein, ist genau die inaktive Definition von Töden 0.

Jedenfalls dann, wenn man da Gugolz gut fand.

Ja, das ist auch so nicht schwer, dass man sich da in Arbeit spart.

Klar, aber auf die Weise muss man versuchen, nur hinschreiben und dann sagt man Laster Tarsky und ist fertig.

Das ist doch auch wieder nichts anderes als Partition Refinement.

Einfach nur jetzt alle Schritte auf einmal hinschrieben.

Ja, ja, das ist verständlich. Das unterscheidet sich alles nicht groß.

Wenn man jetzt Partition Refinement alles ausnehmen würde, hätte man sehr viel.

Das ist ja quasi Partition Refinement bis Schritt Ende.

Genau, das ist ja am Anfang gesagt, dass eine Bissimilarität bis Schritt Ende ist Partition Refinement bis Schritt Ende.

Eine Bissimilarität, der auch am Ende hiegen ist nicht Partition Refinement bis Schritt Ende.

Kann auch weniger sein.

Aber man kann es auch so definieren, dass es Partition Refinement bis Schritt Ende ist.

Dann hat man zwar mehr drin als nötig, aber es wäre trotzdem eine Bissimilarität.

Ja, es wäre einfach dasselbe, wie das, was wir mit Boberstromm nicht angefangen haben.

Ja, aber ja.

Das wäre insbesondere nicht anerhob zur Situation mit der Bissimulation in keiner Weise.

Die ja genau beruht auf dem Satz von Kraster Taske, wie ihn sagt.

Also Bissimilarität ist der größte Postfixpunkt und dann auch ein Fixpunkt.

Und eine Bissimulation ist irgendein Postfixpunkt.

Das ist die Analogie, um die es hier letztlich geht.

Okay, also Zehntens. Spiele.

Ich habe es auch nicht groß bewiesen. Ich habe einfach nur gesagt...

Ja, das ist zumindest im Prinzip korrekt gelöst.

Im Prinzip korrekt gelöst? Ich bin einfach kein Mathematiker.

Das ist hier ein Oberziehungslage.

Ja, ich sehe schon. Ich bin nicht genau genug.

Ich habe es einfach nur gesagt. Es ist eigentlich nichts analog zu dem, wie wir es vorher gesagt haben.

Ja, wenn man es tatsächlich analog hat, ist das insofern sogar korrekt.

Also entweder, Spoiler, Hartnäckige Gewinnstrategie in I-Zyken.

Daraus folgt S nicht. Oder umgekehrt.

Duplikator, Hartnäckige Gewinnstrategie.

Daraus folgt S.

Tilde I-Relation mit T steht.

Was da jetzt so ein bisschen fehlt, sind die genauen Regeln des Spiels.

Die Regeln sind analog zu den anderen Regeln, die wir vorher über die B-Simulation hatten.

Das ist aber ein bisschen komisch. Das Spiel ist für N runden und dann pfeife ich ab.

Wenn es nach 90 Minuten unentschieden steht, gewinnt er.

Bei unentschieden gewinnt Duplikator.

Gut, schreibt noch hin. Nach I-Zyken gewinnt Duplikator.

Also Spoiler, wenn er gewinnen muss, vorher gewinnt.

Das dachte ich wäre jetzt intimitiv klar. Das sind meine bösen Anahmen, die man als Physiker trifft.

Duplikator wird bevorzugt.

Der Beweis ist tatsächlich analog. Das kann man tatsächlich so stehen lassen.

Da steht genauer bei mir.

Genauer bezieht sich vor allem auf die Regeln.

Ich glaube, die Relation ist die Gewinnstrategie.

Ja, ja, ja. Aber wenn man sich dann anguckt, was die Relation ist, gemäß der angeblichen Lösung von offKBP, dann wird es schon ein bisschen schwierig.

Ja, okay. In der Tat ist die in mich eine B-Singulation der Ordnung N eine Gewinnstrategie.

Die ist eine Familie von N-Relationen. In jedem Schritt sagt mir die jeweils I-Zyken-Relation, wie ich gerade zu spielen habe.

Das ist auch ein bisschen anders als vorher, wo ich eine einzige Relation habe, die mir für jeden Schritt fragt, wie ich spielen muss.

Denn hier habe ich für jede Phase des Spiels eine Relation, wie man das sagt.

Na ja, aber ist die I-Relation nicht eigentlich auch eine Gewinnstrategie für alle Züge?

Das ist ja immer nur Refine. Das heißt ja nicht, dass Züge rausfallen.

Das teilen keine Züge raus. Das ist wahr. Aber dann ist die I-Klick.

Ja. Das klingt jetzt aber richtig, weil ich dann ja zu vorsichtig spielen muss gestern.

Nein, es gibt quasi mehr Möglichkeiten zu gewinnen eventuell, aber man fährt auf jeden Fall mit der Gewinnstrategie, die man durch die I-Ther-Relation kriegt, nicht falsch.

Nein, nein, nein. Eine Gewinnstrategie muss ja so sein, dass sie mir in jedem Zug auch noch eine Antwort liefert.

Man konnte ja eigentlich als Beispiel sagen, wir haben hier irgendwie zwei Sachen, die sind beide einfach nur so strecken und man kann halt immer genau eins weiterziehen und es besteht überhaupt keine Auswahlmöglichkeit.

Dann kann man als Gewinnstrategie und als B-Simulation der Ordnung N die RI jeweils so wählen, dass sie immer nur ein solches Paar von Zuständen enthalten.

Und dann muss es nicht mehr erfüllt sein, dass das irgendwie so absteigend ist.

Ja, das ist in der Tat nicht so. Das Paraligm of partition refining täuscht hier. Eine B-Simulation der Ordnung N ist im allgemeinen nicht absteigend.

Also es steht da, dass RI Teilmenge von F von RI ist, es steht nicht da, dass RI Teilmenge von RI-1 ist. Also RI ist eine Teilmenge von F RI-1, aber es ist nicht eine Teilmenge von RI-1 selbst.

Aber nach F von RI-1 ist keine Teilmenge von F von RI-1.

Genau, wenn wir Partition refining machen und bei Q-Qualsq angefangen haben, dann ist das so. Aber im Allgemeinen ist das nicht so.

Das ist der eine Einwand. Es müsste aber noch ein anderer Einwand gelten.

Also selbst wenn ich sage, ich vergesse das mit den B-Simulationen, nehme einfach das Tilde N. Ich nehme B-Similarität. Dann müsste ja, also wenn ich sage, ich nehme B-Similarität bis zur Tiefe N als Gewinnstrategie.

Ich nehme mir also genau das Beispiel hier.

Also die sind B-Similar bis zur Tiefe 3, wenn ich hier oben anfange, obwohl sie nicht B-Similar sind. Und nenne ich mir jetzt hier Tilde N an. Guck mal, Tilde 3.

Nun, die beiden, die sind in Relation Tilde 3 und das sind aber die Einzigen.

Das sind die Einzigen?

Ja, schon die beiden sind nicht mehr.

Aber der ganz oben wäre mit dem zweiten hinter rechts.

Achso, ja. Das ist wahr, die sind auch noch in Tilde 3. Das sind dann die Einzigen.

Wirklich? Wäre nicht der noch mit dem in Relation Tilde 3 und der noch mit dem?

Nein, nein, nein, nur Tilde 2.

Wieso Tilde 3? Der kann dann einfach keine Züge mehr machen.

Das sind jetzt sogar B-Similar. Also die sind definitiv in Relation Tilde 3.

Welche beiden?

Die jetzt, also der und der. Achso, die hier, der und der. Die sind immer noch, achso, die sind in Tilde 3.

Und der eins weiter unten auch.

Der ist auch mal in Tilde 3. Das ist wahr, aber das eben nicht in Relation Tilde 3 wie ich sind.

Okay.

So, und wenn ich jetzt also hier meine Gewinnstrategie Tilde 3 fahre, den nehme ich mal wieder weg hier.

So, ja, jetzt habe ich hier meine Tilde 3. Das ist auch kein Fall, weil ich habe eine Tilde.

Ja, wenn ich hier versuche Tilde 3 als Gewinnstrategie zu verwenden, ich fange an, ich sehe, aha, ich gewinne.

Also ich bin in Relation Tilde 3.

Okay, Duplikator, Spoiler nach dem Zug, sagen wir mal, der macht hier ein Zug, das macht Duplikator.

Muss ich nachmachen.

Meine Gewinnstrategie müsste mir sagen, ich kann in irgendeinem anderen Zug, in irgendeinem anderen Zustand ziehen,

wo ich hier jetzt immer noch gewinne. Kein Problem.

Aber die nicht in Relation?

Die stehen ja nicht in Relation. Das ist kein Gewinnstrategie.

Ah, okay.

War auch kein Strafgewinnstrategie.

Ja, okay, gut. Schönes Gegenbeispiel.

Jo.

Okay.

Gut geglaubt.

So, wo sind wir? Wir haben 10 Tilde 3 von Fixpunkt Ohnotation.

Genau, Fixpunkt Ohnotation, sehr richtig.

Aber 100 Euro bis das, was ich hier mache, in einem settle M adheren, steht dieseshong hier für NO CHAMPARSOM younger,

das heißt 200 Euro.

guer knitise hogrande.

Also, ahh, 100 Euro bis das, was ich hier mache, steckt da auf.

Dempselnsek compliant.

vielleicht nicht so richtig sinnvoll gestellt, aber so würde ich fast Vorschlages

überstecken. Also die eigentliche Rechnung, die ich da anschweren wollte, war eine,

wo wir eine fürchterlich schlechte Schranke kriegen, weil wir sagen,

wir bilden Fixpunkte im Power Set von Q Kreuz Q hoch N plus 1. Und die Ketten, die wir da

bilden können, die absteigenden Ketten in diesem Ding, die sind zunächst mal

naiv betrachtet, dann sind das so viele Ding-Elemente.

Das bedeutet, weil es keine Potenzmenge ist, ich kann im Q-Kreuz Q

kann ich quadratisch absteigen, quadratisch in der Anzahl der Zustände

und das kann ich womöglich n plus eins mal nacheinander machen. Ich kriege n plus

eins mal mal die quadratische Anzahl der Zustände an iteration. Aber die Struktur

dieses Funktionales, die sagt mir natürlich, dass es die Möglichkeit viel

schneller gibt. Ja, also dieses Funktional, das ist so gebaut, dass es nach

den Schritten stabilisiert. Also insofern vergessen wir einfach mal die ganze Rechnung.

Gut.

Und ich habe noch gedacht, man könnte vielleicht sogar noch besser abschätzen.

Naja, also die Abschätzung ist klar. Also es ist letztlich nachher, also den Fixpunkt von dem Ding zu berechnen, ist

wieder nachher. Wir sollten jetzt abgewöhnen, hier Partition-Refinement zu sagen. Partition-Refinement wird es

wirklich nur, wenn das Ganze auf einem System stattfindet. Wenn man hier

zwischen zwei Systemen rechnet, dann ist ja das Wort Partition-Refinement nicht mehr

gerechtfertigt, weil es sich nicht mehr um eine Partition handelt.

Partition wäre ja eine Reklivalenzrelation. Also eine Fixpunkt-Berechnung. Ja, also das wäre einfach nur die Fixpunkt-Berechnung.

Also in den ersten Schritten der Fixpunkt-Berechnung. Die kommt dann hier, in diesem Funktional ist das dann ein echter Fixpunkt.

Ja, in dem anderen haben wir ja den Fixpunkt noch nicht erreicht. Wenn wir Q equals Q rechnen,

und dann nur F anwenden, wenn wir das N mal machen, sind wir nicht sicher, dass der Fixpunkt schon erreicht ist.

Aber hier in unserem komischen Funktional hier, ist das schon ein echter Fixpunkt.

Wenn man sich auf jeden Fall dieses Ding da anguckt, das N mal iteriert, dann hat man erreicht,

genau die Sequenzen der Tildes und die Liste an den Fixpunkt.

Jetzt kommt also schon der Modal der Verzeihung.

Das kommt natürlich zur Endlichverzeihung.

Ach richtig, das kommt zur Endlichverzeihung.

Die hier kann eigentlich auch schon weg.

Weil mit dem Fixpunkt haben wir jetzt auch nichts mehr zu schaffen.

Scheinbar nicht klar, was ich gemeint habe.

Ich meinte damit eigentlich, dass diese Relation für alle, das hätte ich anders herum,

Tili-ungleich-Lehremenge für alle, oder für alle i, das war die Leeremenge.

Ich meinte einfach nur, dass das hier nicht die Leeremenge ist, weil das für alle i die ungleiche Wertenmenge ist,

aber das hier ist die Leeremenge, also könnte die nicht gleich sein.

Das Tilde, die Leeremenge ist hier, das tritt ja gar nicht zu.

Also der da ist zum Beispiel.

Ja, okay, bei den beiden Punkten.

Die beiden sind nicht drissimilar.

Aber die beiden Punkte sind in jeder dieser Tili-Is enthalten.

Das ist etwas komisch.

Man muss doch noch mal sagen, nicht nur genau sein, sondern auch nur sagen, was man meint.

Das ist hockey.

Das war ja einer von den Teilpunkten, die ich noch von dir gegeben habe.

Weiß ich nicht, ich stehe ja nicht dabei.

Das habe ich jetzt nicht genau aufgedrückt.

Die ist ja auch nicht so wichtig wie die Punkte.

Okay, das würde es sein.

Ich glaube, wir müssen noch mal über endlich Vertreibung reden.

Ja, das ist gut.

So generell, was das eigentlich bedeutet,

weil irgendwie bin ich mir nicht mehr so sicher, was es bedeutet jetzt.

Ja, es bedeutet unter jeder Aktion habe ich immer nur endlich eine Nacht vor Garn.

Moment, ist die Frage, habe ich für jede Aktion

nur endlich viele Zustände, die diese Aktion ausführen?

Nein.

Nein, okay, gut, interessant.

Ich dachte nämlich, das ist es.

Das Wort heißt das, was man denkt eigentlich.

Also endlich verzweigend heißt, ich habe,

also ich stelle mir vor, das Ding ist ein Baum

und an jeder Stelle, wo es sich verzweigt, habe ich nur endlich viele Zweige.

Der Baum kann unendlich sein.

Also ein unendlicher, wie näherer Baum oder sowas ist durchaus endlich verzweigend.

Das ist ein Erfolg.

Okay.

Okay.

Wenn wir zeigen wollen, dass die eine Impression gilt,

dann brauchen wir diese endlich Überzweigung gar nicht zu verwenden.

Wir können einfach sagen, in dem Fall ist wahrscheinlich das Einste,

die B zu nehmen und sagen, wir geben die Simulation der Rocken N an.

Und dann nehme ich halt einfach das Ding.

Da haben wir gerade mal wieder das richtig, was davon.

Wir können irgendeine B-Similarität angehen, die in dem Falle kleiner ist.

Nicht das Ding da.

Also diese Sequenz von N plus 1 mal B-Similarität,

das ist ganz sicher kleiner als die entsprechende Familie

der beschränkten B-Similaritäten, Tilde N, Tilde N bis Tilde N.

Ich verlange schon in der Nölbenphase, dass die echt B-Similarität.

Okay.

Jetzt kommen wir zu der anderen Richte.

Und weil wir ja wissen, das ist die größte B-Simulation,

reicht es zu zeigen, dass das hier eine B-Similarität ist.

Das ist doch ein Fakt.

Okay.

Das heißt, wir geben uns einfach mal zwei Elemente vor,

die in dieser Relation zueinander stehen.

Jetzt müssen wir halt wieder diese beiden Bedingungen nachdrücken.

Da sieht man dann auch wieder, dass beide analog zueinander gehen werden.

Nebenfrage noch mal zu den N-D-Verzweigungen.

Heißt das auch, dass die Menge der Aktionen endlich sein muss?

In der Tat heißt es das nicht.

Nein, gemeint ist dann pro Aktion endlich verzweigend.

Es kann durchaus und endlich viele Aktionen geben,

nur hauptsache für viele Aktionen gibt es nur endlich viele Nachdrücke.

Das werden wir hier auch sehen, dass das reicht.

Okay.

Wir besuchen jetzt einen Y-Strich, das in Relation tilde n zu x-Strich steht,

für beliebig großes n.

Wir nehmen jetzt einfach an, es gibt kein solches Y-Strich.

Das heißt, wir müssen das Ganze jetzt dann negieren.

Wir bekommen dann das für alle, ein Y-Strich, ein N,

sodass...

Also das ist einfach die Negation von der Ausseibe, die wir zeigen wollen.

Jetzt kommt die endlichste Beilung ins Spiel.

Und weil es endlich verzweigend ist, können wir jetzt einfach alle diese J von Y-Strichs nehmen

und das Maximum davon bilden.

Dieses J existiert dann.

Andersherum kann das natürlich eine unendlich große Menge sein, dann kann die nach oben unbeschränkt sein.

Dann gilt das hier. Dazu muss man sich halt noch überlegen, was wir jetzt streng genug noch nicht getan haben,

dass jeweils diese Beufe wieder tilde j absteigen müssen. Wir haben das jetzt noch nicht geliefert.

Daraus folgt dann das x nicht tilde j plus eins Y.

Wir haben wirklich nur gebraucht, dass für dieses eine Alpha, das wir uns jetzt gerade gegriffen hatten, die Menge der Y-Strich nicht über Alpha erreichen kann.

Wir haben nicht unterstellt, dass es überhaupt erreicht war.

Dann folgt eben das.

Jetzt war noch gefragt, wie das eben für unendlich verzweigendes T ist. Und dann kann man eben dieses Gegenbeispiel nehmen, was wir in der Polys

konzeptuell wichtig haben.

Das hat zwei Richtungen. Vielleicht mal hier die erste. Ich frage mich gerade, warum das nicht gilt. Fällt da noch ein plus eins oder so was?

Die Anzahl, wie oft sie nacheinander kommen. Wie viele hintereinander stehende Boxen und Diamonds haben die?

Die hintereinander stehen. Die Hintereinander vorn. Dann definieren wir gerade mal den Rand von Phi.

Man kann es ja für jede Aktion in Phi vordefinieren, aber das haben wir ja auch schon in meiner Vorlesung gemacht.

Jetzt sollte man zeigen, wenn S und T gilt, dann ist die Zyntelogischung wahrscheinlich bezüglich Formel der Schachtungstiefe I.

Genau. Die Verhalten sich durch Maximal, durch gezüglich.

Die Verhalten sich bezüglich der Maximal-I-Transaktion der reichbaren Nachfolger gleich.

Das bedeutet ja genau das, dass ich die Transitionen von hier aus machen kann und die hier nachmachen kann, sodass die Zustände dann in Relation stehen.

Logische Äquivalenz bezüglich Formel mit Maximal-Rang I bedeutet genau das, dass die durch Maximal-I-Transaktionen reichbaren Zustände soweit kann man nur die Tiefe kuppeln.

Das ist das informelle Argument und man kann es ja jetzt auch formal beweisen. Wie sieht denn der formale Beweis aus?

K. Der formale Beweis, schön. Was ist überhaupt das Beweisprinzip, das ich verwende? Die Luktion über I.

Also gut, okay. Also, Form I. S0t, gut, okay. Das gilt, wenn die logische Äquivalenz sind.

Ja, eine Formel von Rang 0 ist die überhaupt eine Aussage? Ja, die kann eine normale Formel sein.

Die kann sein top und bottom. Das war es eigentlich schon, oder?

Eine Formel von Rang 0 enthält keine modalen Apparaten. Kann also maximal top oder bottom sein.

Oder eine wilde propositionale Kombination von top oder bottom. Was mache ich mit einer so wilden kombination?

Die kann ich wieder auf top oder bottom übertragen. Genau, die ist die Influenz entweder top oder bottom.

Wir können es also zurückziehen, wie der Formel von Rang somewhere shape portions.

Es ist genau so blöd, ist es nicht?

Und S erfüllt nie Bottle.

Ende.

Ja, T erfüllt auch nie Bottle.

Gut, und S und T stehen immer in Relation.

Gut, wunderbar.

Hau hin.

So, das ist go.

Wunderbar, klasse.

So, und jetzt ist die Frage...

Jetzt haben wir S steht in Relation I zu T.

Und jetzt machen wir hier einfach mal ein Stift,

die nach I plus eins.

Gut, jetzt wird mir die Keil zu kurz.

Wir haben geschritten, dass S nach I plus eins macht.

Dann sollte aber S besser in Relation I plus eins zu stehen.

Sollte es?

Ja, wahrscheinlich.

Ich habe das mir jetzt noch nicht so ganz gut ausgedacht.

Also, so.

Gut.

Wenn jetzt S einen Übergang,

einen Alpha Übergang nach S macht,

dann folgt daraus, dass T auch einen Alpha Übergang nach T macht.

Und das gilt, S ist in Relation I mit T.

So, und wenn wir jetzt den Übergang von I nach I plus eins machen wollen...

Na gut, wenn S und T äquivalent bezüglich Modaloperatoren betriefe I sind,

also wir haben jetzt, wir nehmen jetzt mal unten eine Formel.

Was ist unser nächstes?

Also die Aussage ist einfach mal, wir haben jetzt eine Formel vom Rang V gleich I.

Und die gilt...

I plus eins, besser.

Ich würde jetzt einfach mal damit anfangen, dass wir das I haben,

und dann können wir die Formel box V bilden.

Und die dann gucken, ob die hier gilt.

Gut.

Das kann man auch machen, ich weiß es nicht.

Also sinnvoll ist es einfach sauber, der logischen Struktur zu folgen.

Also wir müssen zeigen, wenn S und T bisimilar bis Tiefe I plus eins sind,

dass sie dann die gleichen Formel vom Rang I plus eins, höchstens I plus eins zappeln.

Wir nehmen also eine Formel vom Rang höchstens I plus eins her, nennen wir sie mal Phi.

Dann müssen wir überlegen, was wir mit dieser Formel jetzt anfangen.

Ich glaube, man kann es auch andersrum aufzäumen, dass man sagt,

die beiden erfüllende Formel vom Rang I und dann ist der einzige Weg,

wie ich zu I plus eins komme, indem ich entweder Box oder Diamond drauf anwende.

Oder söde propositionale Kombinationen davon löse.

Ah, okay, das ist einfach zu eklig.

Oder andere Formeln nehme, also warum sollte ich ausgerechnet die nehmen,

die ich jetzt gerade in der Hand habe für jetzt, für die Striche?

Das ist ja eine verliebige Formel, die lag ja nix über die Formel, die sie selber aus.

Ah, es geht schon.

Also wir machen das mal schön.

Wir haben S steht in Relation I plus eins T.

Daraus folgt S Strich in Relation I zu T Strich.

Wir wissen noch überhaupt nicht, woher S Strich in T Strich kommt.

Das würde ich noch gar nicht bringen mit Recht und Recht.

Na gut, okay.

Jetzt muss jetzt noch als erstes die Formel kommen.

Wir müssen zeigen, dass für alle Fee, die Rang höchstens I plus eins haben,

dass die Formel von S erfüllt wird, wenn sie von T kommt.

So, S erfüllt Fee.

Wann erfüllt es das?

Wenn alle S Strich,

dann ist die Frage, was für ein Modalapparat da drin steht.

Das ist das Fee.

Das Fee besteht zunächst mal potenziell aus irgendeiner guischen Formel.

Und unter den guischen Operatoren kommen irgendwann Modaloperatoren.

Also welches Beweisprinzip verwenden wir jetzt, um mit dem Fee umzugehen?

Induktion über alle Operatoren?

Induktion über Fee, genau.

Das ist alles nichts. Das müssen wir uns alle operatoren angucken.

Müssen wir das? Nein, wir handeln die meisten ganz schön schnell ab.

Negation ist geschenkt.

Und? Was gibt es noch?

Top, Bottom.

Das ist geschenkt, haben wir gesehen.

Und und oder? Die werde ich sagen.

Und ist nicht so schön oder, ist relativ einfach.

Und ist genauso geschenkt.

Ich beweise diese Äquivalenz.

Ich beweise, S erfüllt Fee genau dann, wenn T erfüllt Fee.

Das beweise ich durch Induktion über Fee.

Und wenn ich mir das so etwas angucke, das ist eine Äquivalenz.

Die guischen Schritte sind immer geschenkt.

Ich bitte mal den vor für Konjunktion.

S erfüllt Fee 1 und Fee 2, genau dann, wenn S Fee 1 erfüllt und S Fee 2 erfüllt.

Innovationsvoraussetzung, genau dann, wenn T Fee 1 erfüllt und T.

Also, guische Schritte sind fast immer geschenkt.

Okay, gut.

Falls solange das irgendwie eine Äquivalenz ist.

Also, dann können wir ja sowas machen, wie S erfüllt Box Alpha Vieh Strich.

Genau.

Ja, was bedeutet das?

Für alle S Strich mit der Eigenschaft S macht einen Alpha-Übergang nach S Strich,

gilt S Strich erfüllt Vieh Strich.

Oder?

Ja.

Gut, okay.

Ja, das ist dann genau dann, wenn...

Na ja, gut, wie schreibt man das jetzt im Prinzip?

Ja, so schreibt man das nicht auf mich.

Also, das nächste Friede ist, man sollte sich nicht darauf einlassen,

zwischen durch geschlossene Sätze im First-Order-Logik hinzuschreiben,

also sich hier so ein Quantor ans Bein zu binden.

Also, man kommt jetzt einfach nicht ungezwungen dahin, dass das Äquivalent dazu ist,

dass alle Nachfolger T Strich von T jetzt irgendwie Vieh Strich erfüllen.

Sondern was man machen muss, ist, man muss diese Quantoren aufbrechen.

Das heißt, jetzt müssen wir erstmal sagen, welche Welten...

Man muss jetzt erstmal sagen, und zweitens sollte man gedanklich rückwärts fortgehen.

Rückwärts fortgehen?

Also, was will ich zeigen?

Ich will zeigen, dass T das hier erfüllt.

Genau.

Was muss ich also tun, um zu zeigen, dass T das da erfüllt?

Ja, um zu zeigen, dass das T das da erfüllt, muss gelten, na ja, für alle T.

Also, dass hier genau dann wenn, für alle T Strich,

so dass T nach Alpha T Strich übergeht, mit T Strich erfüllt man T Strich.

Genau.

So, und ich würde mich möglichst dann zurückziehen hier auf eine Richtung dieser Äquivalenz,

um gleich anschließend zu sagen, die andere ist natürlich analog.

Das heißt, wir zeigen nur die Implikation von links nach rechts.

Das heißt, wir setzen voraus, Alpha, das erfüllt Box Alpha Pi Strich,

und wir zeigen diese universell quantifizierte Formel da rechts.

So, wie gehen wir vor, um eine universell quantifizierte Formel zu beweisen?

Na ja, jeden einzeln und einen halb beweisen.

Also, wir nehmen uns ein so ein Ding her.

Wir nehmen uns ein T Strich hier, mit T Alpha T Strich, und zeigen T Strich.

Na gut, für T Strich, C macht einen Alpha-Übergang nach T Strich,

existiert S Strich, S noch ein Alpha-Übergang nach S Strich.

Genau.

Gut, und?

Da fehlt noch was.

Das ist dann nicht nur mal S einen Alpha-Übergang nach S Strich, sondern...

Na ja, S Strich erfüllt die Formel, aber...

Das freu ich auch, aber es fehlt noch was.

Es fehlt ja noch...

Ach so, ja.

S Strich steht in i-Relation mit V Strich.

Aha, genau.

Genau, und jetzt, S Strich erfüllt V Strich.

Gut, das kommt daraus.

Okay, und dann machen wir hier noch S Strich erfüllt V Strich,

und daraus folgt C Strich erfüllt V Strich.

Na, TV.

Ja, das ist das, was da steht, und dann...

Passt das.

Okay.

Jo.

Beweisschema und Überziehungslage haben wir hier.

Das ist die Hauptmessage hier.

Quantoren immer auseinandernehmen.

Also wenn ich einen Halbquantor sehe, den ich beweisen will, dann sage ich als erstes S EI,

und hinter dem S EI kommt das, was der Alpha-Übergang befiziert ist.

S EI also T Strich, so dass T einen Alpha-Übergang nach T Strich macht.

Wenn ich einen Existenzquantor habe, wie ich ihn an dieser Stelle will kommen,

dann nehme ich den auch auseinander und zwar ebenfalls mit S EI.

Es existiert so eines Striches, also nehme ich es mir her und arbeite dann damit.

Sonst wenn ich das unter dem Quantor lasse, das ist so explizit, dass das hier nicht passiert,

aber wenn ich das unter dem Quantor lasse, komme ich ja immer nicht ran.

Also das, was tief unten in der Formel steht, kann ich nicht manipulieren.

Inwiefern?

Also wenn ich eine komplizierte Formel habe, wie man Existenzquantor anfängt,

dann kann ich relativ wenig unter ihr anfangen,

weil ich habe wirklich göttliche Einsichten, diese Formeln,

und genau sich da die tiefen Schlüsse tief innerhalb der Formel verhalten.

Das kann man schon machen, das Gipfelogikern tun das, aber das ist also exotisch,

um es höflich auszudrücken.

Also was man macht, ist sogenanntes natürliches Schließen.

Natürliches Schließen hat insbesondere folgende Schlussregeln.

Natürliches Schließen läuft mit Unterbeweisen.

Unterbeweisen verschaffe ich mir Entitäten lokal.

Also wenn ich ein frisches C einfüge, frischen Bezeichen,

frisch heißt, kommt mir irgendwo vor, das heißt,

ich habe noch keine laufenden Annahmen über ihn.

So, und ich nehme an, nichts eigentlich,

und ich zeige, es gilt Phi von C für dieses Ding, das ich frisch eingeführt habe,

dann kann ich als nächstes schließen, für alle x Phi von x.

Das ist die Art, wie ich ein Eiferno beweise, sei C beliebig gegeben,

gut, meistens will ich hier eine Implikation beweisen.

Das übliche Schema lautet,

Psi von x impliziert Phi von x, dann nehme ich an dieser Stelle hier an Psi von C,

weil das so eine Implikation für alle in einem Ablassschliss am Maße ist.

Und die Regel, wenn ich einen Existenzquantor verwenden will, sagen wir mal, ich weiß, es

existiert x so, dass phi von x gilt und ich will irgendwas zeigen.

Chi.

Was mache ich?

Ich nehme in einem Unterbeweis her ein frisches C, von dem ich annehme, es gelte phi von C,

dann beweise ich phi und kann dann, weil ich weiß, dass es so ein Ding gibt,

kann ich phi insgesamt schließen.

Und Texte A sind beide diese frischen Cs, jeweils einfach nur ein Psi.

Also im Prinzip kann man hier sagen, Psi ist so, dass das gilt, dann gilt das.

Oder um das mal gut zu sagen, das Psi, also man kann auch deutlicher machen,

wenn man ein Existenzquanto ausnutzt, dann existiert in Worten s', sodass und so weiter.

Das ist so ein sprachlicher Trick, damit habe ich also den Existenzquanto erwähnt

und mir gleichzeitig per se das xs' verschafft.

Das ist also shorthand für dann existiert, also formal jetzt mit Existenzquanto s', sodass und so weiter,

sei also s' ein solches.

Das möchte man nicht überschreiben, deswegen schreibt man kurz in Worten,

dann existiert s'.

Es ist wirklich vermeidend, in solchen Stellen auch wirklich nur den Existenzquanto zu schreiben, weil das...

Genau, also in mathematischen Beweisen sollten also diese exklusiven Existenz- und Altquanturen eigentlich

nur in Ausnahmefällen zu tun.

Ich habe viel mehr Erfahrung mit solchen Formen.

Wenn, dann sehe ich dich.

So, schön. Jetzt zeigen wir es noch für die Diamant oder schenken uns das?

Nein, wir schenken es uns, weil wir ja Negation schon erledigt haben.

Richtig, das ist ja eigentlich nur Negation von Negation.

Also Negation von Box-Negation.

Jetzt bleiben wir mal was über, das schaffen wir in den verbleibenden zwei Minuten nicht mehr.

Das ist also das mit der umgekehrten Lichtung.

Ach so.

Diese Normalformen kommt man da wahrscheinlich auch nicht aus, oder?

Normalformen?

Also hier diese Formen, die die Normalform von der Ordnung n zu diesem einen Element,

also die Formen, die dieses eine Element von dem Transitionssystem charakterisiert.

Ach so.

Ja, gut. Was wäre...

Was sind das für Normalformen?

Was man da beobachtet, ist einfach nur, dass man die Aussage verschärfen kann.

Also ich brauche gar nicht alle Formeln, es reichen mir Formeln bestimmten Typs.

Also ich kann mich sogar einschränken auf Formeln, die überhaupt keine Konjunktion enthalten.

Ich kann sagen, es reichen mir völlig Formeln wie mit Box oder Diamant.

Oder Diamant und Legit und Diamant.

Wenn ich Funk theory war, episode vielleicht,

plus wenn ich DIAMANT und DIVIRT series nehme, dann kann ich es für mich wirklich nur

Weglassen, ich hier habe eine perlu.

Das können wir zum nächsten Mal noch kurz diskutieren

Solange wohnen wir darauf, dass es, dass das ist eigentlich eine geck nach dem Gonzen aus prov Server

Dass also Modale Iglobig Seokieкрütern��고 das die Unangene才 tego voraussetze

Exakt dieser beschränkten angle sich ohne dass es sagt das ist prepared

Das ist ja nur dann, wenn ich von beschränkter Lisminabilität zu echter Lisminabilität gehen will.

Dann brauche ich die endliche Verzweiflung.

Okay, also das eben noch nächstes Mal.

Und dann haben wir noch einen Nachtrag nächstes Mal.

Und dann haben wir noch einen kurzen Exkurs zum TKQ.

Genau, nicht?

Alles klar.

Einfach etwas abwägen, dann kriegt ihr eine abzählbare, unendliche, total geordnete Menge, die ihr eigenes Supremum enthält.

Moment, eine abzählbare, unendliche, total geordnete Menge, die ihr eigenes Supremum enthält.

Du enthalten die natürlichen Zahlen, die ihr eigenes...

Du kannst einfach die Ordnung umdrehen. Dann ist Null das Supremum.

Aber man kann ja nicht schon unendlich anfangen zu zählen.

Also, nee, das eigentliche... Wo uns mit geht, ist sowas wie...

Also wir hatten das im Ende-endlich-verzweifelten-System. Ich hab mir nur überlegt, ob man nicht irgendwie sowas konstruieren kann, wie...

Ach, ich seh' die Hüten. Keine Ahnung.

Also, das System ist ja nicht endlich verzweifelt, weil wir jetzt mal annehmen, dass das Deck...

Also wenn man das hier so weiterdrüllt, dann ist das andere System.

So, unser schönes Standardbeispiel.

Und dann geht das dann.

Das ist ja nicht endlich verzweigend, aus dem einfachen Grund, weil wir immer die gleiche Aktion annehmen.

Ja.

Wenn wir jetzt aber für jeden Pfad eine eigene Aktion annehmen, dann wäre es endlich verzweigend.

Ja.

Und wenn... Die Frage ist, was nimmt man für diesen Pfad für eine Aktion an?

Weil so kann man einfach sagen, okay, dann ist das Aktion 1, Aktion 2, Aktion 3, etc., etc., etc.

Und das wäre dann so etwas wie Aktion unendlich.

Die Aktionen sind ja nicht geordnet.

Naja, man kann die Aktion aber indizieren.

Oder? Mit einer Indexmenge einfach.

Und dann kann ich sagen, das hier ist Aktion 1, das ist Aktion 2, usw., usf.

Und dann habe ich ja im Prinzip so etwas wie, okay, gut, dann wäre doch nach unserer endlich verzweigenden Sache für n Element unendlich, die beiden hier wie Sie mir nach.

Nein, denn wenn ich dann noch so eine zusätzliche Aktion unendlich einführe, mit der ich dann nach rechts laufe, das kann ich ja links nicht nachmachen.

Ja doch, das ist ja genau deswegen die Frage, ob es eine Menge gibt, die ihr Supremum enthält.

Weil wenn ich hier mit dem hier einfach hochlaufe, laufe ich ja irgendwann zum Supremum.

Ja, nee, das gibt ja der ganze Formatismus nicht her.

Der hat keine Grenzwertstruktur.

Also man kann das gar nicht machen, mit Folgen von Aktionen, die irgendwann ein Grenzwert haben.

Irgendwohin konvergieren, das geht gar nicht.

Okay, das war nur eine Idee, weil wenn es so etwas gäbe, könnte man das ja hier quasi als unendliche Aktion enthalten.

Ja, aber das wäre dann ja ein völlig anderer Formatismus, es mag schon sein, dass der sich dann anders verhält.

Okay, nur ein Spiel, leider.

Eine Frage, wie macht man im Satich ein Alpha über den Pfeil?

Mit übergrade, nee, stackrobe.

Das habe ich tatsächlich schon mal gebraucht.

Ich bis jetzt noch nicht, deswegen habe ich das i-Ride als Index angemessen.

Oder das Alternativ, das man machen kann, ist man lädt halt einfach x, y, das braucht man sowieso dauernd.

Dann findet man da...

Ich weiß jetzt zwar nicht, was das ist, aber...

Das ist sehr nützlich, das braucht man.

Da würde man das dann einfach so schreiben.

Okay.

Pfeil nach rechts mit Alpha oben drauf.

Das ist dann in der ganz normalen Formel und Bindung zwischen so Donners.

Das ist gemeint eigentlich für komplexe Diagramme, aber man kann es auch in einer normalen Formel und Bindung verwenden.

Okay, dann bis morgen. Bis dann.