Update assets/src/semantics-of-regular-expressions/Languages.dfy

Co-authored-by: Rustan Leino <leino@amazon.com>
dafny-lang · Jan 3, 2024 · 62227be · 62227be
1 parent 927cbbb
commit 62227be
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/assets/src/semantics-of-regular-expressions/Languages.dfy b/assets/src/semantics-of-regular-expressions/Languages.dfy
@@ -193,7 +193,9 @@ module Languages {
       if k != 0 {
         BisimilarCuttingPrefixesPointwise(k, a, L1, L2);
         var k' :| k == k' + 1;
-        forall n: nat ensures n <= k' + 1 ==> Bisimilar#[n](Star(L1), Star(L2)) {
+        forall n: nat
+          ensures n <= k' + 1 ==> Bisimilar#[n](Star(L1), Star(L2))
+        {
           if 0 < n <= k' + 1 {
             var n' :| n == n' + 1;
             StarCongruenceHelper(n', L1,L2);