[1378] | 1 | include "LIN/joint_LTL_LIN.ma". |
---|

[722] | 2 | |
---|

[2286] | 3 | definition LTL ≝ mk_graph_params LTL_LIN. |
---|

[1168] | 4 | |
---|

[2286] | 5 | (* aid unification *) |
---|

| 6 | unification hint 0 ≔ |
---|

| 7 | (*---------------*) ⊢ |
---|

| 8 | acc_a_reg LTL ≡ unit. |
---|

| 9 | unification hint 0 ≔ |
---|

| 10 | (*---------------*) ⊢ |
---|

| 11 | acc_a_arg LTL ≡ unit. |
---|

| 12 | unification hint 0 ≔ |
---|

| 13 | (*---------------*) ⊢ |
---|

| 14 | acc_b_reg LTL ≡ unit. |
---|

| 15 | unification hint 0 ≔ |
---|

| 16 | (*---------------*) ⊢ |
---|

| 17 | acc_a_arg LTL ≡ unit. |
---|

| 18 | unification hint 0 ≔ |
---|

| 19 | (*---------------*) ⊢ |
---|

| 20 | snd_arg LTL ≡ hdw_argument. |
---|

| 21 | unification hint 0 ≔ |
---|

| 22 | (*---------------*) ⊢ |
---|

| 23 | ext_seq LTL ≡ ltl_lin_seq. |
---|

| 24 | unification hint 0 ≔ |
---|

| 25 | (*---------------*) ⊢ |
---|

| 26 | pair_move LTL ≡ registers_move. |
---|

[1271] | 27 | |
---|

[2286] | 28 | definition ltl_program ≝ joint_program LTL. |
---|

[2946] | 29 | unification hint 0 ≔ ⊢ ltl_program ≡ joint_program LTL. |
---|

[2286] | 30 | |
---|

| 31 | coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝ |
---|

| 32 | hdw_argument_from_byte on _b : Byte to snd_arg LTL. |
---|

| 33 | coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝ |
---|

| 34 | hdw_argument_from_reg on _r : Register to snd_arg LTL. |
---|

[2946] | 35 | |
---|

[3037] | 36 | definition LTL_premain : ∀p : ltl_program. |
---|

| 37 | joint_closed_internal_function LTL (prog_names … p) ≝ |
---|

[2946] | 38 | λp. |
---|

| 39 | let l1 : label ≝ an_identifier … one in |
---|

| 40 | let l2 : label ≝ an_identifier … (p0 one) in |
---|

| 41 | let l3 : label ≝ an_identifier … (p1 one) in |
---|

| 42 | let res ≝ |
---|

[3037] | 43 | mk_joint_internal_function LTL (prog_names … p) |
---|

[2946] | 44 | (mk_universe … (p0 (p0 one))) |
---|

| 45 | (mk_universe … one) |
---|

| 46 | it it 0 0 (empty_map …) l1 in |
---|

| 47 | (* todo: args for main? *) |
---|

| 48 | let res ≝ add_graph … l1 |
---|

| 49 | (sequential … (COST_LABEL … (init_cost_label … p)) l2) |
---|

| 50 | res in |
---|

| 51 | let res ≝ add_graph … l2 |
---|

[2952] | 52 | (sequential … (CALL LTL ? (inl … (prog_main … p)) 0 it) l3) |
---|

[2946] | 53 | res in |
---|

| 54 | let res ≝ add_graph … l3 |
---|

| 55 | (GOTO ? l3) |
---|

| 56 | res in |
---|

| 57 | res. |
---|

| 58 | % |
---|

| 59 | [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct |
---|

| 60 | % |
---|

| 61 | [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct |
---|

| 62 | |2: % |
---|

| 63 | |4,6: % whd in ⊢ (??%%→?); #EQ destruct |
---|

| 64 | ] |
---|

| 65 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} |
---|

| 66 | | ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // |
---|

| 67 | | ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I |
---|

| 68 | | %{l2} %{(init_cost_label … p)} % |
---|

| 69 | ] |
---|

| 70 | qed. |
---|