Changeset 1571 for src/ASM/CostsProof.ma
 Timestamp:
 Nov 28, 2011, 1:39:49 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1570 r1571 248 248 qed. 249 249 250 axiomcurrent_instruction_cost_non_zero:250 lemma current_instruction_cost_non_zero: 251 251 ∀s: Status. 252 current_instruction_cost s > 0. 252 0 ≤ current_instruction_cost s. 253 // 254 qed. 255 256 lemma le_monotonic_plus: 257 ∀m, n, o: nat. 258 m ≤ n → m + o ≤ n + o. 259 #m #n #o #hyp 260 elim o 261 [ // 262  #o' #ind_hyp 263 <plus_n_Sm <plus_n_Sm 264 @le_S_S 265 assumption 266 ] 267 qed. 268 269 lemma le_plus_to_minus_l: 270 ∀m, n, o: nat. 271 n ≤ o → m ≤ o  n → m + n ≤ o. 272 #m #n #o #le_hyp #hyp 273 generalize in match (le_monotonic_plus m (o  n) n hyp); 274 generalize in match (plus_minus_m_m o n le_hyp); 275 #assm <assm in ⊢ (% → ?); #finished assumption 276 qed. 253 277 254 axiom minus_m_n_gt_o_0_le_n_m:278 lemma minus_m_n_le_n_m: 255 279 ∀m, n, o. 256 m  n = o → o > 0 → n ≤ m. 280 m  n = o → o > 0 → n ≤ m. 281 #m #n #o #eq_hyp 282 cases o 283 [ #absrd normalize in absrd; @le 284 normalize in ⊢ (% → ?); 285 <eq_hyp in ⊢ (% → ?); 286 #lt_hyp 287 generalize in match (le_plus_to_minus_l 1 n m ? lt_hyp); 288 [1: /2/  289 qed. 290 257 291 258 292 let rec compute_max_trace_label_label_cost_is_ok
Note: See TracChangeset
for help on using the changeset viewer.