Das ist schon so, wenn ich einen Prozess habe, der keinen Langloch-Fretlock hat, dann habe ich keine Falschding Traces.

Wenn man einen Prozess hat, der keinen Deadlock hat, dann hat man keine vollständigen Traces, wohl aber normale Traces.

Die starke Trace-Equivalenz schließt explizit die normale Trace-Equivalenz ein.

Es besteht keine Verpflichtung, die Abgaben zu techen.

Die meisten Leute machen das mit Ticks. Ich selber habe mich nie daran gewöhnen können und es sieht immer nicht so ganz spitze aus.

Statt Ticks nehme ich gerne einen XY-Pick. Das kann ich ganz viel.

Thorsten hat ein Monolog gehalten, warum man Ticks benutzen möchte.

Das muss man aber auch nehmen. Die meisten machen das mit normalen Ticks.

Das würde ich mir dann auch mal anlernen. Vielleicht geht Thorsten ein Tutorial.

Unter anderem kann man den normalen Ticks nicht anständig labelen.

Wir haben gerne handstiftliche Textechnik mit reingemalten.

Wir haben uns angeguckt, dass Schwache B-Similarität ist.

Wir haben uns überzeugt, dass das ein Begriff ist, der vieles leistet, was wir von ihm erwarten.

Jetzt wollen wir noch ein paar metatheoretische Eigenschaften von Schwacher B-Similarität angucken.

Die sind fast alle in Gänze analog zu den, die wir uns für Stärke B-Similarität angesehen hatten.

Man muss aber aufpassen.

Wir haben am Anfang einen Katalog von Eigenschaften aufgestellt,

die wir von einer Prozess-Äquivalenz erwarten.

Insbesondere sollte es gerne eine Äquivalenz sein.

Ich habe das Blöken hier in meinen Metizen. Einfach zielisch stehen für Schwache B-Similarität.

Also, macht vor, dass du nicht als Satz, also Schwache B-Similarität ist tatsächlich nicht erledigt.

Wir haben drei Eigenschaften abzuhaken.

Ich kann es dir zeigen. Schwache B-Similarität ist reflexiv.

Reflexivität verlangt nur, dass bestimmte Dinge zur anderen Relation stehen.

Zum Beispiel Schach B-Similarität.

Das ist auch wieder klar, und zwar für Konstruktion.

Es ist zwar nicht etwa jede B-Simulation symmetrisch, aber wenn es eine schwache B-Simulation ist, dann auch S-.

Mit S ist auch S- eine schwache B-Simulation.

Es müssen nicht gleich sein, aber die Definition ist so gebaut, dass die Umkehrrelation auch eine schwache B-Simulation ist.

Warum? Einfach durch das Format des Begriffs B-Simulation.

Der Gegenteil ist der Herd, der in der praktischen B-Simulation nur in einem anderen System eingeführt hat.

Z.B. ben flying tree, ein Hotel, mit streckaffle oder

Ja, nee, aha, das geht ja sogar alles noch.

Das ist die alles nicht schön.

Rechen bitte die Weiß hier ab und dann kannst du es sagen.

Per-Diffusion sind ja zwei Zustände in irgendwelchen Transitionssystemen, die genau dann schwachen wie Simila.

In den Erweiterten, ich schreibe das mal, hatten wir dem Namen gegeben T-Quer oder hatten wir die Zeitaltion anders geschrieben?

Also T-1-Quer soll jetzt mal das System mit der erweiterten Zustandsübergangsrelation sein.

Genauso natürlich dann T-2-Quer, denn die sind gelastet.

Das ist Per-Diffusion, weil eine weibliche Relation zwischen Q1 und Q2 genau dann eine schwache B-Simulation ist, wenn sie zwischen den erweiterten Systemen eine B-Simulation ist.

An der Stelle können wir Beweis haben.

Es geht uns ja jetzt nur um die Relation auf zwei Mengen. Die Mengen ändern sich ja nicht durch den Übergang zu dieser erweiterten Relation.

Die Zustandsmengen waren die gleichen. Insofern folgt aus dieser Äquivalenz sofort das schwache B-Simulation.

So, mal gucken.

Vielleicht erschlagen wir dann den ganzen Rest fort.

Das nächste, was man zeigen will, das hier ist ja nicht ganz genau die Definition von schwacher B-Simularität, aber das ist ein Faktum, dass man sofort aus der Definition weiß.

Dieser ganze Beweis hier ersetzt uns nicht unmittelbar aus Fakt 1.

Okay, jetzt kommt man uns den nächsten Zielsatz an.

Wir hatten ein paar Eigenschaften über Wiesen, die nicht unbedingt direkt auf unserer Liste standen, die aber trotzdem ganz nett sind.

Wir haben natürlich abgewandelt auf schwache B-Simularität.