Changeset 757 for src/ERTL/ERTLToLTL.ma
- Timestamp:
- Apr 18, 2011, 12:30:53 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ERTL/ERTLToLTL.ma
r753 r757 3 3 4 4 axiom translate_ERTL_func: 5 ∀globals: list Identifier.6 list ( Identifier × ERTLFunction) → list (Identifier × (LTLFunctionDefinition globals)).5 ∀globals: list ident. 6 list (ident × ertl_function) → list (ident × (ltl_function_definition globals)). 7 7 8 definition translate: ∀e: ERTLProgram. LTLProgram (ERTL_Pr_Vars e) ≝8 definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝ 9 9 λp. 10 let globals ≝ map ? ? \fst ( ERTL_Pr_Vars p) in11 let ltl_pr_funcs ≝ map ? ? ? ( ERTL_Pr_Funcs p) in12 mk_ LTLProgram (ERTL_Pr_Vars p) ltl_pr_funcs (ERTL_Pr_Main p).10 let globals ≝ map ? ? \fst (ertl_pr_vars p) in 11 let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in 12 mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p). 13 13 # H1 14 @ (translate_ ERTL_func globals) in ⊢ (? × %) (* dpm here *)14 @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *)
Note: See TracChangeset
for help on using the changeset viewer.