diff --git a/src/content/blocking-queue/10-notify-nondeterministic.md b/src/content/blocking-queue/10-notify-nondeterministic.md
index a1c3c49..641daea 100644
--- a/src/content/blocking-queue/10-notify-nondeterministic.md
+++ b/src/content/blocking-queue/10-notify-nondeterministic.md
@@ -105,14 +105,3 @@ NEXT Next
 
 INVARIANT Invariant
 INVARIANT TypeInv
-
-CONSTANTS 
-    curBuf <- AliascurBuf
-    nxtBuf <- AliasnxtBuf
-    Waiting <- AliasWaiting
-    Scheduled <- AliasScheduled
-    ConsBuf <- AliasConsBuf
-    
-ALIAS AnimAlias
-
-INVARIANT AnimInv
diff --git a/src/content/blocking-queue/11-notify-all.md b/src/content/blocking-queue/11-notify-all.md
index 03657d5..8fbccce 100644
--- a/src/content/blocking-queue/11-notify-all.md
+++ b/src/content/blocking-queue/11-notify-all.md
@@ -102,14 +102,3 @@ NEXT Next
 
 INVARIANT Invariant
 INVARIANT TypeInv
-
-CONSTANTS 
-    curBuf <- AliascurBuf
-    nxtBuf <- AliasnxtBuf
-    Waiting <- AliasWaiting
-    Scheduled <- AliasScheduled
-    ConsBuf <- AliasConsBuf
-    
-ALIAS AnimAlias
-
-INVARIANT AnimInv
diff --git a/src/content/blocking-queue/12-two-mutexes.md b/src/content/blocking-queue/12-two-mutexes.md
index 4b68b69..f39035a 100644
--- a/src/content/blocking-queue/12-two-mutexes.md
+++ b/src/content/blocking-queue/12-two-mutexes.md
@@ -109,14 +109,3 @@ NEXT Next
 
 INVARIANT Invariant
 INVARIANT TypeInv
-
-CONSTANTS 
-    curBuf <- AliascurBuf
-    nxtBuf <- AliasnxtBuf
-    Waiting <- AliasWaiting
-    Scheduled <- AliasScheduled
-    ConsBuf <- AliasConsBuf
-    
-ALIAS AnimAlias
-
-INVARIANT AnimInv