Changeset 3551


Ignore:
Timestamp:
Apr 9, 2015, 4:44:52 PM (5 years ago)
Author:
piccolo
Message:

closed all daeomns

File:
1 edited

Legend:

Unmodified
Added
Removed

  • LTS/Lang_meas.ma

    r3550 r3551  
    351351∀prf :execute_l p p' (env … prog) l s1 s2.
    352352state_rel … m keep abs_top abs_tail s1 s1' →
     353(is_call_act … l → bool_to_Prop (is_call_post_label … (operational_semantics … p' prog) … s1)) →
    353354∃abs_top'.∃s2'.
    354355execute_l p p' (env … t_prog) l s1' s2' ∧
    … …  
    395396          ]
    396397          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct
    397     %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} %
     398    #_ %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} %
    398399    [% [ @(empty … EQcode_s1' EQcont_s1') // #_ %{lbl'} %]
    399400       whd >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta % // % // % // % // >EQclean %]
    … …  
    429430  inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #genlab #cleaned #EQcleaned
    430431  cases opt_l' in EQcode_s1'; normalize nodelta [|#lbl'] #EQcode_s1' [| inversion(?==?) normalize nodelta #EQget]
    431   whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQst #EQioinfo #EQ destruct
     432  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQst #EQioinfo #EQ destruct #_
    432433  %{genlab} %{(mk_state … i' (cont … s1') (store … s2) false)} % [ %
    433434  [ @(seq_sil … EQcode_s1') // ]
    434435  whd <EQcont >EQcheck normalize nodelta % // % // % // % // >EQcleaned %]
    435436  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >(\P EQget) >append_nil %
    436 | cases daemon
    437 | cases daemon
    438 | cases daemon
    439 | cases daemon
     437| #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct
     438  #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *]
     439  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
     440  [1,2,3,5,6,7:
     441    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
     442       | #lin #io #lout #instr #_ ]
     443          #_ whd in ⊢ (??%% → ?);
     444          [ |
     445          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     446          | cases(call_post_clean ?????) normalize nodelta
     447            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     448               [| #y cases(?∧?) normalize nodelta
     449               ]
     450            ]
     451          | cases(call_post_clean ?????) normalize nodelta
     452             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     453                [ cases (?==?) normalize nodelta ]
     454             ]]
     455          | cases(call_post_clean ?????) normalize nodelta
     456             [| #x cases(? ∧ ?) normalize nodelta ]
     457          ]
     458          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     459  ]
     460  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     461  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
     462  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
     463  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
     464  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
     465  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_
     466  %{a_top3} %{(mk_state … i_true' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} %
     467  [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] %
     468  [ @(cond_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
     469  change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
     470  >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_true' %
     471| #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct
     472  #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *]
     473  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
     474  [1,2,3,5,6,7:
     475    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
     476       | #lin #io #lout #instr #_ ]
     477          #_ whd in ⊢ (??%% → ?);
     478          [ |
     479          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     480          | cases(call_post_clean ?????) normalize nodelta
     481            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     482               [| #y cases(?∧?) normalize nodelta
     483               ]
     484            ]
     485          | cases(call_post_clean ?????) normalize nodelta
     486             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     487                [ cases (?==?) normalize nodelta ]
     488             ]]
     489          | cases(call_post_clean ?????) normalize nodelta
     490             [| #x cases(? ∧ ?) normalize nodelta ]
     491          ]
     492          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     493  ]
     494  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     495  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
     496  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
     497  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
     498  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
     499  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_
     500  %{a_top2} %{(mk_state … i_false' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} %
     501  [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] %
     502  [ @(cond_false … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
     503  change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
     504  >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_false' %
     505| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
     506  #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
     507  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
     508  [1,2,3,4,6,7:
     509    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
     510       | #lin #io #lout #instr #_ ]
     511          #_ whd in ⊢ (??%% → ?);
     512          [ |
     513          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     514          | cases(call_post_clean ?????); normalize nodelta
     515            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     516               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     517                 [| #z cases(?∧?) normalize nodelta
     518                 ]
     519               ]
     520            ]
     521          | cases(call_post_clean ?????) normalize nodelta
     522             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     523                [ cases (?==?) normalize nodelta ]
     524             ]]
     525          | cases(call_post_clean ?????) normalize nodelta
     526             [| #x cases(? ∧ ?) normalize nodelta ]
     527          ]
     528          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     529   ]
     530   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     531   inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false''
     532   #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true''
     533   #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct]
     534   inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     535   #EQstore #EQio #EQ destruct #_ %{a_top2}
     536   %{(mk_state … i_true' (〈cost_act … (None ?),LOOP … exp ltrue i_true' lfalse i_false'〉::(cont … s1')) (store … s2) false)}
     537   % [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] %
     538    [ @(loop_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
     539    change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
     540    whd in match (call_post_clean ??????); >EQi_false' normalize nodelta >EQi_true'
     541    >m_return_bind >(\P EQget1) >(\P EQget2) >(\b (refl …)) >(\b (refl …)) normalize nodelta
     542    % // % // % // % [ % // % //] >EQi_true' %
     543| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
     544  #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
     545  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
     546  [1,2,3,4,6,7:
     547    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
     548       | #lin #io #lout #instr #_ ]
     549          #_ whd in ⊢ (??%% → ?);
     550          [ |
     551          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     552          | cases(call_post_clean ?????); normalize nodelta
     553            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     554               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     555                 [| #z cases(?∧?) normalize nodelta
     556                 ]
     557               ]
     558            ]
     559          | cases(call_post_clean ?????) normalize nodelta
     560             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     561                [ cases (?==?) normalize nodelta ]
     562             ]]
     563          | cases(call_post_clean ?????) normalize nodelta
     564             [| #x cases(? ∧ ?) normalize nodelta ]
     565          ]
     566          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     567   ]
     568   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     569   inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false''
     570   #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true''
     571   #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct]
     572   inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     573   #EQstore #EQio #EQ destruct #_ %{a_top1}
     574   %{(mk_state … i_false' (cont … s1') (store … s2) false)}
     575   % [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] %
     576    [ @(loop_false … EQcode_s1') // ] >EQcont_s2 >EQcheck normalize nodelta
     577    % // % // % // % // >EQi_false' %
    440578| #s1 #s2 #lin #io #lout #i #store #EQcode_s1 #EQeval #EQcode_s2 #EQcont_s2. #EQ destruct #EQio_s2 *
    441579  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta [#_ *]
    … …  
    466604  #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct]
    467605  * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
    468   #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct %{[]}
     606  #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct #_ %{[]}
    469607  %{(mk_state … (EMPTY …) (〈cost_act p (Some ? lout),i'〉::(cont … s1')) (store … s2) true)} % [%
    470608  [ @(io_in … EQcode_s1') // ]
    … …  
    475613  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >append_nil >append_nil inversion(? == ?) in EQget';
    476614  [2: #_ *] #EQget' #_ >(\P EQget') %
    477 |*: cases daemon
    478 ]
     615| #s1 #s2 #f #act_p #r_lb #i #mem #env_it #EQcode_s1 #EQlook #EQeval #EQ destruct #EQcode_s2 #EQcont_s2
     616  #Hio1 #Hio2 * whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
     617  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
     618   [1,2,3,4,5,7:
     619    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     620        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_  ]
     621          #_ whd in ⊢ (??%% → ?);
     622          [ |
     623          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     624          | cases(call_post_clean ?????); normalize nodelta
     625            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     626               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     627                 [| #z cases(?∧?) normalize nodelta
     628                 ]
     629               ]
     630            ]
     631          | cases(call_post_clean ?????) normalize nodelta
     632            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     633               [| #y cases(?∧?) normalize nodelta
     634               ]
     635            ]
     636         | cases(call_post_clean ?????) normalize nodelta
     637             [| #x cases(? ∧ ?) normalize nodelta ]
     638         ]
     639         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     640     ]
     641     #f' #act_p' #r_lb #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean …) normalize nodelta
     642     [ #_ #EQ destruct] * #a_top1 #i'' #EQi' inversion(r_lb) normalize nodelta [ #_ #EQ destruct] #lbl #EQ
     643     destruct inversion(? ∈ ?) normalize nodelta #EQmem [ inversion(?==?) normalize nodelta #EQget]
     644     whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct
     645     lapply(trans_env_ok … no_dup) >EQt_prog normalize nodelta #H cases(H … EQlook) -H #env_it' * #n
     646     ** #Hfresh #EQlook' ***** #EQt_code #EQget1 #EQsig #EQlab #same_fresh #same_keep whd in match (is_call_post_label ???);
     647     >EQcode_s1 normalize nodelta [ #_ | * %{f} %{(f_lab … env_it)} %]
     648     %{(gen_labels … (call_post_trans … (f_body … env_it) n []))}
     649     %{(mk_state … (f_body … env_it') (〈ret_act … (Some … lbl),i'〉 :: (cont … s1')) (store … s2) false)}
     650     % [2,4: whd in ⊢ (??%%); >append_nil >EQlab >EQget1 % ] % [1,3: >EQlab @(call … EQcode_s1') //]
     651     >EQcont_s2 whd in match (check_continuations ??????);
     652     change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
     653     >EQi' normalize nodelta whd in match ret_costed_abs; normalize nodelta >EQmem normalize nodelta
     654     % // % // % // % [ % [ % // % //]  >(\P EQget) % ] <EQt_code @inverse_call_post_trans //
     655     [ >EQcode_s2 @no_duplicates_domain_of_fun //
     656     | >EQcode_s2 #H20 #H21 >same_fresh //
     657     | >EQcode_s2 #H23 #H24 >same_keep //
     658     ]
     659| #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode_s1 #EQcont_s1 #EQ destruct #Hio1 #Hio2 #EQeval #EQ1 #EQ2 destruct *
     660  whd in match state_rel; normalize nodelta >EQcont_s1 inversion(cont … s1') [| * #lab #i' #stack' #_ ] #EQcont_s1'
     661  whd in match (check_continuations ??????); [*] change with (check_continuations ??????) in match (foldr2 ???????);
     662  inversion(check_continuations ??????) normalize nodelta [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta
     663  inversion(call_post_clean …) normalize nodelta [ #_ *****] * #a_top1 #i'' #EQi' inversion lab normalize nodelta
     664  [ #f #lb ****** |3: * [| #x] #EQ destruct normalize nodelta ****** [|*] #EQ destruct] * [|#lb] #EQ destruct
     665  normalize nodelta [****** #EQ destruct] whd in match ret_costed_abs; normalize nodelta inversion(? ∈ ?) #EQmem
     666  normalize nodelta ****** [*] #EQ destruct #HH1 #EQ destruct #EQget >EQcode_s1 inversion(code … s1')
     667  [1,3,4,5,6,7:
     668       [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
     669        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_  ]
     670          #_ whd in ⊢ (??%% → ?);
     671          [
     672          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     673          | cases(call_post_clean ?????); normalize nodelta
     674            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     675               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     676                 [| #z cases(?∧?) normalize nodelta
     677                 ]
     678               ]
     679            ]
     680          | cases(call_post_clean ?????) normalize nodelta
     681            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     682               [| #y cases(?∧?) normalize nodelta
     683               ]
     684            ]
     685         | cases(call_post_clean ?????) normalize nodelta
     686             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     687                [ cases (?==?) normalize nodelta ]
     688             ]]
     689         | cases(call_post_clean ?????) normalize nodelta
     690             [| #x cases(? ∧ ?) normalize nodelta ]
     691         ]
     692         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     693   ] #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     694  #EQstore #EQio #EQ destruct #_
     695  %{a_top1} %{(mk_state … i' stack' (store … s2) false)} % [2: whd in ⊢ (??%%); >EQget >append_nil %]
     696  % [ @(ret_instr … EQcode_s1' … EQcont_s1') // ] >EQcheck normalize nodelta % // % // % // % // >EQi' %
     697] 
    479698qed.
    480699
    … …  
    501720#abs_top1 * #s0' * #t_i0' * #Rs0_s0' #sil_ti0'
    502721lapply(labelled_action_is_correct … p' prog no_dup) >EQt_prog normalize nodelta #Hmove
    503 cases(Hmove … prf1 … Rs0_s0') //
     722cases(Hmove … prf1 … Rs0_s0') // [2: @Hcall_init]
    504723#abs_top2 * #s1' ** #prf1' #Rs1_s1' #EQmap_l1
    505724lapply(correctness_lemma … p' prog no_dup) >EQt_prog normalize nodelta #H
    506725cases(H … pre_t12 … Rs1_s1') -H
    507726#abs_top3 * #s2' * #t12' ***** #Rs2_s2' #Hperm #_ #_ #pre_t12' #_
    508 cases(Hmove … prf2 … Rs2_s2') -Hmove //
     727cases(Hmove … prf2 … Rs2_s2') -Hmove // [2: @Hcall_fin]
    509728#abs_top4 * #s3' ** #prf2' #Rs3_s3' #EQmap_l2
    510729cases(Hsilent … sil_t3n … Rs3_s3')
Note: See TracChangeset for help on using the changeset viewer.