Changeset 2128 for src/ASM/ASM.ma
 Timestamp:
 Jun 27, 2012, 5:05:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r2124 r2128 244 244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN; 245 245 cases (is_a hd am) in ISIN; /2/ 246 qed. 247 248 lemma is_in_monotonic_wrt_append: 249 ∀m, n: nat. 250 ∀p: Vector addressing_mode_tag m. 251 ∀q: Vector addressing_mode_tag n. 252 ∀to_search: addressing_mode. 253 bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search). 254 #m #n #p #q #to_search #assm 255 elim q try assumption 256 #n' #hd #tl #inductive_hypothesis 257 normalize 258 cases (is_a ??) try @I 259 >inductive_hypothesis @I 260 qed. 261 262 corollary is_in_hd_tl: 263 ∀to_search: addressing_mode. 264 ∀hd: addressing_mode_tag. 265 ∀n: nat. 266 ∀v: Vector addressing_mode_tag n. 267 bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search). 268 #to_search #hd #n #v 269 elim v 270 [1: 271 #absurd 272 normalize in absurd; cases absurd 273 2: 274 #n' #hd' #tl #inductive_hypothesis #assm 275 >vector_cons_append >(vector_cons_append … hd' tl) 276 @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search) 277 assumption 278 ] 246 279 qed. 247 280
Note: See TracChangeset
for help on using the changeset viewer.