tom_correct2[(IMPORTING tom_conft,fpu_impl_ui_types)
	       initial_vamp:initial_conft,
	       fpu_spec_op : fpu_spec_op_t,
	       (IMPORTING fpu_impl_ui_ok_types[fpu_spec_op])
	       add_spec:add_spec_t,
	       md_spec :md_spec_t,
	       fpm_spec:fpm_spec_t,
	     TOMadd : add_circuit_t,
	     TOMmd  : md_circuit_t,
	     TOMfpm : fpm_circuit_t,
	     mif_next:mif_next_t,
	    (IMPORTING tom_impl_spec[TOMadd,TOMmd,TOMfpm,mif_next,fpu_spec_op])
	    input:tom_impl_input_funct,
	    initial_vamp_mem:mem_state]: THEORY
BEGIN

  IMPORTING tom_correct2a[initial_vamp,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,initial_vamp_mem];

%% step 2, sub-step a: continued...
% and finally the (admittedly still rather lengthy) my definition
  my(T:nat): RECURSIVE
	[# cI: cIt, ROBhead, ROBtail: tagt, 
	   ROBcount: bvec[tag_width+1], S1: S1conft,
	   PCp, DPC : registert,
	   sI_issue, sI_writeback, sI_S1: nat, 
	   sI_RS :[rsnot->upfrom(-1)],
	   fu_sI :[funot->nat],
	   CDB_arbiter : arbiter_conft[no_fu],
	   alurs_arbiter : arbiter_conft[4],
	   fu_conf : fu_conft #]=
    IF T=0 THEN
	(# cI           := cIinitial,
	   sI_issue     := 0,
	   sI_RS        := LAMBDA(rs:rsnot):-1,
	   sI_writeback := 0,
	   sI_S1	:= 0,
	   fu_sI	:= LAMBDA(fu:funot):0,
           S1		:= initial_vamp`S1,
	   DPC		:= initial_vamp`S2`DPC,
	   PCp		:= initial_vamp`S2`PCp,
	   ROBtail      := initial_vamp`S4`ROBtail,
	   ROBhead      := initial_vamp`S4`ROBhead,
	   ROBcount     := initial_vamp`S4`ROBcount,
	   CDB_arbiter  := initial_vamp`S3`CDB_arbiter,
	   alurs_arbiter:= initial_vamp`S2`alurs_arbiter,
	   fu_conf	:= (#   mem  := initial_vamp`S3`mem,
				fpu1 := initial_vamp`S3`fpu1,
				fpu2 := initial_vamp`S3`fpu2,
				fpu3 := initial_vamp`S3`fpu3,
				alu  := initial_vamp`S3`alu #)
    	#)
    ELSE
      LET Tminus1:below(T)  = T-1,
	  my_old      	    = my(Tminus1),
	  conf		    = tom_impl_conf(initial_vamp,input,Tminus1),
	  issue       	    = cIissue(my_old`cI,my_old`ROBhead,my_old`ROBtail,
			  	my_old`ROBcount, my_old`S1,my_old`CDB_arbiter),
	  issue_with_result = cIissue_with_result(my_old`S1),
          completion  	    = cIcompletion(my_old`cI),
	  compl_p     	    = cIcompl_p(my_old`cI,my_old`CDB_arbiter),
          writeback   	    = cIwriteback(my_old`cI,my_old`ROBhead,my_old`ROBtail,
				my_old`ROBcount),
	  dispatch_rs 	    = LAMBDA(rs:rsnot):
			       	cIdispatch_rs(my_old`cI,my_old`ROBhead,my_old`ROBtail,
				my_old`ROBcount, my_old`alurs_arbiter,
				my_old`CDB_arbiter,my_old`fu_conf,rs),
	  dispatch_fu 	    = LAMBDA (fu:funot):
			    	cIdispatch_fu(my_old`cI,my_old`ROBhead,my_old`ROBtail,
				my_old`ROBcount, my_old`alurs_arbiter,
				my_old`CDB_arbiter,my_old`fu_conf,fu),
	  issue_rs    	    = LAMBDA(rs:rsnot):
			    	cIissue_rs(my_old`cI,my_old`ROBhead,my_old`ROBtail,
				my_old`ROBcount, my_old`S1,rs),
	  CDB               = CDB(my_old`cI,my_old`CDB_arbiter),
	  issue_op          = LAMBDA (r:regnot):
				issue_op(my_old`cI,my_old`CDB_arbiter,r),

	  JISR		    = JISR(my_old`cI,my_old`ROBhead,my_old`ROBtail,
				my_old`ROBcount),
	  mem_step:tommem_stept	= tommem_step_ui(my_old`fu_conf`mem,
					mem_input(my_old`cI, my_old`ROBhead, my_old`ROBtail, my_old`ROBcount, 
	    				my_old`alurs_arbiter, my_old`CDB_arbiter,
					my_old`fu_conf, my_old`sI_RS,
	    				input(Tminus1),my_old`S1,my_old`PCp,my_old`DPC)),
	  imem_busy	    = mem_step`imem_busy,
	  S1     	    = cIS1(my_old`cI,my_old`ROBhead,my_old`ROBtail,
				my_old`ROBcount, my_old`S1,my_old`CDB_arbiter,imem_busy),
	  fu_sI:[funot->nat]= LAMBDA (fu:funot):
     			        LET fuin=LAMBDA(Tp:below(T)):fu_inputs(my(Tp)`cI,my(Tp)`ROBhead,my(Tp)`ROBtail,my(Tp)`ROBcount,
					my(Tp)`alurs_arbiter,my(Tp)`CDB_arbiter,my(Tp)`fu_conf,my(Tp)`sI_RS),
			            fuout=fu_out(my_old`cI,my_old`ROBhead,my_old`ROBtail,my_old`ROBcount,
					my_old`alurs_arbiter,my_old`CDB_arbiter,my_old`fu_conf,my_old`sI_RS,
					input(Tminus1),my_old`S1,my_old`PCp,my_old`DPC),
			            set=LAMBDA(Tp:below(T)):
				      fuin(Tp)(fu)`tag=fuout(fu)`tag AND fuin(Tp)(fu)`valid IN
			         IF nonempty?(set) THEN
				   LET my_bla=my(max[T](set)),
				       sI_RS =my_bla`sI_RS(cIdispatch_fu(my_bla`cI,my_bla`ROBhead,my_bla`ROBtail,
				     			   my_bla`ROBcount, my_bla`alurs_arbiter,
				     			   my_bla`CDB_arbiter,my_bla`fu_conf,fu)) IN
				    IF sI_RS>=0 THEN sI_RS ELSE 0 ENDIF				     
			         ELSE
				   0
			         ENDIF,	
	  writeback_p:cIt   = writeback_f(my_old`cI,my_old`ROBhead,writeback,my_old`sI_writeback),
	  snoop_p:cIt       = snoop_f(writeback_p,my_old`cI,CDB,my_old`sI_RS),
	  completion_p:cIt  = completion_f(snoop_p,my_old`cI,CDB,completion,compl_p,
				LAMBDA (fu:funot):fuspec(my_old`cI, my_old`ROBhead, my_old`ROBtail, my_old`ROBcount, 
	    					my_old`alurs_arbiter, my_old`CDB_arbiter,
					    	my_old`fu_conf, my_old`sI_RS,
	    					input(Tminus1),my_old`S1,my_old`PCp,my_old`DPC,fu,fu_sI(fu))),
	  dispatch_p:cIt= completion_p WITH [ RS := LAMBDA (rs:rsnot):
			IF dispatch_rs(rs) THEN
			  completion_p`RS(rs) WITH [valid := FALSE]
			ELSE
			  completion_p`RS(rs)
			ENDIF ] IN
      (# sI_issue    := IF issue THEN
			  my_old`sI_issue+1
			ELSE
			  my_old`sI_issue
			ENDIF,
	 sI_RS       := LAMBDA(rs:rsnot):
			     IF issue_rs(rs) THEN
				my_old`sI_issue
			     ELSE
				my_old`sI_RS(rs)
			     ENDIF,
	 sI_writeback := IF writeback THEN
			   my_old`sI_writeback+1
			 ELSE
			   my_old`sI_writeback
			 ENDIF,
  	 sI_S1	      := IF S1 THEN
      			   my(Tminus1)`sI_S1+1
    			 ELSE
      			   my(Tminus1)`sI_S1
    			 ENDIF,
	 fu_sI	      := fu_sI,
	 ROBtail      := IF issue THEN
			   my_old`ROBtail+1
			 ELSE
			   my_old`ROBtail
			 ENDIF,
	 ROBhead      := IF writeback THEN
			   my_old`ROBhead+1
			 ELSE
			   my_old`ROBhead
			 ENDIF,
	 ROBcount     := IF issue AND NOT writeback THEN
			    my_old`ROBcount+1
			 ELSIF NOT issue AND writeback THEN
			    my_old`ROBcount-1
			 ELSE
			    my_old`ROBcount
			 ENDIF,
	 S1	      := IF S1 THEN
     			 (# full   := TRUE,
			    CAipf  := ipf(dlx_conf_without_interrupt_IEEEf(init_conf,my_old`sI_S1)),
			    CAimal := imal(dlx_conf_without_interrupt_IEEEf(init_conf,my_old`sI_S1)),
			    IR	   := Iw(dlx_conf_without_interrupt_IEEEf(init_conf,my_old`sI_S1)) #)
   			 ELSIF issue THEN
     			   my_old`S1 WITH [full := FALSE]
   			 ELSE
     			   my_old`S1
   			 ENDIF,
	 PCp	      := IF issue THEN
			   LET op1=issue_op(cSspec`S(my_old`sI_issue,0))`data IN
			   dlxispec_nextpc(my_old`S1`IR, op1, my_old`PCp, my_old`cI`R(64+nspr_EPC)`data)
			 ELSE
			   my_old`PCp
			 ENDIF,
	 DPC	      := IF issue THEN
			   next_DPC(my_old`cI,my_old`S1,my_old`PCp)
			 ELSE
			   my_old`DPC
			 ENDIF,
   	 CDB_arbiter  := arbiter_step_spec[no_fu](my_old`CDB_arbiter,TRUE,FALSE),
	 alurs_arbiter:= arbiter_step_spec[4](my_old`alurs_arbiter,
					      NOT fu_stall_out(my_old`cI,my_old`CDB_arbiter,my_old`fu_conf)(fu_alu),FALSE),
	 fu_conf      := (# mem  := mem_step`reg,
			    fpu1 := tomfpu1_step_ui(my_old`fu_conf`fpu1,FALSE,
					fu_stall_in(my_old`cI,my_old`CDB_arbiter)(fu_fpu1),
					fu_inputs(my_old`cI,my_old`ROBhead,my_old`ROBtail,my_old`ROBcount,
					my_old`alurs_arbiter,my_old`CDB_arbiter,my_old`fu_conf,my_old`sI_RS)(fu_fpu1))`reg,
			    fpu2 := tomfpu2_step_ui(my_old`fu_conf`fpu2,FALSE,
					fu_stall_in(my_old`cI,my_old`CDB_arbiter)(fu_fpu2),
					fu_inputs(my_old`cI,my_old`ROBhead,my_old`ROBtail,my_old`ROBcount,
					my_old`alurs_arbiter,my_old`CDB_arbiter,my_old`fu_conf,my_old`sI_RS)(fu_fpu2))`reg,
			    fpu3 := tomfpu3_step_ui(my_old`fu_conf`fpu3,FALSE,
					fu_stall_in(my_old`cI,my_old`CDB_arbiter)(fu_fpu3),
					fu_inputs(my_old`cI,my_old`ROBhead,my_old`ROBtail,my_old`ROBcount,
					my_old`alurs_arbiter,my_old`CDB_arbiter,my_old`fu_conf,my_old`sI_RS)(fu_fpu3))`reg,
			    alu  :=tomalu_step_spec(my_old`fu_conf`alu, FALSE,
					fu_stall_in(my_old`cI,my_old`CDB_arbiter)(fu_alu),
					fu_inputs(my_old`cI,my_old`ROBhead,my_old`ROBtail,my_old`ROBcount,
					my_old`alurs_arbiter,my_old`CDB_arbiter,my_old`fu_conf,my_old`sI_RS)(fu_alu))`reg #),
	 cI           := IF issue THEN
			   LET i=my_old`sI_issue IN dispatch_p WITH 
			   [ R   := LAMBDA (r:regnot):
				    IF instr_has_dest(i,r) THEN
					dispatch_p`R(r) WITH 
					[ valid := FALSE,
					  tag   := my_old`ROBtail ]
				    ELSE
					dispatch_p`R(r)
				    ENDIF,
			     RS  := LAMBDA (rs:rsnot):
				    IF issue_rs(rs) THEN
				    (# valid := TRUE,
				       tag   := my_old`ROBtail,
				       op    := LAMBDA (x:st):issue_op(S(i,x)) #)
				    ELSE
				       dispatch_p`RS(rs)
				    ENDIF,
			     ROB := dispatch_p`ROB WITH
				    [(my_old`ROBtail):=
				      	IF issue_with_result THEN
					(# valid  := TRUE,
					   result := cSspec`result(my_old`sI_issue) #)
					ELSE
					(# valid  := FALSE,
					   result := dispatch_p`ROB(my_old`ROBtail)`result #)
					ENDIF ]]
			ELSE
			  dispatch_p
			ENDIF #)
    ENDIF
    MEASURE T;

% now we can define the cycle-based inputs for Daniel
  cIwriteback_t(T:nat):bool=
   cIwriteback(my(T)`cI,my(T)`ROBhead,my(T)`ROBtail,my(T)`ROBcount);

  cIissue_t(T:nat):bool=
   cIissue(my(T)`cI,my(T)`ROBhead,my(T)`ROBtail,my(T)`ROBcount, my(T)`S1,
     my(T)`CDB_arbiter);

  cIissue_with_result_t(T:nat):bool=
   cIissue_with_result(my(T)`S1);

  cIcompletion_t(T:nat):bool=
   cIcompletion(my(T)`cI);

  cIissue_rs_t(T: nat, rs: rsnot):bool=
   cIissue_rs(my(T)`cI,my(T)`ROBhead,my(T)`ROBtail,my(T)`ROBcount, my(T)`S1, rs);

  cIdispatch_rs_t(T: nat, rs: rsnot):bool=
   cIdispatch_rs(my(T)`cI,my(T)`ROBhead,my(T)`ROBtail,my(T)`ROBcount, 
		my(T)`alurs_arbiter,my(T)`CDB_arbiter,my(T)`fu_conf,rs);

  cIdispatch_fu_t(T: nat, fu: funot):rsnot=
   cIdispatch_fu(my(T)`cI,my(T)`ROBhead,my(T)`ROBtail,my(T)`ROBcount, 
		my(T)`alurs_arbiter,my(T)`CDB_arbiter,my(T)`fu_conf,fu);

  cIcompl_p_t(T:nat):funot=
   cIcompl_p(my(T)`cI,my(T)`CDB_arbiter);

% timed version of S1 scheduling function
  cIS1_t(T:nat):bool=
    cIS1(my(T)`cI,my(T)`ROBhead,my(T)`ROBtail,my(T)`ROBcount, my(T)`S1,
	my(T)`CDB_arbiter,tommem_step_ui(my(T)`fu_conf`mem,
					mem_input(my(T)`cI, my(T)`ROBhead, my(T)`ROBtail, my(T)`ROBcount, 
	    				my(T)`alurs_arbiter, my(T)`CDB_arbiter,
					my(T)`fu_conf, my(T)`sI_RS,
	    				input(T),my(T)`S1,my(T)`PCp,my(T)`DPC))`imem_busy);

% issue_with_result takes a special position in Daniel's proof 
% since it is defined on the instruction i instead of the cycle t
% so we have do some additional proving...
  in_order_my_issue : LEMMA
    FORALL(T:nat):
      FORALL(Tp:upfrom(T)):
	my(Tp)`sI_issue>=my(T)`sI_issue;
  
  issue_with_result_helper : LEMMA
    FORALL (i:nat):
    empty?(LAMBDA (T:nat): my(T)`sI_issue=i AND cIissue_t(T)) OR
    singleton?(LAMBDA (T:nat): my(T)`sI_issue=i AND cIissue_t(T));

  cIissue_with_result_i(i:nat):bool =
    IF NOT empty?(LAMBDA (T:nat): my(T)`sI_issue=i AND cIissue_t(T)) THEN
    	cIissue_with_result_t(the(LAMBDA (T:nat): my(T)`sI_issue=i AND cIissue_t(T)))
    ELSE
	FALSE
    ENDIF;

  issue_with_result_rewrite : LEMMA
    FORALL(T:nat):
    cIissue_t(T) IMPLIES
    	cIissue_with_result_i(my(T)`sI_issue)=
    	cIissue_with_result_t(T);

% that was it... we can import Daniels cI definition
  cIspec: cIspect =
    (#
      initial:=cIinitial,
      issue:=cIissue_t, 
      writeback:=cIwriteback_t,
      completion:=cIcompletion_t,
      issue_with_result:=cIissue_with_result_i, % result available during issue?
      issue_rs:=cIissue_rs_t,                   % RS for issue
      dispatch_rs:=cIdispatch_rs_t,             % RS for dispatch
      dispatch_fu:=cIdispatch_fu_t,             % Dispatch from RS to FU
      compl_p:=cIcompl_p_t
    #);

  fuspec_t: [funot->fusIt]=
    LAMBDA (fu: funot):
      LAMBDA (T: nat):
        fuspec(my(T)`cI, my(T)`ROBhead, my(T)`ROBtail, my(T)`ROBcount, 
	    my(T)`alurs_arbiter, my(T)`CDB_arbiter,
	    my(T)`fu_conf, my(T)`sI_RS,
	    input(T),my(T)`S1,my(T)`PCp,my(T)`DPC,fu,my(T+1)`fu_sI(fu));

  IMPORTING tomasulo@tomieeefrewrites[
    no_reg,   % number of registers
    no_rs,    % number of reservation stations
    no_fu,    % number of function units
    cSspec,   % cSspec: cSspect
    cIspec,   % cIspec: cIspect
    fuspec_t, % fuspec: [funot->fut]
    idx_ieeef,
    f_ieeef];

% definitions that make the following lemma a non-recursive auto-rewrite
  DPC(T:nat):registert=my(T)`DPC;
  PCp(T:nat):registert=my(T)`PCp;
  S1(T:nat):S1conft=my(T)`S1;
  sI_S1(T:nat):nat=my(T)`sI_S1;
  alurs_arbiter(T:nat):arbiter_conft[4]=my(T)`alurs_arbiter;
  CDB_arbiter(T:nat):arbiter_conft[no_fu]=my(T)`CDB_arbiter;
  fu_conf(T:nat):fu_conft=my(T)`fu_conf;
  fu_sI(T:nat):[funot->nat]=my(T)`fu_sI;

% and finally, once again the 'obvious' lemma:
% "my" equals the cI-Tomasulo implementation
  cI_is_my_cI : LEMMA
    FORALL(T:nat):
    my(T)=(# 	cI		:= cIc_ieeef(T),
		ROBtail 	:= ROBtail(T),
		ROBhead 	:= ROBhead(T),
		ROBcount	:= ROBcount(T),
		sI_issue	:= sI_issue(T),
		sI_RS		:= LAMBDA (rs:rsnot): sI_RS(rs,T),
		sI_writeback	:= sI_writeback(T),
		sI_S1		:= sI_S1(T),
		S1		:= S1(T),
	        PCp		:= PCp(T),
		DPC		:= DPC(T),
		alurs_arbiter   := alurs_arbiter(T),
		CDB_arbiter	:= CDB_arbiter(T),
		fu_conf		:= fu_conf(T),
		fu_sI		:= fu_sI(T) #);


% a few helper lemmas that are later needed in order to show Daniel's assumptions
  initial_RS_not_full: LEMMA
    FORALL (rs:rsnot):
      NOT cIspec`initial`RS(rs)`valid;

  issue_rs_impl_issue: LEMMA
    FORALL (T:nat,rs:rsnot):
      cIspec`issue_rs(T, rs)=>cIspec`issue(T);

% correctness of stage 1
  sI_S1_helper : LEMMA
      FORALL (T:nat):
	my(T)`sI_S1 = IF my(T)`S1`full THEN my(T)`sI_issue+1 ELSE my(T)`sI_issue ENDIF;

  S1_strongly_correct : LEMMA
    FORALL (T:nat):
      LET j=sI_S1(T)-1 IN
      j>=0 IMPLIES 
	S1(T)`IR    =  Iw(dlx_conf_without_interrupt_IEEEf(init_conf,j)) AND
	S1(T)`CAipf = ipf(dlx_conf_without_interrupt_IEEEf(init_conf,j)) AND
	S1(T)`CAimal=imal(dlx_conf_without_interrupt_IEEEf(init_conf,j));

  S1_correct : LEMMA
    FORALL (T:nat):
      LET j=sI_issue(T) IN
      S1(T)`full IMPLIES 
	S1(T)`IR    =  Iw(dlx_conf_without_interrupt_IEEEf(init_conf,j)) AND
	S1(T)`CAipf = ipf(dlx_conf_without_interrupt_IEEEf(init_conf,j)) AND
	S1(T)`CAimal=imal(dlx_conf_without_interrupt_IEEEf(init_conf,j));

% additional implementation registers:
% RS: operation f and flag fprh,
% ROB: destination register and PCs
  aux_conf(T:nat):RECURSIVE
	[#  RS  : [rsnot -> [# f : registert, fprh : bvec[6] #]],
       	    ROB : [below(rob_entries) -> 
			[# dest : tomaddrt, 
			   nextPCp,nextDPC,oPCp,oDPC : registert #] ] #] =
    IF T=0 THEN
	(# RS  := LAMBDA (rs:rsnot): 
	      	(# f    := initial_vamp`S2`RS(rs)`f,
	      	   fprh := initial_vamp`S2`RS(rs)`fprh #),
	   ROB := LAMBDA (rob:below(rob_entries)):
		(# dest    := initial_vamp`S4`rob(rob)`dest,
		   nextPCp := initial_vamp`S4`rob(rob)`nextPCp,
		   nextDPC := initial_vamp`S4`rob(rob)`nextDPC,
		   oPCp    := initial_vamp`S4`rob(rob)`oPCp,
		   oDPC    := initial_vamp`S4`rob(rob)`oDPC #) #)
    ELSIF cIspec`issue(T-1) THEN
	LET i=sI_issue(T-1) IN
	(# RS := LAMBDA (rs:rsnot): 
		   IF cIspec`issue_rs(T-1,rs) THEN
	      	     (# f    := Iw(dlx_conf_without_interrupt_IEEEf(init_conf,i)),
	      	   	fprh := LAMBDA (x:below(6)):
				tomIA(tomID(Iw(dlx_conf_without_interrupt_IEEEf(init_conf,i))))`sop(x)`fprh #)
		   ELSE
		     aux_conf(T-1)`RS(rs)
		   ENDIF,
	   ROB := aux_conf(T-1)`ROB WITH 
		    [ (bv2nat(ROBtail(T-1))):= 
			(# dest    := tomIA(tomID(Iw(dlx_conf_without_interrupt_IEEEf(init_conf,i))))`dest,
		   	   nextPCp := nextPCpu(dlx_conf_without_interrupt_IEEEf(init_conf,i)),
		   	   nextDPC := nextDPCu(dlx_conf_without_interrupt_IEEEf(init_conf,i)),
		   	   oPCp    := dlx_conf_without_interrupt_IEEEf(init_conf,i)`PCp,
		   	   oDPC    := dlx_conf_without_interrupt_IEEEf(init_conf,i)`DPC #) ] #)	
    ELSE
	aux_conf(T-1)
    ENDIF
    MEASURE T;

% and the correctness of these constructions
  my_issue_ge_RS : LEMMA
    FORALL (T:nat,rs:rsnot):
      sI_issue(T)>=sI_RS(rs,T);

  aux_conf_correct_rs : LEMMA
    FORALL (T:nat, rs:rsnot):
      IF sI_RS(rs,T)>=0 THEN
	aux_conf(T)`RS(rs)`f   =Iw(dlx_conf_without_interrupt_IEEEf(init_conf,sI_RS(rs,T))) AND
	aux_conf(T)`RS(rs)`fprh=LAMBDA (x:below(6)):(cSspec`e(S(sI_RS(rs,T),x))=1)
      ELSE
	aux_conf(T)`RS(rs)`f   =initial_vamp`S2`RS(rs)`f AND
	aux_conf(T)`RS(rs)`fprh=initial_vamp`S2`RS(rs)`fprh
      ENDIF;

  aux_conf_correct_rob : LEMMA
    FORALL (T:nat, tag:tagt):
      LET j=sI_ROB(tag,T) IN
      j>=0 IMPLIES
	aux_conf(T)`ROB(bv2nat(tag))=
	(# dest    := tomIA(tomID(Iw(dlx_conf_without_interrupt_IEEEf(init_conf,j))))`dest,
   	   nextPCp := nextPCpu(dlx_conf_without_interrupt_IEEEf(init_conf,j)),
   	   nextDPC := nextDPCu(dlx_conf_without_interrupt_IEEEf(init_conf,j)),
   	   oDPC    := dlx_conf_without_interrupt_IEEEf(init_conf,j)`DPC,
   	   oPCp    := dlx_conf_without_interrupt_IEEEf(init_conf,j)`PCp #);

% finally, we show that the instructions are distributed correctly on the different RS
  RS_alu_correct : LEMMA
    FORALL (T:nat,rs:below(4)):
    cIc_ieeef(T)`RS(rs)`valid IMPLIES
      sI_RS(rs,T)>= 0 AND I_is_alu(aux_conf(T)`RS(rs)`f);
  
  RS_fpu1_correct : LEMMA
    FORALL (T:nat):
    cIc_ieeef(T)`RS(4)`valid IMPLIES
      sI_RS(4,T)>= 0 AND I_faddsub(aux_conf(T)`RS(4)`f);

  RS_fpu2_correct : LEMMA
    FORALL (T:nat):
    cIc_ieeef(T)`RS(5)`valid IMPLIES
      sI_RS(5,T)>= 0 AND I_fmuldiv(aux_conf(T)`RS(5)`f);

  RS_fpu3_correct : LEMMA
    FORALL (T:nat):
    cIc_ieeef(T)`RS(6)`valid IMPLIES
       sI_RS(6,T)>= 0 AND LET Iw=aux_conf(T)`RS(6)`f IN
         I_fnegabs(Iw) OR I_fsqrt(Iw) OR I_frem(Iw) OR I_fmov(Iw) OR
	 I_fcvt(Iw) OR I_mi2f(Iw) OR I_mf2i(Iw) OR I_fcond(Iw);

  RS_mem_correct : LEMMA
    FORALL (T:nat):
    cIc_ieeef(T)`RS(7)`valid IMPLIES
      sI_RS(7,T)>= 0 AND I_mem(aux_conf(T)`RS(7)`f);

END tom_correct2