Changeset 2863 for src/joint/Joint.ma


Ignore:
Timestamp:
Mar 13, 2013, 2:22:29 PM (8 years ago)
Author:
piccolo
Message:

Added new invariant to good_if
Generalized version of cond case for the correctness proof of each translate step

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2843 r2863  
    520520
    521521include alias "basics/logic.ma".
    522 
     522check stmt_at
    523523record good_if
    524524(p : params) (globals : list ident) (def : joint_internal_function p globals)
     
    539539; regs_are_in_univers :
    540540  regs_in_universe … (joint_if_code … def) (joint_if_runiverse … def)
     541; entry_is_cost :
     542  ∃nxt,c.
     543  stmt_at p globals (joint_if_code … def) (joint_if_entry … def) =
     544  Some ? (sequential p ? (COST_LABEL ?? c) nxt)
    541545}.
    542546 
Note: See TracChangeset for help on using the changeset viewer.