Ignore:
Timestamp:
Jun 27, 2012, 3:36:54 PM (9 years ago)
Author:
sacerdot
Message:

More stuff moved around in proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2121 r2122  
    765765    eq_instruction i1 i2 = true → i1 ≃ i2.
    766766  #i1 #i2
    767   cases i1 cases i2 cases daemon (*
     767  cases i1 cases i2 cases daemon (* easy but tedious
    768768  [1,10,19,28,37,46:
    769769    #arg1 #arg2
     
    14401440qed.
    14411441
    1442 (*CSC: move elsewhere*)
    1443 example sub_minus_one_seven_eight:
    1444   ∀v: BitVector 7.
    1445   false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
    1446   \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
    1447  cases daemon.
    1448 qed.
    1449 
    14501442(*
    14511443lemma blah:
Note: See TracChangeset for help on using the changeset viewer.