#include <vcc.h>
#include "Z2RZ1.h"
#include <limits.h>

void startScheduler()
{
	taskID runningZ1,runningZ1;
//	_(assert \false )
	_( unwrap &(sstm) )
	_( unwrap lsts )
//	_( assert (	( lsts->delayedLength == lsts->delayedLengthZ2 + lsts->oDelayedLength ) ) )
	_( ghost 
		{
			sstm.currentTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];
			sstm.tickCount = 0;
			sstm.schedulerRunning = \true;
		}	
	 )
	_( wrap lsts )
	_( wrap &(sstm) )
}

void taskDelayUntil1(  _( ghost \natural pWT )
								_( ghost \natural delay )
							 )
{
///////////////////////Z1////////////////////////////
	runningAndPWTZ1 resultZ1;
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay )
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	runningAndPWTZ2 resultZ2;
	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTAZ2 = pWT + delay )
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
///////////////////////Z2////////////////////////////

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}

void taskDelayUntil2(	_( ghost \natural pWT )
						_( ghost \natural delay )
					)
{
///////////////////////Z1////////////////////////////
	runningAndPWTZ1 resultZ1;
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay )
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	runningAndPWTZ2 resultZ2;
	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTAZ2 = pWT + delay )
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
///////////////////////Z2////////////////////////////

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}

void taskDelayUntil3(	_( ghost \natural pWT )
						_( ghost \natural delay )
				    )
{
///////////////////////Z1////////////////////////////
	runningAndPWTZ1 resultZ1;
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay )
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA - ( maxNumVal + 1 ) )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	runningAndPWTZ2 resultZ2;
	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTAZ2 = pWT + delay - ( maxNumVal + 1 ) )
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
///////////////////////Z2////////////////////////////

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}


void taskDelayUntil4	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
{
	_( ghost taskID prevTask )
///////////////////////Z1////////////////////////////
	runningAndPWTZ1 resultZ1;
	_( ghost \natural position ) 
				/*	The index in 'delayed' list at which the
					the currently running task need to be placed.
					In Z2 this is an index in 'delayedZ2'.
				*/
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay )

	_( assume ( position <= lsts->delayedLength ) )

	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )

	/*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	*/
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	runningAndPWTZ2 resultZ2;

	_( ghost \natural positionZ2 ) 
				/*	The index in 'delayedZ2' list at which the
					the currently running task need to be placed.
				*/
	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayedZ2 queue.
						*/
	_( ghost tTAZ2 = pWT + delay )

	_( assume ( positionZ2 <= lsts->delayedLengthZ2 ) )

	_( assume \forall \natural j;
			( j < positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] <= tTAZ2 )
	 )

	_( assume 
			( positionZ2 < lsts->delayedLengthZ2 - 1 ) ==> 
				( lsts->timeToAwakeZ2[ positionZ2 + 1 ] > tTAZ2 )
	 )

	_( assume \forall \natural j;
			( j >= positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] > tTAZ2 )
	 )

	/*	The above assume statements 
		specify that 'i' is the index 
		in list 'delayedZ2' at which the
		running task need to be added
	*/
///////////////////////Z2////////////////////////////
	_( assume ( position == positionZ2 ) )

	_( unwrap &sstm )
	_( unwrap lsts )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( ghost
			{
				sstm.currentTask = lsts->ready[ sstm.topReadyPriority ].list[ 1 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					( i < lsts->ready[ sstm.topReadyPriority ].length - 1 )
						? lsts->ready[ sstm.topReadyPriority ].list[ i + 1 ]
						: UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( lsts->ready[ sstm.topReadyPriority ].index[ t ] < 
								  lsts->ready[ sstm.topReadyPriority ].length 
					)	?	(	( t == prevTask )
									? lsts->ready[ sstm.topReadyPriority ].length - 1
									: lsts->ready[ sstm.topReadyPriority ].index[ t ] - 1
							)
						:	lsts->ready[ sstm.topReadyPriority ].length - 1
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 
					lsts->ready[ sstm.topReadyPriority ].length - 1
				;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;
/////////UpdateDelayed

/////////UpdateDelayedZ2
				lsts->delayedZ2 = \lambda \natural i;
					( i <= lsts->delayedLengthZ2 )
						?	(	( i < positionZ2 ) 
									? lsts->delayedZ2[ i ] 
									:	(	( i == positionZ2 ) 
												? prevTask
						  						: lsts->delayedZ2[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayedZ2 = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2	)	
									?	(	( lsts->indexDelayedZ2[ t ] < positionZ2 )
												? lsts->indexDelayedZ2[ t ]
												: lsts->indexDelayedZ2[ t ] + 1
										)
									:	lsts->delayedLengthZ2 + 1
							)
						:	positionZ2
				;

				lsts->timeToAwakeZ2 = \lambda \natural i; 
					( i <= lsts->delayedLengthZ2 ) 
						?	(	( i < positionZ2 ) 
									? lsts->timeToAwakeZ2[ i ] 
									:	(	( i == positionZ2 )
											? tTAZ2
											: lsts->timeToAwakeZ2[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLengthZ2 = lsts->delayedLengthZ2 + 1;
/////////UpdateDelayedZ2
			}
	  )

	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( wrap &sstm )

///////////////////////Z1////////////////////////////
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )

///////////////////////Z2////////////////////////////

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}

void taskDelayUntil5(	_( ghost \natural pWT )
						_( ghost \natural delay )
				    )
{
	_(ghost taskID prevTask )
	_( ghost unsigned runnerUpPrty ) 
				//	The index of the second highest nonempty
				//	sequence in ready. As the ready 
				//  sequence at index 'sstm.topReadyPriority'
				//  is empty, the next task to schedule 
				//  need to be from index 'runnerUpPrty', 
				//  which is assured bu the assume statements
				//  on 'runnerUpPrty' below
///////////////////////Z1////////////////////////////
	runningAndPWTZ1 resultZ1;
	_( ghost \natural position ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
				//  In Z2 this is an index in 'delayedZ2'.
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay )

	_( assume ( position <= lsts->delayedLength ) )
	 	
	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )

	 /*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	 */
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	runningAndPWTZ2 resultZ2;
	_( ghost \natural positionZ2 ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
				//  In Z2 this is an index in 'delayedZ2'.

	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayedZ2 queue.
						*/
	_( ghost tTAZ2 = pWT + delay )

	_( assume ( positionZ2 <= lsts->delayedLengthZ2 ) )

	_( assume \forall \natural j;
			( j < positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] <= tTAZ2 )
	 )

	_( assume 
			( positionZ2 < lsts->delayedLengthZ2 - 1 ) ==> 
				( lsts->timeToAwakeZ2[ positionZ2 + 1 ] > tTAZ2 )
	 )

	_( assume \forall \natural j;
			( j >= positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] > tTAZ2 )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in list 'delayedZ2' at which the
		running task need to be added
	 */
///////////////////////Z2////////////////////////////
	_( assume ( position == positionZ2 ) )

	_( assume (	( runnerUpPrty > 0 ) &&
				( runnerUpPrty < sstm.topReadyPriority )
			  )	
	 )
	_( assume ( lsts->ready[ runnerUpPrty ].length > 0 ) )	
	_( assume ( &( lsts->ready[ runnerUpPrty ] ) \in ( &sstm )->\owns ) )	
	_( assume \forall unsigned j;
			(	( j >= 1 ) &&
				( j <= maxPrio ) &&
				( j != sstm.topReadyPriority ) &&
 				( lsts->ready[ j ].length > 0 ) 
			) ==> ( j <= runnerUpPrty )
	 )
	 /*	The above four assume statements 
		specify that 'runnerUpPrty' is the index 
		of the sencond highest nonempty
		ready sequence.
	 */

	_( assume (	( runnerUpPrty > 0 ) &&
				( runnerUpPrty < sstm.topReadyPriority )
			  )	
	 )
	_( assume ( lsts->ready[ runnerUpPrty ].length > 0 ) )	
	_( assume ( &( lsts->ready[ runnerUpPrty ] ) \in ( &sstm )->\owns ) )	
	_( assume \forall unsigned j;
			(	( j >= 1 ) &&
				( j <= maxPrio ) &&
				( j != sstm.topReadyPriority ) &&
 				( lsts->ready[ j ].length > 0 ) 
			) ==> ( j <= runnerUpPrty )
	 )
	 /*	The above four assume statements 
		specify that 'runnerUpPrty' is the index 
		of the sencond highest nonempty
		ready sequence.
	 */

	_( unwrap &sstm )
	_( assert \inv( &sstm ) )
	_( unwrap lsts )
	_( assert \inv( lsts ) )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )

	 _( ghost
			{
				sstm.currentTask = lsts->ready[ runnerUpPrty ].list[ 0 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( \natural ) 0
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 0;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;
/////////UpdateDelayed

/////////UpdateDelayedZ2
				lsts->delayedZ2 = \lambda \natural i;
					( i <= lsts->delayedLengthZ2 )
						?	(	( i < positionZ2 ) 
									? lsts->delayedZ2[ i ] 
									:	(	( i == positionZ2 ) 
												? prevTask
						  						: lsts->delayedZ2[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayedZ2 = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2	)	
									?	(	( lsts->indexDelayedZ2[ t ] < positionZ2 )
												? lsts->indexDelayedZ2[ t ]
												: lsts->indexDelayedZ2[ t ] + 1
										)
									:	lsts->delayedLengthZ2 + 1
							)
						:	positionZ2
				;

				lsts->timeToAwakeZ2 = \lambda \natural i; 
					( i <= lsts->delayedLengthZ2 ) 
						?	(	( i < positionZ2 ) 
									? lsts->timeToAwakeZ2[ i ] 
									:	(	( i == positionZ2 )
											? tTAZ2
											: lsts->timeToAwakeZ2[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLengthZ2 = lsts->delayedLengthZ2 + 1;
/////////UpdateDelayedZ2
			}
	  )

	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( ghost sstm.topReadyPriority = runnerUpPrty )
	_( wrap lsts )
	_( wrap &sstm )
///////////////////////Z1////////////////////////////
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
///////////////////////Z2////////////////////////////

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}


void taskDelayUntil6(	_( ghost \natural pWT )
						_( ghost \natural delay )
					)
{
	_( ghost taskID prevTask )
///////////////////////Z1////////////////////////////
	runningAndPWTZ1 resultZ1;
	_( ghost \natural position ) 
				/*	The index in 'delayed' list at which the
					the currently running task need to be placed.
					In Z2 this is an index in 'delayedZ2'.
				*/
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay )

	_( assume ( position <= lsts->delayedLength ) )

	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )

	/*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	*/
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////	
runningAndPWTZ2 resultZ2;
	_( ghost \natural positionOD ) 
				/*	The index in 'delayed' list at which the
					the currently running task need to be placed.
					In Z2 this is an index in 'delayedZ2'.
				*/
	_( ghost \natural tTAOD )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the oDelayed queue.
						*/
	_( ghost tTAOD = pWT + delay - ( maxNumVal + 1 ) )

	_( assume ( positionOD <= lsts->oDelayedLength ) )

	_( assume \forall \natural j;
			( j < positionOD ) ==> ( lsts->timeToAwakeOD[ j ] <= tTAOD )
	 )

	_( assume 
			( positionOD < lsts->oDelayedLength - 1 ) ==> 
				( lsts->timeToAwakeOD[ positionOD + 1 ] > tTAOD )
	 )

	_( assume \forall \natural j;
			( j >= positionOD ) ==> ( lsts->timeToAwakeOD[ j ] > tTAOD )
	 )

	/*	The above assume statements 
		specify that 'i' is the index 
		in list 'oDelayed' at which the
		running task need to be added
	*/
///////////////////////Z2////////////////////////////	
	_( assume ( position == lsts->delayedLengthZ2 + positionOD ) )

	_( unwrap &sstm )
	_( unwrap lsts )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( ghost
			{
				sstm.currentTask = lsts->ready[ sstm.topReadyPriority ].list[ 1 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					( i < lsts->ready[ sstm.topReadyPriority ].length - 1 )
						? lsts->ready[ sstm.topReadyPriority ].list[ i + 1 ]
						: UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( lsts->ready[ sstm.topReadyPriority ].index[ t ] < 
								  lsts->ready[ sstm.topReadyPriority ].length 
					)	?	(	( t == prevTask )
									? lsts->ready[ sstm.topReadyPriority ].length - 1
									: lsts->ready[ sstm.topReadyPriority ].index[ t ] - 1
							)
						:	lsts->ready[ sstm.topReadyPriority ].length - 1
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 
					lsts->ready[ sstm.topReadyPriority ].length - 1
				;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;
/////////UpdateDelayed

/////////UpdateODelayed
				lsts->oDelayed = \lambda \natural i;
					( i <= lsts->oDelayedLength )
						?	(	( i < positionOD ) 
									? lsts->oDelayed[ i ] 
									:	(	( i == positionOD ) 
												? prevTask
						  						: lsts->oDelayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexODelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexODelayed[ t ] < lsts->oDelayedLength	)	
									?	(	( lsts->indexODelayed[ t ] < positionOD )
												? lsts->indexODelayed[ t ]
												: lsts->indexODelayed[ t ] + 1
										)
									:	lsts->oDelayedLength + 1
							)
						:	positionOD
				;

				lsts->timeToAwakeOD = \lambda \natural i; 
					( i <= lsts->oDelayedLength ) 
						?	(	( i < positionOD ) 
									? lsts->timeToAwakeOD[ i ] 
									:	(	( i == positionOD )
											? tTAOD
											: lsts->timeToAwakeOD[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->oDelayedLength = lsts->oDelayedLength + 1;
/////////UpdateODelayed
			}
	  )

	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( wrap &sstm )
///////////////////////Z1////////////////////////////	
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA - ( maxNumVal + 1 ) )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////	
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAOD )
///////////////////////Z2////////////////////////////	

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}

void taskDelayUntil7	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
{
	_(ghost taskID prevTask )
	_( ghost unsigned runnerUpPrty ) 
				//	The index of the second highest nonempty
				//	sequence in ready. As the ready 
				//  sequence at index 'sstm.topReadyPriority'
				//  is empty, the next task to schedule 
				//  need to be from index 'runnerUpPrty', 
				//  which is assured bu the assume statements
				//  on 'runnerUpPrty' below

///////////////////////Z1////////////////////////////
	runningAndPWTZ1 resultZ1;
	_( ghost \natural position ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
				//  In Z2 this is an index in 'delayedZ2'.

	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay )

	_( assume ( position <= lsts->delayedLength ) )
	 	
	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )

	 /*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	 */
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////	
	runningAndPWTZ2 resultZ2;
	_( ghost \natural positionOD ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
				//  In Z2 this is an index in 'delayedZ2'.

	_( ghost \natural tTAOD )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTAOD = pWT + delay - ( maxNumVal + 1 ) )

	_( assume ( positionOD <= lsts->oDelayedLength ) )

	_( assume \forall \natural j;
			( j < positionOD ) ==> ( lsts->timeToAwakeOD[ j ] <= tTAOD )
	 )

	_( assume 
			( positionOD < lsts->oDelayedLength - 1 ) ==> 
				( lsts->timeToAwakeOD[ positionOD + 1 ] > tTAOD )
	 )

	_( assume \forall \natural j;
			( j >= positionOD ) ==> ( lsts->timeToAwakeOD[ j ] > tTAOD )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in list 'oDelayed' at which the
		running task need to be added
	 */
///////////////////////Z2////////////////////////////	
	_( assume ( position == lsts->delayedLengthZ2 + positionOD ) )

	_( assume (	( runnerUpPrty > 0 ) &&
				( runnerUpPrty < sstm.topReadyPriority )
			  )	
	 )
	_( assume ( lsts->ready[ runnerUpPrty ].length > 0 ) )	
	_( assume ( &( lsts->ready[ runnerUpPrty ] ) \in ( &sstm )->\owns ) )	
	_( assume \forall unsigned j;
			(	( j >= 1 ) &&
				( j <= maxPrio ) &&
				( j != sstm.topReadyPriority ) &&
 				( lsts->ready[ j ].length > 0 ) 
			) ==> ( j <= runnerUpPrty )
	 )
	 /*	The above four assume statements 
		specify that 'runnerUpPrty' is the index 
		of the sencond highest nonempty
		ready sequence.
	 */

	_( unwrap &sstm )
	_( assert \inv( &sstm ) )
	_( unwrap lsts )
	_( assert \inv( lsts ) )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )

	 _( ghost
			{
				sstm.currentTask = lsts->ready[ runnerUpPrty ].list[ 0 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( \natural ) 0
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 0;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;
/////////UpdateDelayed

/////////UpdateODelayed
				lsts->oDelayed = \lambda \natural i;
					( i <= lsts->oDelayedLength )
						?	(	( i < positionOD ) 
									? lsts->oDelayed[ i ] 
									:	(	( i == positionOD ) 
												? prevTask
						  						: lsts->oDelayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexODelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexODelayed[ t ] < lsts->oDelayedLength	)	
									?	(	( lsts->indexODelayed[ t ] < positionOD )
												? lsts->indexODelayed[ t ]
												: lsts->indexODelayed[ t ] + 1
										)
									:	lsts->oDelayedLength + 1
							)
						:	positionOD
				;

				lsts->timeToAwakeOD = \lambda \natural i; 
					( i <= lsts->oDelayedLength ) 
						?	(	( i < positionOD ) 
									? lsts->timeToAwakeOD[ i ] 
									:	(	( i == positionOD )
											? tTAOD
											: lsts->timeToAwakeOD[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->oDelayedLength = lsts->oDelayedLength + 1;
/////////UpdateODelayed
			}
	  )

	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( ghost sstm.topReadyPriority = runnerUpPrty )
	_( wrap &sstm )
///////////////////////Z1////////////////////////////	
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA - ( maxNumVal + 1 ) )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////	
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAOD )
///////////////////////Z2////////////////////////////	

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}

void taskDelayUntil8	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
{
	_( ghost taskID prevTask )
///////////////////////Z1////////////////////////////	
	runningAndPWTZ1 resultZ1;
	_( ghost \natural position ) 
				/*	The index in 'delayed' list at which the
					the currently running task need to be placed.
					In Z2 this is an index in 'delayedZ2'.
				*/
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay - ( maxNumVal + 1 ) )

	_( assume ( position <= lsts->delayedLength ) )

	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )

	/*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	*/
///////////////////////Z1////////////////////////////	

///////////////////////Z2////////////////////////////	
	runningAndPWTZ2 resultZ2;
	_( ghost \natural positionZ2 ) 
				/*	The index in 'delayed' list at which the
					the currently running task need to be placed.
					In Z2 this is an index in 'delayedZ2'.
				*/
	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayedZ2 queue.
						*/
	_( ghost tTAZ2 = pWT + delay - ( maxNumVal + 1 ) )

	_( assume ( positionZ2 <= lsts->delayedLengthZ2 ) )

	_( assume \forall \natural j;
			( j < positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] <= tTAZ2 )
	 )

	_( assume 
			( positionZ2 < lsts->delayedLengthZ2 - 1 ) ==> 
				( lsts->timeToAwakeZ2[ positionZ2 + 1 ] > tTAZ2 )
	 )

	_( assume \forall \natural j;
			( j >= positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] > tTAZ2 )
	 )

	/*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	*/
///////////////////////Z2////////////////////////////	
	_( assume position == positionZ2 )

	_( unwrap &sstm )
	_( unwrap lsts )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( ghost
			{
				sstm.currentTask = lsts->ready[ sstm.topReadyPriority ].list[ 1 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					( i < lsts->ready[ sstm.topReadyPriority ].length - 1 )
						? lsts->ready[ sstm.topReadyPriority ].list[ i + 1 ]
						: UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( lsts->ready[ sstm.topReadyPriority ].index[ t ] < 
								  lsts->ready[ sstm.topReadyPriority ].length 
					)	?	(	( t == prevTask )
									? lsts->ready[ sstm.topReadyPriority ].length - 1
									: lsts->ready[ sstm.topReadyPriority ].index[ t ] - 1
							)
						:	lsts->ready[ sstm.topReadyPriority ].length - 1
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 
					lsts->ready[ sstm.topReadyPriority ].length - 1
				;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;
/////////UpdateDelayed

/////////UpdateDelayedZ2
				lsts->delayedZ2 = \lambda \natural i;
					( i <= lsts->delayedLengthZ2 )
						?	(	( i < positionZ2 ) 
									? lsts->delayedZ2[ i ] 
									:	(	( i == positionZ2 ) 
												? prevTask
						  						: lsts->delayedZ2[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayedZ2 = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2	)	
									?	(	( lsts->indexDelayedZ2[ t ] < positionZ2 )
												? lsts->indexDelayedZ2[ t ]
												: lsts->indexDelayedZ2[ t ] + 1
										)
									:	lsts->delayedLengthZ2 + 1
							)
						:	positionZ2
				;

				lsts->timeToAwakeZ2 = \lambda \natural i; 
					( i <= lsts->delayedLengthZ2 ) 
						?	(	( i < positionZ2 ) 
									? lsts->timeToAwakeZ2[ i ] 
									:	(	( i == positionZ2 )
											? tTAZ2
											: lsts->timeToAwakeZ2[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLengthZ2 = lsts->delayedLengthZ2 + 1;
/////////UpdateDelayedZ2
			}
	  )
	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( wrap &sstm )
///////////////////////Z1////////////////////////////	
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
///////////////////////Z2////////////////////////////

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}

void taskDelayUntil9	(	_( ghost \natural pWT )
							_( ghost \natural delay )
						)
{
	_(ghost taskID prevTask )
	_( ghost unsigned runnerUpPrty ) 
				//	The index of the second highest nonempty
				//	sequence in ready. As the ready 
				//  sequence at index 'sstm.topReadyPriority'
				//  is empty, the next task to schedule 
				//  need to be from index 'runnerUpPrty', 
				//  which is assured bu the assume statements
				//  on 'runnerUpPrty' below

///////////////////////Z1////////////////////////////	
	runningAndPWTZ1 resultZ1;
	_( ghost \natural position ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
				//  In Z2 this is an index in 'delayedZ2'.

	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = pWT + delay - ( maxNumVal + 1 ) )

	_( assume ( position <= lsts->delayedLength ) )
	 	
	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	 */
///////////////////////Z1////////////////////////////	

///////////////////////Z2////////////////////////////	
	runningAndPWTZ2 resultZ2;
	_( ghost \natural positionZ2 ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
				//  In Z2 this is an index in 'delayedZ2'.

	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayedZ2 queue.
						*/
	_( ghost tTAZ2 = pWT + delay - ( maxNumVal + 1 ) )

	_( assume ( positionZ2 <= lsts->delayedLengthZ2 ) )

	_( assume \forall \natural j;
			( j < positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] <= tTAZ2 )
	 )

	_( assume 
			( positionZ2 < lsts->delayedLengthZ2 - 1 ) ==> 
				( lsts->timeToAwakeZ2[ positionZ2 + 1 ] > tTAZ2 )
	 )

	_( assume \forall \natural j;
			( j >= positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] > tTAZ2 )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in list 'delayedZ2' at which the
		running task need to be added
	 */
///////////////////////Z2////////////////////////////	
	_( assume position == positionZ2 )

	_( assume (	( runnerUpPrty > 0 ) &&
				( runnerUpPrty < sstm.topReadyPriority )
			  )	
	 )
	_( assume ( lsts->ready[ runnerUpPrty ].length > 0 ) )	
	_( assume ( &( lsts->ready[ runnerUpPrty ] ) \in ( &sstm )->\owns ) )	
	_( assume \forall unsigned j;
			(	( j >= 1 ) &&
				( j <= maxPrio ) &&
				( j != sstm.topReadyPriority ) &&
 				( lsts->ready[ j ].length > 0 ) 
			) ==> ( j <= runnerUpPrty )
	 )
	 /*	The above four assume statements 
		specify that 'runnerUpPrty' is the index 
		of the sencond highest nonempty
		ready sequence.
	 */
	_( unwrap &sstm )
	_( assert \inv( &sstm ) )
	_( unwrap lsts )
	_( assert \inv( lsts ) )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )

	 _( ghost
			{
				sstm.currentTask = lsts->ready[ runnerUpPrty ].list[ 0 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( \natural ) 0
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 0;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;
/////////UpdateDelayed

/////////UpdateDelayedZ2
				lsts->delayedZ2 = \lambda \natural i;
					( i <= lsts->delayedLengthZ2 )
						?	(	( i < positionZ2 ) 
									? lsts->delayedZ2[ i ] 
									:	(	( i == positionZ2 ) 
												? prevTask
						  						: lsts->delayedZ2[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayedZ2 = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2	)	
									?	(	( lsts->indexDelayedZ2[ t ] < positionZ2 )
												? lsts->indexDelayedZ2[ t ]
												: lsts->indexDelayedZ2[ t ] + 1
										)
									:	lsts->delayedLengthZ2 + 1
							)
						:	positionZ2
				;

				lsts->timeToAwakeZ2 = \lambda \natural i; 
					( i <= lsts->delayedLengthZ2 ) 
						?	(	( i < positionZ2 ) 
									? lsts->timeToAwakeZ2[ i ] 
									:	(	( i == positionZ2 )
											? tTAZ2
											: lsts->timeToAwakeZ2[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLengthZ2 = lsts->delayedLengthZ2 + 1;
/////////UpdateDelayedZ2
			}
	  )

	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( ghost sstm.topReadyPriority = runnerUpPrty )
	_( wrap &sstm )

///////////////////////Z1////////////////////////////
	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////	
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
///////////////////////Z2////////////////////////////	

	_( assert resultZ2.running == resultZ1.running )
	_( assert resultZ2.pWT == resultZ1.pWT)
}

void taskDelay1( _( ghost \natural delay ) )
{
	taskID running;
	_( assume ( running == sstm.currentTask ) )

}

void taskDelay2A( _( ghost \natural delay ) )
{
	_( ghost taskID prevTask )
	taskID running;

///////////////////////Z1////////////////////////////
	_( ghost \natural position ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = sstm.tickCount + delay )

	_( assume ( position <= lsts->delayedLength ) )

	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	 */
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	_( ghost \natural positionZ2 ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayedZ2 queue.
						*/
	_( ghost tTAZ2 = sstm.tickCount + delay )

	_( assume ( positionZ2 <= lsts->delayedLengthZ2 ) )

	_( assume \forall \natural j;
			( j < positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] <= tTAZ2 )
	 )

	_( assume 
			( positionZ2 < lsts->delayedLengthZ2 - 1 ) ==> 
				( lsts->timeToAwakeZ2[ positionZ2 + 1 ] > tTAZ2 )
	 )

	_( assume \forall \natural j;
			( j >= positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] > tTAZ2 )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in list 'delayedZ2' at which the
		running task need to be added
	 */
///////////////////////Z2////////////////////////////
	_( assume position == positionZ2 )

	_( unwrap &sstm )
	_( unwrap lsts )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( ghost
			{
				sstm.currentTask = lsts->ready[ sstm.topReadyPriority ].list[ 1 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					( i < lsts->ready[ sstm.topReadyPriority ].length - 1 )
						? lsts->ready[ sstm.topReadyPriority ].list[ i + 1 ]
						: UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( lsts->ready[ sstm.topReadyPriority ].index[ t ] < 
								  lsts->ready[ sstm.topReadyPriority ].length 
					)	?	(	( t == prevTask )
									? lsts->ready[ sstm.topReadyPriority ].length - 1
									: lsts->ready[ sstm.topReadyPriority ].index[ t ] - 1
							)
						:	lsts->ready[ sstm.topReadyPriority ].length - 1
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 
					lsts->ready[ sstm.topReadyPriority ].length - 1
				;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;

/////////UpdateDelayed

/////////UpdateDelayedZ2
				lsts->delayedZ2 = \lambda \natural i;
					( i <= lsts->delayedLengthZ2 )
						?	(	( i < positionZ2 ) 
									? lsts->delayedZ2[ i ] 
									:	(	( i == positionZ2 ) 
												? prevTask
						  						: lsts->delayedZ2[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayedZ2 = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2	)	
									?	(	( lsts->indexDelayedZ2[ t ] < positionZ2 )
												? lsts->indexDelayedZ2[ t ]
												: lsts->indexDelayedZ2[ t ] + 1
										)
									:	lsts->delayedLengthZ2 + 1
							)
						:	positionZ2
				;

				lsts->timeToAwakeZ2 = \lambda \natural i; 
					( i <= lsts->delayedLengthZ2 ) 
						?	(	( i < positionZ2 ) 
									? lsts->timeToAwakeZ2[ i ] 
									:	(	( i == positionZ2 )
											? tTAZ2
											: lsts->timeToAwakeZ2[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLengthZ2 = lsts->delayedLengthZ2 + 1;
/////////UpdateDelayedZ2
			}
	  )
	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( assume running == sstm.currentTask )
	_( wrap &sstm )

}

void taskDelay2B( _( ghost \natural delay ) )
{
	_( ghost taskID prevTask )
	taskID running;

///////////////////////Z1////////////////////////////
	_( ghost \natural position ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/
	_( ghost tTA = sstm.tickCount + delay )

	_( assume ( position <= lsts->delayedLength ) )

	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	 */
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	_( ghost \natural positionOD ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
	_( ghost \natural tTAOD )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the oDelayed queue.
						*/
	_( ghost tTAOD = sstm.tickCount + delay - ( maxNumVal + 1 ) )

	_( assume ( positionOD <= lsts->oDelayedLength ) )

	_( assume \forall \natural j;
			( j < positionOD ) ==> ( lsts->timeToAwakeOD[ j ] <= tTAOD )
	 )

	_( assume 
			( positionOD < lsts->oDelayedLength - 1 ) ==> 
				( lsts->timeToAwakeOD[ positionOD + 1 ] > tTAOD )
	 )

	_( assume \forall \natural j;
			( j >= positionOD ) ==> ( lsts->timeToAwakeOD[ j ] > tTAOD )
	 )
	/*	The above assume statements 
		specify that 'i' is the index 
		in list 'oDelayed' at which the
		running task need to be added
	*/
///////////////////////Z2////////////////////////////
	_( assume ( position == lsts->delayedLengthZ2 + positionOD ) )

	_( unwrap &sstm )
	_( unwrap lsts )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( ghost
			{
				sstm.currentTask = lsts->ready[ sstm.topReadyPriority ].list[ 1 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					( i < lsts->ready[ sstm.topReadyPriority ].length - 1 )
						? lsts->ready[ sstm.topReadyPriority ].list[ i + 1 ]
						: UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( lsts->ready[ sstm.topReadyPriority ].index[ t ] < 
								  lsts->ready[ sstm.topReadyPriority ].length 
					)	?	(	( t == prevTask )
									? lsts->ready[ sstm.topReadyPriority ].length - 1
									: lsts->ready[ sstm.topReadyPriority ].index[ t ] - 1
							)
						:	lsts->ready[ sstm.topReadyPriority ].length - 1
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 
					lsts->ready[ sstm.topReadyPriority ].length - 1
				;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;

/////////UpdateDelayed

/////////UpdateODelayed
				lsts->oDelayed = \lambda \natural i;
					( i <= lsts->oDelayedLength )
						?	(	( i < positionOD ) 
									? lsts->oDelayed[ i ] 
									:	(	( i == positionOD ) 
												? prevTask
						  						: lsts->oDelayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexODelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexODelayed[ t ] < lsts->oDelayedLength	)	
									?	(	( lsts->indexODelayed[ t ] < positionOD )
												? lsts->indexODelayed[ t ]
												: lsts->indexODelayed[ t ] + 1
										)
									:	lsts->oDelayedLength + 1
							)
						:	positionOD
				;

				lsts->timeToAwakeOD = \lambda \natural i; 
					( i <= lsts->oDelayedLength ) 
						?	(	( i < positionOD ) 
									? lsts->timeToAwakeOD[ i ] 
									:	(	( i == positionOD )
											? tTAOD
											: lsts->timeToAwakeOD[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->oDelayedLength = lsts->oDelayedLength + 1;
/////////UpdateODelayed
			}
	  )
	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( assume running == sstm.currentTask )
	_( wrap &sstm )
}

void taskDelay3A( _( ghost \natural delay ) )
{
	taskID running;
	_(ghost taskID prevTask )
	_( ghost unsigned runnerUpPrty ) 
				//	The index of the second highest nonempty
				//	sequence in ready. As the ready 
				//  sequence at index 'sstm.topReadyPriority'
				//  is empty, the next task to schedule 
				//  need to be from index 'runnerUpPrty', 
				//  which is assured bu the assume statements
				//  on 'runnerUpPrty' below


///////////////////////Z1////////////////////////////
	_( ghost \natural position ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed

	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/

	_( ghost tTA = sstm.tickCount + delay )

	_( assume ( position <= lsts->delayedLength ) )

	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )

	 /*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	 */
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
	_( ghost \natural positionZ2 ) 
				//	The index in 'delayedZ2' list at which the
				//	the currently running need to be placed

	_( ghost \natural tTAZ2 )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayedZ2 queue.
						*/
	_( ghost tTAZ2 = sstm.tickCount + delay )

	_( assume ( positionZ2 <= lsts->delayedLengthZ2 ) )

	_( assume \forall \natural j;
			( j < positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] <= tTAZ2 )
	 )

	_( assume 
			( positionZ2 < lsts->delayedLengthZ2 - 1 ) ==> 
				( lsts->timeToAwakeZ2[ positionZ2 + 1 ] > tTAZ2 )
	 )

	_( assume \forall \natural j;
			( j >= positionZ2 ) ==> ( lsts->timeToAwakeZ2[ j ] > tTAZ2 )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in list 'delayedZ2' at which the
		running task need to be added
	 */
///////////////////////Z2////////////////////////////
	_( assume position == positionZ2 )


	_( assume (	( runnerUpPrty > 0 ) &&
				( runnerUpPrty < sstm.topReadyPriority )
			  )	
	 )
	_( assume ( lsts->ready[ runnerUpPrty ].length > 0 ) )	
	_( assume ( &( lsts->ready[ runnerUpPrty ] ) \in ( &sstm )->\owns ) )	
	_( assume \forall unsigned j;
			(	( j >= 1 ) &&
				( j <= maxPrio ) &&
				( j != sstm.topReadyPriority ) &&
 				( lsts->ready[ j ].length > 0 ) 
			) ==> ( j <= runnerUpPrty )
	 )
	 /*	The above four assume statements 
		specify that 'runnerUpPrty' is the index 
		of the sencond highest nonempty
		ready sequence.
	 */
	_( unwrap &sstm )
	_( unwrap lsts )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )

	 _( ghost
			{
				sstm.currentTask = lsts->ready[ runnerUpPrty ].list[ 0 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( \natural )0
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 0;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;

/////////UpdateDelayed

/////////UpdateDelayedZ2
				lsts->delayedZ2 = \lambda \natural i;
					( i <= lsts->delayedLengthZ2 )
						?	(	( i < positionZ2 ) 
									? lsts->delayedZ2[ i ] 
									:	(	( i == positionZ2 ) 
												? prevTask
						  						: lsts->delayedZ2[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayedZ2 = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayedZ2[ t ] < lsts->delayedLengthZ2	)	
									?	(	( lsts->indexDelayedZ2[ t ] < positionZ2 )
												? lsts->indexDelayedZ2[ t ]
												: lsts->indexDelayedZ2[ t ] + 1
										)
									:	lsts->delayedLengthZ2 + 1
							)
						:	positionZ2
				;

				lsts->timeToAwakeZ2 = \lambda \natural i; 
					( i <= lsts->delayedLengthZ2 ) 
						?	(	( i < positionZ2 ) 
									? lsts->timeToAwakeZ2[ i ] 
									:	(	( i == positionZ2 )
											? tTAZ2
											: lsts->timeToAwakeZ2[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLengthZ2 = lsts->delayedLengthZ2 + 1;
/////////UpdateDelayedZ2
			}
	  )

	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( ghost sstm.topReadyPriority = runnerUpPrty )
	_( wrap &sstm )
	_( assume ( running == sstm.currentTask ) )
}

void taskDelay3B( _( ghost \natural delay ) )
{
	taskID running;
	_(ghost taskID prevTask )
	_( ghost unsigned runnerUpPrty ) 
				//	The index of the second highest nonempty
				//	sequence in ready. As the ready 
				//  sequence at index 'sstm.topReadyPriority'
				//  is empty, the next task to schedule 
				//  need to be from index 'runnerUpPrty', 
				//  which is assured bu the assume statements
				//  on 'runnerUpPrty' below


///////////////////////Z1////////////////////////////
	_( ghost \natural position ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed

	_( ghost \natural tTA )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the delayed queue.
						*/

	_( ghost tTA = sstm.tickCount + delay )

	_( assume ( position <= lsts->delayedLength ) )

	_( assume \forall \natural j;
			( j < position ) ==> ( lsts->timeToAwake[ j ] <= tTA )
	 )

	_( assume 
			( position < lsts->delayedLength - 1 ) ==> 
				( lsts->timeToAwake[ position + 1 ] > tTA )
	 )

	_( assume \forall \natural j;
			( j >= position ) ==> ( lsts->timeToAwake[ j ] > tTA )
	 )

	/*	The above assume statements 
		specify that 'i' is the index 
		in delayed list at which the
		running task need to be added
	*/
///////////////////////Z1////////////////////////////

///////////////////////Z2////////////////////////////
_( ghost \natural positionOD ) 
				//	The index in 'oDelayed' list at which the
				//	the currently running need to be placed
	_( ghost \natural tTAOD )
						/*	to compute the value for 
							time to awake for the 
							currently running task 
							in the oDelayed queue.
						*/
	_( ghost tTAOD = sstm.tickCount + delay - ( maxNumVal + 1 ) )

	_( assume ( positionOD <= lsts->oDelayedLength ) )

	_( assume \forall \natural j;
			( j < positionOD ) ==> ( lsts->timeToAwakeOD[ j ] <= tTAOD )
	 )

	_( assume 
			( positionOD < lsts->oDelayedLength - 1 ) ==> 
				( lsts->timeToAwakeOD[ positionOD + 1 ] > tTAOD )
	 )

	_( assume \forall \natural j;
			( j >= positionOD ) ==> ( lsts->timeToAwakeOD[ j ] > tTAOD )
	 )
	 /*	The above assume statements 
		specify that 'i' is the index 
		in list 'oDelayed' at which the
		running task need to be added
	 */
///////////////////////Z2////////////////////////////
	_( assume ( position == lsts->delayedLengthZ2 + positionOD ) )


	_( assume (	( runnerUpPrty > 0 ) &&
				( runnerUpPrty < sstm.topReadyPriority )
			  )	
	 )
	_( assume ( lsts->ready[ runnerUpPrty ].length > 0 ) )	
	_( assume ( &( lsts->ready[ runnerUpPrty ] ) \in ( &sstm )->\owns ) )	
	_( assume \forall unsigned j;
			(	( j >= 1 ) &&
				( j <= maxPrio ) &&
				( j != sstm.topReadyPriority ) &&
 				( lsts->ready[ j ].length > 0 ) 
			) ==> ( j <= runnerUpPrty )
	 )
	 /*	The above four assume statements 
		specify that 'runnerUpPrty' is the index 
		of the sencond highest nonempty
		ready sequence.
	 */
	_( unwrap &sstm )
	_( unwrap lsts )
	_( unwrap &( lsts->ready[ sstm.topReadyPriority ] ) )

	 _( ghost
			{
				sstm.currentTask = lsts->ready[ runnerUpPrty ].list[ 0 ];

				prevTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];

/////////UpdateReady[ topReadyPriority ]
				lsts->ready[ sstm.topReadyPriority ].list = \lambda \natural i; 
					UINT_MAX
				;

				lsts->ready[ sstm.topReadyPriority ].index = \lambda taskID t; 
					( \natural )0
				;

				lsts->isInReady = \lambda taskID t; 
					( t == prevTask ) 
						? \false
						: lsts->isInReady[ t ] 
				;	

				lsts->ready[ sstm.topReadyPriority ].length = 0;
/////////UpdateReady[ topReadyPriority ]

/////////UpdateDelayed
				lsts->delayed = \lambda \natural i;
					( i <= lsts->delayedLength )
						?	(	( i < position ) 
									? lsts->delayed[ i ] 
									:	(	( i == position ) 
												? prevTask
						  						: lsts->delayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexDelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexDelayed[ t ] < lsts->delayedLength	)	
									?	(	( lsts->indexDelayed[ t ] < position )
												? lsts->indexDelayed[ t ]
												: lsts->indexDelayed[ t ] + 1
										)
									:	lsts->delayedLength + 1
							)
						:	position
				;

				lsts->timeToAwake = \lambda \natural i; 
					( i <= lsts->delayedLength ) 
						?	(	( i < position ) 
									? lsts->timeToAwake[ i ] 
									:	(	( i == position )
											? tTA
											: lsts->timeToAwake[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->delayedLength = lsts->delayedLength + 1;

/////////UpdateDelayed

/////////UpdateODelayed
				lsts->oDelayed = \lambda \natural i;
					( i <= lsts->oDelayedLength )
						?	(	( i < positionOD ) 
									? lsts->oDelayed[ i ] 
									:	(	( i == positionOD ) 
												? prevTask
						  						: lsts->oDelayed[ i-1 ] 	
										)
							)
						:	UINT_MAX
				;

				lsts->indexODelayed = \lambda taskID t; 
					( t != prevTask ) 
						?	(	( lsts->indexODelayed[ t ] < lsts->oDelayedLength	)	
									?	(	( lsts->indexODelayed[ t ] < positionOD )
												? lsts->indexODelayed[ t ]
												: lsts->indexODelayed[ t ] + 1
										)
									:	lsts->oDelayedLength + 1
							)
						:	positionOD
				;

				lsts->timeToAwakeOD = \lambda \natural i; 
					( i <= lsts->oDelayedLength ) 
						?	(	( i < positionOD ) 
									? lsts->timeToAwakeOD[ i ] 
									:	(	( i == positionOD )
											? tTAOD
											: lsts->timeToAwakeOD[ i - 1 ] 
										)
							)
						: 0
				;

				lsts->oDelayedLength = lsts->oDelayedLength + 1;
/////////UpdateODelayed
			}
	  )

	_( wrap &( lsts->ready[ sstm.topReadyPriority ] ) )
	_( wrap lsts )
	_( ghost sstm.topReadyPriority = runnerUpPrty )
	_( wrap &sstm )
	_( assume ( running == sstm.currentTask ) )
}