Ignore:
Timestamp:
Aug 1, 2012, 4:56:20 PM (8 years ago)
Author:
sacerdot
Message:

PUSH finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2283 r2284  
    23762376    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
    23772377    cases bitone #bit_one_seven_bits_refl normalize nodelta
    2378     [ @eq_bv_elim #seven_bits_refl normalize nodelta
    2379     | FUFFA inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
    2380       #lookup_from_internal_ram_refl ]
     2378    [ @eq_bv_elim #seven_bits_refl normalize nodelta ]
    23812379    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
    23822380    whd in ⊢ (??%?);
     
    23852383    whd in match execute_1_preinstruction; normalize nodelta
    23862384    >bit_one_seven_bits_refl
    2387     [ alias id "write_at_stack_pointer_accA" = "cic:/matita/cerco/ASM/Test3/write_at_stack_pointer_accA.def(29)".
    2388       >seven_bits_refl
     2385    [ >seven_bits_refl
    23892386      @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉)
    2390       [ @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
    2391         try %
    2392         change with (add ??? = ?); @eq_f2 try %
    2393         @(pose … (set_clock ????)) #status #status_refl
    2394         @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
    2395       | >EQs /demod nohyps/ >add_commutative % ]
    2396     |
    2397     |
    2398     |
    2399     ]
     2387    | @write_at_stack_pointer_status_of_pseudo_status_sfr_not_accA [1:assumption]
     2388    | @write_at_stack_pointer_status_of_pseudo_status_low ]
     2389    [1,3,5: @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
     2390      try %
     2391      change with (add ??? = ?); @eq_f2 try %
     2392      @(pose … (set_clock ????)) #status #status_refl
     2393      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
     2394    |*: >EQs /demod nohyps/ >add_commutative % ]
    24002395  |43: (* POP *)
    24012396    cases daemon
Note: See TracChangeset for help on using the changeset viewer.