#include <vcc.h>
#include "Z1.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;
}


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

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

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

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

	runningAndPWTZ1 resultZ1;
	_( ghost taskID prevTask )
	_( ghost \natural position ) 
				/*	The index in 'delayed' list at which the
					the currently running task 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 = 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
	*/

	_( 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
			}
	  )

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

	_( wrap lsts )

	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
	_( wrap &sstm )
	return resultZ1;
}


runningAndPWTZ1 taskDelayUntil5(	_( ghost \natural pWT )
									_( ghost \natural delay )
							   )
{
	runningAndPWTZ1 resultZ1;
	_(ghost taskID prevTask )
	_( 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 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 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
	 */
	_( 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
			}
	  )

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

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

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

	_( 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
			}
	  )

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

	_( wrap lsts )

	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA - ( maxNumVal + 1 ) )
	_( wrap &sstm )
	return resultZ1;
}


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

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


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

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

	_( 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
			}
	  )

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

	_( wrap lsts )

	_( ghost resultZ1.running = sstm.currentTask )
	_( ghost resultZ1.pWT = tTA )
	_( wrap &sstm )
	return resultZ1;
}

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

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


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


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

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


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

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