Also, letztes Mal war mein Nagi stehengeblieben.

Die Simulation ist tatsächlich in dem Sinne eine Prozess-Äquivalenz,

dass es zumindest mal eine Äquivalenz-Relation ist vom Vorgang.

Das eben was war, was man richtig zeigen musste.

Anders als bei Trace-Äquivalenz, weil bei Trace-Äquivalenz ist das anhand der Definition abliber klar,

dass das eine Äquivalenz ist und bei V-Simulationen wenig.

So, und jetzt kommt eben das nächste. Die Frage ist,

ist die Simulation auch eine Combo-Äquivalenz?

So, ach ja, wir wollen noch mehr machen.

Also auf dem Weg dahin machen wir noch ein paar Dinge.

Nicht beizuzugehen, zu sehr auswendig soll man dann doch nicht.

Also ein Blick auf gerade die Titel.

Also, das Ding ist eine Combo-Äquivalenz-Relation.

Combo-Äquivalenz kommt noch, jetzt kommen erst mal noch ein paar nützliche Eigenschaften.

Eine des folgenden.

Und zwar, dass V-Similarität die größte V-Simulation ist.

Das klingt jetzt irgendwie nach so Begriffshuberei.

Das klingt auch so, als müsste das aus der Definition so vorfolgen.

Die Frage ist, was fehlt da überhaupt?

Das hier ist die Relation, die zwischen zwei Prozessen dann gilt,

wenn es eine V-Simulation gibt, die sie in Beziehung setzt.

Was also ist da noch zu zeigen, um diesen Satz zu zeigen, was fehlt?

Was ist größte in dem Fall?

Ach so, größte bezüglich Mengen-Inklusion zwischen Relationen.

Eine Relation ist eine Teilmenge des Kreuzprodukts.

Und da habe ich die Implosionsrelation zwischen.

Das heißt also, eine Relation ist groß, wenn sie viele Elemente in Beziehung setzt.

Ich frage mich gerade, wenn es eine B-Simulation ist, ist es doch eine B-Simulation.

Ich verstehe nicht, wie etwas größer sein kann als etwas anderes, wenn...

Wohlgemerkt, es gibt B-Similarität und es gibt B-Simulation.

Ja, es klingt nur trivial, weil die Begriffe so genügend sind.

Aber da deutet sich gerade schon an, was noch zu zeigen ist.

Das ist jetzt die Vogelperspektive gefragt.

Meint das so etwas wie, dass die B-Similarität Dinge in Relation setzt und alle Dinge, die sie in Relation setzt,

also die Äquivalenten unter denen sind, bilden zusammen die größte B-Simulation?

Das ist zu kompliziert ausgedrückt, aber essentiell richtig.

Was noch zu zeigen ist, ist, dass die B-Similaritätsrelation,

dass die selber eine B-Simulation ist.

Also per Definition ist T eine Vereinigung von Stapelrelationen,

nämlich die Vereinigung einer Relation R, so dass R eine B-Simulation ist.

Denn per Definition sind zwei Zustände B-Similar, wenn es eine B-Simulation gibt, die sie in Beziehung setzt.

Also mit anderen Worten, die B-Similaritätsrelation ist eine große Vereinigung, nicht die große Vereinigung aller B-Simulation.

Damit ist also per Definition die B-Similaritätsrelation größer bezüglich Mengen und Funktion als jede B-Simulation.

Was noch zu zeigen ist, ist eben die Gesetze, die ist selber eine B-Simulation, dann ist sie die größte B-Simulation,

da wir schon gesehen haben, dass sie größer ist als alle anderen.

Was noch zu zeigen bleibt, ist eine B-Simulation.

Fangen wir erstmal mechanisch an.

An dieser Stelle, wenn ich beim automatischen Beweiser den Knopf drücken an,

wird die Definition von B-Simulation aufgefaltet.

Dann sage ich noch einmal Auto und dann wird die eifantifizierte Implikation,