Changeset 1509
 Timestamp:
 Nov 15, 2011, 5:21:28 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1506 r1509 1 1 2 include "ASM/ASMCosts.ma". 2 3 include "ASM/WellLabeled.ma". … … 206 207 pred (m  n) = m  n  1. 207 208 #m #n 208 elimm209 cases m 209 210 [ #proof 210 211 cases(lt_to_not_zero … proof) 211  #m' # ind_hyp #proof212  #m' #proof 212 213 normalize in ⊢ (???%) 213 214 cases n 214 215 [ normalize // 215 216  #n' normalize 216 <ind_hyp 217 cases(m'  n') 218 [ % 219  #Sm_n' 220 normalize // 221 ] 222 ] 223 ] 224 qed. 225 226 lemma succ_m_plus_one: 227 ∀m: nat. 228 S m = m + 1. 229 #m 230 elim m 231 [ % 217 232  #m' #ind_hyp 233 normalize 234 <ind_hyp 235 % 236 ] 237 qed. 238 239 lemma minus_m_n_minus_minus_plus_1: 240 ∀m, n: nat. 241 ∀proof: n < m. 242 m  n = (m  n  1) + 1. 243 #m 244 elim m 245 [ #n #proof 246 cases(lt_to_not_zero … proof) 247  #m' #ind_hyp #n 218 248 normalize 219 249 cases n 220 250 [ normalize // 221  #n' normalize 251  #n' #proof normalize 252 <ind_hyp 253 [ % 254  @le_S_S_to_le 255 assumption 256 ] 257 ] 258 ] 259 qed. 222 260 223 261 lemma plus_minus_rearrangement: … … 228 266 #m #n #o 229 267 elim m 230 [1: #proof_n_m 268 [1: #proof_n_m 231 269 cases(lt_to_not_zero … proof_n_m) 232 270 2: #m' #ind_hyp … … 237 275 assumption 238 276 1: >eq_minus_S_pred 239 [2: /2/ 240 3: normalize 241 normalize in proof_n_m'; 242 elim(le_S … proof_n_m') 243 @le_S 244 1: 277 >pred_minus_1 278 [1: >(succ_m_plus_one (m'  n)) 279 >(associative_plus (m'  n) 1 (o  m'  1)) 280 <commutative_plus in match (1 + (o  m'  1)); 281 <(minus_m_n_minus_minus_plus_1 o m') in match (o  m'  1 + 1) 282 [1: >ind_hyp 283 [1: % 284 2: normalize 285 normalize in proof_m_o; 286 @le_S_S_to_le 287 @(le_S ? ? proof_m_o) 288 3: cases daemon (* XXX: problem here *) 289 ] 290 2: normalize in proof_m_o; 291 normalize 292 @le_S_S_to_le 293 @(le_S (S (S m')) o proof_m_o) 294 ] 295 2: normalize 296 normalize in proof_m_o; 297 @le_S_S_to_le 298 @(le_S (S (S m')) o proof_m_o) 245 299 ] 300 ] 301 ] 302 qed. 246 303 247 304 lemma status_execution_progresses_processor_clock:
Note: See TracChangeset
for help on using the changeset viewer.