 val cooperate : ((int * int kolejka.kol) kolejka.kol) -> wyniki.tablica -> bool

 val isNotEmpty : ((int * int kolejka.kol) kolejka.kol) -> bool
 
 val isValid : ((int * int kolejka.kol) kolejka.kol) -> bool

  axiom Forall (r, k, w, wlk, who, modulo) => 
  let 
  	val pmodulo = rdzen.numItems r

  	val (k, (gr, pk)) = kolejka.delete k
  	val (pk, pwho) = kolejka.delete pk
  in
	((cooperate k w) andalso (isValid k) andalso (isNotEmpty k)
	andalso (who == pwho) andalso (modulo = pmodulo)) 
	implies 
	(do_ins (r, k, w, wlk, who, modulo) proper)
  end

  axiom Forall (r, k, w, wlk, who, modulo) => 
  let 
  	val pmodulo = rdzen.numItems r

  	val (k, (gr, pk)) = kolejka.delete k
  	val (pk, pwho) = kolejka.delete pk
  in
	((cooperate k w) andalso (isValid k) andalso (isNotEmpty k)
	andalso (who == pwho) andalso (modulo = pmodulo)) 
	implies 
  	let
	  	val (nr , nk , nw) = do_ins (r, k, w, wlk, who, modulo)

	  	(* obrobka rdzenia *)
	  	val (p , a1 , w1 , a2 , w2 ) = rdzen.suball ( r , who ) 
	  	val (sw1, r) = rdzen.do_address (r, a1, w1, who, modulo)
	  	val (sw2, r) = rdzen.do_address (r, a2, w2, who, modulo)
	  	val r = (if a1 = rdzen.Ins then 
	  		let
	  			val (stp, sta1, stw1, sta2, stw2) = rdzen.suball (r, sw2)
	  		in
	  			rdzen.updateall (r,sw2,stp, sta1, stw1, sta2, w1)
	  		end
	  		else 
			rdzen.updateall (r,sw2, (rdzen.subOpcode (r,sw1)), 
	  		(rdzen.subAddr1 (r,sw1)), (rdzen.subVal1 (r,sw1)), 
	  		(rdzen.subAddr2 (r,sw1)), (rdzen.subVal2 (r,sw1))))

	  	(* obrobka kolejki *)
	  	val (K, (gr, pk)) = kolejka.topc k
	  	val (PK, wh) = kolejka.topc pk
		val k = kolejka.Ruch (k, fn n => n + 1) 

  	in
  		(r == nr)
		andalso
		(k == nk)
		andalso
		(w == nw)
	end
  end

(* czesc dla aksjomatow *)
(*=================================================*)
fun cooperate kol tab= 
let
	val wk = wyniki.size tab

	fun miniSize (k, j) = 
	let
		fun do_iteracja (f, i) = 
		let
			val (nk, (gr, pk)) = kolejka.delete f
		in
			if (gr = i) then (kolejka.sizeK pk) else (do_iteracja (nk, i))
		end
		handle kolejka.Pusta_lista_del => 0
	in
		do_iteracja (k, j)
	end

	fun do_iteracja tab kol i wlk = 
			
		if (i < wlk) then
			if (wyniki.sub (tab, i) = miniSize (kol, i)) then 
			do_iteracja tab kol (i + 1) wlk
			else false
		else true
in
	if (wyniki.stillLive tab = kolejka.sizeK kol) then 
	do_iteracja tab kol 0 wk 
	else false
end

(* wlasciwosci kolejki *)
fun isValid kol = 
let
	fun do_sprawdz kol i czy =
	let
		val (k, (gr, pk)) = kolejka.delete kol
	in
		if czy then
			if gr < i then
				do_sprawdz kol gr false
			else
				if gr = i then
					false
				else
					do_sprawdz kol gr czy
		else
			if gr <= i then
				false
			else
				do_sprawdz kol gr czy
	end
	handle kolejka.Pusta_lista_del => true
in
	do_sprawdz kol (~1) true
end

fun isNotEmpty k = 
let
	val (_) = kolejka.delete (k)
in
	true
end
handle kolejka.Pusta_lista_del => false

(*=================================================*)
