Merge pull request #379 from h4iku/sim-sent-patch

Bisimulation: Fixed a sentence
This commit is contained in:
Philip Wadler 2019-08-12 11:42:38 +01:00 committed by GitHub
commit c4ab883b02
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -232,7 +232,7 @@ where appropriate (in this case, only for the body of an abstraction).
## Simulation commutes with substitution
The third technical result is that simulation commutes with substitution.
It is more complex than substitution, because where we had one renaming map
It is more complex than renaming, because where we had one renaming map
`ρ` here we need two substitution maps, `σ` and `σ†`.
The proof first requires we establish an analogue of extension.