Changeset 2122 for src/ASM/AssemblyProofSplitSplit.ma
 Timestamp:
 Jun 27, 2012, 3:36:54 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplitSplit.ma
r2110 r2122 32 32 instruction_has_label id (\fst i) → 33 33 occurs_exactly_once ASMTag pseudo_instruction id instr_list. 34 35 (*CSC: move elsewhere *)36 axiom sub_16_to_add_16_8_0:37 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.38 get_index' ? 2 0 flags = false →39 sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →40 v1 = add ? v2 (sign_extension (false:::v3)).41 42 (*CSC: move elsewhere *)43 axiom sub_16_to_add_16_8_1:44 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.45 get_index' ? 2 0 flags = true →46 sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →47 v1 = add ? v2 (sign_extension (true:::v3)).48 49 (*CSC: move elsewhere *)50 lemma vsplit_ok:51 ∀A: Type[0].52 ∀m, n: nat.53 ∀v: Vector A (m + n).54 ∀upper: Vector A m.55 ∀lower: Vector A n.56 〈upper, lower〉 = vsplit A m n v →57 upper @@ lower = v.58 #A #m #n #v #upper #lower59 cases daemon60 qed.61 34 62 35 lemma short_jump_cond_ok:
Note: See TracChangeset
for help on using the changeset viewer.