Changeset 1071 for src/ASM/I8051.ma


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (9 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r1066 r1071  
    137137
    138138(* dpm: registers for stack manipulation *)
    139 definition RegisterSST ≝ Register03.
    140 definition RegisterST0 ≝ Register04.
    141 definition RegisterST1 ≝ Register05.
     139definition RegisterSST ≝ Register10.
     140definition RegisterST0 ≝ Register02.
     141definition RegisterST1 ≝ Register03.
     142definition RegisterST2 ≝ Register04.
     143definition RegisterST3 ≝ Register05.
     144definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
    142145definition RegisterSPL ≝ Register06.
    143146definition RegisterSPH ≝ Register07.
     147definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
    144148
    145149definition register_address: Register → [[ acc_a; direct; registr ]] ≝
Note: See TracChangeset for help on using the changeset viewer.