Changeset 1522 for src/ASM/CostsProof.ma
 Timestamp:
 Nov 21, 2011, 3:49:04 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1514 r1522 1 2 1 include "ASM/ASMCosts.ma". 3 2 include "ASM/WellLabeled.ma". … … 209 208 cases(lt_to_not_zero … proof) 210 209  #m' #proof 211 normalize in ⊢ (???%) 210 normalize in ⊢ (???%); 212 211 cases n 213 212 [ normalize // … … 256 255 ] 257 256 qed. 257 258 include alias "arithmetics/nat.ma". 258 259 259 260 lemma plus_minus_rearrangement_1: … … 277 278 >(associative_plus (m'  n) 1 (o  m'  1)) 278 279 <commutative_plus in match (1 + (o  m'  1)); 279 <(minus_m_n_minus_minus_plus_1 o m') in match (o  m'  1 + 1) 280 <(minus_m_n_minus_minus_plus_1 o m') in match (o  m'  1 + 1); 280 281 [1: >ind_hyp 281 282 [1: % … … 338 339 clock … (write_at_stack_pointer … s sp) = clock … s. 339 340 #s #sp 340 change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp) with (341 change in match (write_at_stack_pointer (BitVectorTrie Byte 16) s sp); with ( 341 342 let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in 342 343 ?);
Note: See TracChangeset
for help on using the changeset viewer.