Skip to content

Commit

Permalink
Update assets/src/semantics-of-regular-expressions/Semantics.dfy
Browse files Browse the repository at this point in the history
Co-authored-by: Rustan Leino <[email protected]>
  • Loading branch information
stefan-aws and RustanLeino authored Jan 3, 2024
1 parent a9b8965 commit 6548587
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion assets/src/semantics-of-regular-expressions/Semantics.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,9 @@ module Semantics {
lemma DenotationalIsAlgebraHomomorphism<A(!new)>()
ensures IsAlgebraHomomorphism<A>(Denotational)
{
forall e ensures IsAlgebraHomomorphismPointwise<A>(Denotational, e) {
forall e
ensures IsAlgebraHomomorphismPointwise<A>(Denotational, e)
{
BisimilarityIsReflexive<A>(Denotational(e));
}
}
Expand Down

0 comments on commit 6548587

Please sign in to comment.