From a9b89656fc6a3ad141e7c894ce324110052e4120 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche <120379523+stefan-aws@users.noreply.github.com> Date: Wed, 3 Jan 2024 11:26:24 +0000 Subject: [PATCH] Update assets/src/semantics-of-regular-expressions/Semantics.dfy Co-authored-by: Rustan Leino --- assets/src/semantics-of-regular-expressions/Semantics.dfy | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/assets/src/semantics-of-regular-expressions/Semantics.dfy b/assets/src/semantics-of-regular-expressions/Semantics.dfy index 278835c..cec7eab 100644 --- a/assets/src/semantics-of-regular-expressions/Semantics.dfy +++ b/assets/src/semantics-of-regular-expressions/Semantics.dfy @@ -108,7 +108,9 @@ module Semantics { lemma DenotationalIsCoalgebraHomomorphism() ensures IsCoalgebraHomomorphism(Denotational) { - forall e ensures Denotational(e).eps == Eps(e) { + forall e + ensures Denotational(e).eps == Eps(e) + { DenotationalIsCoalgebraHomomorphismHelper1(e); } forall e, a