Changeset 2672 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Feb 16, 2013, 6:49:13 PM (7 years ago)
Author:
sacerdot
Message:

One less axiom on bitvectors.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/ASMCosts.ma

    r2664 r2672  
    166166  @execute_1_and_program_counter_after_other_in_lockstep0 assumption.
    167167qed. 
    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 daemon
    174 qed.
    175168
    176169lemma sublist_tal_pc_list_all_program_counter_list:
Note: See TracChangeset for help on using the changeset viewer.