Ignore:
Timestamp:
May 7, 2012, 11:12:13 AM (8 years ago)
Author:
mulligan
Message:

Fixes to get everything compiling again

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1899 r1919  
    4141        λ${ident E}.$s ] ] (refl ? $t) }.
    4242
     43lemma succ_nat_of_bitvector_aux_half_add_1:
     44  ∀n: nat.
     45  ∀bv: BitVector n.
     46  ∀buffer: nat.
     47  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
     48    S (nat_of_bitvector_aux n buffer bv) =
     49      nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)).
     50  #n #bv elim bv
     51  [1:
     52    #buffer normalize #absurd
     53    cases (lt_to_not_zero … absurd)
     54  |2:
     55    #n' #hd #tl #inductive_hypothesis #buffer
     56    cases daemon
     57  ]
     58qed.
     59   
     60lemma succ_nat_of_bitvector_half_add_1:
     61  ∀n: nat.
     62  ∀bv: BitVector n.
     63  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
     64    S (nat_of_bitvector … bv) = nat_of_bitvector …
     65      (\snd (half_add n (bitvector_of_nat … 1) bv)).
     66  #n #bv elim bv
     67  [1:
     68    normalize #absurd
     69    cases (lt_to_not_zero … absurd)
     70  |2:
     71    #n' #hd #tl #inductive_hypothesis
     72    cases daemon
     73  ]
     74qed.
     75   
    4376let rec traverse_code_internal
    4477  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
Note: See TracChangeset for help on using the changeset viewer.