Changeset 2946 for src/LTL/LTL.ma
 Timestamp:
 Mar 24, 2013, 11:29:01 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/LTL/LTL.ma
r2286 r2946 27 27 28 28 definition ltl_program ≝ joint_program LTL. 29 unification hint 0 ≔ ⊢ ltl_program ≡ joint_program LTL. 29 30 30 31 coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝ … … 32 33 coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝ 33 34 hdw_argument_from_reg on _r : Register to snd_arg LTL. 35 36 definition LTL_premain : ∀p : ltl_program.joint_closed_internal_function LTL (prog_var_names ?? p) ≝ 37 λp. 38 let l1 : label ≝ an_identifier … one in 39 let l2 : label ≝ an_identifier … (p0 one) in 40 let l3 : label ≝ an_identifier … (p1 one) in 41 let res ≝ 42 mk_joint_internal_function LTL (prog_var_names … p) 43 (mk_universe … (p0 (p0 one))) 44 (mk_universe … one) 45 it it 0 0 (empty_map …) l1 in 46 (* todo: args for main? *) 47 let res ≝ add_graph … l1 48 (sequential … (COST_LABEL … (init_cost_label … p)) l2) 49 res in 50 let res ≝ add_graph … l2 51 (sequential … (CALL LTL ? (inl … (prog_main … p)) 4 it) l3) 52 res in 53 let res ≝ add_graph … l3 54 (GOTO ? l3) 55 res in 56 res. 57 % 58 [ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct 59 % 60 [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct 61 2: % 62 4,6: % whd in ⊢ (??%%→?); #EQ destruct 63 ] 64  ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} 65  ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // 66  ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I 67  %{l2} %{(init_cost_label … p)} % 68 ] 69 qed.
Note: See TracChangeset
for help on using the changeset viewer.