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

More stuff moved around in proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2110 r2122  
    3232      instruction_has_label id (\fst i) →
    3333        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 #lower
    59   cases daemon
    60 qed.
    6134
    6235lemma short_jump_cond_ok:
Note: See TracChangeset for help on using the changeset viewer.