diff --git a/tasks.c b/tasks.c
index e8d2094eb..9c9b67cb5 100644
--- a/tasks.c
+++ b/tasks.c
@@ -84,6 +84,8 @@
     #include "verifast_port_contracts.h"
     #include "verifast_lock_predicates.h"
     #include "verifast_lists_extended.h"
+    #include "single_core_proofs/scp_list_predicates.h"
+    #include "single_core_proofs_extended/scp_list_predicates_extended.h"
 
     #include "snippets/rp2040_port_c_snippets.c"
 
@@ -1100,84 +1102,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
                      */
                     /*@
                     if( gTaskItem_0 == gListEnd ) {
-                        open DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, 
-                                 gCells, gVals, gReadyList);
-                        // open DLS and xLIST_ITEM predicates to justify
-                        // accessing `gTaskItem_0->pxNext`
-                        assert( xLIST_ITEM(gListEnd, ?gV, ?gNext, gEndPrev2, gReadyList) );
-                        open xLIST_ITEM(gListEnd, gV, gNext, gEndPrev2, gReadyList);
-                        assert( DLS(gNext, gListEnd, gListEnd, gEndPrev2, drop(1, gCells), drop(1, gVals), gReadyList ) );
-                        open DLS(gNext, gListEnd, gListEnd, gEndPrev2, drop(1, gCells), drop(1, gVals), gReadyList );
-                        
-                        // open DLS and xLIST_ITEM predicates to prove
-                        // `mem( gTaskItem_0->pxNext, gCells) == true )`
-                        // which requires accessing `gTaskItem_0->pxNext`
-                        assert( xLIST_ITEM(gNext, ?gV_next, ?gNextNext, gListEnd, gReadyList) );
-                        open xLIST_ITEM(gNext, gV_next, gNextNext, gListEnd, gReadyList);
-                        assert( mem(gTaskItem_0->pxNext, gCells) == true );
-                        close xLIST_ITEM(gNext, gV_next, gNextNext, gListEnd, gReadyList);
+                        DLS_end_next_open(gReadyList, gTaskItem_0);
                     } else {
-                        // open DLS and xLIST_ITEM predicates to justify
-                        // accessing `gTaskItem_0->pxNext`
-                        split(gListEnd, gEndPrev2, gListEnd, gEndPrev2, 
-                              gCells, gVals, gTaskItem_0, gTaskItemIndex_0);
-                        // DLS prefix
-                        assert( DLS(gListEnd, gEndPrev2, gTaskItem_0, ?gTaskItem_0_prev, 
-                                    take(gTaskItemIndex_0, gCells), take(gTaskItemIndex_0, gVals),
-                                    gReadyList) );
-                        // DLS suffix
-                        assert( DLS(gTaskItem_0, gTaskItem_0_prev, gListEnd, gEndPrev2, 
-                                    drop(gTaskItemIndex_0, gCells), drop(gTaskItemIndex_0, gVals),
-                                    gReadyList) );
-                        open DLS(gTaskItem_0, gTaskItem_0_prev, gListEnd, gEndPrev2, 
-                                    drop(gTaskItemIndex_0, gCells), drop(gTaskItemIndex_0, gVals),
-                                    gReadyList);
-                        assert( xLIST_ITEM(gTaskItem_0, ?gV, ?gTaskItem_0_next,  gTaskItem_0_prev, gReadyList) );
-                        
-                        
-                        // open DLS and xLIST_ITEM predicates to prove
-                        // `mem( gTaskItem_0->pxNext, gCells) == true )`
-                        // which requires accessing `gTaskItem_0->pxNext`
-                        if(gTaskItem_0 == gEndPrev2) {
-                            // `gTaskItem_0` is last element in DLS suffix
-                            // -> `gTaskItem_0_next` is head fo DLS prefix
-                            // open DLS prefix
-                            pxTaskItem->pxNext;
-                            assert( mem(gTaskItem_0->pxNext, gCells) == true );
-                            ;
-                        } else {
-                            // `gTaskItem_0` is not end of DLS suffix
-                            // -> `gTaskItem_0_next` is also in DLS suffix
-                            // open DLS suffix one step further
-                            
-                            
-                            assert( DLS(gTaskItem_0_next, gTaskItem_0, gListEnd, gEndPrev2, 
-                                        drop(1, drop(gTaskItemIndex_0, gCells)), drop(1, drop(gTaskItemIndex_0, gVals)), //drop(gTaskItemIndex_0 + 1, gCells), drop(gTaskItemIndex_0 + 1, gVals), 
-                                        gReadyList) );
-                            open DLS(gTaskItem_0_next, gTaskItem_0, gListEnd, gEndPrev2, 
-                                            drop(1, drop(gTaskItemIndex_0, gCells)), drop(1, drop(gTaskItemIndex_0, gVals)),
-                                            gReadyList);
-                            assert( xLIST_ITEM(gTaskItem_0_next, ?gNextVal, ?gTaskItem_0_next_next, gTaskItem_0, gReadyList) );
-                            //open xLIST_ITEM(gTaskItem_0_next, gNextVal, gTaskItem_0_next_next, gTaskItem_0, gReadyList);
-                            pxTaskItem->pxNext;
-                            assert( gTaskItem_0_next == pxTaskItem->pxNext );
-                            assert( mem(gTaskItem_0_next, drop(1, drop(gTaskItemIndex_0, gCells))) == true );
-                            //assert( gCells == cons(_, drop(1, drop(gTaskItemIndex_0, gCells)) );
-                            assert( mem(gTaskItem_0_next, drop(gTaskItemIndex_0, gCells)) == true );
-                            mem_suffix_implies_mem(gTaskItem_0_next, gCells, gTaskItemIndex_0);
-                            assert( mem(gTaskItem_0_next, gCells) == true );
-                            assert( mem(gTaskItem_0->pxNext, gCells) == true );
-
-                            close xLIST_ITEM(gTaskItem_0_next, gNextVal, gTaskItem_0_next_next, gTaskItem_0, gReadyList);
-                            close DLS(gTaskItem_0_next, gTaskItem_0, gListEnd, gEndPrev2, 
-                                      drop(1, drop(gTaskItemIndex_0, gCells)), drop(1, drop(gTaskItemIndex_0, gVals)),
-                                      gReadyList);
-
-                        }
-                        
-                        
-                        
-                        
+                        DLS_nonEndItem_next_open(gReadyList, gTaskItem_0); 
                     }
                     @*/
                     pxTaskItem = pxTaskItem->pxNext;
diff --git a/verification/verifast/proof/single_core_proofs_extended/README.md b/verification/verifast/proof/single_core_proofs_extended/README.md
new file mode 100644
index 000000000..05888276b
--- /dev/null
+++ b/verification/verifast/proof/single_core_proofs_extended/README.md
@@ -0,0 +1,4 @@
+This directory contains proofs that concern the predicates and proofs written
+by Aalok Thakkar and Nathan Chong, see directory `single_core_proofs`.
+For now, we want to have a clear separation between the reused proofs in
+`single_core_proofs` and any new proofs.
\ No newline at end of file
diff --git a/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
new file mode 100644
index 000000000..65c34f379
--- /dev/null
+++ b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
@@ -0,0 +1,180 @@
+#ifndef SCP_LIST_PREDICATES_EXTENDED_H
+#define SCP_LIST_PREDICATES_EXTENDED_H
+
+#include "single_core_proofs/scp_list_predicates.h"
+
+/*@
+lemma void DLS_end_next_open(struct xLIST* gReadyList, struct xLIST_ITEM* gTaskItem_0)
+requires
+    DLS(?gListEnd, ?gEndPrev2, gListEnd, gEndPrev2, ?gCells, ?gVals, gReadyList) &*&
+    mem(gTaskItem_0, gCells) == true &*&
+    gListEnd == head(gCells) &*&
+    length(gCells) == length(gVals) &*&
+    length(gCells) > 1 
+    &*&
+    gTaskItem_0 == gListEnd;
+ensures xLIST_ITEM(gListEnd, ?gV, ?gNext, gEndPrev2, gReadyList) &*&
+        DLS(gNext, gListEnd, gListEnd, gEndPrev2, drop(1, gCells), drop(1, gVals), gReadyList ) &*&
+        mem(gNext, gCells) == true;
+{
+    open DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, 
+             gCells, gVals, gReadyList);
+    // open DLS and xLIST_ITEM predicates to justify
+    // accessing `gTaskItem_0->pxNext`
+    assert( xLIST_ITEM(gListEnd, ?gV, ?gNext, gEndPrev2, gReadyList) );
+    open xLIST_ITEM(gListEnd, gV, gNext, gEndPrev2, gReadyList);
+    assert( DLS(gNext, gListEnd, gListEnd, gEndPrev2, drop(1, gCells), drop(1, gVals), gReadyList ) );
+    open DLS(gNext, gListEnd, gListEnd, gEndPrev2, drop(1, gCells), drop(1, gVals), gReadyList );
+    
+    // open DLS and xLIST_ITEM predicates to prove
+    // `mem( gTaskItem_0->pxNext, gCells) == true )`
+    // which requires accessing `gTaskItem_0->pxNext`
+    assert( xLIST_ITEM(gNext, ?gV_next, ?gNextNext, gListEnd, gReadyList) );
+    open xLIST_ITEM(gNext, gV_next, gNextNext, gListEnd, gReadyList);
+    assert( mem(gTaskItem_0->pxNext, gCells) == true );
+    close xLIST_ITEM(gNext, gV_next, gNextNext, gListEnd, gReadyList);
+
+    // closing what we opened above
+    close DLS(gNext, gListEnd, gListEnd, gEndPrev2, drop(1, gCells), drop(1, gVals), gReadyList );
+    close xLIST_ITEM(gListEnd, gV, gNext, gEndPrev2, gReadyList);
+}
+
+
+lemma void DLS_nonEndItem_next_open(struct xLIST* gReadyList, struct xLIST_ITEM* gTaskItem_0)
+requires
+    DLS(?gListEnd, ?gEndPrev2, gListEnd, gEndPrev2, ?gCells, ?gVals, gReadyList) &*&
+    mem(gTaskItem_0, gCells) == true &*&
+    gListEnd == head(gCells) &*&
+    length(gCells) == length(gVals) &*&
+    length(gCells) > 1 
+    &*&
+    gTaskItem_0 != gListEnd;
+ensures // DLS prefix
+        DLS(gListEnd, gEndPrev2, gTaskItem_0, ?gTaskItem_0_prev, 
+            take(index_of(gTaskItem_0, gCells), gCells), 
+            take(index_of(gTaskItem_0, gCells), gVals),
+            gReadyList)
+        &*&
+        // item of interest
+        xLIST_ITEM(gTaskItem_0, ?gV, ?gTaskItem_0_next, gTaskItem_0_prev, gReadyList)
+        &*&
+        // DLS suffix
+        (gTaskItem_0 != gEndPrev2
+            ? DLS(gTaskItem_0_next, gTaskItem_0, gListEnd, gEndPrev2, 
+                    drop(1, drop(index_of(gTaskItem_0, gCells), gCells)), 
+                    drop(1, drop(index_of(gTaskItem_0, gCells), gVals)),
+                    gReadyList)
+            : true
+        )
+        &*&
+        mem(gTaskItem_0_next, gCells) == true;
+{
+    int gTaskItemIndex_0 = index_of(gTaskItem_0, gCells);
+
+
+    // open DLS and xLIST_ITEM predicates to justify
+    // accessing `gTaskItem_0->pxNext`
+    split(gListEnd, gEndPrev2, gListEnd, gEndPrev2, 
+            gCells, gVals, gTaskItem_0, gTaskItemIndex_0);
+    // DLS prefix
+    assert( DLS(gListEnd, gEndPrev2, gTaskItem_0, ?gTaskItem_0_prev, 
+                take(gTaskItemIndex_0, gCells), take(gTaskItemIndex_0, gVals),
+                gReadyList) );
+    // DLS suffix
+    assert( DLS(gTaskItem_0, gTaskItem_0_prev, gListEnd, gEndPrev2, 
+                drop(gTaskItemIndex_0, gCells), drop(gTaskItemIndex_0, gVals),
+                gReadyList) );
+    open DLS(gTaskItem_0, gTaskItem_0_prev, gListEnd, gEndPrev2, 
+                drop(gTaskItemIndex_0, gCells), drop(gTaskItemIndex_0, gVals),
+                gReadyList);
+    assert( xLIST_ITEM(gTaskItem_0, ?gV, ?gTaskItem_0_next, gTaskItem_0_prev, gReadyList) );
+    
+    
+    // open DLS and xLIST_ITEM predicates to prove
+    // `mem( gTaskItem_0->pxNext, gCells) == true )`
+    // which requires accessing `gTaskItem_0->pxNext`
+    if(gTaskItem_0 == gEndPrev2) {
+        // `gTaskItem_0` is last element in DLS suffix
+        // -> `gTaskItem_0_next` is head fo DLS prefix
+        // open DLS prefix
+        open xLIST_ITEM(gTaskItem_0, gV, gTaskItem_0_next, gTaskItem_0_prev, gReadyList);
+        assert( gCells == cons(_, _) );
+        assert( mem(gTaskItem_0->pxNext, gCells) == true );
+        
+        // close item of interest
+        close xLIST_ITEM(gTaskItem_0, gV, gTaskItem_0_next, gTaskItem_0_prev, gReadyList);
+    } else {
+        // `gTaskItem_0` is not end of DLS suffix
+        // -> `gTaskItem_0_next` is also in DLS suffix
+        // open DLS suffix one step further
+        
+        // rest of DLS suffix
+        assert( DLS(gTaskItem_0_next, gTaskItem_0, gListEnd, gEndPrev2, 
+                    drop(1, drop(gTaskItemIndex_0, gCells)), drop(1, drop(gTaskItemIndex_0, gVals)), //drop(gTaskItemIndex_0 + 1, gCells), drop(gTaskItemIndex_0 + 1, gVals), 
+                    gReadyList) );
+        open DLS(gTaskItem_0_next, gTaskItem_0, gListEnd, gEndPrev2, 
+                        drop(1, drop(gTaskItemIndex_0, gCells)), drop(1, drop(gTaskItemIndex_0, gVals)),
+                        gReadyList);
+        assert( xLIST_ITEM(gTaskItem_0_next, ?gNextVal, ?gTaskItem_0_next_next, gTaskItem_0, gReadyList) );
+        open xLIST_ITEM(gTaskItem_0, gV, gTaskItem_0_next, gTaskItem_0_prev, gReadyList); 
+        assert( gTaskItem_0_next == gTaskItem_0->pxNext );
+        assert( mem(gTaskItem_0_next, drop(1, drop(gTaskItemIndex_0, gCells))) == true );
+        //assert( gCells == cons(_, drop(1, drop(gTaskItemIndex_0, gCells)) );
+        assert( mem(gTaskItem_0_next, drop(gTaskItemIndex_0, gCells)) == true );
+        mem_suffix_implies_mem(gTaskItem_0_next, gCells, gTaskItemIndex_0);
+        assert( mem(gTaskItem_0_next, gCells) == true );
+        assert( mem(gTaskItem_0->pxNext, gCells) == true );
+
+        // close rest of DLS suffix
+        close xLIST_ITEM(gTaskItem_0_next, gNextVal, gTaskItem_0_next_next, gTaskItem_0, gReadyList);
+        close DLS(gTaskItem_0_next, gTaskItem_0, gListEnd, gEndPrev2, 
+                    drop(1, drop(gTaskItemIndex_0, gCells)), drop(1, drop(gTaskItemIndex_0, gVals)),
+                    gReadyList);
+
+        // close item of interest
+        close xLIST_ITEM(gTaskItem_0, gV, gTaskItem_0_next, gTaskItem_0_prev, gReadyList); 
+    }
+}
+@*/
+
+/* By verifying the following function, we can validate that the above lemmas
+ * apply to the use cases they are meant for.
+ */
+void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem)
+/*@ requires
+        DLS(?gListEnd, ?gEndPrev2, gListEnd, gEndPrev2, ?gCells, ?gVals, ?gReadyList) &*&
+        mem(pxTaskItem, gCells) == true &*&
+        gListEnd == head(gCells) &*&
+        length(gCells) == length(gVals) &*&
+        length(gCells) > 1;
+@*/
+/*@ ensures
+        DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) &*&
+        mem(pxTaskItem, gCells) == true;
+@*/
+{
+    //@ int gTaskItemIndex_0 = index_of(pxTaskItem, gCells);
+    //@ struct xLIST_ITEM* gTaskItem_0 = pxTaskItem;
+
+    /*@
+    if( gTaskItem_0 == gListEnd ) {
+        DLS_end_next_open(gReadyList, gTaskItem_0);
+    } else {
+        DLS_nonEndItem_next_open(gReadyList, gTaskItem_0);
+    }
+    @*/
+    pxTaskItem = pxTaskItem->pxNext;
+
+    //@ struct xLIST_ITEM* gTaskItem_1 = pxTaskItem;
+
+    //@ assert( mem(gTaskItem_1, gCells) == true );
+
+
+
+    // ignore post condition until closing lemmas are finished
+    //@ assume(false);
+}
+
+
+
+#endif /* SCP_LIST_PREDICATES_EXTENDED_H */
\ No newline at end of file