Changeset 3506
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3504 r3506 361 361 sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O; 362 362 cambiare la definizione di traccia tornando a una sola etichetta sugli archi *) 363 363 364 (* 364 (* measurable fattorizzata sotto come measurable'365 definition measurable ≝366 λL,s1,s2.λt: raw_trace … s1 s2.367 ∃L',s0,so. as_execute … s0 s1 L ∧368 pre_measurable_trace … t ∧369 well_formed_trace … t ∧370 as_execute … s2 so L'. *)371 372 record measurable_trace (S : abstract_status) : Type[0] ≝373 { L_label: option ActionLabel374 ; R_label : option ActionLabel375 ; L_pre_state : option S376 ; L_s1 : S377 ; R_s2: S378 ; R_post_state : option S379 ; trace : raw_trace S L_s1 R_s2380 ; pre_meas : pre_measurable_trace … trace381 ; L_init_ok : match L_pre_state with382 [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = None ?383  Some s ⇒ ∃l. L_label = Some ? l ∧ is_costlabelled_act l ∧384 as_execute … l s L_s1385 ]386 ; R_fin_ok : match R_label with387 [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?388  Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧389 (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧390 ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'391 ]392 }.393 394 365 lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s. 395 366 #P #H1 #H2 * // @H2 % #EQ destruct qed. … … 474 445 ] 475 446 qed. 476 477 theorem simulate_LR_trace : 478 ∀S1,S2 : abstract_status. 479 ∀t : measurable_trace S1. 480 ∀rel : relations S1 S2. 481 simulation_conditions … rel → 482 ∀s2 : S2. 483 match L_pre_state … t with 484 [ None ⇒ 485 as_classify … s2 ≠ cl_io ∧ 486 Srel … rel (L_s1 … t) s2 487  Some s1 ⇒ Srel … rel s1 s2 ] → 488 ∃t' : measurable_trace S2. 489 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ 490 get_costlabels_of_trace … (trace … t) = 491 get_costlabels_of_trace … (trace … t') ∧ 492 match L_pre_state … t with 493 [ None ⇒ L_s1 … t' = s2 494  Some s1 ⇒ 495 ∃ pre_state : S2. 496 L_pre_state … t' = Some ? pre_state ∧ 497 ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i 498 ] ∧ 499 match R_post_state … t with 500 [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') 501  Some s1' ⇒ 502 ∃s2' : S2. Srel … rel s1' s2' ∧ 503 ∃ post_state : S2. 504 R_post_state … t' = Some ? post_state ∧ 505 ∃tr : raw_trace … post_state s2'. silent_trace … tr 506 ]. 507 #S1 #S2 #t #rel #good #s2 inversion(L_pre_state … t) [ #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ] 508 [2: #REL_pre 509 cut 510 (∃pre_state.∃ l. 511 ∃tr_i : raw_trace … s2 pre_state. silent_trace … tr_i ∧ 512 ∃middle_state.L_label … t = Some ? l ∧ 513 as_execute … l pre_state middle_state ∧ 514 ∃final_state. 515 ∃tr_i2: raw_trace … middle_state final_state. silent_trace … tr_i2 ∧ 516 as_classify … final_state ≠ cl_io ∧ 517 Srel … rel (L_s1 … t) final_state) 518 [ lapply(L_init_ok … t) >EQpre normalize nodelta * #l ** #EQllabe #Hcost #exe 519 cases(instr_execute_commute … good … l … exe … REL_pre) 520 [2: % #EQ >EQ in Hcost; * 3: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ] 521 #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall 522 #Hclass %{s2'} %{l} %{t1} %{sil_t1} %{s2''} % [% //] %{s2'''} %{t3} % // % // 523 cases sil_t3 [/2 by pre_silent_io/ ] inversion t3 524 [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ] 525 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125 526 #H @⊥ @H %] 527 * #pre_state * #l' * #tr_i * #silent_i * #middle_state ** #EQl' #step_pre_middle 528 * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL 529  #REL 530 cut(bool_to_Prop (as_initial … s2)∧L_label … t=None ?) 531 [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //] 532 @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label 533 ] 534 cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) // 535 #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t) 536 [2,4: #post_s2] #EQpost normalize nodelta 537 [3,4: cut (match R_label … t in option return λ_:(option ActionLabel).Prop with 538 [None⇒bool_to_Prop (as_final … fin_s2)∧None S2=None S2 539 Some (l:ActionLabel)⇒ 540 (is_costlabelled_act l∨is_unlabelled_ret_act l) 541 ∧(is_call_act l→is_call_post_label … fin_s2) 542 ∧(∃s'.None S2=Some … s'∧as_execute … l fin_s2 s')]) 543 [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta 544 [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption 545 *: #a ** #_ #_ * #x * >EQpost #EQ destruct 546 ] 547 ] #R_label_fin 548 *: cut(∃l.(R_label … t) = Some ? l) 549 [1,3: lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct] 550 #a #_ %{a} % ] * #final_label #EQfinal_label 551 cut 552 (∃middle_state. 553 ∃tr : raw_trace … fin_s2 middle_state. silent_trace … tr ∧ 554 ∃post_state. 555 as_execute … final_label middle_state post_state ∧ 556 (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧ 557 ∃final_state. 558 ∃tr_f2: raw_trace … post_state final_state. silent_trace … tr_f2 ∧ 559 Srel … rel post_s2 final_state) 560 [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin 561 * >EQpost #EQ destruct #exe 562 cases(instr_execute_commute … good … final_label … exe … REL') 563 [2,5: % #EQ destruct cases H1 [1,3,5,7: * *: normalize #EQ destruct] 564 3,6: %1 @tail_of_premeasurable_is_not_io // 565 ] 566 #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' 567 #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //] 568 % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe' 569 #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel 570 ] 571 [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)} 572 normalize nodelta /5 by conj/ 573 3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)} 574 normalize nodelta [2: %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' 575 #EQ destruct // 576 3: /3 by append_silent_premeasurable, append_premeasurable_silent/ 577 4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/] 578 >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] 579 >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%))); 580 /2 by refl, pair_destruct_1/ 581  lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_ 582 % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] // 583 ] 584  %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)} 585 normalize nodelta 586 [ assumption 587  %{l'} % // % // lapply(L_init_ok … t) >EQpre normalize nodelta * #l'' ** >EQl' #EQ destruct // 588  /4 by append_premeasurable_silent/ 589  % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append 590 >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/ 591 ] 592  %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)} 593 normalize nodelta 594 [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_ 595 % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] // 596  /2/ 597  /3 by append_silent_premeasurable/ 598  % [2: %{final_state'} /5 by ex_intro, conj/ 599  % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%)); 600 // ] 601 ] 602 ] 603 qed. 604 (* 605 xxxxxxxxxxxxxxxxxxxx 606 607 theorem simulate_LR_trace : 608 ∀S : abstract_status. 609 ∀t : measurable_trace S. 610 ∀rel : relations S. 611 simulation_conditions … rel → 612 ∀s2 : S. 613 match L_pre_state … t with 614 [ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → 615 ∃t' : measurable_trace S.L_s1 … t' = s2 ∧ 616 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ 617 get_costlabels_of_trace … (trace … t) = 618 get_costlabels_of_trace … (trace … t') ∧ 619 match R_post_state … t with 620 [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') 621  Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?). 622 ∃post_state : S. 623 ∃tr : raw_trace S (opt_safe … prf) post_state. 624 silent_trace … tr ∧ Srel … rel s2' post_state 625 ] 626  Some s1 ⇒ Srel … rel s1 s2 → 627 ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state. 628 silent_trace … tr_i ∧ 629 ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧ 630 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ 631 get_costlabels_of_trace … (trace … t) = 632 get_costlabels_of_trace … (trace … t') ∧ 633 match R_post_state … t with 634 [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') 635  Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?). 636 ∃post_state : S. 637 ∃tr : raw_trace S (opt_safe … prf) post_state. 638 silent_trace … tr ∧ Srel … rel s2' post_state 639 ] 640 ]. 641 #S #t #rel #good #s2 inversion(L_pre_state … t) [ #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ] 642 #REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta 643 [1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption] 644 #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL 645 [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)} 646 [ inversion(R_label … t) normalize nodelta 647 [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t) 648 >EQnone normalize nodelta * // 649  #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x * 650 >EQpost #EQ destruct 651 ] 652  normalize nodelta % 653 [ REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t) 654 >EQpre normalize nodelta * // 655  /6 by conj/ 656 ] 657  lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct] 658 #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 * 659 #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post)) 660 [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ] 661 * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) // 662 [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 * 663 ** #sil_t1 #exe' #Hx2 #REL1 664 %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)} 665 [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %] 666 @notb_Prop % #ABS @(as_final_ok … ABS exe') 667  normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ] 668 REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption 669  /3 by append_silent_premeasurable/ 670  % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] % 671 [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption 672 ] 673  (*go by cases on the instruction executed TODO *) cases daemon 674 ] 675 ] 676 *: cases daemon (*TODO*) 677 ] 678 qed. 679 680 681 682 683 #L_label * [ #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t 684 normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe *: #EQ destruct(EQ) ] 685 * [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) *: 686 687 688 whd in ⊢ (% → ?); 689 690 691 692 693 (*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se 694 non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio 695 il teorema sotto sembra suggerire il merge *) 696 697 definition unmovable_entry_label ≝ 698 λS : abstract_status.λl. 699 match l with 700 [ call_act _ _ ⇒ false 701  ret_act _ ⇒ false 702  cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c 703  None ⇒ false 704 ] 705 ]. 706 707 definition unmovable_exit_label ≝ 708 λS : abstract_status.λl. 709 match l with 710 [ call_act _ _ ⇒ false 711  ret_act _ ⇒ false 712  cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c 713  None ⇒ false 714 ] 715 ]. 716 717 theorem simulates_LR_raw_trace : 718 ∀S : abstract_status. 719 ∀t : LR_raw_trace S. 720 ∀rel : relations S. 721 simulation_conditions … rel → 722 measurable S t → 723 ∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' → 724 ∃ t' : LR_raw_trace S. 725 measurable S t' ∧ 726 if as_initial … (LR_s1 … t) ∨ unmovable_entry_label S (L_label … t) then 727 LR_s1 … t' = s1' 728 else 729 ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t') 730 ∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧ 731 if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then 732 LR_s2 … t' = s1'' 733 else 734 ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t') 735 ∧ 736 get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t'). 737 #S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL 738 cases(simulates_pre_mesurable … (LR_t … t) … REL) 739 [2: @good 3: @pre_t 4: @wf_t 5: @Hs1' ] 740 #s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1 741 inversion(as_initial … (LR_s1 … t)) #Has_initial 742 inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry 743 inversion(as_final … (LR_s2 … t)) #Has_final 744 inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit 745 normalize nodelta 746 [ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2: 747 748 749 750 qed. 751 752 xxxx 753 754 theorem simulates_L_raw_trace: 755 ∀t: L_raw_trace. 756 pre_measurable_trace … (L_t t1) → 757 well_formed_trace … (L_t t1) → 758 ∀s1'. 759 S (L_s1 t) s1' → 760 s1' flat→ (L_s1 t2) → 761 ∃s2',t2: L_raw_trace. 762 pre_mesurable_trace … (L_t t2) ∧ 763 well_formed_trace … (L_t t2) ∧ 764 t1 = t2 ∧ 765 S (L_s2 t1) s2' ∧ 766 (L_s2 t2) flat→ s2'. 767 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e 768 nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *) 769 770 771 (*********************************************************************) 772 773 (* quello che segue tentava di permettere di evitare l'emissione di label 774 associate a codice morto *) 775 776 replace_last x : weak_trace → weak_trace 777 [] ⇒ [], Some x 778  l::t ⇒ 779 let 〈t',x'〉 ≝ replace_last x t in 780 match x' with 781 [ None ⇒ l::t', None 782  Some x'' ⇒ [], Some x'' 783 784 theorem simulates: 785 ∀s1,s2. ∀τ1: raw_trace … s1 s2. 786 pre_measurable_trace … t1 → 787 well_formed_trace … t1. 788 ∀l1: option NonFunctionalLabel. 789 ∀s1'. 790 S s1 s1' → 791 ∃dead_labels. 792 ∃s2'. ∃t2: raw_trace … s1' s2'. 793 pre_mesurable_trace … t2 ∧ 794 well_formed_trace … t2. 795 ∃l2: option NonFunctionalLabel. 796 match l1 with 797 [ None ⇒ 798 match l2 with 799 [ None ⇒ t1 = t2 800  Some l2' ⇒ t1 = l2'::t2 ] 801  Some l1' ⇒ 802 match l2 with 803 [ None ⇒ t1 = replace_last l1' t2 ∧ ends_with l1' t1 804  Some l2' ⇒ 805 if t2 = [] then t1 = [l1'] ∧ l2' = l1' 806 else t1 = l2' :: replace_last l1' t2 ∧ ends_with l1' t1 807 ] 808 ] 809 *) 447 *) 
LTS/Traces.ma
r3487 r3506 418 418 ] 419 419 qed. 420 420 421 definition measurable : 422 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝ 423 λS,si,s1,s3,sn,t. 424 pre_measurable_trace … t ∧ 425 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn. 426 ∃l1,l2,prf1,prf2. 427 t = ti0 @ t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n)) 428 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n. 429 430 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S) 431 (t : raw_trace S st1 st2) on t : list CostLabel ≝ 432 match t with 433 [ t_base st ⇒ [ ] 434  t_ind st1' st2' st3' l prf t' ⇒ 435 let tl ≝ get_costlabels_of_trace … t' in 436 match l with 437 [ call_act f c ⇒ [ c ] 438  ret_act x ⇒ match x with 439 [ Some c ⇒ [ a_return_post c ] 440  None ⇒ [] 441 ] 442  cost_act x ⇒ match x with 443 [ Some c ⇒ [ a_non_functional_label c ] 444  None ⇒ [] 445 ] 446 ] @ tl 447 ]. 448 449 lemma get_cost_label_silent_is_empty : ∀S : abstract_status. 450 ∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ]. 451 #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ] 452 #H inversion H 453 [#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3 454 destruct #_ @IH % assumption 455 qed. 456 457 lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S. 458 ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3. 459 get_costlabels_of_trace … (t1 @ t2) = 460 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2). 461 #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' * 462 [#f * #l  * [ * #l]  * [ #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH 463 qed. 464 
LTS/Vm.ma
r3505 r3506 702 702 ] 703 703 qed. 704 705 include "Simulation.ma".706 704 707 705 definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ … … 1102 1100 qed. 1103 1101 1104 definition measurable :1105 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝1106 λS,si,s1,s3,sn,t.1107 pre_measurable_trace … t ∧1108 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.1109 ∃l1,l2,prf1,prf2.1110 t = ti0 @ t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))1111 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n.1112 1113 1102 lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs). 1114 1103 #A #x * [ #H cases(absurd ?? H) % ] // qed.
Note: See TracChangeset
for help on using the changeset viewer.