Changeset 2079 for src/ASM/Assembly.ma
- Timestamp:
- Jun 14, 2012, 11:45:49 AM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2078 r2079 773 773 λsigma: Word → Word. 774 774 λpolicy: Word → bool. 775 sigma (zero …) = zero … ∧ 775 776 ∀ppc: Word. ∀ppc_ok. 776 777 let instr_list ≝ \snd program in … … 780 781 let instruction ≝ \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in 781 782 let next_pc ≝ sigma (add 16 ppc (bitvector_of_nat 16 1)) in 782 sigma (zero …) = zero … 783 ∧ 784 (nat_of_bitvector … ppc ≤ |instr_list| → 783 (nat_of_bitvector … ppc ≤ |instr_list| → 785 784 next_pc = add 16 pc (bitvector_of_nat … (instruction_size lookup_labels sigma policy ppc instruction))) 786 785 ∧
Note: See TracChangeset
for help on using the changeset viewer.