diff --git a/src/Makefile.am b/src/Makefile.am
index 1079f0d..b2597e0 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -9,10 +9,12 @@ scyther_SOURCES = main.c \
 		 scanner.l parser.y \
 		 memory.c memory.h \
 		 terms.c terms.h \
+		 termmaps.c termmaps.h \
 		 termlists.c termlists.h \
 		 symbols.c symbols.h \
 		 knowledge.c knowledge.h \
 		 runs.c runs.h \
+		 claims.c claims.h \
 		 modelchecker.c modelchecker.h \
 		 report.c report.h \
 		 error.c error.h \
diff --git a/src/compiler.c b/src/compiler.c
index bd624df..7694375 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -57,6 +57,7 @@ Term CLAIM_Nisynch;
  * Global stuff
  */
 
+//! Levels of scope: global, protocol, role
 #define MAXLEVELS 3
 static Termlist leveltl[MAXLEVELS];
 static int level;
@@ -66,10 +67,11 @@ static Role thisRole;
 
 /* ------------------------------------------------------------------- */
 
-/*
-   Compile the tac into the system
-*/
-
+//! Compile the tac into the system
+/**
+ *@todo Currently, the semantics assume all labels are globally unique, but this is not enforced yet. There should be some automatic renaming when compositing protocols.
+ *\sa oki_nisynch
+ */
 void
 compile (System mysys, Tac tc, int maxrunsset)
 {
@@ -108,6 +110,10 @@ compile (System mysys, Tac tc, int maxrunsset)
   levelDone ();
 }
 
+//! Print error line number.
+/**
+ *@todo This is obsolete, and should all go to stderr
+ */
 void
 errorTac (int lineno)
 {
@@ -115,6 +121,7 @@ errorTac (int lineno)
   exit (1);
 }
 
+//! Enter nested scope.
 void
 levelInit (void)
 {
@@ -126,6 +133,7 @@ levelInit (void)
   leveltl[level] = NULL;
 }
 
+//! Leave nested scope.
 void
 levelDone (void)
 {
diff --git a/src/main.c b/src/main.c
index 9021958..ffdeeeb 100644
--- a/src/main.c
+++ b/src/main.c
@@ -261,6 +261,7 @@ main (int argc, char **argv)
 
   /* initialize symbols */
   termsInit ();
+  termmapsInit ();
   termlistsInit ();
   knowledgeInit ();
   symbolsInit ();
@@ -404,6 +405,7 @@ main (int argc, char **argv)
   symbolsDone ();
   knowledgeDone ();
   termlistsDone ();
+  termmapsDone ();
   termsDone ();
 
   /* memory clean up? */
diff --git a/src/termmaps.c b/src/termmaps.c
new file mode 100644
index 0000000..78a7ef0
--- /dev/null
+++ b/src/termmaps.c
@@ -0,0 +1,107 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include "termmaps.h"
+#include "debug.h"
+#include "memory.h"
+
+//! Open termmaps code.
+void
+termmapsInit (void)
+{
+  return;
+}
+
+//! Close termmaps code.
+void
+termmapsDone (void)
+{
+  return;
+}
+
+//! Allocate memory for a termmap node.
+/**
+ *@return A pointer to uninitialised memory of the size of a termmap node.
+ */
+Termmap
+makeTermmap (void)
+{
+  /* inline candidate */
+  return (Termmap) memAlloc (sizeof (struct termmap));
+}
+
+//! Get function result
+/**
+ *@return Yields f(x), or -1 when it is not present.
+ */
+int
+termmapGet (Termmap f, const Term x)
+{
+  while (f != NULL)
+    {
+      if (isTermEqual (x, f->term))
+	  return f->result;
+      f = f->next;
+    }
+  return -1;
+}
+
+//! Add a value to a function.
+/**
+ *@return Adds f(x)=y to an existing function f. If f is NULL, a function is created. If x is already in the domain, the value is replaced.
+ */
+Termmap
+termmapSet (const Termmap f, const Term x, const int y)
+{
+  Termmap fscan;
+
+  //! Determine whether term already occurs
+  fscan = f;
+  while (fscan != NULL)
+    {
+      if (isTermEqual (x, fscan->term))
+	{
+	  //! Is the result correct already?
+	  if (fscan->result != y)
+	      fscan->result = y;
+          return f;
+	}
+      fscan = fscan->next;
+    }
+  //! Not occurred yet, make new node
+  fscan = makeTermmap ();
+  fscan->term = x;
+  fscan->result = y;
+  fscan->next = f;
+  return fscan;
+}
+
+//! Duplicate a function
+Termmap
+termmapDuplicate (const Termmap f)
+{
+  if (f != NULL)
+    {
+      Termmap g;
+
+      g = makeTermmap ();
+      g->term = f->term;
+      g->result = f->result;
+      g->next = termmapDuplicate (f->next);
+      return g;
+    }
+  else
+    {
+      return NULL;
+    }
+}
+
+//! Delete a function
+void
+termmapDelete (const Termmap f)
+{
+  if (f != NULL)
+    {
+      termmapDelete (f->next);
+      memFree (f, sizeof (struct termmap));
+    }
+}
diff --git a/src/termmaps.h b/src/termmaps.h
new file mode 100644
index 0000000..98d32ad
--- /dev/null
+++ b/src/termmaps.h
@@ -0,0 +1,30 @@
+#ifndef TERMMAPS
+#define TERMMAPS
+
+#include "terms.h"
+
+//! The function container for the term to integer function type.
+/**
+ *\sa term
+ */
+struct termmap
+{
+  //! The term element for this node.
+  Term term;
+  //! Next node pointer or NULL for the last element of the function.
+  struct termmap *next;
+  //! Function result
+  int result;
+};
+
+//! Shorthand for termmap pointers.
+typedef struct termmap *Termmap;
+
+void termmapsInit (void);
+void termmapsDone (void);
+int termmapGet (Termmap f, const Term x);
+Termmap termmapSet (const Termmap f, const Term x, const int y);
+Termmap termmapDuplicate (const Termmap f);
+void termmapDelete (const Termmap f);
+
+#endif