Changeset 2274 for src/ASM/StatusProofsSplit.ma
- Timestamp:
- Jul 30, 2012, 1:14:40 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/StatusProofsSplit.ma
r2272 r2274 603 603 qed. 604 604 605 lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051: 606 ∀M: internal_pseudo_address_map. 607 ∀cm: pseudo_assembly_program. 608 ∀ps. 609 ∀sigma: Word → Word. 610 ∀policy: Word → bool. 611 ∀sfr. 612 ∀result: Byte. 613 eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false → 614 special_function_registers_8051 (BitVectorTrie Byte 16) 615 (code_memory_of_pseudo_assembly_program cm sigma policy) 616 (set_8051_sfr (BitVectorTrie Byte 16) 617 (code_memory_of_pseudo_assembly_program cm sigma policy) 618 (status_of_pseudo_status M cm ps sigma policy) sfr result) = 619 sfr_8051_of_pseudo_sfr_8051 M 620 (special_function_registers_8051 pseudo_assembly_program cm 621 (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma. 622 #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm 623 whd in match (set_8051_sfr ?????); 624 cases M * #low #high * try % * * 625 whd in match (special_function_registers_8051 ???); 626 whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta 627 @pair_elim #high #low #high_low_refl normalize nodelta 628 cases (eq_upper_lower ??) normalize nodelta 629 whd in match (set_8051_sfr ?????); 630 @set_index_set_index_commutation @nmk #relevant 631 @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm)) 632 qed. 633 605 (*CSC: dead and unfinished code 634 606 lemma special_function_registers_8051_set_arg_8: 635 607 ∀M: internal_pseudo_address_map. … … 695 667 cases not_implemented *) 696 668 qed. 669 *)
Note: See TracChangeset
for help on using the changeset viewer.