Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma")

28 files changed, 342 insertions, 338 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 9aca7306..452c71e4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -567,8 +567,8 @@ namespace Microsoft.Dafny
       if (m is Constructor) {

         return new Constructor(Tok(m.tok), m.Name, tps, ins,

           req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

-      } else if (m is CoMethod) {

-        return new CoMethod(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

+      } else if (m is CoLemma) {

+        return new CoLemma(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

           req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);

       } else if (m is Lemma) {

         return new Lemma(Tok(m.tok), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

@@ -584,8 +584,8 @@ namespace Microsoft.Dafny
   }

 

   /// <summary>

-  /// Subclass of Cloner that collects some common functionality between CoMethodPostconditionSubstituter and

-  /// CoMethodBodyCloner.

+  /// Subclass of Cloner that collects some common functionality between CoLemmaPostconditionSubstituter and

+  /// CoLemmaBodyCloner.

   /// </summary>

   abstract class CoCloner : Cloner

   {

@@ -609,16 +609,16 @@ namespace Microsoft.Dafny
   }

 

   /// <summary>

-  /// The CoMethodPostconditionSubstituter clones the postcondition declared on a comethod, but replaces

+  /// The CoLemmaPostconditionSubstituter clones the postcondition declared on a colemma, but replaces

   /// the calls and equalities in "coConclusions" with corresponding prefix versions.  The resulting

-  /// expression is then appropriate to be a postcondition of the comethod's corresponding prefix method.

+  /// expression is then appropriate to be a postcondition of the colemma's corresponding prefix lemma.

   /// It is assumed that the source expression has been resolved.  Note, the "k" given to the constructor

   /// is not cloned with each use; it is simply used as is.

   /// </summary>

-  class CoMethodPostconditionSubstituter : CoCloner

+  class CoLemmaPostconditionSubstituter : CoCloner

   {

     readonly ISet<Expression> coConclusions;

-    public CoMethodPostconditionSubstituter(ISet<Expression> coConclusions, Expression k, Resolver resolver)

+    public CoLemmaPostconditionSubstituter(ISet<Expression> coConclusions, Expression k, Resolver resolver)

       : base(k, resolver)

     {

       Contract.Requires(coConclusions != null);

@@ -660,13 +660,13 @@ namespace Microsoft.Dafny
   }

 

   /// <summary>

-  /// The task of the CoMethodBodyCloner is to fill in the implicit _k-1 arguments in corecursive comethod calls.

+  /// The task of the CoLemmaBodyCloner is to fill in the implicit _k-1 arguments in corecursive colemma calls.

   /// The source statement and the given "k" are assumed to have been resolved, and the resulting statement will also be resolved.

   /// </summary>

-  class CoMethodBodyCloner : CoCloner

+  class CoLemmaBodyCloner : CoCloner

   {

-    readonly CoMethod context;

-    public CoMethodBodyCloner(CoMethod context, Expression k, Resolver resolver)

+    readonly CoLemma context;

+    public CoLemmaBodyCloner(CoLemma context, Expression k, Resolver resolver)

       : base(k, resolver)

     {

       Contract.Requires(context != null);

@@ -681,8 +681,8 @@ namespace Microsoft.Dafny
           var call = (CallStmt)s.ResolvedStatements[0];

           var moduleCaller = context.EnclosingClass.Module;

           var moduleCallee = call.Method.EnclosingClass.Module;

-          if (call.Method is CoMethod && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(call.Method)) {

-            // we're looking at a recursive call to a comethod

+          if (call.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(call.Method)) {

+            // we're looking at a recursive call to a colemma

             var args = new List<Expression>();

             args.Add(k);

             foreach (var arg in call.Args) {

@@ -699,11 +699,11 @@ namespace Microsoft.Dafny
         }

       } else if (stmt is CallStmt) {

         var s = (CallStmt)stmt;

-        if (s.Method is CoMethod) {

+        if (s.Method is CoLemma) {

           var moduleCaller = context.EnclosingClass.Module;

           var moduleCallee = s.Method.EnclosingClass.Module;

-          if (s.Method is CoMethod && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

-            // we're looking at a recursive call to a comethod

+          if (s.Method is CoLemma && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

+            // we're looking at a recursive call to a colemma

             var args = new List<Expression>();

             args.Add(k);

             foreach (var arg in s.Args) {

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 51a4785b..563c1d6c 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -559,7 +559,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      BlockStmt body = null;

      bool isLemma = false;

      bool isConstructor = false;

-     bool isCoMethod = false;

+     bool isCoLemma = false;

      IToken signatureEllipsis = null;

      IToken bodyStart = Token.NoToken;

      IToken bodyEnd = Token.NoToken;

@@ -567,8 +567,10 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
   SYNC

   ( "method"

   | "lemma"                         (. isLemma = true; .)

-  | "comethod"                      (. isCoMethod = true; .)

-  | "colemma"                       (. isCoMethod = true; .)

+  | "colemma"                       (. isCoLemma = true; .)

+  | "comethod"                      (. isCoLemma = true;

+                                       errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");

+                                    .)

   | "constructor"                   (. if (allowConstructor) {

                                          isConstructor = true;

                                        } else {

@@ -587,9 +589,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
        if (mmod.IsStatic) {

          SemErr(t, "constructors cannot be declared 'static'");

        }

-     } else if (isCoMethod) {

+     } else if (isCoLemma) {

        if (mmod.IsGhost) {

-         SemErr(t, "comethods cannot be declared 'ghost' (they are automatically 'ghost')");

+         SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')");

        }

      }

   .)

@@ -636,9 +638,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      if (isConstructor) {

        m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

                            req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

-     } else if (isCoMethod) {

-       m = new CoMethod(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

-                      req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

+     } else if (isCoLemma) {

+       m = new CoLemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

+                       req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

      } else if (isLemma) {

        m = new Lemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

                      req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index f29242ab..eee1b06f 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1124,8 +1124,8 @@ namespace Microsoft.Dafny {
     /// declarations.

     /// Note, an iterator declaration is a class, in this sense.

     /// Note, if the given list are the top-level declarations of a module, the yield will include

-    /// co-methods but not their associated prefix methods (which are tucked into the co-method's

-    /// .PrefixMethod field).

+    /// colemmas but not their associated prefix lemmas (which are tucked into the colemma's

+    /// .PrefixLemma field).

     /// </summary>

     public static IEnumerable<ICallable> AllCallables(List<TopLevelDecl> declarations) {

       foreach (var d in declarations) {

@@ -1171,12 +1171,12 @@ namespace Microsoft.Dafny {
       }

     }

 

-      public static IEnumerable<CoMethod> AllCoMethods(List<TopLevelDecl> declarations) {

+      public static IEnumerable<CoLemma> AllCoLemmas(List<TopLevelDecl> declarations) {

       foreach (var d in declarations) {

         var cl = d as ClassDecl;

         if (cl != null) {

           foreach (var member in cl.Members) {

-            var m = member as CoMethod;

+            var m = member as CoLemma;

             if (m != null) {

               yield return m;

             }

@@ -1950,7 +1950,7 @@ namespace Microsoft.Dafny {
 

   /// <summary>

   /// An ImplicitFormal is a parameter that is declared implicitly, in particular the "_k" depth parameter

-  /// of each comethod (for use in the comethod body only, not the specification).

+  /// of each colemma (for use in the comethod body only, not the specification).

   /// </summary>

   public class ImplicitFormal : Formal

   {

@@ -2257,16 +2257,16 @@ namespace Microsoft.Dafny {
   }

 

   /// <summary>

-  /// An PrefixPredicate is the inductive unrolling P# implicitly declared for every copredicate P.

+  /// A PrefixLemma is the inductive unrolling M# implicitly declared for every colemma M.

   /// </summary>

-  public class PrefixMethod : Method

+  public class PrefixLemma : Method

   {

     public readonly Formal K;

-    public readonly CoMethod Co;

-    public PrefixMethod(IToken tok, string name, bool isStatic,

-                        List<TypeParameter> typeArgs, Formal k, List<Formal> ins, List<Formal> outs,

-                        List<MaybeFreeExpression> req, Specification<FrameExpression> mod, List<MaybeFreeExpression> ens, Specification<Expression> decreases,

-                        BlockStmt body, Attributes attributes, CoMethod co)

+    public readonly CoLemma Co;

+    public PrefixLemma(IToken tok, string name, bool isStatic,

+                       List<TypeParameter> typeArgs, Formal k, List<Formal> ins, List<Formal> outs,

+                       List<MaybeFreeExpression> req, Specification<FrameExpression> mod, List<MaybeFreeExpression> ens, Specification<Expression> decreases,

+                       BlockStmt body, Attributes attributes, CoLemma co)

       : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) {

       Contract.Requires(k != null);

       Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k);

@@ -2276,19 +2276,19 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class CoMethod : Method

+  public class CoLemma : Method

   {

-    public PrefixMethod PrefixMethod;  // filled in during resolution (name registration)

-

-    public CoMethod(IToken tok, string name,

-                  bool isStatic,

-                  List<TypeParameter> typeArgs,

-                  List<Formal> ins, [Captured] List<Formal> outs,

-                  List<MaybeFreeExpression> req, [Captured] Specification<FrameExpression> mod,

-                  List<MaybeFreeExpression> ens,

-                  Specification<Expression> decreases,

-                  BlockStmt body,

-                  Attributes attributes, IToken signatureEllipsis)

+    public PrefixLemma PrefixLemma;  // filled in during resolution (name registration)

+

+    public CoLemma(IToken tok, string name,

+                   bool isStatic,

+                   List<TypeParameter> typeArgs,

+                   List<Formal> ins, [Captured] List<Formal> outs,

+                   List<MaybeFreeExpression> req, [Captured] Specification<FrameExpression> mod,

+                   List<MaybeFreeExpression> ens,

+                   Specification<Expression> decreases,

+                   BlockStmt body,

+                   Attributes attributes, IToken signatureEllipsis)

       : base(tok, name, isStatic, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {

       Contract.Requires(tok != null);

       Contract.Requires(name != null);

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d064606f..a52d840c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -860,7 +860,7 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		BlockStmt body = null;

 		bool isLemma = false;

 		bool isConstructor = false;

-		bool isCoMethod = false;

+		bool isCoLemma = false;

 		IToken signatureEllipsis = null;

 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

@@ -873,10 +873,12 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 			isLemma = true; 

 		} else if (la.kind == 42) {

 			Get();

-			isCoMethod = true; 

+			isCoLemma = true; 

 		} else if (la.kind == 43) {

 			Get();

-			isCoMethod = true; 

+			isCoLemma = true;

+			errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");

+			

 		} else if (la.kind == 44) {

 			Get();

 			if (allowConstructor) {

@@ -898,9 +900,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		 if (mmod.IsStatic) {

 		   SemErr(t, "constructors cannot be declared 'static'");

 		 }

-		} else if (isCoMethod) {

+		} else if (isCoLemma) {

 		 if (mmod.IsGhost) {

-		   SemErr(t, "comethods cannot be declared 'ghost' (they are automatically 'ghost')");

+		   SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')");

 		 }

 		}

 		

@@ -959,9 +961,9 @@ bool SemiFollowsCall(bool allowSemi, Expression e) {
 		if (isConstructor) {

 		 m = new Constructor(id, hasName ? id.val : "_ctor", typeArgs, ins,

 		                     req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

-		} else if (isCoMethod) {

-		 m = new CoMethod(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

-		                req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

+		} else if (isCoLemma) {

+		 m = new CoLemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

+		                 req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

 		} else if (isLemma) {

 		 m = new Lemma(id, id.val, mmod.IsStatic, typeArgs, ins, outs,

 		               req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);

@@ -3687,8 +3689,8 @@ public class Errors {
 			case 39: s = "\">\" expected"; break;

 			case 40: s = "\"method\" expected"; break;

 			case 41: s = "\"lemma\" expected"; break;

-			case 42: s = "\"comethod\" expected"; break;

-			case 43: s = "\"colemma\" expected"; break;

+			case 42: s = "\"colemma\" expected"; break;

+			case 43: s = "\"comethod\" expected"; break;

 			case 44: s = "\"constructor\" expected"; break;

 			case 45: s = "\"modifies\" expected"; break;

 			case 46: s = "\"free\" expected"; break;

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 601c5761..a5057286 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -267,10 +267,10 @@ namespace Microsoft.Dafny {
         if (m is Method) {

           if (state != 0) { wr.WriteLine(); }

           PrintMethod((Method)m, indent, false);

-          var com = m as CoMethod;

-          if (com != null && com.PrefixMethod != null) {

+          var com = m as CoLemma;

+          if (com != null && com.PrefixLemma != null) {

             Indent(indent); wr.WriteLine("/***");

-            PrintMethod(com.PrefixMethod, indent, false);

+            PrintMethod(com.PrefixLemma, indent, false);

             Indent(indent); wr.WriteLine("***/");

           }

           state = 2;

@@ -441,9 +441,9 @@ namespace Microsoft.Dafny {
       Contract.Requires(method != null);

 

       Indent(indent);

-      string k = method is Constructor ? "constructor" : method is CoMethod ? "comethod" : method is Lemma ? "lemma" : "method";

+      string k = method is Constructor ? "constructor" : method is CoLemma ? "colemma" : method is Lemma ? "lemma" : "method";

       if (method.IsStatic) { k = "static " + k; }

-      if (method.IsGhost && !(method is Lemma) && !(method is CoMethod)) { k = "ghost " + k; }

+      if (method.IsGhost && !(method is Lemma) && !(method is CoLemma)) { k = "ghost " + k; }

       string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name;

       PrintClassMethodHelper(k, method.Attributes, nm, method.TypeArgs);

       if (method.SignatureIsOmitted) {

diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index acee1845..75dbaad3 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -564,8 +564,8 @@ namespace Microsoft.Dafny
       if (m is Constructor) {

         return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins,

           req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);

-      } else if (m is CoMethod) {

-        return new CoMethod(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),

+      } else if (m is CoLemma) {

+        return new CoLemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),

           req, mod, ens, decreases, body, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null);

       } else if (m is Lemma) {

         return new Lemma(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(refinementCloner.CloneFormal),

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 564e4164..2262c4da 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -354,22 +354,22 @@ namespace Microsoft.Dafny
         foreach (var clbl in ModuleDefinition.AllCallables(module.TopLevelDecls)) {

           ICallable m;

           string s;

-          if (clbl is CoMethod) {

-            var prefixMethod = ((CoMethod)clbl).PrefixMethod;

-            m = prefixMethod;

-            s = prefixMethod.Name + " ";

+          if (clbl is CoLemma) {

+            var prefixLemma = ((CoLemma)clbl).PrefixLemma;

+            m = prefixLemma;

+            s = prefixLemma.Name + " ";

           } else {

             m = clbl;

             s = "";

           }

           FillInDefaultDecreases(m);

 

-          if (m.InferredDecreases || m is PrefixMethod) {

+          if (m.InferredDecreases || m is PrefixLemma) {

             bool showIt = false;

             if (m is Function) {

               // show the inferred decreases clause only if it will ever matter, i.e., if the function is recursive

               showIt = ((Function)m).IsRecursive;

-            } else if (m is PrefixMethod) {

+            } else if (m is PrefixLemma) {

               // always show the decrease clause, since at the very least it will start with "_k", which the programmer did not write explicitly

               showIt = true;

             } else {

@@ -386,7 +386,7 @@ namespace Microsoft.Dafny
               }

               s += ";";  // always terminate with a semi-colon, even in the case of an empty decreases clause

               // Note, in the following line, we use the location information for "clbl", not "m".  These

-              // are the same, except in the case where "clbl" is a CoMethod and "m" is a prefix method.

+              // are the same, except in the case where "clbl" is a CoLemma and "m" is a prefix lemma.

               ReportAdditionalInformation(clbl.Tok, s, clbl.Tok.val.Length);

             }

           }

@@ -402,7 +402,7 @@ namespace Microsoft.Dafny
         return;

       }

       var decr = clbl.Decreases.Expressions;

-      if (decr.Count == 0 || (clbl is PrefixMethod && decr.Count == 1)) {

+      if (decr.Count == 0 || (clbl is PrefixLemma && decr.Count == 1)) {

         // The default for a function starts with the function's reads clause, if any

         if (clbl is Function) {

           var fn = (Function)clbl;

@@ -853,7 +853,7 @@ namespace Microsoft.Dafny
           foreach (MemberDecl m in cl.Members) {

             if (!members.ContainsKey(m.Name)) {

               members.Add(m.Name, m);

-              if (m is CoPredicate || m is CoMethod) {

+              if (m is CoPredicate || m is CoLemma) {

                 var extraName = m.Name + "#";

                 MemberDecl extraMember;

                 var cloner = new Cloner();

@@ -873,24 +873,24 @@ namespace Microsoft.Dafny
                   // In the call graph, add an edge from P# to P, since this will have the desired effect of detecting unwanted cycles.

                   moduleDef.CallGraph.AddEdge(cop.PrefixPredicate, cop);

                 } else {

-                  var com = (CoMethod)m;

+                  var com = (CoLemma)m;

                   // _k has already been added to 'formals', so append the original formals

                   formals.AddRange(com.Ins.ConvertAll(cloner.CloneFormal));

                   // prepend _k to the given decreases clause

                   var decr = new List<Expression>();

                   decr.Add(new IdentifierExpr(com.tok, k.Name));

                   decr.AddRange(com.Decreases.Expressions.ConvertAll(cloner.CloneExpr));

-                  // Create prefix method.  Note that the body is not cloned, but simply shared.

-                  com.PrefixMethod = new PrefixMethod(com.tok, extraName, com.IsStatic,

+                  // Create prefix lemma.  Note that the body is not cloned, but simply shared.

+                  com.PrefixLemma = new PrefixLemma(com.tok, extraName, com.IsStatic,

                     com.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, com.Outs.ConvertAll(cloner.CloneFormal),

                     com.Req.ConvertAll(cloner.CloneMayBeFreeExpr), cloner.CloneSpecFrameExpr(com.Mod),

-                    new List<MaybeFreeExpression>(),  // Note, the postconditions are filled in after the comethod's postconditions have been resolved

+                    new List<MaybeFreeExpression>(),  // Note, the postconditions are filled in after the colemma's postconditions have been resolved

                     new Specification<Expression>(decr, null),

-                    null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the comethod is known

+                    null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the colemma is known

                     cloner.CloneAttributes(com.Attributes), com);

-                  extraMember = com.PrefixMethod;

+                  extraMember = com.PrefixLemma;

                   // In the call graph, add an edge from M# to M, since this will have the desired effect of detecting unwanted cycles.

-                  moduleDef.CallGraph.AddEdge(com.PrefixMethod, com);

+                  moduleDef.CallGraph.AddEdge(com.PrefixLemma, com);

                 }

                 members.Add(extraName, extraMember);

               }

@@ -1119,8 +1119,8 @@ namespace Microsoft.Dafny
       if (m is Constructor) {

         return new Constructor(m.tok, m.Name, tps, ins,

           req, mod, ens, decreases, null, null, null);

-      } else if (m is CoMethod) {

-        return new CoMethod(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

+      } else if (m is CoLemma) {

+        return new CoLemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

           req, mod, ens, decreases, null, null, null);

       } else if (m is Lemma) {

         return new Lemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

@@ -1414,40 +1414,40 @@ namespace Microsoft.Dafny
       }

 

       if (ErrorCount == prevErrorCount) {

-        // fill in the postconditions and bodies of prefix methods

-        foreach (var com in ModuleDefinition.AllCoMethods(declarations)) {

-          var prefixMethod = com.PrefixMethod;

-          if (prefixMethod == null) {

-            continue;  // something went wrong during registration of the prefix method (probably a duplicated comethod name)

-          }

-          Contract.Assume(prefixMethod.Ens.Count == 0 && prefixMethod.Body == null);  // there are not supposed have have been filled in before

-          // compute the postconditions of the prefix method

-          var k = prefixMethod.Ins[0];

+        // fill in the postconditions and bodies of prefix lemmas

+        foreach (var com in ModuleDefinition.AllCoLemmas(declarations)) {

+          var prefixLemma = com.PrefixLemma;

+          if (prefixLemma == null) {

+            continue;  // something went wrong during registration of the prefix lemma (probably a duplicated colemma name)

+          }

+          Contract.Assume(prefixLemma.Ens.Count == 0 && prefixLemma.Body == null);  // there are not supposed have have been filled in before

+          // compute the postconditions of the prefix lemma

+          var k = prefixLemma.Ins[0];

           foreach (var p in com.Ens) {

             var coConclusions = new HashSet<Expression>();

-            CheckCoMethodConclusions(p.E, true, coConclusions);

-            var subst = new CoMethodPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this);

+            CheckCoLemmaConclusions(p.E, true, coConclusions);

+            var subst = new CoLemmaPostconditionSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this);

             var post = subst.CloneExpr(p.E);

-            prefixMethod.Ens.Add(new MaybeFreeExpression(post, p.IsFree));

+            prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree));

           }

-          // Compute the statement body of the prefix method

+          // Compute the statement body of the prefix lemma

           if (com.Body != null) {

             var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1));

-            var subst = new CoMethodBodyCloner(com, kMinusOne, this);

+            var subst = new CoLemmaBodyCloner(com, kMinusOne, this);

             var mainBody = subst.CloneBlockStmt(com.Body);

             var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name));

             var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, kPositive, mainBody, null);

-            prefixMethod.Body = new BlockStmt(com.tok, condBody.EndTok, new List<Statement>() { condBody });

+            prefixLemma.Body = new BlockStmt(com.tok, condBody.EndTok, new List<Statement>() { condBody });

           }

-          // The prefix method now has all its components, so it's finally time we resolve it

-          currentClass = (ClassDecl)prefixMethod.EnclosingClass;

+          // The prefix lemma now has all its components, so it's finally time we resolve it

+          currentClass = (ClassDecl)prefixLemma.EnclosingClass;

           allTypeParameters.PushMarker();

           ResolveTypeParameters(currentClass.TypeArgs, false, currentClass);

-          ResolveTypeParameters(prefixMethod.TypeArgs, false, prefixMethod);

-          ResolveMethod(prefixMethod);

+          ResolveTypeParameters(prefixLemma.TypeArgs, false, prefixLemma);

+          ResolveMethod(prefixLemma);

           allTypeParameters.PopMarker();

           currentClass = null;

-          CheckTypeInference_Member(prefixMethod);

+          CheckTypeInference_Member(prefixLemma);

         }

       }

 

@@ -1666,7 +1666,7 @@ namespace Microsoft.Dafny
           }

         }

         // Check that copredicates are not recursive with non-copredicate functions, and

-        // check that comethods are not recursive with non-comethod methods.

+        // check that colemmas are not recursive with non-colemma methods.

         foreach (var d in declarations) {

           if (d is ClassDecl) {

             foreach (var member in ((ClassDecl)d).Members) {

@@ -1684,10 +1684,10 @@ namespace Microsoft.Dafny
                 if (fn.Body != null) {

                   CoPredicateChecks(fn.Body, fn, CallingPosition.Positive);

                 }

-              } else if (member is CoMethod) {

-                var m = (CoMethod)member;

+              } else if (member is CoLemma) {

+                var m = (CoLemma)member;

                 if (m.Body != null) {

-                  CoMethodChecks(m.Body, m);

+                  CoLemmaChecks(m.Body, m);

                 }

               }

             }

@@ -2160,13 +2160,13 @@ namespace Microsoft.Dafny
     #endregion CoPredicateChecks

 

     // ------------------------------------------------------------------------------------------------------

-    // ----- CoMethodChecks ---------------------------------------------------------------------------------

+    // ----- CoLemmaChecks ----------------------------------------------------------------------------------

     // ------------------------------------------------------------------------------------------------------

-    #region CoMethodChecks

-    class CoMethodChecks_Visitor : ResolverBottomUpVisitor

+    #region CoLemmaChecks

+    class CoLemmaChecks_Visitor : ResolverBottomUpVisitor

     {

-      CoMethod context;

-      public CoMethodChecks_Visitor(Resolver resolver, CoMethod context)

+      CoLemma context;

+      public CoLemmaChecks_Visitor(Resolver resolver, CoLemma context)

         : base(resolver) {

         Contract.Requires(resolver != null);

         Contract.Requires(context != null);

@@ -2175,15 +2175,15 @@ namespace Microsoft.Dafny
       protected override void VisitOneStmt(Statement stmt) {

         if (stmt is CallStmt) {

           var s = (CallStmt)stmt;

-          if (s.Method is CoMethod || s.Method is PrefixMethod) {

+          if (s.Method is CoLemma || s.Method is PrefixLemma) {

             // all is cool

           } else {

-            // the call goes from a comethod context to a non-comethod callee

+            // the call goes from a colemma context to a non-colemma callee

             var moduleCaller = context.EnclosingClass.Module;

             var moduleCallee = s.Method.EnclosingClass.Module;

             if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

-              // we're looking at a recursive call (to a non-comethod)

-              Error(s.Tok, "a recursive call from a comethod can go only to other comethods and prefix methods");

+              // we're looking at a recursive call (to a non-colemma)

+              Error(s.Tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas");

             }

           }

         }

@@ -2192,23 +2192,23 @@ namespace Microsoft.Dafny
       {

         if (expr is FunctionCallExpr) {

           var e = (FunctionCallExpr)expr;

-          // the call goes from a comethod context to a non-comethod callee

+          // the call goes from a colemma context to a non-colemma callee

           var moduleCaller = context.EnclosingClass.Module;

           var moduleCallee = e.Function.EnclosingClass.Module;

           if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(e.Function)) {

-            // we're looking at a recursive call (to a non-comethod)

-            Error(e.tok, "a recursive call from a comethod can go only to other comethods and prefix methods");

+            // we're looking at a recursive call (to a non-colemma)

+            Error(e.tok, "a recursive call from a colemma can go only to other colemmas and prefix lemmas");

           }

         }

       }

     }

-    void CoMethodChecks(Statement stmt, CoMethod context) {

+    void CoLemmaChecks(Statement stmt, CoLemma context) {

       Contract.Requires(stmt != null);

       Contract.Requires(context != null);

-      var v = new CoMethodChecks_Visitor(this, context);

+      var v = new CoLemmaChecks_Visitor(this, context);

       v.Visit(stmt);

     }

-    #endregion CoMethodChecks

+    #endregion CoLemmaChecks

 

     // ------------------------------------------------------------------------------------------------------

     // ----- CheckEqualityTypes -----------------------------------------------------------------------------

@@ -2582,10 +2582,10 @@ namespace Microsoft.Dafny
           ResolveTypeParameters(m.TypeArgs, true, m);

           ResolveMethodSignature(m);

           allTypeParameters.PopMarker();

-          var com = m as CoMethod;

-          if (com != null && com.PrefixMethod != null && ec == ErrorCount) {

-            var mm = com.PrefixMethod;

-            // resolve signature of the prefix method

+          var com = m as CoLemma;

+          if (com != null && com.PrefixLemma != null && ec == ErrorCount) {

+            var mm = com.PrefixLemma;

+            // resolve signature of the prefix lemma

             mm.EnclosingClass = cl;

             allTypeParameters.PushMarker();

             ResolveTypeParameters(mm.TypeArgs, true, mm);

@@ -3091,8 +3091,8 @@ namespace Microsoft.Dafny
         ResolveFrameExpression(fe, "modifies", m);

         if (m is Lemma) {

           Error(fe.tok, "lemmas are not allowed to have modifies clauses");

-        } else if (m is CoMethod) {

-          Error(fe.tok, "comethods are not allowed to have modifies clauses");

+        } else if (m is CoLemma) {

+          Error(fe.tok, "colemmas are not allowed to have modifies clauses");

         }

       }

       foreach (Expression e in m.Decreases.Expressions) {

@@ -3106,8 +3106,8 @@ namespace Microsoft.Dafny
       // Add out-parameters to a new scope that will also include the outermost-level locals of the body

       // Don't care about any duplication errors among the out-parameters, since they have already been reported

       scope.PushMarker();

-      if (m is CoMethod && m.Outs.Count != 0) {

-        Error(m.Outs[0].tok, "comethods are not allowed to have out-parameters");

+      if (m is CoLemma && m.Outs.Count != 0) {

+        Error(m.Outs[0].tok, "colemmas are not allowed to have out-parameters");

       } else {

         foreach (Formal p in m.Outs) {

           scope.Push(p.Name, p);

@@ -3125,18 +3125,18 @@ namespace Microsoft.Dafny
 

       // Resolve body

       if (m.Body != null) {

-        var com = m as CoMethod;

-        if (com != null && com.PrefixMethod != null) {

+        var com = m as CoLemma;

+        if (com != null && com.PrefixLemma != null) {

           // The body may mentioned the implicitly declared parameter _k.  Throw it into the

           // scope before resolving the body.

-          var k = com.PrefixMethod.Ins[0];

+          var k = com.PrefixLemma.Ins[0];

           scope.Push(k.Name, k);  // we expect no name conflict for _k

         }

         var codeContext = m;

         ResolveBlockStatement(m.Body, m.IsGhost, codeContext);

       }

 

-      // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for comethods)

+      // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for colemmas)

       ResolveAttributes(m.Attributes, false, m);

 

       scope.PopMarker();  // for the out-parameters and outermost-level locals

@@ -7735,35 +7735,35 @@ namespace Microsoft.Dafny
     /// <summary>

     /// This method adds to "coConclusions" all copredicate calls and codatatype equalities that occur

     /// in positive positions and not under existential quantification.  If "expr" is the postcondition

-    /// of a comethod, then the "coConclusions" are the subexpressions that need to be replaced in order

-    /// to create the postcondition of the corresponding prefix method.

+    /// of a colemma, then the "coConclusions" are the subexpressions that need to be replaced in order

+    /// to create the postcondition of the corresponding prefix lemma.

     /// </summary>

-    void CheckCoMethodConclusions(Expression expr, bool position, ISet<Expression> coConclusions) {

+    void CheckCoLemmaConclusions(Expression expr, bool position, ISet<Expression> coConclusions) {

       Contract.Requires(expr != null);

       if (expr is ConcreteSyntaxExpression) {

         var e = (ConcreteSyntaxExpression)expr;

-        CheckCoMethodConclusions(e.ResolvedExpression, position, coConclusions);

+        CheckCoLemmaConclusions(e.ResolvedExpression, position, coConclusions);

 

       } else if (expr is LetExpr) {

         var e = (LetExpr)expr;

         // For simplicity, only look in the body of the let expression, that is, ignoring the RHS of the

         // binding and ignoring what that binding would expand to in the body.

-        CheckCoMethodConclusions(e.Body, position, coConclusions);

+        CheckCoLemmaConclusions(e.Body, position, coConclusions);

 

       } else if (expr is UnaryExpr) {

         var e = (UnaryExpr)expr;

         if (e.Op == UnaryExpr.Opcode.Not) {

-          CheckCoMethodConclusions(e.E, !position, coConclusions);

+          CheckCoLemmaConclusions(e.E, !position, coConclusions);

         }

 

       } else if (expr is BinaryExpr) {

         var bin = (BinaryExpr)expr;

         if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.And || bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {

-          CheckCoMethodConclusions(bin.E0, position, coConclusions);

-          CheckCoMethodConclusions(bin.E1, position, coConclusions);

+          CheckCoLemmaConclusions(bin.E0, position, coConclusions);

+          CheckCoLemmaConclusions(bin.E1, position, coConclusions);

         } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {

-          CheckCoMethodConclusions(bin.E0, !position, coConclusions);

-          CheckCoMethodConclusions(bin.E1, position, coConclusions);

+          CheckCoLemmaConclusions(bin.E0, !position, coConclusions);

+          CheckCoLemmaConclusions(bin.E1, position, coConclusions);

         } else if (position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) {

           coConclusions.Add(bin);

         } else if (!position && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.NeqCommon && bin.E0.Type.IsCoDatatype) {

@@ -7772,16 +7772,16 @@ namespace Microsoft.Dafny
 

       } else if (expr is ITEExpr) {

         var ite = (ITEExpr)expr;

-        CheckCoMethodConclusions(ite.Thn, position, coConclusions);

-        CheckCoMethodConclusions(ite.Els, position, coConclusions);

+        CheckCoLemmaConclusions(ite.Thn, position, coConclusions);

+        CheckCoLemmaConclusions(ite.Els, position, coConclusions);

 

       } else if (expr is StmtExpr) {

         var e = (StmtExpr)expr;

-        CheckCoMethodConclusions(e.E, position, coConclusions);

+        CheckCoLemmaConclusions(e.E, position, coConclusions);

 

       } else if (expr is OldExpr) {

         var e = (OldExpr)expr;

-        CheckCoMethodConclusions(e.E, position, coConclusions);

+        CheckCoLemmaConclusions(e.E, position, coConclusions);

 

       } else if (expr is FunctionCallExpr && position) {

         var fexp = (FunctionCallExpr)expr;

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index a65a32eb..92809143 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -511,8 +511,8 @@ public class Scanner {
 			case "returns": t.kind = 36; break;

 			case "method": t.kind = 40; break;

 			case "lemma": t.kind = 41; break;

-			case "comethod": t.kind = 42; break;

-			case "colemma": t.kind = 43; break;

+			case "colemma": t.kind = 42; break;

+			case "comethod": t.kind = 43; break;

 			case "constructor": t.kind = 44; break;

 			case "modifies": t.kind = 45; break;

 			case "free": t.kind = 46; break;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 7013a7ee..cb316008 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1109,10 +1109,10 @@ namespace Microsoft.Dafny {
           // the method spec itself

           sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.InterModuleCall));

           sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.IntraModuleCall));

-          if (m is CoMethod) {

-            // Let the CoCall and Impl forms to use m.PrefixMethod signature and specification (and

-            // note that m.PrefixMethod.Body == m.Body.

-            m = ((CoMethod)m).PrefixMethod;

+          if (m is CoLemma) {

+            // Let the CoCall and Impl forms to use m.PrefixLemma signature and specification (and

+            // note that m.PrefixLemma.Body == m.Body.

+            m = ((CoLemma)m).PrefixLemma;

             sink.TopLevelDeclarations.Add(AddMethod(m, MethodTranslationKind.CoCall));

           }

           if (m.Body != null) {

@@ -2224,7 +2224,7 @@ namespace Microsoft.Dafny {
       

       Bpl.StmtList stmts;

       if (!wellformednessProc) {

-        if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoMethod)) {

+        if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is CoLemma)) {

           var posts = new List<Expression>();

           m.Ens.ForEach(mfe => posts.Add(mfe.E));

           var allIns = new List<Formal>();

@@ -4156,7 +4156,7 @@ namespace Microsoft.Dafny {
     /// CoCall

     ///    This procedure is suitable for (intra-module) co-calls.

     ///    In these calls, some uses of copredicates may be replaced by

-    ///    proof certificates.  Note, unless the method is a comethod, there

+    ///    proof certificates.  Note, unless the method is a colemma, there

     ///    is no reason to include a procedure for co-calls.

     /// Implementation

     ///    This procedure is suitable for checking the implementation of the

@@ -6321,10 +6321,10 @@ namespace Microsoft.Dafny {
       // consult the call graph to figure out if this is a recursive call

       var module = method.EnclosingClass.Module;

       if (codeContext != null && module == currentModule) {

-        // Note, prefix methods are not recorded in the call graph, but their corresponding comethods are.

+        // Note, prefix lemmas are not recorded in the call graph, but their corresponding colemmas are.

         // Similarly, an iterator is not recorded in the call graph, but its MoveNext method is.

         ICallable cllr =

-          codeContext is PrefixMethod ? ((PrefixMethod)codeContext).Co :

+          codeContext is PrefixLemma ? ((PrefixLemma)codeContext).Co :

           codeContext is IteratorDecl ? ((IteratorDecl)codeContext).Member_MoveNext :

           codeContext;

         if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) {

@@ -6334,11 +6334,11 @@ namespace Microsoft.Dafny {
 

       MethodTranslationKind kind;

       var callee = method;

-      if (method is CoMethod && isRecursiveCall) {

+      if (method is CoLemma && isRecursiveCall) {

         kind = MethodTranslationKind.CoCall;

-        callee = ((CoMethod)method).PrefixMethod;

-      } else if (method is PrefixMethod) {

-        // an explicit call to a prefix method is allowed only inside the SCC of the corresponding comethod,

+        callee = ((CoLemma)method).PrefixLemma;

+      } else if (method is PrefixLemma) {

+        // an explicit call to a prefix lemma is allowed only inside the SCC of the corresponding colemma,

         // so we consider this to be a co-call

         kind = MethodTranslationKind.CoCall;

       } else if (module == currentModule) {

@@ -6373,13 +6373,13 @@ namespace Microsoft.Dafny {
 

         var param = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

         Bpl.Expr bActual;

-        if (i == 0 && method is CoMethod && isRecursiveCall) {

-          // Treat this call to M(args) as a call to the corresponding prefix method M#(_k - 1, args), so insert an argument here.

-          var k = ((PrefixMethod)codeContext).K;

+        if (i == 0 && method is CoLemma && isRecursiveCall) {

+          // Treat this call to M(args) as a call to the corresponding prefix lemma M#(_k - 1, args), so insert an argument here.

+          var k = ((PrefixLemma)codeContext).K;

           bActual = Bpl.Expr.Sub(new Bpl.IdentifierExpr(k.tok, k.AssignUniqueName(currentDeclaration), Bpl.Type.Int), Bpl.Expr.Literal(1));

         } else {

           Expression actual;

-          if (method is CoMethod && isRecursiveCall) {

+          if (method is CoLemma && isRecursiveCall) {

             actual = Args[i - 1];

           } else {

             actual = Args[i];

@@ -10084,7 +10084,7 @@ namespace Microsoft.Dafny {
             // The argument position is considered to be "variant" if the function is recursive and...

             // ... it has something to do with why the callee is well-founded, which happens when...

             if (f is ImplicitFormal) {

-              // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix method, or

+              // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or

               variantArgument = true;

             } else if (decr.Exists(ee => ContainsFreeVariable(ee, false, f))) {

               // ... it participates in the effective decreases clause of the function, which happens when it is

diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index d643da5d..7c786d7e 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -171,11 +171,11 @@ namespace DafnyLanguage
               } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {

                 var nm =

                   m is Dafny.Constructor ? "constructor" :

-                  m is Dafny.CoMethod ? "comethod" :

+                  m is Dafny.CoLemma ? "colemma" :

                   m is Dafny.Lemma ? "lemma" :

-                  // m is Dafny.PrefixMethod ? "prefix method" :  // this won't ever occur here

+                  // m is Dafny.PrefixLemma ? "prefix lemma" :  // this won't ever occur here

                   "method";

-                if (m.IsGhost && !(m is Dafny.CoMethod)) {

+                if (m.IsGhost && !(m is Dafny.CoLemma)) {

                   nm = "ghost " + nm;

                 }

                 newRegions.Add(new OutliningRegion(m, nm));

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 88f956bd..b4896e9e 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -264,7 +264,7 @@ namespace DafnyLanguage
                 case "class":

                 case "codatatype":

                 case "colemma":

-                case "comethod":

+                case "colemma":

                 case "constructor":

                 case "copredicate":

                 case "datatype":

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index a41cd0cd..f56af482 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -60,7 +60,7 @@ lemma M(x: int)
 {

 }

 

-comethod M'(x': int)

+colemma M'(x': int)

   ensures true;

 {

 }

@@ -1392,11 +1392,11 @@ CoResolution.dfy(64,10): Error: a copredicate is not allowed to declare any read
 CoResolution.dfy(70,31): Error: a copredicate is not allowed to declare any ensures clause

 CoResolution.dfy(79,20): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(83,20): Error: a recursive call from a copredicate can go only to other copredicates

-CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(106,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(107,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(126,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

-CoResolution.dfy(127,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods

+CoResolution.dfy(92,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(106,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(107,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(126,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

+CoResolution.dfy(127,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas

 CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates

 CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates

 16 resolution/type errors detected in CoResolution.dfy

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 06692314..7c010a09 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -26,7 +26,7 @@ copredicate atmost(a: Stream, b: Stream)
   case Cons(h,t) => b.Cons? && h <= b.head && atmost(t, b.tail)

 }

 

-comethod {:induction false} Theorem0()

+colemma {:induction false} Theorem0()

   ensures atmost(zeros(), ones());

 {

   // the following shows two equivalent ways to getting essentially the

@@ -48,7 +48,7 @@ ghost method Theorem0_Manual()
 

 datatype Natural = Zero | Succ(Natural);

 

-comethod {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

+colemma {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)

   ensures atmost(zeros(), ones());

   decreases y;

 {

@@ -62,7 +62,7 @@ comethod {:induction false} Theorem0_TerminationFailure_ExplicitDecreases(y: Nat
   Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y);

 }

 

-comethod {:induction false} Theorem0_TerminationFailure_DefaultDecreases(y: Natural)

+colemma {:induction false} Theorem0_TerminationFailure_DefaultDecreases(y: Natural)

   ensures atmost(zeros(), ones());

 {

   match (y) {

@@ -80,7 +80,7 @@ ghost method {:induction true} Theorem0_Lemma(k: nat)
 {

 }

 

-comethod {:induction false} Theorem1()

+colemma {:induction false} Theorem1()

   ensures append(zeros(), ones()) == zeros();

 {

   Theorem1();

@@ -98,14 +98,14 @@ copredicate Pos(s: IList)
   s.head > 0 && Pos(s.tail)

 }

 

-comethod {:induction false} Theorem2(n: int)

+colemma {:induction false} Theorem2(n: int)

   requires 1 <= n;

   ensures Pos(UpIList(n));

 {

   Theorem2(n+1);

 }

 

-comethod {:induction false} Theorem2_NotAProof(n: int)

+colemma {:induction false} Theorem2_NotAProof(n: int)

   requires 1 <= n;

   ensures Pos(UpIList(n));

 {  // error: this is not a proof (without automatic induction)

@@ -125,7 +125,7 @@ function GG<T>(h: T): TList<T>
   TCons(h, GG(Next(h)))

 }

 

-comethod {:induction false} Compare<T>(h: T)

+colemma {:induction false} Compare<T>(h: T)

   ensures FF(h) == GG(h);

 {

   assert FF(h).head == GG(h).head;

@@ -143,7 +143,7 @@ comethod {:induction false} Compare<T>(h: T)
   }

 }

 

-comethod {:induction false} BadTheorem(s: IList)

+colemma {:induction false} BadTheorem(s: IList)

   ensures false;

 {  // error: postcondition violation

   BadTheorem(s.tail);

@@ -153,36 +153,36 @@ comethod {:induction false} BadTheorem(s: IList)
 

 // Make sure recursive calls get checked for termination

 module Recursion {

-  comethod X() { Y(); }

-  comethod Y() { X(); }

+  colemma X() { Y(); }

+  colemma Y() { X(); }

 

-  comethod G(x: int)

+  colemma G(x: int)

     ensures x < 100;

   {  // error: postcondition violation (when _k == 0)

     H(x);

   }

-  comethod H(x: int)

+  colemma H(x: int)

     ensures x < 100;

   {  // error: postcondition violation (when _k == 0)

     G(x);

   }

   

-  comethod A(x: int) { B(x); }

-  comethod B(x: int)

+  colemma A(x: int) { B(x); }

+  colemma B(x: int)

   {

     A#[10](x);  // error: this is a recursive call, and the termination metric may not be going down

   }

   

-  comethod A'(x: int) { B'(x); }

-  comethod B'(x: int)

+  colemma A'(x: int) { B'(x); }

+  colemma B'(x: int)

   {

     if (10 < _k) {

       A'#[10](x);

     }

   }

   

-  comethod A''(x: int) { B''(x); }

-  comethod B''(x: int)

+  colemma A''(x: int) { B''(x); }

+  colemma B''(x: int)

   {

     if (0 < x) {

       A''#[_k](x-1);

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index 9ab52d53..a7111a09 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -18,7 +18,7 @@ module TestModule {
     S#[_k](d)  // error: _k is not an identifier in scope

   }

 

-  comethod CM(d: set<int>)

+  colemma CM(d: set<int>)

   {

     var b;

     b := this.S#[5](d);

@@ -82,26 +82,26 @@ module Mojul1 {
   copredicate X() { Y() }

   copredicate Y() { X#[10]() }  // error: X is not allowed to depend on X#

 

-  comethod M()

+  colemma M()

   {

     N();

   }

-  comethod N()

+  colemma N()

   {

     Z();

-    W();  // error: not allowed to make co-recursive call to non-comethod

+    W();  // error: not allowed to make co-recursive call to non-colemma

   }

   ghost method Z() { }

   ghost method W() { M(); }

 

-  comethod G() { H(); }

-  comethod H() { G#[10](); }  // fine for comethod/prefix-method

+  colemma G() { H(); }

+  colemma H() { G#[10](); }  // fine for colemma/prefix-lemma

 }

 

 module CallGraph {

-  // comethod -> copredicate -> comethod

-  // comethod -> copredicate -> prefix method

-  comethod CoLemma(n: nat)

+  // colemma -> copredicate -> colemma

+  // colemma -> copredicate -> prefix lemma

+  colemma CoLemma(n: nat)

   {

     var q := Q(n);  // error

     var r := R(n);  // error

@@ -119,9 +119,9 @@ module CallGraph {
     false

   }

 

-  // comethod -> prefix predicate -> comethod

-  // comethod -> prefix predicate -> prefix method

-  comethod CoLemma_D(n: nat)

+  // colemma -> prefix predicate -> colemma

+  // colemma -> prefix predicate -> prefix lemma

+  colemma CoLemma_D(n: nat)

   {

     var q := Q_D#[n](n);  // error

     var r := R_D#[n](n);  // error

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index b31dc5be..27b279c3 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -133,7 +133,7 @@ module CoPredicateResolutionErrors {
 

 // --------------------------------------------------

 

-module UnfruitfulCoMethodConclusions {

+module UnfruitfulCoLemmaConclusions {

   codatatype Stream<T> = Cons(head: T, tail: Stream);

 

   copredicate Positive(s: Stream<int>)

@@ -141,13 +141,13 @@ module UnfruitfulCoMethodConclusions {
     s.head > 0 && Positive(s.tail)

   }

 

-  comethod BadTheorem(s: Stream)

+  colemma BadTheorem(s: Stream)

     ensures false;

   {

     BadTheorem(s.tail);

   }

 

-  comethod CM(s: Stream<int>)

+  colemma CM(s: Stream<int>)

     ensures true && !false;

     ensures s.head == 8 ==> Positive(s);

     ensures s.tail == s;

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index b7dea89d..d3112233 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -10,14 +10,14 @@ copredicate Pos(s: Stream<int>)
   0 < s.head && Pos(s.tail)

 }

 

-comethod {:induction false} PosLemma0(n: int)

+colemma {:induction false} PosLemma0(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

   PosLemma0(n + 1);  // this completes the proof

 }

 

-comethod {:induction false} PosLemma1(n: int)

+colemma {:induction false} PosLemma1(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

@@ -27,7 +27,7 @@ comethod {:induction false} PosLemma1(n: int)
   }

 }

 

-comethod {:induction false} Outside_CoMethod_Caller_PosLemma(n: int)

+colemma {:induction false} Outside_CoLemma_Caller_PosLemma(n: int)

   requires 1 <= n;

   ensures Pos(Upward(n));

 {

@@ -51,19 +51,19 @@ copredicate X(s: Stream)  // this is equivalent to always returning 'true'
   X(s)

 }

 

-comethod {:induction false} AlwaysLemma_X0(s: Stream)

+colemma {:induction false} AlwaysLemma_X0(s: Stream)

   ensures X(s);  // prove that X(s) really is always 'true'

 {  // error: this is not the right proof

   AlwaysLemma_X0(s.tail);

 }

 

-comethod {:induction false} AlwaysLemma_X1(s: Stream)

+colemma {:induction false} AlwaysLemma_X1(s: Stream)

   ensures X(s);  // prove that X(s) really is always 'true'

 {

   AlwaysLemma_X1(s);  // this is the right proof

 }

 

-comethod {:induction false} AlwaysLemma_X2(s: Stream)

+colemma {:induction false} AlwaysLemma_X2(s: Stream)

   ensures X(s);

 {

   AlwaysLemma_X2(s);

@@ -77,19 +77,19 @@ copredicate Y(s: Stream)  // this is equivalent to always returning 'true'
   Y(s.tail)

 }

 

-comethod {:induction false} AlwaysLemma_Y0(s: Stream)

+colemma {:induction false} AlwaysLemma_Y0(s: Stream)

   ensures Y(s);  // prove that Y(s) really is always 'true'

 {

   AlwaysLemma_Y0(s.tail);  // this is a correct proof

 }

 

-comethod {:induction false} AlwaysLemma_Y1(s: Stream)

+colemma {:induction false} AlwaysLemma_Y1(s: Stream)

   ensures Y(s);

 {  // error: this is not the right proof

   AlwaysLemma_Y1(s);

 }

 

-comethod {:induction false} AlwaysLemma_Y2(s: Stream)

+colemma {:induction false} AlwaysLemma_Y2(s: Stream)

   ensures Y(s);

 {

   AlwaysLemma_Y2(s.tail);

@@ -103,7 +103,7 @@ copredicate Z(s: Stream)
   false

 }

 

-comethod {:induction false} AlwaysLemma_Z(s: Stream)

+colemma {:induction false} AlwaysLemma_Z(s: Stream)

   ensures Z(s);  // says, perversely, that Z(s) is always 'true'

 {  // error: this had better not lead to a proof

   AlwaysLemma_Z(s);

@@ -119,7 +119,7 @@ copredicate Even(s: Stream<int>)
   s.head % 2 == 0 && Even(s.tail)

 }

 

-comethod {:induction false} Lemma0(n: int)

+colemma {:induction false} Lemma0(n: int)

   ensures Even(Doubles(n));

 {

   Lemma0(n+1);

@@ -130,25 +130,25 @@ function UpwardBy2(n: int): Stream<int>
   Cons(n, UpwardBy2(n + 2))

 }

 

-comethod {:induction false} Lemma1(n: int)

+colemma {:induction false} Lemma1(n: int)

   ensures Even(UpwardBy2(2*n));

 {

   Lemma1(n+1);

 }

 

-comethod {:induction false} ProveEquality(n: int)

+colemma {:induction false} ProveEquality(n: int)

   ensures Doubles(n) == UpwardBy2(2*n);

 {

   ProveEquality(n+1);

 }

 

-comethod {:induction false} BadEquality0(n: int)

+colemma {:induction false} BadEquality0(n: int)

   ensures Doubles(n) == UpwardBy2(n);

 {  // error: postcondition does not hold

   BadEquality0(n+1);

 }

 

-comethod {:induction false} BadEquality1(n: int)

+colemma {:induction false} BadEquality1(n: int)

   ensures Doubles(n) == UpwardBy2(n+1);

 {  // error: postcondition does not hold

   BadEquality1(n+1);

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 287b4006..4b39876a 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -13,20 +13,20 @@ copredicate IsSubStream(s: Stream, u: Stream)
   In(s.head, u) && IsSubStream(s.tail, u)

 }

 

-ghost method Lemma_InTail<T>(x: T, s: Stream<T>)

+lemma Lemma_InTail<T>(x: T, s: Stream<T>)

   requires In(x, s.tail);

   ensures In(x, s);

 {

   var n :| 0 <= n && Tail(s.tail, n).head == x;

   assert Tail(s, n+1).head == x;

 }

-comethod Lemma_TailSubStream(s: Stream, u: Stream)

+colemma Lemma_TailSubStream(s: Stream, u: Stream)

   requires IsSubStream(s, u.tail);

   ensures IsSubStream(s, u);

 {

   Lemma_InTail(s.head, u);

 }

-ghost method Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat)  // this lemma could have been used to prove the previous one

+lemma Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat)  // this lemma could have been used to prove the previous one

   requires IsSubStream#[k](s, u.tail);

   ensures IsSubStream#[k](s, u);

 {

@@ -35,7 +35,7 @@ ghost method Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat)  // this lemma c
     Lemma_TailSubStreamK(s.tail, u, k-1);

   }

 }

-ghost method Lemma_InSubStream<T>(x: T, s: Stream<T>, u: Stream<T>)

+lemma Lemma_InSubStream<T>(x: T, s: Stream<T>, u: Stream<T>)

   requires In(x, s) && IsSubStream(s, u);

   ensures In(x, u);

 {

@@ -57,7 +57,7 @@ copredicate AllP(s: Stream, h: PredicateHandle)
 {

   P(s.head, h) && AllP(s.tail, h)

 }

-ghost method Lemma_InAllP<T>(x: T, s: Stream<T>, h: PredicateHandle)

+lemma Lemma_InAllP<T>(x: T, s: Stream<T>, h: PredicateHandle)

   requires In(x, s) && AllP(s, h);

   ensures P(x, h);

 {

@@ -80,7 +80,7 @@ copredicate AlwaysAnother(s: Stream, h: PredicateHandle)
 {

   IsAnother(s, h) && AlwaysAnother(s.tail, h)

 }

-comethod Lemma_AllImpliesAlwaysAnother(s: Stream, h: PredicateHandle)

+colemma Lemma_AllImpliesAlwaysAnother(s: Stream, h: PredicateHandle)

   requires AllP(s, h);

   ensures AlwaysAnother(s, h);

 {

@@ -118,7 +118,7 @@ function Filter(s: Stream, h: PredicateHandle): Stream
     Filter(s.tail, h)

 }

 // properties about Filter

-comethod Filter_AlwaysAnother(s: Stream, h: PredicateHandle)

+colemma Filter_AlwaysAnother(s: Stream, h: PredicateHandle)

   requires AlwaysAnother(s, h);

   ensures AllP(Filter(s, h), h);

   decreases Next(s, h);

@@ -129,7 +129,7 @@ comethod Filter_AlwaysAnother(s: Stream, h: PredicateHandle)
     Filter_AlwaysAnother#[_k](s.tail, h);

   }

 }

-comethod Filter_IsSubStream(s: Stream, h: PredicateHandle)

+colemma Filter_IsSubStream(s: Stream, h: PredicateHandle)

   requires AlwaysAnother(s, h);

   ensures IsSubStream(Filter(s, h), s);

   decreases Next(s, h);

@@ -160,7 +160,7 @@ comethod Filter_IsSubStream(s: Stream, h: PredicateHandle)
 }

 

 // The following says nothing about the order of the elements in the stream

-ghost method Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle)

+lemma Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle)

   requires AlwaysAnother(s, h);

   ensures forall x :: In(x, Filter(s, h)) <==> In(x, s) && P(x, h);

 {

@@ -177,7 +177,7 @@ ghost method Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle)
   }

 }

 

-ghost method FS_Ping<T>(s: Stream<T>, h: PredicateHandle, x: T)

+lemma FS_Ping<T>(s: Stream<T>, h: PredicateHandle, x: T)

   requires AlwaysAnother(s, h) && In(x, Filter(s, h));

   ensures In(x, s) && P(x, h);

 {

@@ -189,7 +189,7 @@ ghost method FS_Ping<T>(s: Stream<T>, h: PredicateHandle, x: T)
   Lemma_InAllP(x, Filter(s, h), h);

 }

 

-ghost method FS_Pong<T>(s: Stream<T>, h: PredicateHandle, x: T, k: nat)

+lemma FS_Pong<T>(s: Stream<T>, h: PredicateHandle, x: T, k: nat)

   requires AlwaysAnother(s, h) && In(x, s) && P(x, h);

   requires Tail(s, k).head == x;

   ensures In(x, Filter(s, h));

@@ -226,19 +226,19 @@ copredicate IncrFrom(s: Stream, low: int, ord: PredicateHandle)
   low <= Ord(s.head, ord) && IncrFrom(s.tail, Ord(s.head, ord) + 1, ord)

 }

 

-comethod Lemma_Incr0(s: Stream, low: int, ord: PredicateHandle)

+colemma Lemma_Incr0(s: Stream, low: int, ord: PredicateHandle)

   requires IncrFrom(s, low, ord);

   ensures Increasing(s, ord);

 {

 }

-comethod Lemma_Incr1(s: Stream, ord: PredicateHandle)

+colemma Lemma_Incr1(s: Stream, ord: PredicateHandle)

   requires Increasing(s, ord);

   ensures IncrFrom(s, Ord(s.head, ord), ord);

 {

   Lemma_Incr1(s.tail, ord);

 }

 

-ghost method Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: PredicateHandle)

+lemma Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: PredicateHandle)

   requires Increasing(s, ord) && AlwaysAnother(s, h);

   ensures Increasing(Filter(s, h), ord);

 {

@@ -246,7 +246,7 @@ ghost method Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord:
   Lemma_FilterPreservesIncrFrom(s, h, Ord(s.head, ord), ord);

   Lemma_Incr0(Filter(s, h), Ord(s.head, ord), ord);

 }

-comethod Lemma_FilterPreservesIncrFrom(s: Stream, h: PredicateHandle, low: int, ord: PredicateHandle)

+colemma Lemma_FilterPreservesIncrFrom(s: Stream, h: PredicateHandle, low: int, ord: PredicateHandle)

   requires IncrFrom(s, low, ord) && AlwaysAnother(s, h) && low <= Ord(s.head, ord);

   ensures IncrFrom(Filter(s, h), low, ord);

   decreases Next(s, h);

diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 8709a6d8..5c5c0412 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -62,7 +62,7 @@ function SAppend(xs: Stream, ys: Stream): Stream
   we also get ==#[k].

 */

 

-ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stream)

+lemma {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c));

   decreases k;

 {

@@ -72,7 +72,7 @@ ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream,
   }

 }

 

-ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream)

+lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

 {

   forall k:nat { SAppendIsAssociativeK(k, a, b, c); }

@@ -80,8 +80,8 @@ ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream)
   assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c)));

 }

 

-// Equivalent proof using the comethod syntax.

-comethod {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream)

+// Equivalent proof using the colemma syntax.

+colemma {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

 {

   match (a) {

@@ -91,26 +91,26 @@ comethod {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream)
 }

 

 // In fact the proof can be fully automatic.

-comethod SAppendIsAssociative_Auto(a:Stream, b:Stream, c:Stream)

+colemma SAppendIsAssociative_Auto(a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

 {

 }

 

-comethod {:induction false} UpPos(n:int)

+colemma {:induction false} UpPos(n:int)

   requires n > 0;

   ensures Pos(Up(n));

 {

   UpPos(n+1);

 }

 

-comethod UpPos_Auto(n:int)

+colemma UpPos_Auto(n:int)

   requires n > 0;

   ensures Pos(Up(n));

 {

 }

 

 // This does induction and coinduction in the same proof.

-comethod {:induction false} FivesUpPos(n:int)

+colemma {:induction false} FivesUpPos(n:int)

   requires n > 0;

   ensures Pos(FivesUp(n));

   decreases 4 - (n-1) % 5;

@@ -124,7 +124,7 @@ comethod {:induction false} FivesUpPos(n:int)
 

 // Again, Dafny can just employ induction tactic and do it automatically.

 // The only hint required is the decrease clause.

-comethod FivesUpPos_Auto(n:int)

+colemma FivesUpPos_Auto(n:int)

   requires n > 0;

   ensures Pos(FivesUp(n));

   decreases 4 - (n-1) % 5;

diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy
index e189dc4a..32a868bb 100644
--- a/Test/dafny3/InfiniteTrees.dfy
+++ b/Test/dafny3/InfiniteTrees.dfy
@@ -10,12 +10,12 @@ function Tail(s: Stream, n: nat): Stream
     if t == Nil then t else t.tail

 }

 

-ghost method Tail_Lemma0(s: Stream, n: nat)

+lemma Tail_Lemma0(s: Stream, n: nat)

   requires s.Cons? && Tail(s, n).Cons?;

   ensures Tail(s, n).tail == Tail(s.tail, n);

 {

 }

-ghost method Tail_Lemma1(s: Stream, k: nat, n: nat)

+lemma Tail_Lemma1(s: Stream, k: nat, n: nat)

   requires k <= n;

   ensures Tail(s, n).Cons? ==> Tail(s, k).Cons?;

   // Note, the contrapositive of this lemma says:  Tail(s, k) == Nil ==> Tail(s, n) == Nil

@@ -24,7 +24,7 @@ ghost method Tail_Lemma1(s: Stream, k: nat, n: nat)
     assert Tail(s, n) == Tail(s, n-1).tail;

   }

 }

-ghost method Tail_Lemma2(s: Stream, n: nat)

+lemma Tail_Lemma2(s: Stream, n: nat)

   requires s.Cons? && Tail(s.tail, n).Cons?;

   ensures Tail(s, n).Cons?;

 {

@@ -48,7 +48,7 @@ function AnInfiniteStream(): Stream<int>
 {

   Cons(0, AnInfiniteStream())

 }

-comethod Proposition0()

+colemma Proposition0()

   ensures IsNeverEndingStream(AnInfiniteStream());

 {

 }

@@ -76,7 +76,7 @@ copredicate LowerThan(s: Stream<Tree>, n: nat)
 // Co-predicate LowerThan(s, n) recurses on LowerThan(s.tail, n).  Thus, a property of LowerThan is that

 // LowerThan(s, h) implies LowerThan(s', h) for any suffix s' of s.

 

-ghost method LowerThan_Lemma(s: Stream<Tree>, n: nat, h: nat)

+lemma LowerThan_Lemma(s: Stream<Tree>, n: nat, h: nat)

   ensures LowerThan(s, h) ==> LowerThan(Tail(s, n), h);

 {

   Tail_Lemma1(s, 0, n);

@@ -113,7 +113,7 @@ function SkinnyTree(): Tree
 {

   Node(Cons(SkinnyTree(), Nil))

 }

-ghost method Proposition1()

+lemma Proposition1()

   ensures IsFiniteSomewhere(SkinnyTree()) && !HasBoundedHeight(SkinnyTree());

 {

   assert forall n :: 0 <= n ==> !LowerThan(SkinnyTree().children, n);

@@ -121,7 +121,7 @@ ghost method Proposition1()
 

 // Any tree where all paths have bounded height are finite somewhere.

 

-ghost method Theorem0(t: Tree)

+lemma Theorem0(t: Tree)

   requires HasBoundedHeight(t);

   ensures IsFiniteSomewhere(t);

 {

@@ -133,7 +133,7 @@ ghost method Theorem0(t: Tree)
   */

   var k := FindNil(t.children, n);

 }

-ghost method FindNil(s: Stream<Tree>, n: nat) returns (k: nat)

+lemma FindNil(s: Stream<Tree>, n: nat) returns (k: nat)

   requires LowerThan(s, n);

   ensures !InfiniteEverywhere#[k](s);

 {

@@ -175,17 +175,17 @@ function ATreeChildren(): Stream<Tree>
 {

   Cons(Node(Nil), ATreeChildren())

 }

-ghost method Proposition2()

+lemma Proposition2()

   ensures !HasFiniteHeightEverywhere_Bad(ATree());

 {

   Proposition2_Lemma0();

   Proposition2_Lemma1(ATreeChildren());

 }

-comethod Proposition2_Lemma0()

+colemma Proposition2_Lemma0()

   ensures IsNeverEndingStream(ATreeChildren());

 {

 }

-comethod Proposition2_Lemma1(s: Stream<Tree>)

+colemma Proposition2_Lemma1(s: Stream<Tree>)

   requires IsNeverEndingStream(s);

   ensures InfiniteHeightSomewhere_Bad(s);

 {

@@ -237,7 +237,7 @@ copredicate ValidPath(t: Tree, p: Stream<int>)
     var ch := Tail(t.children, index);

     ch.Cons? && ValidPath(ch.head, tail)

 }

-ghost method ValidPath_Lemma(p: Stream<int>)

+lemma ValidPath_Lemma(p: Stream<int>)

   ensures ValidPath(Node(Nil), p) ==> p == Nil;

 {

   if ValidPath(Node(Nil), p) {

@@ -258,7 +258,7 @@ predicate HasFiniteHeight(t: Tree)
 

 // From this definition, we can prove that any tree of bounded height is also of finite height.

 

-ghost method Theorem1(t: Tree)

+lemma Theorem1(t: Tree)

   requires HasBoundedHeight(t);

   ensures HasFiniteHeight(t);

 {

@@ -267,7 +267,7 @@ ghost method Theorem1(t: Tree)
     Theorem1_Lemma(t, n, p);

   }

 }

-ghost method Theorem1_Lemma(t: Tree, n: nat, p: Stream<int>)

+lemma Theorem1_Lemma(t: Tree, n: nat, p: Stream<int>)

   requires LowerThan(t.children, n) && ValidPath(t, p);

   ensures !IsNeverEndingStream(p);

   decreases n;

@@ -311,7 +311,7 @@ function EverLongerSkinnyTrees(n: nat): Stream<Tree>
   Cons(SkinnyFiniteTree(n), EverLongerSkinnyTrees(n+1))

 }

 

-ghost method EverLongerSkinnyTrees_Lemma(k: nat, n: nat)

+lemma EverLongerSkinnyTrees_Lemma(k: nat, n: nat)

   ensures Tail(EverLongerSkinnyTrees(k), n).Cons?;

   ensures Tail(EverLongerSkinnyTrees(k), n).head == SkinnyFiniteTree(k+n);

   decreases n;

@@ -330,13 +330,13 @@ ghost method EverLongerSkinnyTrees_Lemma(k: nat, n: nat)
   }

 }

 

-ghost method Proposition3()

+lemma Proposition3()

   ensures !HasBoundedHeight(FiniteUnboundedTree()) && HasFiniteHeight(FiniteUnboundedTree());

 {

   Proposition3a();

   Proposition3b();

 }

-ghost method Proposition3a()

+lemma Proposition3a()

   ensures !HasBoundedHeight(FiniteUnboundedTree());

 {

   var ch := FiniteUnboundedTree().children;

@@ -350,7 +350,7 @@ ghost method Proposition3a()
     LowerThan_Lemma(ch, n+1, n);

   }

 }

-ghost method Proposition3b()

+lemma Proposition3b()

   ensures HasFiniteHeight(FiniteUnboundedTree());

 {

   var t := FiniteUnboundedTree();

@@ -369,7 +369,7 @@ ghost method Proposition3b()
     Proposition3b_Lemma(si, index, p.tail);

   }

 }

-ghost method Proposition3b_Lemma(t: Tree, h: nat, p: Stream<int>)

+lemma Proposition3b_Lemma(t: Tree, h: nat, p: Stream<int>)

   requires LowerThan(t.children, h) && ValidPath(t, p);

   ensures !IsNeverEndingStream(p);

   decreases h;

@@ -495,7 +495,7 @@ function N2S'(n: nat, num: Number): Stream<int>
   case Succ(next) => N2S'(n + 1, next)

 }

 

-ghost method Path_Lemma0(t: Tree, p: Stream<int>)

+lemma Path_Lemma0(t: Tree, p: Stream<int>)

   requires ValidPath(t, p);

   ensures ValidPath_Alt(t, S2N(p));

 {

@@ -503,7 +503,7 @@ ghost method Path_Lemma0(t: Tree, p: Stream<int>)
     Path_Lemma0'(t, p);

   }

 }

-comethod Path_Lemma0'(t: Tree, p: Stream<int>)

+colemma Path_Lemma0'(t: Tree, p: Stream<int>)

   requires ValidPath(t, p);

   ensures ValidPath_Alt(t, S2N(p));

 {

@@ -526,7 +526,7 @@ comethod Path_Lemma0'(t: Tree, p: Stream<int>)
       }

   }

 }

-comethod Path_Lemma0''(tChildren: Stream<Tree>, n: nat, tail: Stream<int>)

+colemma Path_Lemma0''(tChildren: Stream<Tree>, n: nat, tail: Stream<int>)

   requires var ch := Tail(tChildren, n); ch.Cons? && ValidPath(ch.head, tail);

   ensures ValidPath_Alt'(tChildren, S2N'(n, tail));

 {

@@ -545,7 +545,7 @@ comethod Path_Lemma0''(tChildren: Stream<Tree>, n: nat, tail: Stream<int>)
       Path_Lemma0'(tChildren.head, tail);

   }

 }

-ghost method Path_Lemma1(t: Tree, r: CoOption<Number>)

+lemma Path_Lemma1(t: Tree, r: CoOption<Number>)

   requires ValidPath_Alt(t, r);

   ensures ValidPath(t, N2S(r));

 {

@@ -553,7 +553,7 @@ ghost method Path_Lemma1(t: Tree, r: CoOption<Number>)
     Path_Lemma1'(t, r);

   }

 }

-comethod Path_Lemma1'(t: Tree, r: CoOption<Number>)

+colemma Path_Lemma1'(t: Tree, r: CoOption<Number>)

   requires ValidPath_Alt(t, r);

   ensures ValidPath(t, N2S(r));

   decreases 1;

@@ -576,7 +576,7 @@ comethod Path_Lemma1'(t: Tree, r: CoOption<Number>)
       }

   }

 }

-comethod Path_Lemma1''(s: Stream<Tree>, n: nat, num: Number)

+colemma Path_Lemma1''(s: Stream<Tree>, n: nat, num: Number)

   requires ValidPath_Alt'(Tail(s, n), num);

   ensures ValidPath(Node(s), N2S'(n, num));

   decreases 0, num;

@@ -596,14 +596,14 @@ comethod Path_Lemma1''(s: Stream<Tree>, n: nat, num: Number)
       }

   }

 }

-ghost method Path_Lemma2(p: Stream<int>)

+lemma Path_Lemma2(p: Stream<int>)

   ensures IsNeverEndingStream(p) ==> InfinitePath(S2N(p));

 {

   if IsNeverEndingStream(p) {

     Path_Lemma2'(p);

   }

 }

-comethod Path_Lemma2'(p: Stream<int>)

+colemma Path_Lemma2'(p: Stream<int>)

   requires IsNeverEndingStream(p);

   ensures InfinitePath(S2N(p));

 {

@@ -622,7 +622,7 @@ comethod Path_Lemma2'(p: Stream<int>)
     }

   }

 }

-comethod Path_Lemma2''(p: Stream<int>, n: nat, tail: Stream<int>)

+colemma Path_Lemma2''(p: Stream<int>, n: nat, tail: Stream<int>)

   requires IsNeverEndingStream(p) && p.tail == tail;

   ensures InfinitePath'(S2N'(n, tail));

 {

@@ -648,7 +648,7 @@ comethod Path_Lemma2''(p: Stream<int>, n: nat, tail: Stream<int>)
     }

   }

 }

-ghost method Path_Lemma3(r: CoOption<Number>)

+lemma Path_Lemma3(r: CoOption<Number>)

   ensures InfinitePath(r) ==> IsNeverEndingStream(N2S(r));

 {

   if InfinitePath(r) {

@@ -657,7 +657,7 @@ ghost method Path_Lemma3(r: CoOption<Number>)
     }

   }

 }

-comethod Path_Lemma3'(n: nat, num: Number)

+colemma Path_Lemma3'(n: nat, num: Number)

   requires InfinitePath'(num);

   ensures IsNeverEndingStream(N2S'(n, num));

   decreases num;

@@ -678,7 +678,7 @@ comethod Path_Lemma3'(n: nat, num: Number)
   }

 }

 

-ghost method Theorem2(t: Tree)

+lemma Theorem2(t: Tree)

   ensures HasFiniteHeight(t) <==> HasFiniteHeight_Alt(t);

 {

   if HasFiniteHeight_Alt(t) {

diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index 431ff543..37586ec7 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -10,7 +10,7 @@ function Apply<T>(f: FunctionHandle<T>, argument: T): T
 

 // Function composition

 function After(f: FunctionHandle, g: FunctionHandle): FunctionHandle

-ghost method Definition_After<T>(f: FunctionHandle<T>, g: FunctionHandle<T>, arg: T)

+lemma Definition_After<T>(f: FunctionHandle<T>, g: FunctionHandle<T>, arg: T)

   ensures Apply(After(f, g), arg) == Apply(f, Apply(g, arg));

 

 function Lmap(f: FunctionHandle, a: LList): LList

@@ -29,7 +29,7 @@ function Lappend(a: LList, b: LList): LList
 

 // ---------- Section 8.3 ----------

 

-comethod Example6(f: FunctionHandle, g: FunctionHandle, M: LList)

+colemma Example6(f: FunctionHandle, g: FunctionHandle, M: LList)

   ensures Lmap(After(f, g), M) == Lmap(f, Lmap(g, M));

 {

   match M {

@@ -61,7 +61,7 @@ function Iterates<A>(f: FunctionHandle<LList<A>>, M: LList<A>): LList<LList<A>>
   Cons(M, Iterates(f, Apply(f, M)))

 }

 

-comethod Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

+colemma Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

   ensures Lmap(f, Iterates(f, M)) == Iterates(f, Apply(f, M));

 {

   calc {

@@ -80,7 +80,7 @@ comethod Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)
   }

 }

 

-ghost method CorollaryEq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

+lemma CorollaryEq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

   ensures Iterates(f, M) == Cons(M, Lmap(f, Iterates(f, M)));

 {

   Eq24(f, M);

@@ -92,7 +92,7 @@ ghost method CorollaryEq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)
 // Let h be any function

 function h<A>(f: FunctionHandle<LList<A>>, M: LList<A>): LList<LList<A>>

 // ... that satisfies the property in CorollaryEq24:

-ghost method Definition_h<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

+lemma Definition_h<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

   ensures h(f, M) == Cons(M, Lmap(f, h(f, M)));

 

 // Functions to support the proof:

@@ -107,19 +107,19 @@ function LmapIter(n: nat, f: FunctionHandle, arg: LList): LList
   if n == 0 then arg else Lmap(f, LmapIter(n-1, f, arg))

 }

 

-ghost method Lemma25<A>(n: nat, f: FunctionHandle<A>, b: A, M: LList<A>)

+lemma Lemma25<A>(n: nat, f: FunctionHandle<A>, b: A, M: LList<A>)

   ensures LmapIter(n, f, Cons(b, M)) == Cons(Iter(n, f, b), LmapIter(n, f, M));

 {

   // proof is by (automatic) induction

 }

 

-ghost method Lemma26<A>(n: nat, f: FunctionHandle, x: LList)  // (26) in the paper, but with f := LMap f

+lemma Lemma26<A>(n: nat, f: FunctionHandle, x: LList)  // (26) in the paper, but with f := LMap f

   ensures LmapIter(n, f, Lmap(f, x)) == LmapIter(n+1, f, x);

 {

   // proof is by (automatic) induction

 }

 

-comethod BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>)

+colemma BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>)

   ensures LmapIter(n, f, h(f, u)) == LmapIter(n, f, Iterates(f, u));

 {

   calc {

@@ -146,7 +146,7 @@ comethod BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>)
   }

 }

 

-ghost method Example7<A>(f: FunctionHandle<LList<A>>)

+lemma Example7<A>(f: FunctionHandle<LList<A>>)

   // Given the definition of h, prove h(f, _) == Iterates(f, _):

   ensures forall M :: h(f, M) == Iterates(f, M);

 {

@@ -157,13 +157,13 @@ ghost method Example7<A>(f: FunctionHandle<LList<A>>)
 

 // ---------- Section 8.5 ----------

 

-comethod Example8<A>(f: FunctionHandle<A>, M: LList<A>, N: LList<A>)

+colemma Example8<A>(f: FunctionHandle<A>, M: LList<A>, N: LList<A>)

   ensures Lmap(f, Lappend(M, N)) == Lappend(Lmap(f, M), Lmap(f, N));

 {

   // A proof doesn't get any simpler than this

 }

 

-comethod Associativity(a: LList, b: LList, c: LList)

+colemma Associativity(a: LList, b: LList, c: LList)

   ensures Lappend(Lappend(a, b), c) == Lappend(a, Lappend(b, c));

 {

   // Again, Dafny does this proof completely automatically

diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index cc92a6f1..b5b0c8bf 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -18,7 +18,7 @@ function Inc(s: Stream<int>): Stream<int>
   Cons(s.head + 1, Inc(s.tail))

 }

 

-ghost method {:induction false} UpLemma(k: nat, n: int)

+lemma {:induction false} UpLemma(k: nat, n: int)

   ensures Inc(Up(n)) ==#[k] Up(n+1);

 {

   if (k != 0) {

@@ -26,18 +26,18 @@ ghost method {:induction false} UpLemma(k: nat, n: int)
   }

 }

 

-comethod {:induction false} CoUpLemma(n: int)

+colemma {:induction false} CoUpLemma(n: int)

   ensures Inc(Up(n)) == Up(n+1);

 {

   CoUpLemma(n+1);

 }

 

-ghost method UpLemma_Auto(k: nat, n: int)

+lemma UpLemma_Auto(k: nat, n: int)

   ensures Inc(Up(n)) ==#[k] Up(n+1);

 {

 }

 

-comethod CoUpLemma_Auto(n: int)

+colemma CoUpLemma_Auto(n: int)

   ensures Inc(Up(n)) == Up(n+1);

 {

 }

@@ -49,7 +49,7 @@ function Repeat(n: int): Stream<int>
   Cons(n, Repeat(n))

 }

 

-comethod RepeatLemma(n: int)

+colemma RepeatLemma(n: int)

   ensures Inc(Repeat(n)) == Repeat(n+1);

 {

 }

@@ -61,7 +61,7 @@ copredicate True(s: Stream)
   True(s.tail)

 }

 

-comethod AlwaysTrue(s: Stream)

+colemma AlwaysTrue(s: Stream)

   ensures True(s);

 {

 }

@@ -71,7 +71,7 @@ copredicate AlsoTrue(s: Stream)
   AlsoTrue(s)

 }

 

-comethod AlsoAlwaysTrue(s: Stream)

+colemma AlsoAlwaysTrue(s: Stream)

   ensures AlsoTrue(s);

 {

 }

@@ -81,7 +81,7 @@ copredicate TT(y: int)
   TT(y+1)

 }

 

-comethod AlwaysTT(y: int)

+colemma AlwaysTT(y: int)

   ensures TT(y);

 {

 }

@@ -112,12 +112,12 @@ copredicate AtMost(a: IList<int>, b: IList<int>)
   case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail)

 }

 

-comethod ZerosAndOnes_Theorem0()

+colemma ZerosAndOnes_Theorem0()

   ensures AtMost(zeros(), ones());

 {

 }

 

-comethod ZerosAndOnes_Theorem1()

+colemma ZerosAndOnes_Theorem1()

   ensures Append(zeros(), ones()) == zeros();

 {

 }

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index f13c5c0a..1d566545 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -40,7 +40,7 @@ function map_fg(M: Stream<X>): Stream<X>
 // ----- Theorems

 

 // map (f * g) M = map f (map g M)

-comethod Theorem0(M: Stream<X>)

+colemma Theorem0(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

   match (M) {

@@ -49,21 +49,21 @@ comethod Theorem0(M: Stream<X>)
       Theorem0(N);

   }

 }

-comethod Theorem0_Alt(M: Stream<X>)

+colemma Theorem0_Alt(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

   if (M.Cons?) {

     Theorem0_Alt(M.tail);

   }

 }

-ghost method Theorem0_Par(M: Stream<X>)

+lemma Theorem0_Par(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

   forall k: nat {

     Theorem0_Ind(k, M);

   }

 }

-ghost method Theorem0_Ind(k: nat, M: Stream<X>)

+lemma Theorem0_Ind(k: nat, M: Stream<X>)

   ensures map_fg(M) ==#[k] map_f(map_g(M));

 {

   if (k != 0) {

@@ -74,13 +74,13 @@ ghost method Theorem0_Ind(k: nat, M: Stream<X>)
     }

   }

 }

-ghost method Theorem0_AutoInd(k: nat, M: Stream<X>)

+lemma Theorem0_AutoInd(k: nat, M: Stream<X>)

   ensures map_fg(M) ==#[k] map_f(map_g(M));

 // {  // TODO: this is not working yet, apparently

 // }

 

 // map f (append M N) = append (map f M) (map f N)

-comethod Theorem1(M: Stream<X>, N: Stream<X>)

+colemma Theorem1(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

   match (M) {

@@ -89,21 +89,21 @@ comethod Theorem1(M: Stream<X>, N: Stream<X>)
       Theorem1(M', N);

   }

 }

-comethod Theorem1_Alt(M: Stream<X>, N: Stream<X>)

+colemma Theorem1_Alt(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

   if (M.Cons?) {

     Theorem1_Alt(M.tail, N);

   }

 }

-ghost method Theorem1_Par(M: Stream<X>, N: Stream<X>)

+lemma Theorem1_Par(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

   forall k: nat {

     Theorem1_Ind(k, M, N);

   }

 }

-ghost method Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)

+lemma Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));

 {

   // this time, try doing the 'if' inside the 'match' (instead of the other way around)

@@ -115,24 +115,24 @@ ghost method Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)
       }

   }

 }

-ghost method Theorem1_AutoInd(k: nat, M: Stream<X>, N: Stream<X>)

+lemma Theorem1_AutoInd(k: nat, M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));

 // {  // TODO: this is not working yet, apparently

 // }

-ghost method Theorem1_AutoForall()

+lemma Theorem1_AutoForall()

 {

 //  assert forall k: nat, M, N :: map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));  // TODO: this is not working yet, apparently

 }

 

 // append NIL M = M

-ghost method Theorem2(M: Stream<X>)

+lemma Theorem2(M: Stream<X>)

   ensures append(Nil, M) == M;

 {

   // trivial

 }

 

 // append M NIL = M

-comethod Theorem3(M: Stream<X>)

+colemma Theorem3(M: Stream<X>)

   ensures append(M, Nil) == M;

 {

   match (M) {

@@ -141,7 +141,7 @@ comethod Theorem3(M: Stream<X>)
       Theorem3(N);

   }

 }

-comethod Theorem3_Alt(M: Stream<X>)

+colemma Theorem3_Alt(M: Stream<X>)

   ensures append(M, Nil) == M;

 {

   if (M.Cons?) {

@@ -150,7 +150,7 @@ comethod Theorem3_Alt(M: Stream<X>)
 }

 

 // append M (append N P) = append (append M N) P

-comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)

+colemma Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)

   ensures append(M, append(N, P)) == append(append(M, N), P);

 {

   match (M) {

@@ -159,7 +159,7 @@ comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)
       Theorem4(M', N, P);

   }

 }

-comethod Theorem4_Alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)

+colemma Theorem4_Alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)

   ensures append(M, append(N, P)) == append(append(M, N), P);

 {

   if (M.Cons?) {

@@ -241,7 +241,7 @@ function Prepend<T>(x: T, M: Stream<Stream>): Stream<Stream>
   case Cons(s, N) => Cons(Cons(x, s), Prepend(x, N))

 }

 

-comethod Prepend_Lemma<T>(x: T, M: Stream<Stream>)

+colemma Prepend_Lemma<T>(x: T, M: Stream<Stream>)

   ensures StreamOfNonEmpties(Prepend(x, M));

 {

   match M {

@@ -250,7 +250,7 @@ comethod Prepend_Lemma<T>(x: T, M: Stream<Stream>)
   }

 }

 

-ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)

+lemma Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)

   ensures

     StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;

                                           // but until (co-)method can be called from functions,

@@ -261,7 +261,7 @@ ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)
   Lemma_Flatten(Nil, M, startMarker);

 }

 

-comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)

+colemma Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)

   ensures

     StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;

                                           // but until (co-)method can be called from functions,

@@ -325,7 +325,7 @@ comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)
   }

 }

 

-comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)

+colemma Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)

   ensures PrependThenFlattenStartMarker(s, M, startMarker) == append(s, PrependThenFlattenStartMarker(Nil, M, startMarker));

 {

   match (s) {

@@ -335,7 +335,7 @@ comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)
   }

 }

 

-comethod Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)

+colemma Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)

   requires StreamOfNonEmpties(M);

   ensures PrependThenFlattenNonEmpties(s, M) == append(s, PrependThenFlattenNonEmpties(Nil, M));

 {

diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy
index e381726e..3fa99256 100644
--- a/Test/dafny3/WideTrees.dfy
+++ b/Test/dafny3/WideTrees.dfy
@@ -36,12 +36,12 @@ function SmallTrees(n: nat): Stream<Tree>
   if n == 0 then SNil else SCons(SmallTree(n-1), SmallTrees(n))

 }

 // prove that the tree returned by SmallTree is finite

-ghost method Theorem(n: nat)

+lemma Theorem(n: nat)

   ensures HasBoundedHeight(SmallTree(n));

 {

   Lemma(n);

 }

-comethod Lemma(n: nat)

+colemma Lemma(n: nat)

   ensures LowerThan(SmallTrees(n), n);

 {

   if 0 < n {

diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 80e8cd91..629861f9 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -23,11 +23,11 @@ function even(xs: Stream): Stream
 function odd(xs: Stream): Stream

   { even(xs.tl) }

 

-comethod EvenOddLemma(xs: Stream)

+colemma EvenOddLemma(xs: Stream)

   ensures zip(even(xs), odd(xs)) == xs;

 { EvenOddLemma(xs.tl.tl); }

 

-comethod EvenZipLemma(xs:Stream, ys:Stream)

+colemma EvenZipLemma(xs:Stream, ys:Stream)

   ensures even(zip(xs, ys)) == xs;

 { /* Automatic. */ }

 

@@ -35,7 +35,7 @@ function bzip(xs: Stream, ys: Stream, f:bool) : Stream
   { if f then Cons(xs.hd, bzip(xs.tl, ys, !f))

     else      Cons(ys.hd, bzip(xs, ys.tl, !f)) }

 

-comethod BzipZipLemma(xs:Stream, ys:Stream)

+colemma BzipZipLemma(xs:Stream, ys:Stream)

   ensures zip(xs, ys) == bzip(xs, ys, true);

 { BzipZipLemma(xs.tl, ys.tl); }

 

@@ -54,7 +54,7 @@ function blink(): Stream<int>
   Cons(0, Cons(1, blink()))

 }

 

-comethod BzipBlinkLemma()

+colemma BzipBlinkLemma()

   ensures zip(const(0), const(1)) == blink();

 {

   BzipBlinkLemma(); 

@@ -66,13 +66,13 @@ function zip2(xs: Stream, ys: Stream): Stream
   Cons(xs.hd, zip2(ys, xs.tl))

 }

 

-comethod Zip201Lemma()

+colemma Zip201Lemma()

   ensures zip2(const(0), const(1)) == blink();

 {

   Zip201Lemma();

 }

 

-comethod ZipZip2Lemma(xs:Stream, ys:Stream)

+colemma ZipZip2Lemma(xs:Stream, ys:Stream)

   ensures zip(xs, ys) == zip2(xs, ys);

 {

   ZipZip2Lemma(xs.tl, ys.tl);

@@ -84,13 +84,13 @@ function bswitch(xs: Stream, f:bool) : Stream
   else      Cons(xs.hd,      bswitch(xs.tl, !f))

 }

 

-comethod BswitchLemma(xs:Stream)

+colemma BswitchLemma(xs:Stream)

   ensures zip(odd(xs), even(xs)) == bswitch(xs, true);

 {

   BswitchLemma(xs.tl.tl);

 }

 

-comethod Bswitch2Lemma(xs:Stream, ys:Stream)

+colemma Bswitch2Lemma(xs:Stream, ys:Stream)

   ensures zip(xs, ys) == bswitch(zip(ys, xs), true);

 {

   Bswitch2Lemma(xs.tl, ys.tl);

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index c77fed74..d663665b 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -32,7 +32,7 @@
    `(,(dafny-regexp-opt '(

         "class" "datatype" "codatatype" "type" "iterator"

         "function" "predicate" "copredicate"

-        "ghost" "var" "method" "lemma" "constructor" "comethod" "colemma"

+        "ghost" "var" "method" "lemma" "constructor" "colemma"

         "abstract" "module" "import" "default" "as" "opened" "static" "refines"

         "returns" "yields" "requires" "ensures" "modifies" "reads" "free"

         "invariant" "decreases" "include"

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index fe7c6638..d8ec579a 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -17,7 +17,7 @@ namespace Demo
         StringLiteral stringLiteral = TerminalFactory.CreateCSharpString("String");

 

         this.MarkReservedWords(  // NOTE: these keywords must also appear once more below

-          "class", "ghost", "static", "var", "method", "constructor", "comethod", "datatype", "codatatype",

+          "class", "ghost", "static", "var", "method", "constructor", "colemma", "datatype", "codatatype",

           "iterator", "type",

           "assert", "assume", "new", "this", "object", "refines",

           "abstract", "module", "import", "as", "default", "opened",

@@ -267,7 +267,7 @@ namespace Demo
           | "var"

           | "method"

           | "constructor"

-          | "comethod"

+          | "colemma"

           | "datatype"

           | "codatatype"

           | "type"

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index d4624def..41e0779b 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -9,7 +9,7 @@
       bool,nat,int,real,object,set,multiset,seq,array,array2,array3,map,

       function,predicate,copredicate,

       ghost,var,static,refines,

-      method,lemma,constructor,comethod,colemma,

+      method,lemma,constructor,colemma,

       returns,yields,abstract,module,import,default,opened,as,in,

       requires,modifies,ensures,reads,decreases,free,include

       % expressions

diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim
index 06e1252e..f533a621 100644
--- a/Util/vim/dafny.vim
+++ b/Util/vim/dafny.vim
@@ -6,7 +6,7 @@
 syntax clear
 syntax case match
 syntax keyword dafnyFunction function predicate copredicate
-syntax keyword method lemma constructor comethod colemma
+syntax keyword method lemma constructor colemma
 syntax keyword dafnyTypeDef class datatype codatatype type iterator
 syntax keyword abstract module import opened as default
 syntax keyword dafnyConditional if then else match case