diff --git a/Source/Concurrency/RefinementInstrumentation.cs b/Source/Concurrency/RefinementInstrumentation.cs
index 4e5a49dac..ebc4cd1c3 100644
--- a/Source/Concurrency/RefinementInstrumentation.cs
+++ b/Source/Concurrency/RefinementInstrumentation.cs
@@ -75,13 +75,11 @@ public override List<Cmd> CreateAssertCmds()
 
         public override List<Cmd> CreateUnchangedGlobalsAssertCmds()
         {
-            var cmds = new List<Cmd>();
             var assertExpr = Expr.And(this.oldGlobalMap.Select(kvPair => Expr.Eq(Expr.Ident(kvPair.Key), Expr.Ident(kvPair.Value)))); 
             assertExpr.Typecheck(new TypecheckingContext(null));
             AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
             skipAssertCmd.ErrorData = "Globals must not be modified";
-            cmds.Add(skipAssertCmd);
-            return cmds;
+            return new List<Cmd> { skipAssertCmd };
         }
     }
 
@@ -91,8 +89,8 @@ class ActionRefinementInstrumentation : SkipRefinementInstrumentation
         private List<Variable> newLocalVars;
         private Variable pc;
         private Variable ok;
-        private Expr alpha;
-        private Expr beta;
+        private Expr gate;
+        private Expr transitionRelation;
 
         private Dictionary<AtomicAction, Expr> transitionRelationCache;
 
@@ -153,86 +151,74 @@ public ActionRefinementInstrumentation(
 
             Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap);
             Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);
-            Expr betaExpr = GetTransitionRelation(atomicAction);
-            beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);
-            Expr alphaExpr = Expr.And(atomicAction.gate.Select(g => g.Expr));
-            alphaExpr.Type = Type.Bool;
-            alpha = Substituter.Apply(always, alphaExpr);
+            Expr transitionRelationExpr = GetTransitionRelation(atomicAction);
+            transitionRelation = Substituter.ApplyReplacingOldExprs(always, forold, transitionRelationExpr);
+            Expr gateExpr = Expr.And(atomicAction.gate.Select(g => g.Expr));
+            gateExpr.Type = Type.Bool;
+            gate = Substituter.Apply(always, gateExpr);
         }
 
         public override List<Variable> NewLocalVars => newLocalVars;
 
         public override List<Cmd> CreateInitCmds()
         {
-            var cmds = new List<Cmd>();
-            List<AssignLhs> lhss = new List<AssignLhs>();
-            List<Expr> rhss = new List<Expr>();
-            lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)));
-            rhss.Add(Expr.False);
-            lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok)));
-            rhss.Add(Expr.False);
-            cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
+            List<AssignLhs> lhss = new List<AssignLhs> {
+                new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)),
+                new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))
+            };
+            List<Expr> rhss = new List<Expr> { Expr.False, Expr.False };
+            var cmds = new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) };
             cmds.AddRange(CreateUpdatesToOldOutputVars());
             return cmds;
         }
 
         public override List<Cmd> CreateAssumeCmds()
         {
-            var cmds = new List<Cmd>();
-            // assume pc || alpha(i, g);
-            Expr assumeExpr = Expr.Or(Expr.Ident(pc), alpha);
+            // assume pc || gate(i, g);
+            Expr assumeExpr = Expr.Or(Expr.Ident(pc), gate);
             assumeExpr.Type = Type.Bool;
-            cmds.Add(new AssumeCmd(Token.NoToken, assumeExpr));
-            return cmds;
+            return new List<Cmd> { new AssumeCmd(Token.NoToken, assumeExpr) };
         }
 
         public override List<Cmd> CreateAssertCmds()
         {
             Expr assertExpr;
-            var cmds = new List<Cmd>();
 
-            // assert pc || g_old == g || beta(i, g_old, o, g);
-            assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(OldEqualityExprForGlobals(), beta));
+            // assert pc || g_old == g || transitionRelation(i, g_old, o, g);
+            assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(OldEqualityExprForGlobals(), transitionRelation));
             assertExpr.Typecheck(new TypecheckingContext(null));
-            var skipOrBetaAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
-            skipOrBetaAssertCmd.ErrorData = "Transition invariant violated in initial state";
-            cmds.Add(skipOrBetaAssertCmd);
+            var skipOrTransitionRelationAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
+            skipOrTransitionRelationAssertCmd.ErrorData = "Transition invariant violated in initial state";
 
-            // assert pc ==> o_old == o && g_old == g;
-            assertExpr = Expr.Imp(Expr.Ident(pc), OldEqualityExpr());
+            // assert pc ==> g_old == g && o_old == o;
+            assertExpr = Expr.Imp(Expr.Ident(pc), Expr.And(OldEqualityExprForGlobals(), OldEqualityExprForOutputs()));
             assertExpr.Typecheck(new TypecheckingContext(null));
             AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
             skipAssertCmd.ErrorData = "Transition invariant violated in final state";
-            cmds.Add(skipAssertCmd);
-            return cmds;
+            return new List<Cmd> { skipOrTransitionRelationAssertCmd, skipAssertCmd };
         }
 
         public override List<Cmd> CreateReturnAssertCmds()
         {
-            var cmds = CreateUnchangedOutputsAssertCmds();
             AssertCmd assertCmd = new AssertCmd(Token.NoToken, Expr.Ident(ok));
             assertCmd.ErrorData = "Failed to execute atomic action before procedure return";
-            cmds.Add(assertCmd);
-            return cmds;
+            return new List<Cmd> { assertCmd };
         }
 
         public override List<Cmd> CreateUnchangedOutputsAssertCmds()
         {
             // assert pc ==> o_old == o;
-            var cmds = new List<Cmd>();
-            Expr bb = OldEqualityExprForOutputs();
-            var assertExpr = Expr.Imp(Expr.Ident(pc), bb);
+            var assertExpr = Expr.Imp(Expr.Ident(pc), OldEqualityExprForOutputs());
             assertExpr.Typecheck(new TypecheckingContext(null));
             AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr);
             skipAssertCmd.ErrorData = "Outputs must not be modified";
-            cmds.Add(skipAssertCmd);
-            return cmds;
+            return new List<Cmd> { skipAssertCmd };
         }
 
         public override List<Cmd> CreateUpdatesToRefinementVars()
         {
-            // pc, ok := g_old == g ==> pc, beta(i, g_old, o, g) || o_old == o && ok;
-            Expr aa = OldEqualityExprForGlobals();
+            // pc := g_old == g ==> pc;
+            // ok := transitionRelation(i, g_old, o, g) || (o_old == o && ok);
             List<AssignLhs> pcUpdateLHS = new List<AssignLhs>
             {
                 new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc)),
@@ -241,14 +227,14 @@ public override List<Cmd> CreateUpdatesToRefinementVars()
             List<Expr> pcUpdateRHS = new List<Expr>(
                 new Expr[]
                 {
-                    Expr.Imp(aa, Expr.Ident(pc)),
-                    Expr.Or(beta, Expr.And(OldEqualityExprForOutputs(), Expr.Ident(ok))),
+                    Expr.Imp(OldEqualityExprForGlobals(), Expr.Ident(pc)),
+                    Expr.Or(transitionRelation, Expr.And(OldEqualityExprForOutputs(), Expr.Ident(ok))),
                 });
             foreach (Expr e in pcUpdateRHS)
             {
                 e.Typecheck(new TypecheckingContext(null));
             }
-            return new List<Cmd> {new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS)};
+            return new List<Cmd> { new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS) };
         }
 
         public override List<Cmd> CreateUpdatesToOldOutputVars()
@@ -260,12 +246,7 @@ public override List<Cmd> CreateUpdatesToOldOutputVars()
                 lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(oldOutputMap[o])));
                 rhss.Add(Expr.Ident(o));
             }
-            var cmds = new List<Cmd>();
-            if (lhss.Count > 0)
-            {
-                cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
-            }
-            return cmds;
+            return lhss.Count > 0 ? new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) } : new List<Cmd>();
         }
 
         private Expr GetTransitionRelation(AtomicAction atomicAction)
@@ -279,11 +260,6 @@ private Expr GetTransitionRelation(AtomicAction atomicAction)
             return transitionRelationCache[atomicAction];
         }
 
-        private Expr OldEqualityExpr()
-        {
-            return Expr.And(OldEqualityExprForGlobals(), OldEqualityExprForOutputs());
-        }
-
         private Expr OldEqualityExprForGlobals()
         {
             return Expr.And(this.oldGlobalMap.Select(kvPair => Expr.Eq(Expr.Ident(kvPair.Key), Expr.Ident(kvPair.Value))));