Ignore:
Timestamp:
Mar 25, 2013, 9:48:01 PM (8 years ago)
Author:
sacerdot
Message:

Some advance/repairing in ERTLptrToLTLProof. In particular, we know take in
account that the fixpoint computation only returns a pre-fixpoint.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/liveness.ma

    r2942 r2949  
    33include "utilities/adt/set_adt.ma".
    44include "utilities/fixpoints.ma".
     5
     6definition rl_included ≝
     7 λleft,right.
     8  set_subset … (eq_identifier RegisterTag) (\fst left) (\fst right) ∧
     9  set_subset … eq_Register (\snd left) (\snd right).
    510
    611definition register_lattice : property_lattice ≝
     
    1217  set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
    1318  set_equal … eq_Register (\snd left) (\snd right))
    14  (λleft.
    15   λright.
    16   set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧
    17   set_subset … eq_Register (\snd left) (\snd right))
     19 rl_included
    1820 (λ_.false).
    1921
Note: See TracChangeset for help on using the changeset viewer.