Changeset 753 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Apr 14, 2011, 5:54:37 PM (9 years ago)
Author:
mulligan
Message:

Work from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r752 r753  
    11include "ERTL/ERTL.ma".
    2  
    3 axiom translate_func:
     2include "LTL/LTL.ma".
     3 
     4axiom translate_ERTL_func:
    45  ∀globals: list Identifier.
    56    list (Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).
    67 
    7 definition translate: ERTLProgram → LTLProgram
     8definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e)
    89  λp.
    9     let globals ≝ map ? ? \fst (ERTL_Pr_Vars e) in
    10     let ltl_pr_var ≝ ERTL_Pr_Vars e in
    11     let ltl_pr_funcs ≝ map ? ? (translate_func globals) (ERTL_Pr_Funcs e) in
     10    let globals ≝ map ? ? \fst (ERTL_Pr_Vars p) in
     11    let ltl_pr_funcs ≝ map ? ? ? (ERTL_Pr_Funcs p) in
     12      mk_LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main p).
     13    # H1
     14    @ (translate_ERTL_func globals) in ⊢ (? × %) (* dpm here *)
Note: See TracChangeset for help on using the changeset viewer.