Ignore:
Timestamp:
Apr 5, 2013, 6:04:14 PM (7 years ago)
Author:
tranquil
Message:

preliminary work on closing correctness.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTLAxiom.ma

    r2946 r3096  
    55include "common/StatusSimulation.ma".
    66
    7 axiom RTLabsToRTL_ok :
     7axiom RTLToERTL_ok :
    88∀stacksizes : ident → option ℕ. (* are hypotheses needed here? *)
    99∀p_in : rtl_program.
    1010let p_out ≝ rtl_to_ertl p_in in
     11  ∀init_in.make_initial_state
     12    (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
     13∃init_out.
     14  make_initial_state
     15   (mk_prog_params ERTL_semantics p_out stacksizes) =
     16    OK ? init_out ∧
    1117∃[1] R.
    12   status_simulation
     18  status_simulation_with_init
    1319    (joint_status RTL_semantics_unique p_in stacksizes)
    1420    (joint_status ERTL_semantics p_out stacksizes)
    15     R ∧
    16   ∀init_in.make_initial_state
    17     (mk_prog_params RTL_semantics_unique p_in stacksizes) = OK … init_in →
    18   ∃init_out.
    19     make_initial_state
    20      (mk_prog_params ERTL_semantics p_out stacksizes) =
    21       OK ? init_out ∧
    22    R init_in init_out.
     21    R init_in init_out.
Note: See TracChangeset for help on using the changeset viewer.