Ja, fangen wir doch einfach mal an.

Und zwar vielleicht am besten mit Aufgabe 1.

Ja, das ist hier sein Parallelkomposition Assoziativ.

Ich dachte, das wäre klar.

Also das ist etwas, was ich tatsächlich als trivial klar gesehen hätte.

Aber das ist nicht mehr oder weniger trivial als die anderen Statements auch.

Okay, verdammt.

Also 1.1 würde man zeigen, dass das hier gilt.

Also das hier ist B-Simulation-Equivalenz.

Und dazu reicht es, eine B-Simulation anzugeben.

B, U, P.

Das ist sowieso, weil sonst würde das ja gar nicht gelten.

Und dann eben fortgesetzt mit allen möglichen Kombinationen.

Sodass eben, wenn hier P-Strich ist, hier drüben auch P-Strich ist.

Und das geht immer, weil wenn man einen Übergang hier mit Komp 1 macht, kann man hier drüben mit Komp 2 machen.

Und umgekehrt, wenn hier Komp 3 einen Übergang macht, macht das auch Komp 3 einen Übergang.

Und zwar in dieselben Zuständen, einfach nur getauscht.

Das kann man jetzt beliebig fortsetzen, auch mit Q.

Das kann man jetzt beliebig fortsetzen, das ist natürlich nicht wundervoll.

Man möchte ja schon von dem R mal eine definitive Definition dastehen haben.

Ist das jetzt doppelt gemobbelt, eine definitive Definition zu sagen?

Also man möchte eine Definition von R sehen und nicht nur irgendwie sich überzeugen lassen, dass man das einsammeln kann.

Die wird kurz und knapp das R definiert.

Man kann sich das natürlich aus sämtlichen Nachfolgern zusammenbauen.

Aber das ist jetzt erstmal nicht verpflichtend gewesen, das R möglichst sparsam zu definieren.

Klar, das möchte man jetzt nicht machen, aber es dürfen gerne in dem R ja auch irrelevante Dinge vorkommen.

Es ist nun mal geschrieben, dass alles was diesem Vilar ist irgendwie erreichbar sein muss von dem, wo man dann hängt.

Achso.

Dann ist das ja im Prinzip so etwas wie...

Das ist für alle Bs die Nachfolger von Qs sind und alle As die Nachfolger von Bs im Prinzip.

Also man muss sich da nicht mehr Kopfschmerzen machen als nenne ich.

Klar haben wir mal gesagt, die Semantik dieser Prozesse ist der erreichbare Teil von dem LTS, das letztlich durch alle Prozesszerme gebündigt wird.

Das ist offensichtlich in manchen Kontexten relevant und in manchen Kontexten irgendwie wieder nicht relevant.

Wenn man nur zeigen möchte, dass irgendwelche Sachen diesimilar sind,

und man zwanglos eine Bsimularität auch dem gesamten großen System angeben kann, dann eine Bsimulation.

Und das geht wieder derzeit auch nicht.

Das heißt wir brauchen auch dieses A und B und gar keine Expektion.

Okay, dann für alle AP.

Für alle Prozesse AP, das kann man ja auch ausprobieren.

Man muss jetzt zeigen, dass das eine Bsimulation ist.

Das macht man ernst, nicht so irgendwie durcheinander, dass man handwaved während man die Bsimulation noch hinschreibt, dass es ja auch hinhaut,

sondern man schreibt sie erst hin und dann sagt man, dass es hinhaut.

Dann sieht es besser aus.

Dann kann man argumentieren und schreibt man sich hier so ein schönes Ding hin.

Dann macht das hier irgendeinen Alterübergang nach.

Ein Übergang, der dann zu A-Strich führt.

Und dann sagt mir das, hier existiert aber auch ein B-A-Strich.

Und der Übergang kommt durch, also wenn das jetzt, kann das entweder Komm 1 sein, ja das muss Komm 1 sein, so.

Dann existiert der hier drüben aber auch, weil das A einfach das gleiche ist.

Der existiert nach.