Ignore:
Timestamp:
Jan 9, 2013, 1:23:29 PM (7 years ago)
Author:
garnier
Message:

Progress on toCminorCorrectness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/memoryInjections.ma

    r2569 r2572  
    388388| 3: #Habsurd destruct (Habsurd)
    389389| 4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ]
    390 qed.
     390qed.
     391
     392lemma value_eq_null_inversion :
     393  ∀E,v. value_eq E Vnull v → v = Vnull.
     394#E #v #Heq inversion Heq //
     395#p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd)
     396#Habsurd' destruct
     397qed.
    391398
    392399(* A cleaner version of inversion for [value_eq] *)
     
    443450    Zltb (block_id b) (nextblock m) = true ∧
    444451    Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧
    445  
    446452    Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true.
    447453#ty #m * #brg #bid #off #v
Note: See TracChangeset for help on using the changeset viewer.