Changeset 3101


Ignore:
Timestamp:
Apr 6, 2013, 4:08:30 PM (4 years ago)
Author:
mckinna
Message:

Removed redundant lemma execute_1_technical,
which is covered by ASM/is_in_subvector_is_in_supervector

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r3066 r3101  
    33
    44include "ASM/AbstractStatus.ma". (* includes "ASM/Fetch.ma".*)
    5    
    6 lemma execute_1_technical:
     5
     6(* JHM: order of includes changes *)
     7include alias "ASM/Arithmetic.ma".
     8include alias "ASM/BitVectorTrie.ma".
     9include alias "arithmetics/nat.ma".
     10
     11(* JHM: redundant;superseded by ASM/is_in_subvector_is_in_supervector *
     12
     13lemma execute_1_technical:
    714  ∀n, m: nat.
    815  ∀v: Vector addressing_mode_tag (S n).
     
    1724 # q
    1825 # a
     26     
     27    #a_is_in #is_subvec @is_in_subvector_is_in_supervector //
     28   
     29(*
    1930 elim v
    2031 [ normalize
     
    6273   ]
    6374 ]
     75*)
    6476qed.
    65 
    66 (* JHM: order of includes changes *)
    67 include alias "ASM/Arithmetic.ma".
    68 include alias "ASM/BitVectorTrie.ma".
    69 include alias "arithmetics/nat.ma".
     77*)
    7078
    7179definition execute_1_preinstruction:
     
    8593            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
    8694                                                   (get_arg_8 … s false addr2) false in
    87             let cy_flag ≝ get_index' ? O  ? flags in
     95            let cy_flag ≝ get_index' ? O ? flags in
    8896            let ac_flag ≝ get_index' ? 1 ? flags in
    8997            let ov_flag ≝ get_index' ? 2 ? flags in
     
    482490    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    483491    try (
    484       @(execute_1_technical … (subaddressing_modein …))
     492      @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    485493      @I
    486494    ) (*66s*)
     
    910918    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
    911919    try (
    912       @(execute_1_technical … (subaddressing_modein …))
     920      @(is_in_subvector_is_in_supervector … (subaddressing_modein …))
    913921      @I
    914922    ) (*66s*)
Note: See TracChangeset for help on using the changeset viewer.