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

More stuff moved around in proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2121 r2122  
    409409
    410410include alias "ASM/Vector.ma".
    411 
    412 axiom sub16_with_carry_overflow:
    413   ∀left, right, result: BitVector 16.
    414   ∀flags: BitVector 3.
    415   ∀upper: BitVector 9.
    416   ∀lower: BitVector 7.
    417     sub_16_with_carry left right false = 〈result, flags〉 →
    418       vsplit bool 9 7 result = 〈upper, lower〉 →
    419         get_index_v bool 3 flags 2 ? = true →
    420           upper = [[true; true; true; true; true; true; true; true; true]].
    421   //
    422 qed.
    423411
    424412lemma main_lemma_preinstruction:
Note: See TracChangeset for help on using the changeset viewer.