 Timestamp:
 Oct 20, 2011, 11:12:38 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/liveness.ma
r1282 r1425 264 264 definition equations ≝ label → rhs. 265 265 266 axiom fix_lfp: equations → valuation. 266 record fixpoint: Type[0] ≝ 267 { 268 fix_lfp :1> equations → valuation; 269 fix_correct: ∀f: equations. 270 ∀v: label. 271 lattice_equal (f v (fix_lfp f)) (fix_lfp f v) 272 }. 273 274 axiom the_fixpoint: fixpoint. 267 275 268 276 definition livebefore ≝ … … 296 304 λglobals. 297 305 λint_fun. 298 fix_lfp(liveafter globals int_fun (livebefore globals int_fun)).306 the_fixpoint (liveafter globals int_fun (livebefore globals int_fun)).
Note: See TracChangeset
for help on using the changeset viewer.