Ignore:
Timestamp:
Jun 16, 2011, 12:22:57 AM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r971 r972  
    10061006qed.
    10071007
     1008lemma does_not_occur_absurd:
     1009 ∀id,i,list_instr.
     1010  does_not_occur id (list_instr@[〈Some ? id,i〉]) = false.
     1011 #id #i #list_instr elim list_instr
     1012  [ normalize change with (if (if eq_bv ??? then ? else ?) then ? else ? = ?)
     1013    >eq_bv_refl %
     1014  | * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %]
     1015qed.
     1016
    10081017let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝
    10091018 match l with
     
    10541063     [ #H @ (IH H)
    10551064     | #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)
    1056        change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv 16 x id) normalize nodelta;
    1057        [ #H  | #H @IH @H]
     1065       change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;
     1066       [generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
     1067        /2/ #H >does_not_occur_Some //
     1068       | #H @IH @H]]]
    10581069qed.
    10591070
Note: See TracChangeset for help on using the changeset viewer.