 Timestamp:
 May 31, 2011, 2:56:16 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r862 r863 451 451 let pre' ≝ 〈preamble,pre〉 in 452 452 let 〈labels,pc_costs〉 ≝ res in 453 let 〈ignore,costs〉 ≝ pc_costs in 453 let 〈program_counter,costs〉 ≝ pc_costs in 454 tech_pc_sigma0 pre' = Some … program_counter ∧ 454 455 ∀id. occurs_exactly_once id pre → 455 456 lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id)) … … 478 479 let 〈pc, costs〉 ≝ pc_costs in 479 480 〈labels, costs〉. 480 [ whd cases construct in p3 #PC #CODE #JMEQ whd #id #Hid 481 generalize in match (sig2 … t) whd in ⊢ (% → ?) 482 >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1 483 whd in ⊢ (??(????%?)?) labels1; 484 cases label in Hid 485 [ #Hid whd in ⊢ (??(????%?)?) >IH1 IH1 486 [ >(address_of_word_labels_code_mem_None … Hid) 487 (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *) 488  whd in Hid >occurs_exactly_once_None in Hid // ] 489  label #label #Hid whd in ⊢ (??(????%?)?) 481 [ whd cases construct in p3 #PC #CODE #JMEQ whd % 482 [ 483  #id #Hid 484 generalize in match (sig2 … t) whd in ⊢ (% → ?) 485 >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) * #IH0 #IH1 486 whd in ⊢ (??(????%?)?) labels1; 487 cases label in Hid 488 [ #Hid whd in ⊢ (??(????%?)?) >IH1 IH1 489 [ >(address_of_word_labels_code_mem_None … Hid) 490 (* MANCA LEMMA: INDIRIZZO TROVATO NEL PROGRAMMA! *) 491  whd in Hid >occurs_exactly_once_None in Hid // ] 492  label #label #Hid whd in ⊢ (??(????%?)?) 490 493 491 ]494 ]] 492 495  (* dummy case *) 493  whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ]496  whd % // #pc normalize in ⊢ (% → ?) #abs @⊥ // ] 494 497 qed. 495 498
Note: See TracChangeset
for help on using the changeset viewer.