- Timestamp:
- May 30, 2011, 6:43:14 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r859 r860 395 395 qed. 396 396 397 axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop. 398 397 399 definition build_maps' ≝ 398 400 λpseudo_program. … … 405 407 let 〈labels,pc_costs〉 ≝ res in 406 408 let 〈ignore,costs〉 ≝ pc_costs in 407 ∀ pc. (nat_of_bitvector … pc) < length … pre→408 lookup ?? pc labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre pc)))409 ∀id. occurs_exactly_once id instr_list → 410 lookup ?? id labels (zero …) = sigma pre' (\snd (fetch_pseudo_instruction pre id))) 409 411 instr_list 410 412 (λprefix,i,tl,prf,t. … … 431 433 let 〈pc, costs〉 ≝ pc_costs in 432 434 〈labels, costs〉. 433 [ whd cases construct in p3 #PC #CODE #JMEQ whd # pc #Hpc435 [ whd cases construct in p3 #PC #CODE #JMEQ whd #id #Hid 434 436 generalize in match (sig2 … t) whd in ⊢ (% → ?) 435 437 >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1 436 >length_append in Hpc <plus_n_Sm in ⊢ (% → ?) <plus_n_O in ⊢ (% → ?) #Hpc437 438 whd in ⊢ (??(????%?)?) -labels1; 438 439 cases label 439 440 [ whd in ⊢ (??(????%?)?) 440 cases (le_to_or_lt_eq … Hpc) 441 [ #H1 >(IH1 pc) [2: @(le_S_S_to_le … H1)] 442 (* lemmas needed here *) 443 | #H1 generalize in match (injective_S … H1) -H1 #H1 444 (* ??? *) 445 ] 441 (* COMPLETARE *) 442 >IH1 446 443 | -label #label whd in ⊢ (??(????%?)?) 447 444
Note: See TracChangeset
for help on using the changeset viewer.