Changeset 863


Ignore:
Timestamp:
May 31, 2011, 2:56:16 AM (8 years ago)
Author:
sacerdot
Message:

Yet another fix to the statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r862 r863  
    451451      let pre' ≝ 〈preamble,pre〉 in
    452452      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 ∧
    454455       ∀id. occurs_exactly_once id pre →
    455456        lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id))
     
    478479   let 〈pc, costs〉 ≝ pc_costs in
    479480    〈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 ⊢ (??(????%?)?)
    490493     
    491     ]
     494       ]]
    492495 | (* dummy case *)
    493  | whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
     496 | whd % // #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
    494497qed.
    495498
Note: See TracChangeset for help on using the changeset viewer.