diff --git a/assets/src/semantics-of-regular-expressions/Semantics.dfy b/assets/src/semantics-of-regular-expressions/Semantics.dfy index cec7eab..bd36072 100644 --- a/assets/src/semantics-of-regular-expressions/Semantics.dfy +++ b/assets/src/semantics-of-regular-expressions/Semantics.dfy @@ -98,7 +98,9 @@ module Semantics { lemma DenotationalIsAlgebraHomomorphism() ensures IsAlgebraHomomorphism(Denotational) { - forall e ensures IsAlgebraHomomorphismPointwise(Denotational, e) { + forall e + ensures IsAlgebraHomomorphismPointwise(Denotational, e) + { BisimilarityIsReflexive(Denotational(e)); } }