Changeset 2712 for src/joint/Joint.ma


Ignore:
Timestamp:
Feb 22, 2013, 8:04:38 PM (8 years ago)
Author:
tranquil
Message:

changed some fields of joint_internal_function's invariant
fixed linearise

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2688 r2712  
    446446(p : params) (globals : list ident) (def : joint_internal_function p globals)
    447447: Prop ≝
    448 { unique_cost_labels :
    449   ∀l1,l2,c,nxt1,nxt2.
    450         stmt_at … (joint_if_code … def) l1 =
    451           Some … (sequential … (COST_LABEL … c) nxt1) →
    452         stmt_at … (joint_if_code … def) l2 =
    453           Some … (sequential … (COST_LABEL … c) nxt2) →
    454         l1 = l2
    455 ; entry_costed :
     448{ entry_costed :
    456449  ∃l,nxt.
    457450        stmt_at … (joint_if_code … def) (joint_if_entry … def) =
    458451          Some … (sequential … (COST_LABEL … l) nxt)
     452; entry_unused :
     453  let entry ≝ pi1 … (joint_if_entry … def) in
     454  let code ≝ joint_if_code … def in
     455  forall_statements_i …
     456    (λpt,stmt.stmt_forall_labels … (λlbl.point_of_label … code lbl ≠ Some ? entry) stmt ∧
     457              stmt_forall_succ … (λnxt.point_of_succ … pt nxt ≠ entry) stmt) code
    459458; code_is_closed : code_closed … (joint_if_code … def)
    460459; code_is_in_universe :
Note: See TracChangeset for help on using the changeset viewer.