Changeset 2820


Ignore:
Timestamp:
Mar 8, 2013, 12:26:06 AM (6 years ago)
Author:
sacerdot
Message:

Proof obligation closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToERTLptr.ma

    r2818 r2820  
    7575definition translate_data :
    7676  ∀globals.joint_closed_internal_function ERTL globals →
    77    bound_b_graph_translate_data ERTL ERTLptr globals
    78 λglobals,def.bret ….
    79    [try @(mk_b_graph_translate_data …
     77  bind_new register (b_graph_translate_data ERTL ERTLptr globals)
     78λglobals,def.bret …
     79   (mk_b_graph_translate_data …
    8080    (* init_ret ≝ *) (joint_if_result … def)
    8181    (* init_params ≝ *) (joint_if_params … def)
     
    8585    (* f_step ≝ *) (translate_step globals)
    8686    (* f_fin ≝ *) (translate_fin_step globals)
    87     ????)
    88    | cases daemon ]
    89 @hide_prf cases daemon (*
     87    ????).
     88@hide_prf
    9089[ #l * [ #c' | * #f #args #dest | #a #ltrue | #s ] #c whd
    9190  [3: #r1 ] #l' #EQ destruct try %
     
    109108  [ #X #l1 #l2 #EQ destruct elim l2 [ % ] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #H %2{H} ]
    110109  #aux @aux cases s //
    111 ]*)
     110]
    112111qed.
    113112
    114113definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
    115114  b_graph_transform_program ERTL ERTLptr translate_data.
     115%
     116qed.
Note: See TracChangeset for help on using the changeset viewer.