Changeset 1941 for src/ASM/Fetch.ma
 Timestamp:
 May 14, 2012, 4:33:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Fetch.ma
r1642 r1941 10 10 definition code_memory_size ≝ bitvector_max_nat 16. 11 11 12 definition add ≝ 13 λn: nat. 14 λl, r: BitVector n. 15 \snd (half_add n l r). 16 17 axiom add_zero: 18 ∀n: nat. 19 ∀l: BitVector n. 20 l = add n l (zero …). 21 22 axiom add_associative: 23 ∀n: nat. 24 ∀l, c, r: BitVector n. 25 add … l (add … c r) = add … (add … l c) r. 26 27 include alias "ASM/BitVectorTrie.ma". 28 12 29 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. Word × Byte ≝ 13 30 λpmem: BitVectorTrie Byte 16. 14 31 λpc: Word. 15 〈 \snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉.32 〈add … pc (bitvector_of_nat 16 1), lookup … pc pmem (zero …)〉. 16 33 17 34 lemma Prod_inv_rect_Type0:
Note: See TracChangeset
for help on using the changeset viewer.