Changeset 2946 for src/LTL/LTLToLINAxiom.ma
- Timestamp:
- Mar 24, 2013, 11:29:01 AM (8 years ago)
- File:
-
- 1 moved
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/LTLToLINAxiom.ma
r2868 r2946 8 8 axiom LTLToLIN_ok : 9 9 ∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *) 10 ∀p_in : LTL_program.10 ∀p_in : joint_program LTL. 11 11 let p_out ≝ ltl_to_lin p_in in 12 12 ∃[1] R. … … 14 14 (joint_status LTL_semantics p_in stacksizes) 15 15 (joint_status LIN_semantics p_out stacksizes) 16 R. 16 R ∧ 17 ∀init_in.make_initial_state 18 (mk_prog_params LTL_semantics p_in stacksizes) = OK … init_in → 19 ∃init_out. 20 make_initial_state 21 (mk_prog_params LIN_semantics p_out stacksizes) = 22 OK ? init_out ∧ 23 R init_in init_out.
Note: See TracChangeset
for help on using the changeset viewer.