Changeset 2655 for src/joint/Joint.ma


Ignore:
Timestamp:
Feb 11, 2013, 4:52:37 PM (7 years ago)
Author:
tranquil
Message:

new step in code semantic lemma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2645 r2655  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "basics/lists/listb.ma".
    910include "joint/String.ma".
    1011
     
    9798  | POP: acc_a_reg p → joint_seq p globals
    9899  | PUSH: acc_a_arg p → joint_seq p globals
    99   | ADDRESS: ∀i: ident. (member ? (eq_identifier ?) i globals) → dpl_reg p → dph_reg p → joint_seq p globals
     100  | ADDRESS: ∀i: ident. i ∈ globals → dpl_reg p → dph_reg p → joint_seq p globals
    100101  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
    101102  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
Note: See TracChangeset for help on using the changeset viewer.