Changeset 2672 for src/ASM/ASMCosts.ma
- Timestamp:
- Feb 16, 2013, 6:49:13 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r2664 r2672 166 166 @execute_1_and_program_counter_after_other_in_lockstep0 assumption. 167 167 qed. 168 169 lemma nat_of_bitvector_lt_bound:170 ∀n: nat.171 ∀b: BitVector n.172 nat_of_bitvector n b < 2^n.173 #n #b cases daemon174 qed.175 168 176 169 lemma sublist_tal_pc_list_all_program_counter_list:
Note: See TracChangeset
for help on using the changeset viewer.