Ignore:
Timestamp:
Aug 1, 2012, 4:56:20 PM (9 years ago)
Author:
sacerdot
Message:

PUSH finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2282 r2284  
    445445    BitVectorTrie C n.
    446446
     447(*
    447448axiom is_in_domain:
    448449  ∀A: Type[0].
     
    462463        f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2) = f (lookup_opt … addr bvt_1) (lookup_opt … addr bvt_2')) →
    463464          bvt_map2 … bvt_1 bvt_2 f = bvt_map2 … bvt_1 bvt_2' f.
     465*)
     466
     467axiom lookup_opt_bvt_map2:
     468 ∀A,B,C,n,map1,map2,f,addr.
     469lookup_opt … addr (bvt_map2 A B C n map1 map2 f) =
     470 f (lookup_opt … addr map1) (lookup_opt … addr map2).
    464471
    465472definition lookup_from_internal_ram:
Note: See TracChangeset for help on using the changeset viewer.