Changeset 1596 for src/RTLabs/Traces.ma
 Timestamp:
 Dec 7, 2011, 4:24:42 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1595 r1596 243 243 ] qed. 244 244 245 (* 246 (* If we'll return then we must return from calls. *) 247 lemma will_return_call : ∀ge,depth,s,trace. 248 will_return ge (S depth) s trace → 249 will_return ge depth s trace. 250 #ge #depth #s #trace #H elim H in ⊢ ?; 251 [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/ 252  #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/ 253  #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/ 254  #H215 #H216 #H217 #H218 #H219 #H220 #H221 255 inversion H221 256 [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct 257  #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct 258  #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct 259  #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct 260 ] qed. check will_return_call. 261  #H130 #H131 #H132 #H133 #H134 #H135 262 inversion H 263 [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct 264 cases H196 #E destruct 265 266 267 let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace) 268 on H : will_return ge depth s trace ≝ 269 match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with 270 [ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ? 271  wr_call s tr s' d EX trace CL H' ⇒ λE. ? 272  wr_ret s tr s' d EX trace CL H' ⇒ λE. ? 273  wr_base s tr s' EX trace CL ⇒ λE. ? 274 ] (refl ? (S depth)). 275 [ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H') 276 @(will_return_call … H'') 277  *: cases daemon ] qed. 278  %2 /2/ 279  destruct cases d in H' ⊢ %; 280 [ #H' @wr_base // 281  #d' #H' %3 /2/ 282 ] 283  destruct 284 ] qed. 285 286 (* If we'll return then we must return from calls. *) 287 lemma will_return_call : ∀ge,depth,s,trace. 288 will_return ge (S depth) s trace → 289 will_return ge depth s trace. 290 #ge #depth #s #trace #H lapply (refl ? (S depth)) 291 generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %); 292 [ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/ 293  #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3 294 295 discriminator nat. 296 297 298 299 (* Find time until a nested call completes. *) 300 lemma nth_is_return_down : ∀ge,n,depth,s,trace. 301 nth_is_return ge n (S depth) s trace → 302 ∃m. nth_is_return ge m depth s trace. 303 #ge #n elim n 304 (* It's impossible to run out of time... *) 305 [ #depth #s #trace #H inversion H 306 [ #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct 307  #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct 308  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct 309  #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct 310 ] 311  #n' #IH #depth #s #trace #H inversion H 312 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 313 cases (IH depth s1' trace1 ?) 314 [ #m' #H' %{(S m')} %1 // 315  // 316 ] 317  #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 318 cases (IH (S depth) s1' trace1 ?) 319 [ #m' #H' %{(S m')} %2 // 320  // 321 ] 322  #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 323 cases (depth1) in H2 ⊢ %; 324 [ #H2 %{O} %4 // 325  #depth' #H2 cases (IH depth' s1' trace1 ?) 326 [ #m' #H' %{(S m')} %3 // 327  // 328 ] 329 ] 330  #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct 331 ] 332 ] qed. 333 334 lemma nth_is_return_call : ∀ge,n,s,tr,s',EX,trace. 335 RTLabs_classify s = cl_call → 336 nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → 337 ∃m. nth_is_return ge m O s' trace. 338 #ge #n #s #tr #s' #EX #trace #CLASS #H 339 inversion H 340 [ #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 * #H1 #H2 #_ #E1 #E2 #E3 @⊥ 341 H2 destruct >H1 in CLASS; #E destruct 342  #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 #E4 #E5 destruct 343 @nth_is_return_down // 344  #n1 #s1 #tr1 #s1' #depth1 #EX1 #trace1 #H1 #H2 #_ #E1 #E2 #E3 @⊥ 345 H2 destruct 346  #s1 #tr1 #s1' #EX1 #trace1 #E1 #E2 #E3 #E4 destruct @⊥ >E1 in CLASS; #E destruct 347 ] qed. 348 349 lemma nth_is_return_notfn : ∀ge,n,s,tr,s',EX,trace. 245 246 lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace. 350 247 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → 351 nth_is_return ge n O s (ft_step ?? ge s tr s' EX trace) → 352 nth_is_return ge (pred n) O s' trace. 353 #ge #n #s #tr #s' #EX #trace * #CL #TERM inversion TERM 354 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // 355  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct >H40 in CL; #E destruct 356  #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 destruct 357  #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 destruct >H70 in CL; #E destruct 358  #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 destruct // 359  #H93 #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct >H100 in CL; #E destruct 360  #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct 361  #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct 362 ] qed. 363 *) 364 365 lemma will_return_notfn : ∀ge,s,tr,s',EX,trace. 366 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → 367 will_return ge O s (ft_step ?? ge s tr s' EX trace) → 368 will_return ge O s' trace. 369 #ge #s #tr #s' #EX #trace * #CL #TERM inversion TERM 248 will_return ge d s (ft_step ?? ge s tr s' EX trace) → 249 will_return ge d s' trace. 250 #ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM 370 251 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct // 371 252  #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct 372  #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct 253  #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct >CL in H324; #E destruct 373 254  #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct 374 255  #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct // 375 256  #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct 376  #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct 257  #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct >CL in H377; #E destruct 377 258  #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct 378 259 ] qed. … … 522 403 (* Don't need to know that labels break loops because we have termination. *) 523 404 524 record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ { 405 (* A bit of mucking around with the depth to avoid proving termination after 406 termination. *) 407 record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) : Type[0] ≝ { 525 408 new_state : state; 526 409 remainder : flat_trace io_out io_in ge new_state; 527 410 cost_labelled : well_cost_labelled_state new_state; 528 new_trace : T new_state 411 new_trace : T new_state; 412 terminates : match depth with 413 [ O ⇒ True 414  S d ⇒ will_return ge d new_state remainder 415 ] 529 416 }. 530 417 531 record sub_trace_result (ge:genv) ( T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {418 record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ { 532 419 ends : trace_ends_with_ret; 533 trace_res :> trace_result ge (T ends); 534 terminates : 535 (* We handle returns specially *) 536 match ends with 537 [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res) 538  ends_with_ret ⇒ True 539 ] 420 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (T ends) 540 421 }. 541 422 542 definition replace_sub_trace : ∀ge, T1,T2.543 ∀r:sub_trace_result ge T1. T2 (ends … r) (new_state … r) →sub_trace_result geT2 ≝544 λge, T1,T2,r,trace.545 mk_sub_trace_result ge T2423 definition replace_sub_trace : ∀ge,trm,T1,T2. 424 ∀r:sub_trace_result ge trm T1. T2 (ends … r) (new_state … r) → sub_trace_result ge trm T2 ≝ 425 λge,trm,T1,T2,r,trace. 426 mk_sub_trace_result ge trm T2 546 427 (ends … r) 547 (mk_trace_result ge (T2 (ends … r))428 (mk_trace_result ge ? (T2 (ends … r)) 548 429 (new_state … r) 549 430 (remainder … r) 550 431 (cost_labelled … r) 551 432 trace 433 (terminates … r) 552 434 ) 553 (terminates … r)554 435 . 555 436 556 definition replace_trace : ∀ge, T1,T2.557 ∀r:trace_result ge T1. T2 (new_state … r) → trace_result geT2 ≝558 λge, T1,T2,r,trace.559 mk_trace_result ge T2437 definition replace_trace : ∀ge,trm,T1,T2. 438 ∀r:trace_result ge trm T1. T2 (new_state … r) → trace_result ge trm T2 ≝ 439 λge,trm,T1,T2,r,trace. 440 mk_trace_result ge trm T2 560 441 (new_state … r) 561 442 (remainder … r) 562 443 (cost_labelled … r) 563 444 trace 445 (terminates … r) 564 446 . 565 447 566 let rec make_label_return ge s448 let rec make_label_return ge depth s 567 449 (trace: flat_trace io_out io_in ge s) 568 450 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 569 451 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 570 452 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 571 (TERMINATES: will_return ge Os trace)572 : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝573 574 let r ≝ make_label_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in575 match ends … r return λx. trace_ label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?_⇒ ?]→ ? with576 [ ends_with_ret ⇒ λ tll,term.577 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)578  doesnt_end_with_ret ⇒ λ tll,term.579 let r' ≝ make_label_return ge (new_state … r)580 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? termin453 (TERMINATES: will_return ge depth s trace) 454 : trace_result ge depth (trace_label_return (RTLabs_status ge) s) ≝ 455 456 let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in 457 match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) → ? with 458 [ ends_with_ret ⇒ λr. 459 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) 460  doesnt_end_with_ret ⇒ λr. 461 let r' ≝ make_label_return ge depth (new_state … r) 462 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (terminates ??? r) in 581 463 replace_trace … r' 582 (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll(new_trace … r'))583 ] ( new_trace … r) (terminates … r)584 585 and make_label_label ge s464 (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r')) 465 ] (trace_res … r) 466 467 and make_label_label ge depth s 586 468 (trace: flat_trace io_out io_in ge s) 587 469 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 588 470 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 589 471 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 590 (TERMINATES: will_return ge Os trace)591 : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝592 let r ≝ make_any_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in593 replace_sub_trace ???r472 (TERMINATES: will_return ge depth s trace) 473 : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) ≝ 474 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in 475 replace_sub_trace … r 594 476 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) 595 477 596 and make_any_label ge s478 and make_any_label ge depth s 597 479 (trace: flat_trace io_out io_in ge s) 598 480 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 599 481 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 600 (TERMINATES: will_return ge Os trace)601 : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝602 match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with482 (TERMINATES: will_return ge depth s trace) 483 : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) ≝ 484 match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) with 603 485 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? 604 486  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES. … … 607 489 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 608 490 [ true ⇒ λCS. 609 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? 491 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) 492 doesnt_end_with_ret 493 (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?) 610 494  false ⇒ λCS. 611 let r ≝ make_any_label ge next trace' ENV_COSTLABELLED ?? in612 replace_sub_trace ???r495 let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? in 496 replace_sub_trace … r 613 497 (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??) 614 498 ] (refl ??) 615 499  cl_jump ⇒ λCL. 616 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ? 500 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) 501 doesnt_end_with_ret 502 (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?) 617 503  cl_call ⇒ λCL. 618 let r ≝ make_label_return ge next trace' ENV_COSTLABELLED ??? in619 let r' ≝ make_any_label ge (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in620 replace_sub_trace ??? r'504 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? in 505 let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in 506 replace_sub_trace ???? r' 621 507 (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r')) 622 508  cl_return ⇒ λCL. 623 mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ? 509 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) 510 ends_with_ret 511 (mk_trace_result ge ?? 512 next 513 trace' 514 ? 515 (tal_base_return (RTLabs_status ge) start next ? CL) 516 ?) 624 517 ] (refl ? (RTLabs_classify start)) 625 518  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ 626 519 ] STATE_COSTLABELLED TERMINATES. 627 520 628 [ @(trace_label_label_label … tll)521 [ @(trace_label_label_label … (new_trace … r)) 629 522  523  inversion TERMINATES 524 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 TERMINATES destruct >CL in H7; * #E destruct 525  #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 TERMINATES destruct >CL in H21; #E destruct 526  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 TERMINATES destruct @H36 527  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 whd @I 528 ] 630 529  %{tr} @EV 631 530  @(well_cost_labelled_state_step … EV) // 632  @I531  whd @(will_return_notfn … TERMINATES) %2 @CL 633 532  %{tr} @EV 634 533  % whd in ⊢ (% → ?); >CL #E destruct 635 534  @(well_cost_labelled_jump … EV) // 636 535  @(well_cost_labelled_state_step … EV) // 637  @(will_return_notfn … TERMINATES) %2 @CL638 536  (* oh dear *) 639 537  %{tr} @EV 640 538  @(cost_labelled … r) 641  642  643  644 645 @(well_cost_labelled_state_step … EV) // 539  @(terminates … r) 540  @(well_cost_labelled_state_step … EV) // 541  @(well_cost_labelled_call … EV) // 542  inversion TERMINATES 543 [ #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 TERMINATES destruct >CL in H60; * #E destruct 544  #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 TERMINATES destruct @H75 545  #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 TERMINATES destruct >CL in H88; #E destruct 546  #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 TERMINATES destruct >CL in H101; #E destruct 547 ] 548  whd @(will_return_notfn … TERMINATES) %1 @CL 549  %{tr} @EV 646 550  % whd in ⊢ (% → ?); >CL #E destruct 647 551  @CS 648  @( nth_is_return_notfn … TERMINATES) %1 @CL552  @(well_cost_labelled_state_step … EV) // 649 553  % whd in ⊢ (% → ?); >CS #E destruct 650 554  @CL 651 555  %{tr} @EV 652 556  @(well_cost_labelled_state_step … EV) // 653  @( nth_is_return_notfn … TERMINATES) %1 @CL557  @(will_return_notfn … TERMINATES) %1 @CL 654 558  inversion TERMINATES 655 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15TERMINATES destruct656  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31TERMINATES destruct657  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47TERMINATES destruct658  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11TERMINATES destruct559 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 TERMINATES destruct 560  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 TERMINATES destruct 561  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 TERMINATES destruct 562  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 TERMINATES destruct 659 563 ] 660 564 
Note: See TracChangeset
for help on using the changeset viewer.