Om in AFA te laten zien dat twee knopen dezelfde kleuring hebben kan men gebruik maken van het begrip bisimulatie. In week twee van dit college hebben we hier ook over gesproken.

Definitie Bisimulatie Zijn G_{1} en G_{2} twee gelabelde grafen zoals we die in de AFA setting gebruiken om (niet wel-gefundeerde) verzamelingen te beschrijven. Een relatie ≡ tussen de knopen van G_{1} en de knopen van G_{2} is een bisimulatie als aan de drie volgende eisen is voldaan:

Blad Als g_{1} ∈ G_{1} een blad is met label a, en g_{1} ≡ g_{2}, dan is g_{2} ∈ G_{2} ook een blad met dezelfde labeling i. e. a en vice versa. (In plaats van te spreken over een knoop zonder labeling spreken wij over een knoop met de lege verzameling als labeling.)

Zig Als g_{1} ≡ g_{2} en g_{1} → g′_{1}, dan is er een g′_{2} ∈ G_{2} met g_{2} → g′_{2} zó dat g′_{1} ≡ g′_{2}.

Zag Als g_{1} ≡ g_{2} en g_{2} → g′_{2}, dan is er een g′_{1} ∈ G_{1} met g_{1} → g′_{1} zó dat g′_{1} ≡ g′_{2}.

We zeggen dat G_{1} en G_{2} bisimulair zijn als er een bisimulatie tussen G_{1} en G_{2} bestaat (er kunnen er meerderen zijn) en we schrijven in dit geval G_{1} ≡ G_{2}. Op het college hebben we de volgende stelling behandeld.

Stelling over gelijkheid van verzamelingen Zijn G_{1} en G_{2} twee gelabelde grafen zoals we die in de AFA setting gebruiken om (niet wel-gefundeerde) verzamelingen te beschrijven. g_{1} ∈ G_{1} en g_{2} ∈ G_{2} hebben dezelfde labeling desda er een bisimulatie ≡_{0} is tussen G_{1} en G_{2} zó dat g_{1} ≡_{0} g_{2}.