Changeset 1484


Ignore:
Timestamp:
Nov 2, 2011, 2:46:59 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1333 r1484  
    11711171qed.
    11721172
     1173(*
    11731174lemma split_prod_exists:
    11741175  ∀A, m, n.
     
    11861187      ]
    11871188  ]
    1188 
    1189 lemma split_elim:
     1189*)
     1190
     1191axiom split_elim:
    11901192 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
    11911193  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
    1192   #A #l #m #v #P #hyp
     1194(*  #A #l #m #v #P #hyp
    11931195  normalize
    11941196  <(split_prod A l m v ? ? ?)
     1197*)
    11951198
    11961199example half_add_SO:
     
    12321235  | cons hd tl ⇒
    12331236    let 〈new_pc, byte〉 ≝ next code_memory pc in
    1234       hd = byte ∧ encoding_check code_memory new_c final_pc tl
     1237      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
    12351238  ].
    12361239
Note: See TracChangeset for help on using the changeset viewer.