tom_correct4_JISR[(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,
	       (IMPORTING fpu_impl_ui_ok[fpu_spec_op,add_spec,md_spec,fpm_spec])
	     TOMadd : add_circuit_ok_t,
	     TOMmd  : md_circuit_ok_t,
	     TOMfpm : fpm_circuit_ok_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_correct4[initial_vamp,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,input,initial_vamp_mem]


%% Now, we want to include interrupts. This entails:
%% * defining correctness with interrupts
%% * showing that correctness with interrupts holds until one
%%   cycle AFTER the first interrupt
%% In the next theory, we will then put this together to reach overall correctness


%% a scheduling function with interrupts
%% counting eihter instructions or interrupts
  sI_inst(T:nat):RECURSIVE upto(T)=
    IF T=0 THEN
      0
    ELSE
    LET conf = tom_impl_conf(initial_vamp,input,T-1),
	s4   = signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),FALSE) IN
      IF s4`writeback OR s4`JISR THEN
        sI_inst(T-1)+1
      ELSE
        sI_inst(T-1)
      ENDIF
    ENDIF
    MEASURE T;
      

%% basically boring helper definitions
  real_mem_input_t(T:nat):tommem_inputt =
    LET conf=tom_impl_conf(initial_vamp,input,T),
	s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(T)`reset),
        s3  =signals3_spec(conf`S3),
        s2  =signals2_spec(conf`S3, conf`S2, input(T)`reset, s3, s4`clear),
        s1  =signals1_spec(conf`S1, conf`S2, conf`S4, conf`S5,input(T)`reset,s3, s4),
        g_0DPC=IF s1`full_1 THEN s1`nextDPC ELSE conf`S2`DPC ENDIF IN
	(# clear    := s4`clear,
           stall_in := s3`FU_stall_in(fu_mem),
           inputs   := s2`fu_inputs(fu_mem),
           PC       := g_0DPC,
           ROBtail  := conf`S4`ROBhead,
           bp_in    := input(T)`bp_in,
           ext_in   := input(T)`ext_in,
           ext_reset:= input(T)`ext_reset #);

  mem_conf_with_interrupts(T:nat):mem_state=
    mif_memory_conf(initial_vamp`S3`mem,initial_vamp_mem,real_mem_input_t)(T);
       
  good_mif_next_with_interrupts?(T:nat):bool=
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(real_mem_input_t);

%% the correctness criterion with interrupts
  vamp_fulfills_spec?(T:nat):bool=
    LET conf = tom_impl_conf(initial_vamp,input,T),
	spec = dlx_conf_IEEEf(init_conf,sI_inst(T)),
   	mem  = mem_conf_with_interrupts(T) IN
    conf`S5`GPR =spec`GPR AND conf`S5`FPRh=spec`FPRh AND conf`S5`FPRl=spec`FPRl AND
    (conf`S5`SPR = LAMBDA(sp:upto(nspr_LAST)):spec`SPR(nat2bv[5](sp))) AND
    ((T=0 OR LET c=tom_impl_conf(initial_vamp,input,T-1) IN
	signals4_spec(c`S4,c`S5`SPR(nspr_SR),FALSE)`JISR) IMPLIES
      (conf`S2`DPC=spec`DPC AND conf`S2`PCp=spec`PCp AND (T>0 IMPLIES mem=spec`mem)));

%% simple decomposition lemma for computations:
%% doing Tp steps is equivalent to first doing T (<=Tp) steps, 
%% and using this as initial configuration for doing Tp-T steps
  vamp_conf_equal : LEMMA
    FORALL (T  : nat):
      FORALL (Tp : upfrom(T)):
      tom_impl_conf(initial_vamp,input,Tp)=
      	tom_impl_conf(tom_impl_conf(initial_vamp,input,T),LAMBDA (n:nat):input(T+n),Tp-T);

%% broing helper lemmas
  mem_conf_with_interupts_strongly_correct : LEMMA
    FORALL (T:nat):
      LET conf=tom_impl_conf(initial_vamp,input,T) IN
      FORALL (Tp:nat):
      tommem_conf[mif_next](conf`S3`mem,Tp,LAMBDA(n:nat):real_mem_input_t(n+T))=
       tom_impl_conf(conf,LAMBDA(n:nat):input(n+T),Tp)`S3`mem;

  mem_conf_with_interupts_correct : LEMMA
    FORALL (T:nat):
      tommem_conf[mif_next](initial_vamp`S3`mem,T,real_mem_input_t)=
       tom_impl_conf(initial_vamp,input,T)`S3`mem;

  mem_conf_with_interupts_equal : LEMMA
    FORALL (T:nat):
      LET conf=tom_impl_conf(initial_vamp,input,T),
	  mem =mem_conf_with_interrupts(T) IN
	FORALL (Tp:nat):
	  mem_conf_with_interrupts(T+Tp)=
    	  mif_memory_conf(conf`S3`mem,mem,LAMBDA(n:nat):real_mem_input_t(n+T))(Tp);

%% further helper lemmas for correctness with interrupts
  vamp_correct_writeback_OR_JISR : LEMMA
  FORALL (T:nat):
    LET conf=tom_impl_conf(initial_vamp,input,T),
	s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(T)`reset) IN
    NOT input(T)`reset AND vamp_correct?(T) IMPLIES 
      cIspec`writeback(T)=(s4`JISR OR s4`writeback);

%% simple, but important lemma stating that sI_inst and sI_wb are equal
%% up to the cycle after the first interrupt 
%% (needed to derive vamp_fulfills_spec from tom_correct)
  sI_inst_helper : LEMMA
  FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(T) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp)) AND NOT input(T)`reset IMPLIES
      FORALL (Tp:upto(T+1)):sI_inst(Tp)=sI_writeback(Tp);

%% This lemma just summarizes the commutative diagram for vamp_correct
  vamp_correct_without_interrupt : LEMMA
  FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(T) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp) AND NOT input(Tp)`ext_reset) IMPLIES
    tom_impl_conf(initial_vamp,input,T)`S5`GPR =dlx_conf_without_interrupt_IEEEf(init_conf,sI_writeback(T))`GPR AND
    tom_impl_conf(initial_vamp,input,T)`S5`FPRh=dlx_conf_without_interrupt_IEEEf(init_conf,sI_writeback(T))`FPRh AND
    tom_impl_conf(initial_vamp,input,T)`S5`FPRl=dlx_conf_without_interrupt_IEEEf(init_conf,sI_writeback(T))`FPRl AND
    tom_impl_conf(initial_vamp,input,T)`S5`SPR =LAMBDA(sp:upto(nspr_LAST)):dlx_conf_without_interrupt_IEEEf(init_conf,sI_writeback(T))`SPR(nat2bv[5](sp));

%% And since no interrupt occurs, we can replace the specification without interrupts
%% by that with interrupts...
  vamp_correct_with_interrupt : LEMMA
  FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(T) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp) AND NOT input(Tp)`ext_reset) IMPLIES
    tom_impl_conf(initial_vamp,input,T)`S5`GPR =dlx_conf_IEEEf(init_conf,sI_writeback(T))`GPR AND
    tom_impl_conf(initial_vamp,input,T)`S5`FPRh=dlx_conf_IEEEf(init_conf,sI_writeback(T))`FPRh AND
    tom_impl_conf(initial_vamp,input,T)`S5`FPRl=dlx_conf_IEEEf(init_conf,sI_writeback(T))`FPRl AND
    tom_impl_conf(initial_vamp,input,T)`S5`SPR =LAMBDA(sp:upto(nspr_LAST)):dlx_conf_IEEEf(init_conf,sI_writeback(T))`SPR(nat2bv[5](sp));

%% Finally, a "hard" lemma:
%% Showing that the register file part of vamp_fulfills_spec holds
%% up to the cycle AFTER the first interrupt
  vamp_correct_with_interrupt_extended : LEMMA
  FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(1+T) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:upto(T)): NOT input(Tp)`reset) AND
    (FORALL (Tp:upto(T)): NOT JISR_t(Tp)) IMPLIES
      FORALL (Tp:upto(T+1)):
    	tom_impl_conf(initial_vamp,input,Tp)`S5`GPR =dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`GPR AND
    	tom_impl_conf(initial_vamp,input,Tp)`S5`FPRh=dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`FPRh AND
    	tom_impl_conf(initial_vamp,input,Tp)`S5`FPRl=dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`FPRl AND
    	tom_impl_conf(initial_vamp,input,Tp)`S5`SPR =LAMBDA(sp:upto(nspr_LAST)):dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`SPR(nat2bv[5](sp));

%  vamp_correct_with_interrupt_extended_inst : LEMMA
%  FORALL (T:nat):
%    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
%    good_tom_impl_input_func_below?(1+T) AND
%    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
%    (FORALL (Tp:upto(T)): NOT input(Tp)`reset) AND
%    (FORALL (Tp:upto(T)): NOT JISR_t(Tp) AND NOT input(Tp)`ext_reset) IMPLIES
%      FORALL (Tp:upto(T+1)):
%  	vamp_fulfills_spec?(Tp);

%% simple helper
  vamp_correct_repeat : LEMMA
  FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(T) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp) AND NOT input(Tp)`ext_reset) AND NOT input(T)`reset AND JISR_t(T) IMPLIES
    LET conf=tom_impl_conf(initial_vamp,input,T),
	s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(T)`reset) IN
      s4`repeat=repeat(dlx_conf_IEEEf(init_conf,sI_writeback(T))) AND
      s4`writeback = NOT s4`repeat;

%% Extend the correctness in the cycle after the interrupt to the PCs
%% Here, we have to assome JISR_t(T) since only then, PC correctness holds in T+1
  vamp_correct_JISR_step : LEMMA
  FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(T) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp) AND NOT input(Tp)`ext_reset) AND NOT input(T)`reset AND JISR_t(T) IMPLIES
    tom_impl_conf(initial_vamp,input,1+T)`S2`DPC =dlx_conf_IEEEf(init_conf,sI_writeback(1+T))`DPC AND
    tom_impl_conf(initial_vamp,input,1+T)`S2`PCp =dlx_conf_IEEEf(init_conf,sI_writeback(1+T))`PCp AND
    tom_impl_conf(initial_vamp,input,1+T)`S5`GPR =dlx_conf_IEEEf(init_conf,sI_writeback(1+T))`GPR AND
    tom_impl_conf(initial_vamp,input,1+T)`S5`FPRh=dlx_conf_IEEEf(init_conf,sI_writeback(1+T))`FPRh AND
    tom_impl_conf(initial_vamp,input,1+T)`S5`FPRl=dlx_conf_IEEEf(init_conf,sI_writeback(1+T))`FPRl AND
    tom_impl_conf(initial_vamp,input,1+T)`S5`SPR =LAMBDA(sp:upto(nspr_LAST)):dlx_conf_IEEEf(init_conf,sI_writeback(1+T))`SPR(nat2bv[5](sp));

%% And now for the missing part, the memory

%% some helpers
  tag_unique_mem_valid : LEMMA
  FORALL (T:nat):
    fu_conf(T)`mem`inst`valid IMPLIES
      sI_mem(T)>=0 AND tag_unique(sI_mem(T),T);

  ridiculous_lemma : LEMMA
    FORALL (a,b:int):
      a>=b IFF (a>b OR a=b);

  commit_helper : LEMMA
  FORALL (T:nat):
    fu_conf(T)`mem`inst`valid AND NOT fu_conf(T)`mem`inst`stalled IMPLIES
      sI_mem(T)>= 0 AND NOT EXISTS (Tp:below(T)):commits?(Tp,sI_mem(T));

  mem_commit_is_writeback_helper : LEMMA
  FORALL (T:nat):
    fu_conf(T)`mem`inst`valid AND NOT fu_conf(T)`mem`inst`stalled AND NOT fu_conf(T)`mem`inst`dmal AND
    fu_conf(T)`mem`inst`tag=ROBhead(T) AND fu_conf(T)`mem`inst`I_s IMPLIES
      sI_writeback(T)=sI_mem(T);

  mem_commit_is_writeback : LEMMA
  FORALL (T,i:nat):
    commits?(T,i) AND I_write(Iw(dlx_conf_without_interrupt_IEEEf(init_conf,i))) IMPLIES
      sI_writeback(T)=sI_M(T+1)-1;

  mem_inst_is_committed : LEMMA
    FORALL (T,i:nat):
      LET conf=dlx_conf_without_interrupt_IEEEf(init_conf,i) IN
	sI_mem(T)>i AND I_mem(Iw(conf)) AND 
	NOT imal(conf) AND NOT ipf(conf) AND NOT dmal(conf) IMPLIES
	  EXISTS (Tp:below(T)): commits?(Tp,i);
       
%% The main lemmas for showing that interrupts are synchronous wrt the memory
  mem_commit_equal1 : LEMMA
    FORALL (T:nat):
%      JISR_t(T) AND
      sI_M(T)>=1+sI_writeback(T) IMPLIES
      FORALL (j:subrange(sI_writeback(T)+1,sI_M(T)-1)):
	LET conf=dlx_conf_without_interrupt_IEEEf(init_conf,j) IN
	NOT (I_write(Iw(conf)) AND NOT imal(conf) AND NOT ipf(conf) AND 
		NOT dmal(conf) AND I_mem(Iw(conf)));
	
  mem_commit_equal1_mem : LEMMA
    FORALL (T:nat):
%      JISR_t(T) AND
      sI_M(T)>=1+sI_writeback(T) IMPLIES
	dlx_conf_without_interrupt_IEEEf(init_conf,sI_M(T))`mem=
	dlx_conf_without_interrupt_IEEEf(init_conf,sI_writeback(T)+1)`mem;
	
  mem_commit_equal2 : LEMMA
    FORALL (T:nat):
      JISR_t(T) AND
      sI_M(T)<1+sI_writeback(T) IMPLIES
      FORALL (j:subrange(sI_M(T),sI_writeback(T))):
	LET conf=dlx_conf_without_interrupt_IEEEf(init_conf,j) IN
	NOT (I_write(Iw(conf)) AND NOT imal(conf) AND NOT ipf(conf) AND 
		NOT dmal(conf) AND I_mem(Iw(conf)));
	
%% And the summary lemma actually stating the desired equality for the memory
  mem_commit_equal_mem : LEMMA
    FORALL (T:nat):
      JISR_t(T) IMPLIES
	dlx_conf_without_interrupt_IEEEf(init_conf,sI_M(T))`mem=
	dlx_conf_without_interrupt_IEEEf(init_conf,sI_writeback(T)+1)`mem;

%% simple helper
  dlx_mem_without_interrupt_correct : LEMMA
  FORALL (init_conf: dlx_conft,
  	  i        : nat):
    (i=0 OR FORALL (j:below(i-1)): NOT JISR(dlx_conf_without_interrupt_IEEEf(init_conf,j))) IMPLIES
      dlx_conf_IEEEf(init_conf,i)`mem=dlx_conf_without_interrupt_IEEEf(init_conf,i)`mem;

%% Putting all the above together, we can conclude the memory part of
%% vamp_fulfills_spec in the cycle after the first interrupt and that
%% no store is interrupted.
  vamp_correct_JISR_step_mem : LEMMA
  FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(T+1) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp) AND NOT input(Tp)`ext_reset) AND NOT input(T)`reset AND JISR_t(T) IMPLIES
    NOT tommem_out(initial_vamp`S3`mem,mem_input_t)(T)`mif_input`data`mw AND
    mif_memory_conf(initial_vamp`S3`mem,initial_vamp_mem,mem_input_t)(1+T)=dlx_conf_IEEEf(init_conf,sI_writeback(1+T))`mem;

%% simple helpers
  vamp_correct_mem_conf_with_interrupts : LEMMA
  FORALL (T:nat):
    good_mif_next_with_interrupts?(T) AND
    good_tom_impl_input_func_below?(T+1) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp) AND 
	NOT input(Tp)`ext_reset) AND NOT input(T)`reset IMPLIES
      FORALL (Tp:upto(T+1)):
	(Tp<T   IMPLIES real_mem_input_t(Tp)=mem_input_t(Tp)) AND
	(Tp<T+1 IMPLIES consistent_mif_next?(Tp,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t)) AND
	(Tp<T+1 IMPLIES tommem_conf[mif_next](initial_vamp`S3`mem,Tp,mem_input_t)=
       	                tom_impl_conf(initial_vamp,input,Tp)`S3`mem) AND
	mem_conf_with_interrupts(Tp)=
    	  mif_memory_conf(initial_vamp`S3`mem,initial_vamp_mem,mem_input_t)(Tp);	

  vamp_correct_JISR_helper0 : LEMMA
    FORALL (T:nat):
    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    good_tom_impl_input_func_below?(T) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:upto(T)): NOT input(Tp)`reset) IMPLIES
      (FORALL (Tp:below(T)): NOT JISR_t(Tp))=
      (FORALL (Tp:below(T)): 
    	LET conf=tom_impl_conf(initial_vamp,input,Tp),
	    s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(Tp)`reset) IN
	   NOT s4`JISR);

  vamp_correct_mem_conf_with_interrupts2 : LEMMA
  FORALL (T:nat):
    good_mif_next_with_interrupts?(T) AND
    good_tom_impl_input_func_below?(T+1) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    (FORALL (Tp:below(T)): 
	NOT input(Tp)`reset AND LET conf=tom_impl_conf(initial_vamp,input,Tp),
	    s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(Tp)`reset) IN
	   NOT s4`JISR AND 
	NOT input(Tp)`ext_reset) AND NOT input(T)`reset IMPLIES
      FORALL (Tp:upto(T+1)):
	(Tp<T   IMPLIES real_mem_input_t(Tp)=mem_input_t(Tp)) AND
	(Tp<T+1 IMPLIES consistent_mif_next?(Tp,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t)) AND
	(Tp<T+1 IMPLIES tommem_conf[mif_next](initial_vamp`S3`mem,Tp,mem_input_t)=
       	                tom_impl_conf(initial_vamp,input,Tp)`S3`mem) AND
	mem_conf_with_interrupts(Tp)=
    	  mif_memory_conf(initial_vamp`S3`mem,initial_vamp_mem,mem_input_t)(Tp);	

%% additional helper that derives synced_code from its version with interrupts
  synced_code_helper : LEMMA
    synced_code_with_interrupt?(init_conf) IMPLIES
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i));

%% a final simple helper
  vamp_correct_JISR_helper : LEMMA
    FORALL (T:nat):
    good_mif_next_with_interrupts?(T) AND
    good_tom_impl_input_func_below?(T+1) AND
    synced_code_with_interrupt?(init_conf) AND
    (FORALL (Tp:upto(T)): NOT input(Tp)`reset) IMPLIES
      (FORALL (Tp:below(T)): NOT JISR_t(Tp))=
      (FORALL (Tp:below(T)): 
    	LET conf=tom_impl_conf(initial_vamp,input,Tp),
	    s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(Tp)`reset) IN
	   NOT s4`JISR);

%% And the final proof that correcntess with interrupts holds
%% up to the cycle after the first interrupt in 2 different versions
  vamp_correct_with_JISR_step : LEMMA
    FORALL (T:nat):
    good_mif_next_with_interrupts?(T) AND
    good_tom_impl_input_func_below?(T+1) AND
    synced_code_with_interrupt?(init_conf) AND
      (FORALL (Tp:upto(T)): NOT input(Tp)`reset) AND 
      (FORALL (Tp:below(T)): NOT JISR_t(Tp)) IMPLIES
        FORALL (Tp:upto(T+1)):
	  (Tp <= T IMPLIES vamp_correct?(Tp)) AND
	  vamp_fulfills_spec?(Tp) AND
	  (Tp>0 AND JISR_t(Tp-1) IMPLIES 
	    NOT tommem_out(initial_vamp`S3`mem,real_mem_input_t)(Tp-1)`mif_input`data`mw);

  vamp_correct_with_JISR_step2 : LEMMA
    FORALL (T:nat):
    good_mif_next_with_interrupts?(T) AND
    good_tom_impl_input_func_below?(T+1) AND
    synced_code_with_interrupt?(init_conf) AND
      (FORALL (Tp:upto(T)): NOT input(Tp)`reset) AND
      (FORALL (Tp:below(T)): 
    	LET conf=tom_impl_conf(initial_vamp,input,Tp),
	    s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(Tp)`reset) IN
	   NOT s4`JISR) IMPLIES
        FORALL (Tp:upto(T+1)):
	  (Tp <= T IMPLIES vamp_correct?(Tp)) AND
	  vamp_fulfills_spec?(Tp) AND
	  ((Tp>0 AND LET old_conf=tom_impl_conf(initial_vamp,input,Tp-1) IN
	    signals4_spec(old_conf`S4,old_conf`S5`SPR(nspr_SR),input(Tp-1)`reset)`JISR) IMPLIES 
	      NOT tommem_out(initial_vamp`S3`mem,real_mem_input_t)(Tp-1)`mif_input`data`mw);

%  vamp_correct_with_JISR_step3 : LEMMA
%    FORALL (T:nat):
%    consistent_mif_next?(T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
%    good_tom_impl_input_func_below?(T+1) AND
%    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
%      (FORALL (Tp:upto(T)): 
%    	LET conf=tom_impl_conf(initial_vamp,input,Tp),
%	    s4  =signals4_spec(conf`S4,conf`S5`SPR(nspr_SR),input(Tp)`reset) IN
%	  NOT input(Tp)`reset AND NOT s4`JISR) 
%	  is_JISR?(tom_impl_conf(initial_vamp,input,T)) IMPLIES
%        FORALL (Tp:upto(T+1)):
%	LET conf=tom_impl_conf(initial_vamp,input,Tp) IN
%          conf`S5`GPR =dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`GPR AND
%          conf`S5`FPRh=dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`FPRh AND
%          conf`S5`FPRl=dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`FPRl AND
%          (conf`S5`SPR =LAMBDA(sp:upto(nspr_LAST)):dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`SPR(nat2bv[5](sp))) AND
%	  ((Tp=0 OR LET old_conf=tom_impl_conf(initial_vamp,input,Tp-1) IN
%		signals4_spec(old_conf`S4,old_conf`S5`SPR(nspr_SR),input(Tp-1)`reset)`JISR) IMPLIES
%    	    (conf`S2`DPC =dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`DPC AND
%    	     conf`S2`PCp =dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`PCp AND
%    	     (Tp>0 IMPLIES mif_memory_conf(initial_vamp`S3`mem,initial_vamp_mem,mem_input_t)(Tp)=dlx_conf_IEEEf(init_conf,sI_writeback(Tp))`mem)));

END tom_correct4_JISR