Changeset 2274 for src/ASM/StatusProofsSplit.ma

Timestamp:

Jul 30, 2012, 1:14:40 AM (8 years ago)

Author:

sacerdot

Message:

Dead code commented out and code out of place moved to Test.ma.

File:

• src/ASM/StatusProofsSplit.ma (modified) (2 diffs)

src/ASM/StatusProofsSplit.ma

@@ -603 +603 @@
 qed.
 
-lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:
-  ∀M: internal_pseudo_address_map.
-  ∀cm: pseudo_assembly_program.
-  ∀ps.
-  ∀sigma: Word → Word.
-  ∀policy: Word → bool.
-  ∀sfr.
-  ∀result: Byte.
-    eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →
-      special_function_registers_8051 (BitVectorTrie Byte 16)
-        (code_memory_of_pseudo_assembly_program cm sigma policy)
-        (set_8051_sfr (BitVectorTrie Byte 16)
-        (code_memory_of_pseudo_assembly_program cm sigma policy)
-        (status_of_pseudo_status M cm ps sigma policy) sfr result) =
-      sfr_8051_of_pseudo_sfr_8051 M
-        (special_function_registers_8051 pseudo_assembly_program cm
-        (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.
-  #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm
-  whd in match (set_8051_sfr ?????);
-  cases M * #low #high * try % * *
-  whd in match (special_function_registers_8051 ???);
-  whd in match (sfr_8051_of_pseudo_sfr_8051 ???); normalize nodelta
-  @pair_elim #high #low #high_low_refl normalize nodelta
-  cases (eq_upper_lower ??) normalize nodelta
-  whd in match (set_8051_sfr ?????);
-  @set_index_set_index_commutation @nmk #relevant
-  @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))
-qed.
-
+(*CSC: dead and unfinished code
 lemma special_function_registers_8051_set_arg_8:
   ∀M: internal_pseudo_address_map.
@@ -695 +667 @@
   cases not_implemented *)
 qed.
+*)