Ignore:
Timestamp:
Jul 30, 2012, 1:14:40 AM (7 years ago)
Author:
sacerdot
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofsSplit.ma

    r2272 r2274  
    603603qed.
    604604
    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
    634606lemma special_function_registers_8051_set_arg_8:
    635607  ∀M: internal_pseudo_address_map.
     
    695667  cases not_implemented *)
    696668qed.
     669*)
Note: See TracChangeset for help on using the changeset viewer.