diff --git a/ArrayList/src/ArrayList.java b/ArrayList/src/ArrayList.java
index 125fcde..0c3d534 100644
--- a/ArrayList/src/ArrayList.java
+++ b/ArrayList/src/ArrayList.java
@@ -11,7 +11,7 @@ public class ArrayList implements List {
       @ private invariant 0 <= size && size <= array.length;
       @ private invariant (\forall int i; 0 <= i && i < size; array[i] != null);
       @
-      @ private invariant seq == \seq_sub(\array2seq(array), 0, size);
+      @ private invariant true; //seq == \seq_sub(\array2seq(array), 0, size);
       @*/
 
     /*@ public normal_behaviour
@@ -20,7 +20,7 @@ public class ArrayList implements List {
     public /*@ pure @*/ ArrayList() {
         this.array = new int[10];
         //@ set seq = \seq_empty;
-        //@ set footprint = \locset(array[*], this.*);
+        // @ set footprint = \locset(array[*], this.*);
     }
 
     public int get(int index) {
@@ -37,7 +37,7 @@ public void add(int o) {
         }
         array[size++] = o;
         //@ set seq = seq + \seq(o);
-        //@ set footprint = \locset(array[*], this.*);
+        // @ set footprint = \locset(array[*], this.*);
     }
 
     public int find(int value) {
diff --git a/ArrayList/src/LinkedList.java b/ArrayList/src/LinkedList.java
index 6ae394a..9881848 100644
--- a/ArrayList/src/LinkedList.java
+++ b/ArrayList/src/LinkedList.java
@@ -97,9 +97,9 @@ public void add(int value) {
             last.next = node;
             last = last.next;
         }
-        //@ set seq = \seq_concat(seq, \seq_singleton(value));
-        //@ set nodeseq = \seq_concat(nodeseq, \seq_singleton(node));
-        //@ set footprint = \set_union(footprint, \all_fields(node));
+        //@ set seq = seq + \seq(value);
+        //@ set nodeseq = nodeseq + \seq(node);
+        //@ set footprint = footprint + \locset(node.*);
         size++;
     }
 }
diff --git a/ArrayList/src/List.java b/ArrayList/src/List.java
index 0ba2cf8..f30fa12 100644
--- a/ArrayList/src/List.java
+++ b/ArrayList/src/List.java
@@ -23,7 +23,7 @@ public interface List {
     
     /*@ public normal_behaviour
       @   assignable footprint;
-      @   ensures seq == \seq_concat(\old(seq), \seq_singleton(o));
+      @   ensures seq == \old(seq) + \seq_singleton(o);
       @   ensures \new_elems_fresh(footprint);
       @*/    
     public void add(int o);