Changeset 1281 for src/LTL/LTL.ma
- Timestamp:
- Sep 28, 2011, 11:08:37 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/LTL.ma
r1280 r1281 1 1 include "joint/Joint.ma". 2 2 3 definition ltl_params_: params_ ≝ 4 label_params__of_params__ 5 (mk_params__ unit unit unit unit registers_move Register nat unit False unit 6 unit unit). 3 definition ltl_params__: params__ ≝ 4 (mk_params__ unit unit unit unit registers_move Register nat unit False). 5 definition ltl_params_ : params_ ≝ graph_params_ ltl_params__. 6 definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit. 7 definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit. 8 definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params1. 7 9 8 10 definition ltl_statement ≝ joint_statement ltl_params_. 9 11 10 definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params_.11 12 12 definition ltl_program ≝ joint_program ltl_params. 13 13 14 definition ltl_internal_function ≝ λglobals. joint_internal_function globals (ltl_params globals). 14 definition ltl_internal_function ≝ 15 λglobals. joint_internal_function … (ltl_params globals).
Note: See TracChangeset
for help on using the changeset viewer.