Changeset 1530


Ignore:
Timestamp:
Nov 22, 2011, 12:37:42 PM (8 years ago)
Author:
campbell
Message:

Update due to Russell changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r1519 r1530  
    110110    ∀prf:is_in ?
    111111     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    112   set_arg_8 ? (set_code_memory T U ps code_mem) b val =
     112  eject … (set_arg_8 ? (set_code_memory T U ps code_mem) b val) =
    113113  set_code_memory T U (set_arg_8 ? ps b val) code_mem.
    114114  [2,3: cases b in prf; *; normalize //]
    115115  #n #l #T #U #ps #code_mem #val * *;
    116116  #x try (#y #H) try #H whd in H; try cases H
    117   whd in ⊢ (??(%)?); whd in ⊢ (???(???(%)?)); try %
     117  whd in ⊢ (??(???(%))?); whd in ⊢ (???(???(???(%))?)); try %
    118118  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    119119  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     
    132132    ∀prf:is_in ?
    133133     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    134   set_arg_8 ? (set_program_counter T ps pc) b val =
     134  eject … (set_arg_8 ? (set_program_counter T ps pc) b val) =
    135135  set_program_counter T (set_arg_8 ? ps b val) pc.
    136136  [2,3: cases b in prf; *; normalize //]
    137137  #n #l #T #ps #pc #val * *;
    138138  #x try (#y #H) try #H whd in H; try cases H
    139   whd in ⊢ (??(%)?); whd in ⊢ (???(??(%)?)); try %
     139  whd in ⊢ (??(???(%))?); whd in ⊢ (???(??(%)?)); try %
    140140  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    141141  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.