source: src/ERTLptr/ERTLToERTLptrAxiom.ma @ 3362

Last change on this file since 3362 was 3018, checked in by sacerdot, 7 years ago

1) some files repaired
2) all stuff related to the aborted pass ERTLptr (now merged with

ERTLToLTL) moved into the ERTLptr directory (no longer used/linked)

File size: 1.7 KB
Line 
1
2(**************************************************************************)
3(*       ___                                                              *)
4(*      ||M||                                                             *)
5(*      ||A||       A project by Andrea Asperti                           *)
6(*      ||T||                                                             *)
7(*      ||I||       Developers:                                           *)
8(*      ||T||         The HELM team.                                      *)
9(*      ||A||         http://helm.cs.unibo.it                             *)
10(*      \   /                                                             *)
11(*       \ /        This file is distributed under the terms of the       *)
12(*        v         GNU General Public License Version 2                  *)
13(*                                                                        *)
14(**************************************************************************)
15
16(* just an axiom stub *)
17include "ERTL/ERTLToERTLptr.ma".
18include "ERTL/ERTL_semantics.ma".
19include "ERTLptr/ERTLptr_semantics.ma".
20include "joint/Traces.ma".
21include "common/StatusSimulation.ma".
22
23axiom ertl_to_ertlptr_ok:
24∀prog.∀stack_sizes.
25let trans_prog ≝ ertl_to_ertlptr prog in
26   ∃[1]R.
27   status_simulation
28    (joint_status ERTL_semantics prog stack_sizes)
29    (joint_status ERTLptr_semantics trans_prog stack_sizes) R ∧
30  ∀init_in.make_initial_state
31    (mk_prog_params ERTL_semantics prog stack_sizes) = OK … init_in →
32  ∃init_out.
33    make_initial_state
34     (mk_prog_params ERTLptr_semantics trans_prog stack_sizes) =
35      OK ? init_out ∧
36   R init_in init_out.
Note: See TracBrowser for help on using the repository browser.