Changeset 2417


Ignore:
Timestamp:
Oct 25, 2012, 4:36:07 PM (9 years ago)
Author:
boender
Message:
  • reverted changes to StructuredTraces? (shouldn't have been committed yet)
  • updated _jaap files to remove function identifier from cl_call and add an as_call predicate
Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed

  • src/common/StructuredTraces.ma

    r2413 r2417  
    1010  | cl_return: status_class
    1111  | cl_jump: status_class
    12   | cl_call: ident → status_class
     12  | cl_call: status_class
    1313  | cl_other: status_class.
    1414
    … …  
    2121  ; as_classifier : as_status → status_class → Prop
    2222  ; as_label_of_pc : as_pc → option costlabel
    23   ; as_after_return : (Σs:as_status. ∃f.as_classifier s (cl_call f)) → as_status → Prop
     23  ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
    2424  ; as_final: as_status → Prop
    2525}.
    … …  
    9090      ∀status_final: S.
    9191        as_execute S status_pre_fun_call status_start_fun_call →
    92         ∀f.∀H:as_classifier S status_pre_fun_call (cl_call f).
    93           as_after_return S (mk_Sig ?? status_pre_fun_call (ex_intro ?? f H)) status_final →
     92        ∀H:as_classifier S status_pre_fun_call cl_call.
     93          as_after_return S «status_pre_fun_call, H» status_final →
    9494          trace_label_return S status_start_fun_call status_final →
    9595          as_costed S status_final →
    … …  
    103103      ∀status_final: S.
    104104        as_execute S status_pre_fun_call status_start_fun_call →
    105         ∀f.∀H:as_classifier S status_pre_fun_call (cl_call f).
    106           as_after_return S (mk_Sig ?? status_pre_fun_call (ex_intro ?? f H)) status_after_fun_call →
     105        ∀H:as_classifier S status_pre_fun_call cl_call.
     106          as_after_return S «status_pre_fun_call, H» status_after_fun_call →
    107107          trace_label_return S status_start_fun_call status_after_fun_call →
    108108          ¬ as_costed S status_after_fun_call →
    … …  
    123123  on tal : list (as_pc S) ≝
    124124 match tal with
    125  [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
     125 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
    126126 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
    127127 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
    128128 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
    129  | tal_base_call pre _ _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
     129 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
    130130 ].
    131131
    … …  
    155155and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
    156156  match tal with
    157   [ tal_step_call fl st1 st2 st3 st4 _ _ _ _ tlr _ tl ⇒
     157  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
    158158    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    159159    tal_unrepeating … tl ∧
    … …  
    162162    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
    163163    tal_unrepeating … tl
    164   | tal_base_call pre _ _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
     164  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
    165165  | _ ⇒ True
    166166  ].
    … …  
    182182cases tal //
    183183#fl' #st1' [#st_fun] #st2' #st3' #H
    184 [ #f #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
     184[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
    185185#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
    186186qed.
    … …  
    198198[ #s1 #s2 #EX #CL #CS
    199199| #s1 #s2 #EX #CL
    200 | #s1 #s2 #s3 #EX #f #CL #AF #tlr #CS
    201 | #fl #s1 #s2 #s3 #s4 #EX #f #CL #AF #tlr #CS #tal
     200| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
     201| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
    202202| #fl #s1 #s2 #s3 #EX #tal #CL #CS
    203203] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
    … …  
    210210[ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
    211211| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
    212 | #pre #start #final #EX #f #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
    213 | #fl' #pre #start #after #final #EX #f #CL #AF #tlr #CS #tal' #CS'
     212| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
     213| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
    214214  cases (tal_pc_list_start … tal')
    215215  #hd #E >E
    … …  
    225225  | tac_base:
    226226      ∀status: S.
    227         (∃f.as_classifier S status (cl_call f)) →
     227        as_classifier S status cl_call →
    228228          trace_any_call S status status
    229229  | tac_step_call:
    … …  
    233233      ∀status_start_fun_call: S.
    234234        as_execute S status_pre_fun_call status_start_fun_call →
    235         ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
     235        ∀H:as_classifier S status_pre_fun_call cl_call.
    236236          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
    237237          trace_label_return S status_start_fun_call status_after_fun_call →
    … …  
    278278        trace_label_call S status_initial status_pre_fun_call →
    279279        as_execute S status_pre_fun_call status_start_fun_call →
    280         ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
     280        ∀H:as_classifier S status_pre_fun_call cl_call.
    281281          trace_label_diverges S status_start_fun_call →
    282282            trace_label_diverges S status_initial.
    … …  
    303303        trace_label_call S status_initial status_pre_fun_call →
    304304        as_execute S status_pre_fun_call status_start_fun_call →
    305         ∀H:∃f.as_classifier S status_pre_fun_call (cl_call f).
     305        ∀H:as_classifier S status_pre_fun_call cl_call.
    306306          trace_label_diverges_exists S status_start_fun_call →
    307307            trace_label_diverges_exists S status_initial.
    … …  
    312312      ∀status_start_fun: S.
    313313      ∀status_final: S.
    314         (∃f.as_classifier S status_initial (cl_call f)) →
     314        as_classifier S status_initial cl_call →
    315315        as_execute S status_initial status_start_fun →
    316316        trace_label_return S status_start_fun status_final →
    … …  
    320320      ∀status_initial: S.
    321321      ∀status_start_fun: S.
    322         (∃f.as_classifier S status_initial (cl_call f)) →
     322        as_classifier S status_initial cl_call →
    323323        as_execute S status_initial status_start_fun →
    324324        trace_label_diverges S status_start_fun →
    … …  
    331331      ∀status_start_fun: S.
    332332      ∀status_final: S.
    333         (∃f.as_classifier S status_initial (cl_call f)) →
     333        as_classifier S status_initial cl_call →
    334334        as_execute S status_initial status_start_fun →
    335335        trace_label_return S status_start_fun status_final →
    … …  
    339339      ∀status_initial: S.
    340340      ∀status_start_fun: S.
    341         (∃f.as_classifier S status_initial (cl_call f)) →
     341        as_classifier S status_initial cl_call →
    342342        as_execute S status_initial status_start_fun →
    343343        trace_label_diverges_exists S status_start_fun →
    … …  
    350350[ tal_base_not_return start final _ _ C ⇒ C
    351351| tal_base_return _ _  _ _ ⇒ I
    352 | tal_base_call _ _ _ _ _ _ _ _ C ⇒ C
    353 | tal_step_call f pre start after final X f C RET LR C' tr' ⇒ trace_any_label_label … tr'
     352| tal_base_call _ _ _ _ _ _ _ C ⇒ C
     353| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
    354354| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
    355355].
    … …  
    371371
    372372lemma trace_any_call_call : ∀S,s,s'.
    373   trace_any_call S s s' → ∃f.as_classifier S s' (cl_call f).
     373  trace_any_call S s s' → as_classifier S s' cl_call.
    374374#S #s #s' #T elim T [1,3: //]
    375375#H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 //
    … …  
    517517    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
    518518      (tal_base_return ? st2mid st2' H G)
    519   | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒
     519  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
    520520    fl2 = doesnt_end_with_ret ∧
    521521    ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
    … …  
    524524      we cannot use trace_any_any as it disallows labels in the end as soon
    525525      as it is non-empty) *)
    526     (∃f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
    527       tal2 ≃ taa @ (tal_base_call … H f G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
    528     ∃st2mid'',f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     526    (∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     527      tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
     528    ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
    529529    ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
    530       tal2 ≃ taa @ (tal_step_call … H f G K tlr2 L tl2) ∧
     530      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    531531      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
    532   | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒
     532  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
    533533    ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
    534     (fl2 = doesnt_end_with_ret ∧ ∃f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
    535       tal2 ≃ taa @ tal_base_call … H f G K tlr2 L ∧
     534    (fl2 = doesnt_end_with_ret ∧ ∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
     535      tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
    536536      tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
    537     ∃st2mid'',f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
     537    ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
    538538    ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
    539       tal2 ≃ taa @ (tal_step_call … H f G K tlr2 L tl2) ∧
     539      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
    540540      tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
    541541  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
    … …  
    552552cases tal1 -fl1 -s1 -s1' //
    553553[ #s1 #s1' #H #I *
    554 | #s1 #s1' #s1'' #s1''' #s1'''' #H #f #I #J #tlr #K #tl *
     554| #s1 #s1' #s1'' #s1''' #s1'''' #H #I #J #tlr #K #tl *
    555555| #fl1 #s1 #s1' #s1'' #H #tl #I #J @(tal_collapsable_eq_fl … tl)
    556556]
    … …  
    563563  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
    564564  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    565   | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
    566   | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
     565  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     566  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    567567  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    568568  ].
    … …  
    570570[1,2,3: -tal_rel_eq_fl #tal2 * //
    571571| #tal2 * #s2_mid * #taa2 * #s2' *#H2 *
    572   [ * #EQ1 *#f *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
    573   | * #s2_mid' *#f *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
     572  [ * #EQ1 *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
     573  | * #s2_mid' *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
    574574     @(tal_rel_eq_fl … step)
    575575  ]
    … …  
    603603  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
    604604  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
    605   | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
    606   | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
     605  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
     606  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
    607607  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
    608608  ].
    … …  
    637637  match the_trace with
    638638  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    639   | tal_base_call pre_fun_call start_fun_call final _ _ _ _ call_trace _ ⇒
     639  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    640640      flatten_trace_label_return … call_trace
    641641  | tal_base_return the_status _ _ _ ⇒ [ ]
    642642  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    643     _ _ _ _ call_trace _ final_trace ⇒
     643    _ _ _ call_trace _ final_trace ⇒
    644644    let call_cost_trace ≝ flatten_trace_label_return … call_trace in
    645645    let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
    … …  
    730730  [ tal_base_not_return st1 st1' H G K ⇒ ?
    731731  | tal_base_return st1 st1' H G ⇒ ?
    732   | tal_base_call st1 st1' st1'' H f G K tlr1 L ⇒ ?
    733   | tal_step_call fl1 st1 st1' st1'' st1''' H f G K tlr1 L tl1 ⇒ ?
     732  | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
     733  | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
    734734  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
    735735  ]
    … …  
    760760    [ *#H' *#G' *#K' #EQ
    761761    | *#H' *#G' #EQ
    762     | *#st_mid' *#H' * [|*#st2_mid''] *#f' *#G' *#K' *#tlr2 *#L'
     762    | *#st_mid' *#H' * [|*#st2_mid''] *#G' *#K' *#tlr2 *#L'
    763763      [|*#tl2 *] * #EQ #H_tlr [| #H_tl]
    764764    | *#st_fun *#H' *
    765       [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#f' *#G' *#K' *#tlr2 *#L'
     765      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#G' *#K' *#tlr2 *#L'
    766766      [| *#tl2] ** #EQ #H_tl #H_tlr
    767767    ] >EQ >taa_append_tal_same_flatten

  • src/joint/Joint_jaap.ma

    r2398 r2417  
    175175  [ step_seq s ⇒
    176176    match s with
    177     [ CALL_ID l _ _ ⇒    cl_call l
    178     | extension_call _ ⇒ cl_call ? (* pointer stuff not yet implemented, it seems *)
     177    [ CALL_ID _ _ _ ⇒    cl_call
     178    | extension_call _ ⇒ cl_call
    179179    | _ ⇒ cl_other
    180180    ]
    181181  | COND _ _ ⇒ cl_jump
    182182  ].
    183  cases daemon
    184 qed.
    185183
    186184record stmt_params : Type[1] ≝

  • src/joint/stacksize.ma

    r2398 r2417  
    4747  [ tal_base_not_return s1 s2 ex cl co ⇒ res
    4848  | tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res
    49   | tal_base_call s1p s1s s2 ex f cl ar tlr co ⇒
     49  | tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒
    5050    extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res)
    51   | tal_step_call end s1p s1s s1a s2 ex f cl ar tlr co tal ⇒
     51  | tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒
    5252    let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in
    5353    extract_list_from_tal … lg top_f … tal res'
    … …  
    8181  ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res =
    8282  extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝
     83  match t1 with
     84  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
     85  | tal_base_return st1 st1' ex cl ⇒ ?
     86  | tal_base_call st1p st1s st1' ex cl f ca ar tlr1 co ⇒ ?
     87  | tal_step_call end st1p st1s st1 st1' ex cl f ca ar tlr1 co tal1 ⇒ ?
     88  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
     89  ].
     90[ cases t2
     91  [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
     92  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
     93  ]
     94| cases t2
     95  [ #st2 #st2' #tll2 normalize #abs cases abs
     96  | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
     97    >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
     98    @(tlr_rel_extract_equal … (proj2 ?? Hsim))
     99  ]
     100| cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
     101  @(tal_rel_extract_equal … H2)
     102| cases t2
     103  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
     104  | #st2 #st2' #ex' #cl' * #abs destruct (abs)
     105  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
     106    #taa * #H * #G * #K inversion taa in ⊢ ?;
     107    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     108    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     109      normalize #abs destruct (abs)
     110    ]
     111  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 normalize *
     112    #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
     113    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     114    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     115      normalize #abs destruct (abs)
     116    ]
     117  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
     118    * #H * #G * #K inversion taa in ⊢ ?;
     119    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     120    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     121      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
     122    ]
     123  ]
     124| cases t2
     125  [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
     126  | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
     127  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #abs destruct (abs)
     128  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
     129    normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
     130    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     131    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     132      normalize #abs destruct (abs)
     133    ]
     134  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
     135    * #taa * #H * #G inversion taa in ⊢ ?;
     136    [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
     137    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     138      destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 
     139    ]
     140  ]
     141| cases t2
     142  [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa
     143    * #st2mid' * #H * * [2: #st2mid'' *] #J * #f' * #G * #K * #tlr2 * #L * #H1
     144    [ * * #H3 #H2 #H4 | #H2 ]
     145    inversion taa in ⊢ ?;
     146    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3)
     147    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     148      normalize in H3; destruct (H3)
     149    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
     150    | #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     151      normalize in H1; destruct (H1)
     152    ]
     153  | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
     154  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #_ * #st2mid *
     155    #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f'' * #G * #K * #tlr2' * #L
     156    inversion taa in ⊢ ?;
     157    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #tal2 * * #H1 destruct (H1)
     158    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     159      destruct normalize * #tal2 * * #H1 destruct (H1)
     160    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
     161      >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
     162    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     163      destruct normalize * #abs destruct (abs)
     164    ]
     165  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
     166    normalize * #H1 * #st2mid * #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f
     167    * #G * #K * #tlr2' * #L
     168    inversion taa in ⊢ ?;
     169    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 #H2 #H3 #res
     170      cases daemon
     171    | #st2p' #st2p'' #st2mid'; #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     172      destruct normalize * #tal2' * * #H1 destruct (H1)
     173    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
     174    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     175      destruct normalize * #abs destruct (abs)
     176    ]
     177  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
     178    #taa * #st2mid' * #H * * [2: #stmid'' * ] #J * #f * #G * #K * #tlr2 * #L
     179    inversion taa in ⊢ ?;
     180    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 destruct (H1)
     181    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     182      destruct normalize * #tal2' * * #H1 #H2 #H3 #res cases daemon
     183    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
     184    | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     185      destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *)
     186    ]
     187  ]
     188| cases t2
     189  [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun *
     190    #st2_after_fun * * [#H | #st2mid'] * #J * #f' * #G * #K * #tlr2 * #L [2: * #tl2]
     191    inversion taa in ⊢ ?;
     192    [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1)
     193    | #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     194      normalize * * #H1 destruct (H1)
     195    | #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
     196    | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     197      normalize * * #abs destruct (abs)
     198    ]
     199  | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2mid' * #H *
     200    [ * #abs destruct (abs) | * #st2mid'' * #J * #f' * #G * #K * #tlr2 * #L * #tl2
     201      inversion taa in ⊢ ?;
     202      [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
     203      | #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
     204        normalize * * #abs destruct (abs)
     205      ]
     206    ]
     207  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #st2mid * #taa
     208    * #st2mid' * #H * * [ #_ | #st2mid'' ] * #J * #f'' * #G * #K * #tlr2' * #L [2: * #tl2]
     209    inversion taa in ⊢ ?;
     210    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
     211    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     212      destruct normalize * * #abs destruct (abs)
     213    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 cases daemon
     214    | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     215      destruct normalize * * #abs destruct (abs)
     216    ]
     217  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
     218    normalize * #st2mid * #taa * #st2mid' * #ex'' * * [ #_ | #st2mid''] * #J *
     219    #f'' * #G * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?;
     220    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
     221      cases daemon (* injectivity needed again *)
     222    | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     223      destruct normalize * * #abs destruct (abs)
     224    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) cases daemon
     225      (* huh? *)
     226    | #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     227      destruct normalize * * #abs destruct (abs) cases daemon (* huh2? *)
     228    ]
     229  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
     230    #st2mid' * #H * * [ #He | #st2mid'' ] * #J * #f' * #G * #K * #tlr2' * #L
     231    [2: * #tl2] inversion taa in ⊢ ?;
     232    [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
     233    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     234      destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)
     235    | #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
     236    | #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
     237      destruct normalize * * #H1 #H2 #H3 #res cases daemon
     238    ]
     239  ]
     240| cases t2
     241  [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
     242    @(tal_rel_extract_equal p g lg top_f … Hsim)
     243  | #ss #fs #ex' #cl' normalize #Hsim #res
     244    @(tal_rel_extract_equal p g lg top_f … Hsim)
     245  | #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize #Hsim #res
     246    @(tal_rel_extract_equal p g lg top_f … Hsim)
     247  | #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2
     248    normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
     249  | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
     250    @(tal_rel_extract_equal p g lg top_f … Hsim)
     251  ]
     252]
     253qed.
     254
     255(* let rec tlr_rel_max_equal (p: params) (g: list ident)
     256  (lg: ident → joint_internal_function p g) (top_f: ident)
     257  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
     258  tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
     259  max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
     260  max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
     261  match t1 with
     262  [ tlr_base st1 st1' tll1 ⇒ ?
     263  | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
     264  ]
     265and tll_rel_extract_equal (p: params) (g: list ident)
     266  (lg: ident → joint_internal_function p g) (top_f: ident)
     267  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
     268  t1 ≈ t2 →
     269  max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
     270  max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
     271  match t1 with
     272  [ tll_base ends st1 st1' tal1 co ⇒ ?
     273  ]
     274and tal_rel_extract_equal (p: params) (g: list ident)
     275  (lg: ident → joint_internal_function p g) (top_f: ident)
     276  S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
     277  t1 ≈ t2 →
     278  max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
     279  max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
    83280  match t1 with
    84281  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    … …  
    88285  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    89286  ].
    90 [ cases t2
    91   [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)
    92   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs
    93   ]
    94 | cases t2
    95   [ #st2 #st2' #tll2 normalize #abs cases abs
    96   | #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res
    97     >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)
    98     @(tlr_rel_extract_equal … (proj2 ?? Hsim))
    99   ]
    100 | cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2
    101   @(tal_rel_extract_equal … H2)
    102 | cases t2
    103   [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %
    104   | #st2 #st2' #ex' #cl' * #abs destruct (abs)
    105   | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *
    106     #taa * #H * #G * #K inversion taa in ⊢ ?;
    107     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    108     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    109       normalize #abs destruct (abs)
    110     ]
    111   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 normalize *
    112     #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;
    113     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    114     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    115       normalize #abs destruct (abs)
    116     ]
    117   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa
    118     * #H * #G * #K inversion taa in ⊢ ?;
    119     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    120     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    121       destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)
    122     ]
    123   ]
    124 | cases t2
    125   [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)
    126   | #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %
    127   | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)
    128   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    129     normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;
    130     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    131     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    132       normalize #abs destruct (abs)
    133     ]
    134   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid
    135     * #taa * #H * #G inversion taa in ⊢ ?;
    136     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)
    137     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    138       destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 
    139     ]
    140   ]
    141 | cases t2
    142   [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa
    143     * #st2mid' * #H * #f' * #G * #K * #tlr2 * #L * #H1 #H2 inversion taa in ⊢ ?;
    144     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)
    145     | #st2'' #st2''' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    146       normalize in H1; destruct (H1)
    147     ]
    148   | #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)
    149   | #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid *
    150     #taa * #st2mid' * #H * #f'' * #G * #K * #tlr2' * #L inversion taa in ⊢ ?;
    151     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res
    152       >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)
    153     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    154       destruct normalize * #abs destruct (abs)
    155     ]
    156   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    157     normalize * #H1 * #st2mid * #taa * #st2mid' * #H * #f * #G * #K * #tlr2' * #L
    158     inversion taa in ⊢ ?;
    159     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    160     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    161       destruct normalize * #abs destruct (abs)
    162     ]
    163   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *
    164     #taa * #st2mid' * #H * #f * #G * #K * #tlr2 * #L inversion taa in ⊢ ?;
    165     [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)
    166     | #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    167       destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *)
    168     ]
    169   ]
    170 | cases t2
    171   [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
    172     * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
    173     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    174     | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    175       normalize * * #abs destruct (abs)
    176     ]
    177   | #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun
    178     * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;
    179     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    180     | #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct
    181       normalize * * #abs destruct (abs)
    182     ]
    183   | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize * #st2mid * #taa
    184     * #st2_fun * #st2_after_fun * #H' * #f'' * #G * #K * #tlr2' * #L * #tl2
    185     inversion taa in ⊢ ?;
    186     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    187     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    188       destruct normalize * * #abs destruct (abs)
    189     ]
    190   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    191     normalize * #st2mid * #taa * #st2_fun * #st2_after_fun * #H * #f'' *
    192     #G * #K * #tlr2' * #L * #tl2 inversion taa in ⊢ ?;
    193     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res
    194       >(tlr_rel_extract_equal … H2) cases daemon (* injectivity needed again *)
    195     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    196       destruct normalize * * #abs destruct (abs)
    197     ]
    198   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *
    199     #st2_fun * #st2_after_fun * #H * #f' * #G * #K * #tlr2' * #L * #tl2
    200     inversion taa in ⊢ ?;
    201     [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)
    202     | #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3
    203       destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)
    204     ]
    205   ]
    206 | cases t2
    207   [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res
    208     @(tal_rel_extract_equal p g lg top_f … Hsim)
    209   | #ss #fs #ex' #cl' normalize #Hsim #res
    210     @(tal_rel_extract_equal p g lg top_f … Hsim)
    211   | #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize #Hsim #res
    212     @(tal_rel_extract_equal p g lg top_f … Hsim)
    213   | #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2
    214     normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)
    215   | #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res
    216     @(tal_rel_extract_equal p g lg top_f … Hsim)
    217   ]
    218 ]
    219 qed.
    220 
    221 let rec tlr_rel_max_equal (p: params) (g: list ident)
    222   (lg: ident → joint_internal_function p g) (top_f: ident)
    223   S1 S2 s1 s1' s2 s2' t1 t2 on t1:
    224   tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →
    225   max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =
    226   max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝
    227   match t1 with
    228   [ tlr_base st1 st1' tll1 ⇒ ?
    229   | tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?
    230   ]
    231 and tll_rel_extract_equal (p: params) (g: list ident)
    232   (lg: ident → joint_internal_function p g) (top_f: ident)
    233   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    234   t1 ≈ t2 →
    235   max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =
    236   max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝
    237   match t1 with
    238   [ tll_base ends st1 st1' tal1 co ⇒ ?
    239   ]
    240 and tal_rel_extract_equal (p: params) (g: list ident)
    241   (lg: ident → joint_internal_function p g) (top_f: ident)
    242   S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:
    243   t1 ≈ t2 →
    244   max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =
    245   max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝
    246   match t1 with
    247   [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    248   | tal_base_return st1 st1' ex cl ⇒ ?
    249   | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?
    250   | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?
    251   | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    252   ].
    253287 cases daemon (* next proof *)
    254 qed.
     288qed. *)
    255289     
    256290     
Note: See TracChangeset for help on using the changeset viewer.