- Timestamp:
- Jun 28, 2012, 2:58:54 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2135 r2136 405 405 (add … (sigma ppc) (bitvector_of_nat … j)))))) 406 406 [1: #j #H <load_code_memory_ok 407 [ @assembly_ok cases daemon407 [ @assembly_ok 408 408 | 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*) 410 411 | #LE @(lt_to_le_to_lt … LE) 411 412 @lt_to_lt_nat_of_bitvector_add 412 413 [ @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? eq_assembly_1_pseudoinstruction) 413 414 / by / 414 | @(transitive_le ???? assembly_ok1) cases daemon 415 | @(transitive_le ???? assembly_ok1) change with (? < ?) cases daemon 416 (*CSC: Same as before*) 415 417 | assumption 416 418 ]
Note: See TracChangeset
for help on using the changeset viewer.