pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

typo

Browse source
This commit is contained in:
Samuel Gruetter 2020-04-12 21:36:38 -04:00
parent 8a554ded4c
commit 1cc82281bf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
MessagesAndRefinement.v
View file

@ -205,7 +205,7 @@ Definition simulates (R : proc -> proc -> Prop) (pr1 pr2 : proc) :=
-> exists pr2', lstepSilent^* pr2 pr2' -> exists pr2', lstepSilent^* pr2 pr2'
/\ R pr1' pr2') /\ R pr1' pr2')
(* Now consider the same scenario where the lefthand process make a nonsilent (* Now consider the same scenario where the lefthand process takes a nonsilent
* step. We require that the righthand process can "catch up" in a way that * step. We require that the righthand process can "catch up" in a way that
* generates the same label that the lefthand process generated. *) * generates the same label that the lefthand process generated. *)
/\ (forall pr1 pr2, R pr1 pr2 /\ (forall pr1 pr2, R pr1 pr2