Changeset 2136


Ignore:
Timestamp:
Jun 28, 2012, 2:58:54 PM (5 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2135 r2136  
    405405            (add … (sigma ppc) (bitvector_of_nat … j))))))
    406406    [1: #j #H <load_code_memory_ok
    407         [ @assembly_ok cases daemon
     407        [ @assembly_ok
    408408        | cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (|assembled|))) ≤ |assembled'|)
    409           [
     409          [ cases sigma_policy_witness #_ #sigma_ok cases daemon
     410            (*CSC: True, propagate already proved invariant*)
    410411          | #LE @(lt_to_le_to_lt … LE)
    411412            @lt_to_lt_nat_of_bitvector_add
    412413            [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction)
    413414              / by /
    414             | @(transitive_le ???? assembly_ok1) cases daemon
     415            | @(transitive_le ???? assembly_ok1) change with (? < ?) cases daemon
     416              (*CSC: Same as before*)
    415417            | assumption
    416418            ]   
Note: See TracChangeset for help on using the changeset viewer.