Changeset 267 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Nov 23, 2010, 5:42:20 PM (9 years ago)
 File:

 1 moved
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r266 r267 85 85 }. 86 86 87 ncheck special_function_registers_8051.88 89 87 naxiom sfr8051_index_nineteen: 90 88 ∀i: SFR8051. … … 218 216 old_special_function_registers_8052. 219 217 218 naxiom less_than_or_equal_monotone: 219 ∀m, n: Nat. 220 m ≤ n → S m ≤ S n. 221 222 alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)". 223 220 224 ndefinition get_cy_flag ≝ 221 225 λs: Status. 222 226 let sfr ≝ special_function_registers_8051 s in 223 let psw ≝ get_index … (sfr_8051_index SFR_PSW) s ? in 224 get_index … Z psw ?. 227 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 228 get_index Bool eight psw Z ?. 229 nnormalize. 230 napply (less_than_or_equal_monotone ? ?). 231 napply (less_than_or_equal_zero). 232 nrepeat (napply (less_than_or_equal_monotone ? ?)). 233 napply (less_than_or_equal_zero). 234 nqed. 235 236 ndefinition get_ac_flag ≝ 237 λs: Status. 238 let sfr ≝ special_function_registers_8051 s in 239 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 240 get_index Bool eight psw (S Z) ?. 241 nnormalize. 242 nrepeat (napply (less_than_or_equal_monotone ? ?)). 243 napply (less_than_or_equal_zero). 244 nrepeat (napply (less_than_or_equal_monotone ? ?)). 245 napply (less_than_or_equal_zero). 246 nqed. 247 248 ndefinition get_fo_flag ≝ 249 λs: Status. 250 let sfr ≝ special_function_registers_8051 s in 251 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 252 get_index Bool eight psw two ?. 253 nnormalize. 254 nrepeat (napply (less_than_or_equal_monotone ? ?)). 255 napply (less_than_or_equal_zero). 256 nrepeat (napply (less_than_or_equal_monotone ? ?)). 257 napply (less_than_or_equal_zero). 258 nqed. 259 260 ndefinition get_rs1_flag ≝ 261 λs: Status. 262 let sfr ≝ special_function_registers_8051 s in 263 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 264 get_index Bool eight psw three ?. 265 nnormalize. 266 nrepeat (napply (less_than_or_equal_monotone ? ?)). 267 napply (less_than_or_equal_zero). 268 nrepeat (napply (less_than_or_equal_monotone ? ?)). 269 napply (less_than_or_equal_zero). 270 nqed. 271 272 ndefinition get_rs0_flag ≝ 273 λs: Status. 274 let sfr ≝ special_function_registers_8051 s in 275 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 276 get_index Bool eight psw four ?. 277 nnormalize. 278 nrepeat (napply (less_than_or_equal_monotone ? ?)). 279 napply (less_than_or_equal_zero). 280 nrepeat (napply (less_than_or_equal_monotone ? ?)). 281 napply (less_than_or_equal_zero). 282 nqed. 283 284 ndefinition get_ov_flag ≝ 285 λs: Status. 286 let sfr ≝ special_function_registers_8051 s in 287 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 288 get_index Bool eight psw five ?. 289 nnormalize. 290 nrepeat (napply (less_than_or_equal_monotone ? ?)). 291 napply (less_than_or_equal_zero). 292 nrepeat (napply (less_than_or_equal_monotone ? ?)). 293 napply (less_than_or_equal_zero). 294 nqed. 295 296 ndefinition get_ud_flag ≝ 297 λs: Status. 298 let sfr ≝ special_function_registers_8051 s in 299 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 300 get_index Bool eight psw six ?. 301 nnormalize. 302 nrepeat (napply (less_than_or_equal_monotone ? ?)). 303 napply (less_than_or_equal_zero). 304 nrepeat (napply (less_than_or_equal_monotone ? ?)). 305 napply (less_than_or_equal_zero). 306 nqed. 307 308 ndefinition get_p_flag ≝ 309 λs: Status. 310 let sfr ≝ special_function_registers_8051 s in 311 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 312 get_index Bool eight psw seven ?. 313 nnormalize. 314 nrepeat (napply (less_than_or_equal_monotone ? ?)). 315 napply (less_than_or_equal_zero). 316 nrepeat (napply (less_than_or_equal_monotone ? ?)). 317 napply (less_than_or_equal_zero). 318 nqed. 225 319 226 320 ndefinition set_high_internal_ram ≝
Note: See TracChangeset
for help on using the changeset viewer.