source: src/LTL/LTL_paolo.ma @ 2205

Last change on this file since 2205 was 2174, checked in by tranquil, 8 years ago
  • factored out script for (axiomatised) fixpoint computation
  • ERTL → LTL pass
File size: 740 bytes
Line 
1include "LIN/joint_LTL_LIN_paolo.ma".
2
3definition ltl_params ≝ mk_graph_params ltl_lin_params.
4
5(* aid unification *)
6unification hint 0 ≔
7(*---------------*) ⊢
8acc_a_reg ltl_params ≡ unit.
9unification hint 0 ≔
10(*---------------*) ⊢
11acc_a_arg ltl_params ≡ unit.
12unification hint 0 ≔
13(*---------------*) ⊢
14acc_b_reg ltl_params ≡ unit.
15unification hint 0 ≔
16(*---------------*) ⊢
17acc_a_arg ltl_params ≡ unit.
18unification hint 0 ≔
19(*---------------*) ⊢
20snd_arg ltl_params ≡ ltl_argument.
21unification hint 0 ≔
22(*---------------*) ⊢
23ext_seq ltl_params ≡ ltl_lin_seq.
24unification hint 0 ≔
25(*---------------*) ⊢
26pair_move ltl_params ≡ registers_move.
27
28definition ltl_program ≝ joint_program ltl_params.
Note: See TracBrowser for help on using the repository browser.