diff --git a/tasks.c b/tasks.c
index 1e5541eb9..f32e5df24 100644
--- a/tasks.c
+++ b/tasks.c
@@ -982,6 +982,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
                 }
             #endif
 
+            //@ open taskISRLockInv();
+            //@ open readyLists_p();
+            //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
             if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
             {
                 
diff --git a/verification/verifast/proof/nathan/list_predicates.h b/verification/verifast/proof/nathan/list_predicates.h
index 439b092b5..400dbf91c 100644
--- a/verification/verifast/proof/nathan/list_predicates.h
+++ b/verification/verifast/proof/nathan/list_predicates.h
@@ -30,6 +30,48 @@ predicate xList_gen(struct xLIST *l) =
 	l->uxNumberOfItems |-> _ &*&
 	l->pxIndex |-> _;
 
+predicate List_p(List_t* l);
+@*/
+
+
+/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
+/* @
+predicate DLS(
+	struct xLIST_ITEM *n,
+	struct xLIST_ITEM *nprev,
+	struct xLIST_ITEM *mnext,
+	struct xLIST_ITEM *m,
+	list<struct xLIST_ITEM * > cells,
+	list<TickType_t > vals,
+	struct xLIST *pxContainer) =
+	n == m
+		? cells == cons(n, nil) &*&
+			vals == cons(?v, nil) &*&
+			xLIST_ITEM(n, v, mnext, nprev, pxContainer)
+		: cells == cons(n, ?cells0) &*&
+			vals == cons(?v, ?vals0) &*&
+			xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
+@*/
+
+
+/* @
+predicate xLIST(
+	struct xLIST *l,
+	int uxNumberOfItems,
+	struct xLIST_ITEM *pxIndex,
+	struct xLIST_ITEM *xListEnd,
+	list<struct xLIST_ITEM *>cells,
+	list<TickType_t >vals) =
+	l->uxNumberOfItems |-> uxNumberOfItems &*&
+	l->pxIndex |-> pxIndex &*&
+	mem(pxIndex, cells) == true &*&
+	xListEnd == &(l->xListEnd) &*&
+	xListEnd == head(cells) &*&
+	portMAX_DELAY == head(vals) &*&
+	struct_xLIST_ITEM_padding(&l->xListEnd) &*&
+	length(cells) == length(vals) &*&
+	uxNumberOfItems + 1 == length(cells) &*&
+	DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
 @*/
 
 #endif /* LIST_PREDICATES_H */
\ No newline at end of file
diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h
index 5918d6b90..a72731d40 100644
--- a/verification/verifast/proof/ready_list_predicates.h
+++ b/verification/verifast/proof/ready_list_predicates.h
@@ -1,8 +1,42 @@
 #ifndef READY_LIST_PREDICATES_H
 #define READY_LIST_PREDICATES_H
 
+
 /*@
-predicate readyLists_p();
+// TODO: Replace List_p by Aaloks list predicate
+predicate List_array_p(List_t* array, int size) =
+    pointer_within_limits(array) == true &*&
+    size > 0 &*&
+    List_p(array) &*&
+    size > 1
+        ? List_array_p(array + 1, size - 1)
+        : true;
+
+// For testing purposes only!
+// TODO: Replace by Aaloks list predicate
+predicate List_p(List_t* l);
+@*/
+
+
+/*@
+predicate readyLists_p() =
+    List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES);
+@*/
+
+
+/*@
+lemma void List_array_p_index_within_limits(List_t* array, int index)
+requires List_array_p(array, ?size) &*&
+         0 <= index &*& index < size;
+ensures List_array_p(array, size) &*&
+        pointer_within_limits(&array[index]) == true;
+{
+    open List_array_p(array, size);
+    if( index > 0) {
+        List_array_p_index_within_limits(&array[1], index-1);
+    }
+    close List_array_p(array, size);
+}
 @*/
 
 #endif /* READY_LIST_PREDICATES_H */
\ No newline at end of file