Changeset 2700 for src/ASM/Policy.ma
 Timestamp:
 Feb 22, 2013, 2:12:24 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2653 r2700 322 322 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) in Hm; 323 323 normalize nodelta 324 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ 324 [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le 325 @monotonic_lt_times_r [/2/] % 325 326  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 326 327 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/ … … 333 334 cases (\snd (bvt_lookup … (bitvector_of_nat ? (t)) (\snd policy) 〈0,short_jump〉)) in Hm; 334 335 normalize nodelta 335 [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/ 336 [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le 337 @monotonic_lt_times_r try % /2/ 336 338  >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) 337 339 <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/
Note: See TracChangeset
for help on using the changeset viewer.