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

taskID startScheduler()
{
	taskID running;
	//_(assert \false )
	_( unwrap &(sstm) )
	_( ghost 
		{
			sstm.currentTask = lsts->ready[ sstm.topReadyPriority ].list[ 0 ];
			sstm.tickCount = 0;
			sstm.schedulerRunning = \true;
		}	
	 )
	_( wrap &(sstm) )
	_( assume ( running == sstm.currentTask ) )
	return running;
}

runningAndPWTZ2 taskDelayUntil1	(	_( ghost \natural pWT )
									_( ghost \natural delay )
								)
{
	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 )
	return resultZ2;
}

runningAndPWTZ2 taskDelayUntil2(	_( ghost \natural pWT )
									_( ghost \natural delay )
							   )
{
	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 )
	return resultZ2;
}

runningAndPWTZ2 taskDelayUntil3	(	_( ghost \natural pWT )
									_( ghost \natural delay )
								)
{
	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 )
	return resultZ2;
}

runningAndPWTZ2 taskDelayUntil4(	_( ghost \natural pWT )
									_( ghost \natural delay )
							 )
{

	runningAndPWTZ2 resultZ2;
	_( ghost taskID prevTask )
	_( 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
	*/

	_( 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 ]

/////////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 resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
	_( wrap &sstm )
	return resultZ2;
}


runningAndPWTZ2 taskDelayUntil5(	_( ghost \natural pWT )
									_( ghost \natural delay )
							   )
{
	runningAndPWTZ2 resultZ2;
	_(ghost taskID prevTask )
	_( 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 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
	_( 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 delayed list at which the
		running task need to be added
	 */
	_( 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 assume statements 
		specify that 'i' is the index 
		in list 'delayedZ2' at which the
		running task need to be added
	 */
	_( 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 ]

/////////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 )
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
	_( wrap &sstm )
	return resultZ2;
}

runningAndPWTZ2 taskDelayUntil6(  _( ghost \natural pWT )
								_( ghost \natural delay )
							 )
{

	runningAndPWTZ2 resultZ2;
	_( ghost taskID prevTask )
	_( 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
	*/

	_( 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 ]

/////////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 resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAOD )
	_( wrap &sstm )
	return resultZ2;
}


runningAndPWTZ2 taskDelayUntil7(  _( ghost \natural pWT )
								_( ghost \natural delay )
							 )
{
	runningAndPWTZ2 resultZ2;
	_(ghost taskID prevTask )
	_( 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 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
	_( 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
	 */

	_( 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 ]

/////////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 )
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAOD  )
	_( wrap &sstm )
	return resultZ2;
}

runningAndPWTZ2 taskDelayUntil8	(  _( ghost \natural pWT )
									_( ghost \natural delay )
								)
{

	runningAndPWTZ2 resultZ2;
	_( ghost taskID prevTask )
	_( 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
	*/

	_( 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 ]

/////////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 resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
	_( wrap &sstm )
	return resultZ2;
}

runningAndPWTZ2 taskDelayUntil9(  _( ghost \natural pWT )
								_( ghost \natural delay )
							 )
{
	runningAndPWTZ2 resultZ2;
	_(ghost taskID prevTask )
	_( 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 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
	_( 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
	 */

	_( 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 ]

/////////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 )
	_( ghost resultZ2.running = sstm.currentTask )
	_( ghost resultZ2.pWT = tTAZ2 )
	_( wrap &sstm )
	return resultZ2;
}

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

taskID taskDelay2A( _( ghost \natural delay ) )
{
	taskID running;
	_( ghost taskID prevTask )
	_( 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
	 */
	_( 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 ]

/////////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 )
	return running;
}

taskID taskDelay2B( _( ghost \natural delay ) )
{
	taskID running;
	_( ghost taskID prevTask )
	_( 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
	*/

	_( 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 ]

/////////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 )
	return running;
}


taskID taskDelay3A( _( ghost \natural delay ) )
{
	taskID running;
	_(ghost taskID prevTask )
	_( ghost \natural positionZ2 ) 
				//	The index in 'delayedZ2' list at which the
				//	the currently running need to be placed
//	unsigned runnerUpPrty;
	_( 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
	_( 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
	 */

	_( 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 ]

/////////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 ) )
	return running;
}



taskID taskDelay3B( _( ghost \natural delay ) )
{
	taskID running;
	_(ghost taskID prevTask )
	_( ghost \natural positionOD ) 
				//	The index in 'delayed' list at which the
				//	the currently running need to be placed
//	unsigned runnerUpPrty;
	_( 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
	_( 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 delayed list at which the
		running task need to be added
	 */

	_( 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 ]

/////////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 ) )
	return running;
}