So, okay, dann können wir auch aufs Graten.

Ja, fangen wir einfach an, wenn es jetzt reicht.

Ja, Aufgabe 1.

Und die ersten beiden, da konnte man irgendwie so richtig viel falsch machen.

Auch die dritte haben im Wesentlichen eigentlich alle richtig, aber vielleicht sehen wir uns noch mal sorgfältig an, wie das Argument dafür geht.

Da könnt ihr erst mal die Zettel haben.

Okay, starten wir.

Okay, die Prozessdefinition war, wenn ich das richtig im Kopf habe.

So, verp.

Okay, das ist sie noch nicht ganz, sondern die haben jeweils noch einen Präfix da, die beiden parallelen Prozesse einmal ab und ab, sonst macht sie auch keine Anweisungen.

Okay, und die Behauptung ist jetzt eben, dass die die gleichen Traces haben.

Und zwar folgt jetzt.

Wenn man sich das jetzt für cool überlegt, dann ist das relativ klar, dass das die Tracen-Hänge ist.

Das heißt, man schaut sich vielleicht eher bei ihr an, weil das das interessantere ist.

Gut, und zwar kann man zunächst mal anschauen, was kann P überhaupt für Übergänge machen?

Und dann sieht man, dass das Einzige, was möglich ist, Tau ist, weil alles mit A oder A quer wird ausgeschlossen.

Und Tau kann man eben herleiten durch Parallelkompositionen mit, also wo die eben wirklich miteinander interagieren.

Das heißt, wenn wir das anschauen, dann sehen wir P geht mit Tau nach zu dem hier.

Und was man jetzt aussieht, ist, okay, jedes von diesen P's kann wieder einen Tau Übergang machen,

dann bekomme ich wieder weitere P's in der Parallelkomposition.

Das heißt, man sieht auf die Weise leicht ein, dass Tau-Spern-Teilmenge von P ist.

Man kann jetzt hier, wie gesagt, in jedem Zustand, der von hier aus erreichbar ist, mindestens so ein P parallel geschaltet.

Das kann wiederum eine Silent Transition machen und auf die Weise kann man beliebige Taufolgen von beliebiger Länge erzeugen.

Dann bekommen wir das Tau-Spern-Teilmenge von P ist.

Und umgekehrt können wir uns auch einfach überlegen, naja, A bleibt die ganze Zeit ausgeschlossen, also was soll da anderes rauskommen?

Das haben wir irgendwann mal, mehr oder weniger bewiesen, als Übung in Induktion über die Heratung.

Dass also ein Prozess nur diejenigen Aktionen machen kann, die er erwähnt, wobei erwähnt so ein bisschen breitgefasst werden muss.

Wenn er noch eine Umbenennung enthält, dann machen wir eine Menge von Aktionen, die unter diesen Umbenennungen abgeschlossen sind, sodass alle explizit im Grafik erlegenden Aktionen in dieser Menge drin liegen.

Wenn man das hat, dann weiß man, dass also nur die in dieser Menge liegenden Aktionen vorkommen.

Hier haben wir das noch einfache Situation, weil eben nirgendwo eine Umbenennung vorkommt, das heißt, ein Prozess ohne Umbenennung.

Da kann ein Prozess immer nur diejenigen Aktionen durchführen, die er explizit erwähnt oder taugt.

Und da alle Aktionen, die hier explizit erwähnt werden, versteckt sind, kann die nur darauf taugt.

Also es ist letztlich ein Induktionsbeweis, eine Induktion über die Heratung.

Jawohl, das war 1C. Schreiben wir vor zu zweitens. Die erste Antwort war auch relativ klar.

Diese beiden Prozesse sind stark tracerequivalent, weil sie erstens tracerequivalent sind und zweitens beide keine komplette Traces haben.

Dann fangen wir an mit Konkurrenz bezüglich Plus.

Ich habe meinen Platz gebraucht. Dann weiß ich zumindest, dass ich die Antwort richtig mache, bevor ich in der Silpester lehne.

Das haben ja alle gleich, insofern ist es egal.

Ich versuche, die Anmerkungen zu verstehen.

Vielleicht schreiben wir erstmal ein Gegenbeispiel an zu der Behauptung, die ihr alle hier beweisen.

Das ist auch eine besondere Behandlung.

Das merkt man, wenn man das Gegenbeispiel zu der Behauptung beschreibt.

Die Charakterisierung von C-Traces von A plus B, die alle beweisen haben, ist wichtig.

Wir haben alle das schon.

Wunderbar. Dann bin ich wenigstens guter Gesellschaft.

Jetzt die Behauptung, dass die C-Traces von A die C-Traces von A vereinigt mit den C-Traces von B.

Ich glaube, ich verstehe jetzt, was die Bemerkung meinte.

Wenn eins der Deadlock ist, dann ist die C-Trace Epsilon.

Aber in dem Fall ist der Deadlock ein neutrales Element.

Das heißt, dann wird nur der ausgeführt. Das taucht hier nicht auf.