Changeset 2456


Ignore:
Timestamp:
Nov 13, 2012, 11:28:59 AM (7 years ago)
Author:
boender
Message:
  • added simple proof
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/stacksize.ma

    r2426 r2456  
    256256qed.
    257257
    258 (* let rec tlr_rel_max_equal (p: params) (g: list ident)
     258let rec tlr_rel_max_equal (p: params) (g: list ident)
    259259  (lg: ident → joint_internal_function p g) (top_f: ident)
    260260  S1 S2 s1 s1' s2 s2' t1 t2 on t1:
     
    284284  [ tal_base_not_return st1 st1' ex cl co ⇒ ?
    285285  | tal_base_return st1 st1' ex cl ⇒ ?
    286   | tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?
    287   | tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?
     286  | tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ?
     287  | tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ?
    288288  | tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?
    289289  ].
    290  cases daemon (* next proof *)
    291 qed. *)
     290[1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) %
     291|3: #Hsim >(tll_rel_extract_equal … Hsim []) %
     292|*: #Hsim >(tal_rel_extract_equal … Hsim []) %
     293]
     294qed.
    292295     
    293296     
Note: See TracChangeset for help on using the changeset viewer.