 Timestamp:
 Jun 16, 2011, 12:22:57 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r971 r972 1006 1006 qed. 1007 1007 1008 lemma 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 ?) %] 1015 qed. 1016 1008 1017 let rec occurs_exactly_once (id:Identifier) (l:list labelled_instruction) on l : bool ≝ 1009 1018 match l with … … 1054 1063 [ #H @ (IH H) 1055 1064  #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]]] 1058 1069 qed. 1059 1070
Note: See TracChangeset
for help on using the changeset viewer.