tom_correct4[(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_correct3[initial_vamp,fpu_spec_op,add_spec,md_spec,fpm_spec,TOMadd,TOMmd,TOMfpm,mif_next,input,initial_vamp_mem]

%% step 2, sub-step c, last part
%% Now for the main induction: vamp_correct(t) for all t

%%
%% induction base
%%
  initial_vamp_correct : LEMMA
    vamp_correct?(0);

%% induction steps for all the parts of the configuration
%% of the form: vamp_correct(t) => part of vamp_correct(t+1)
%% the lemmas are "obvious" unless annotated otherwise

%%
%% correctness of the memory: store instructions
%%
  vamp_induction_step_mem_conf : LEMMA
  FORALL (T:nat):
    good_tom_impl_input_func_below?(T+1) AND NOT input(T)`reset AND
    vamp_correct?(T) IMPLIES 
	dlx_conf_without_interrupt_IEEEf(init_conf,sI_M(1+T))`mem=
	mif_memory_conf(initial_vamp`S3`mem,initial_vamp_mem,mem_input_t)(1+T);

  vamp_induction_step_CDB_arbiter : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES CDB_arbiter(1+T)=nconf`S3`CDB_arbiter;

  vamp_induction_step_alurs_arbiter : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES alurs_arbiter(1+T)=nconf`S2`alurs_arbiter;

  vamp_induction_step_fu_conf : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND NOT input(T)`ext_reset AND
    vamp_correct?(T) IMPLIES
    tom_impl_conf(initial_vamp,input,1+T)`S3`alu=fu_conf(1+T)`alu AND
    tom_impl_conf(initial_vamp,input,1+T)`S3`mem=fu_conf(1+T)`mem AND
    tom_impl_conf(initial_vamp,input,1+T)`S3`fpu1=fu_conf(1+T)`fpu1 AND
    tom_impl_conf(initial_vamp,input,1+T)`S3`fpu2=fu_conf(1+T)`fpu2 AND
    tom_impl_conf(initial_vamp,input,1+T)`S3`fpu3=fu_conf(1+T)`fpu3;

  vamp_induction_step_ROBhead : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES ROBhead(1+T)=nconf`S4`ROBhead;

  vamp_induction_step_ROBtail : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES ROBtail(1+T)=nconf`S4`ROBtail;

  vamp_induction_step_ROBcount : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES ROBcount(1+T)=nconf`S4`ROBcount;

%% helper lemmas and correctness of instrction fetch with
%% sync criterion
  sync_helper : LEMMA
  FORALL (i:nat,T:nat):
    I_sync(Iw(dlx_conf_without_interrupt_IEEEf(init_conf,i))) AND
      (issued(i,T) OR sI_issue(T)=i AND cIspec`issue(T)) IMPLIES
        FORALL (j:below(i)):terminated(j,T);

  self_modifying_helper : LEMMA
  FORALL (T:nat):
    LET conf=LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i) IN
    synced_code?(init_conf,conf) AND
    cIS1_t(T) IMPLIES 
      FORALL (i:below(sI_S1(T))):
	is_write_to_adr?(conf(sI_S1(T))`DPC)(conf(i)) IMPLIES
	  terminated(i,T);

  terminated_memory_instruction_is_committed : LEMMA
  FORALL (T:nat,i:nat):
    LET conf=dlx_conf_without_interrupt_IEEEf(init_conf,i) IN
      I_mem(Iw(conf)) AND NOT imal(conf) AND NOT ipf(conf) AND NOT dmal(conf) AND 
	(terminated(i,T) OR in_ROB(i,T)) IMPLIES
	sI_M(T)>i;

  vamp_induction_step_S1 : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND NOT input(T)`ext_reset AND
    good_tom_impl_input_func_below?(T) AND
    consistent_mif_next?(1+T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    synced_code?(init_conf,LAMBDA (i:nat):dlx_conf_without_interrupt_IEEEf(init_conf,i)) AND
    vamp_correct?(T) IMPLIES S1(1+T)=nconf`S1;

%% End of fetch correctness

  vamp_induction_step_PCs : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES PCp(1+T)=nconf`S2`PCp AND DPC(1+T)=nconf`S2`DPC;

  vamp_induction_step_aux_ROB : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES FORALL (rob:below(rob_entries)):
	nconf`S4`rob(rob)`dest   =aux_conf(1+T)`ROB(rob)`dest AND
	nconf`S4`rob(rob)`nextDPC=aux_conf(1+T)`ROB(rob)`nextDPC AND
	nconf`S4`rob(rob)`nextPCp=aux_conf(1+T)`ROB(rob)`nextPCp AND
	nconf`S4`rob(rob)`oDPC   =aux_conf(1+T)`ROB(rob)`oDPC AND
	nconf`S4`rob(rob)`oPCp   =aux_conf(1+T)`ROB(rob)`oPCp;

  vamp_induction_step_aux_RS : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES FORALL (rs:rsnot):
	nconf`S2`RS(rs)`f=aux_conf(1+T)`RS(rs)`f AND
        nconf`S2`RS(rs)`fprh=aux_conf(1+T)`RS(rs)`fprh;

  vamp_induction_step_R : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES map_cIt(nconf)`R=cIc_ieeef(1+T)`R;

  vamp_induction_step_RS : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES map_cIt(nconf)`RS=cIc_ieeef(1+T)`RS;

  vamp_induction_step_P : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND NOT input(T)`ext_reset AND
    good_tom_impl_input_func_below?(T) AND
    consistent_mif_next?(1+T,initial_vamp`S3`mem,initial_vamp_mem)(mem_input_t) AND
    vamp_correct?(T) IMPLIES map_cIt(nconf)`P=cIc_ieeef(1+T)`P;

  vamp_induction_step_ROB : LEMMA
  FORALL (T:nat):
    LET nconf=tom_impl_conf(initial_vamp,input,1+T) IN
    NOT input(T)`reset AND NOT JISR_t(T) AND
    vamp_correct?(T) IMPLIES map_cIt(nconf)`ROB=cIc_ieeef(1+T)`ROB;

%% putting all this together yields the induction proof...

  vamp_induction : 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-1)): 
	NOT input(Tp)`reset AND NOT JISR_t(Tp) AND NOT input(Tp)`ext_reset) IMPLIES
    vamp_correct?(T);

%% and 2 alternative versions
  vamp_induction2 : 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
    FORALL (Tp:upto(T)):vamp_correct?(Tp);

  vamp_induction3 : 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)):
	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 AND NOT input(Tp)`ext_reset) IMPLIES
    FORALL (Tp:upto(T)):vamp_correct?(Tp);

%% now we have correcntess without interrupts 
%% (given by vamp_correct + Daniels Tomasulo proof + the proof of step 1,
%%  we hava a commutative diagram that the VAMP implementation without
%%  intertups simulates the VAMP specification without interrupts)
END tom_correct4