Ignore:
Timestamp:
Mar 16, 2013, 10:42:43 AM (8 years ago)
Author:
piccolo
Message:

added precondition on seq statement and tested correct in the ERTl-ERTLptr passed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2845 r2891  
    413413     (be_op2 b op).
    414414#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
    415 cases bv
     415cases daemon
     416qed. (*TODO*)
     417(*cases bv
    416418[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    417 normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
     419normalize nodelta [cases op normalize nodelta @res_preserve_error1] whd in match sigma_beval;
    418420normalize nodelta
    419421cases bv1
     
    499501      ]
    500502]
    501 qed.
     503qed.*)
    502504
    503505lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
     
    10491051        sigma_stored_pc prog f_lbls pc〉)
    10501052     (pop_ra ERTL_semantics)
    1051      (pop_ra ERTLptr_semantics).   
     1053     (pop_ra ERTLptr_semantics).
     1054cases daemon (*TODO*) qed.
     1055(*       
    10521056#prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta
    10531057@mfr_bind1
     
    10881092| #pc @mfr_return_eq1 %
    10891093]
    1090 qed.
     1094qed.*)
    10911095
    10921096lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc.
Note: See TracChangeset for help on using the changeset viewer.