Ignore:
Timestamp:
Dec 14, 2011, 1:40:08 PM (8 years ago)
Author:
sacerdot
Message:

Porting to last library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofs.ma

    r1530 r1606  
    110110    ∀prf:is_in ?
    111111     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    112   eject … (set_arg_8 ? (set_code_memory T U ps code_mem) b val) =
     112  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 * *;
    116   #x try (#y #H) try #H whd in H; try cases H
    117   whd in ⊢ (??(???(%))?); whd in ⊢ (???(???(???(%))?)); try %
     116  #x try (#y #H) try #H whd in H; try cases H try %
     117  whd in match set_arg_8; normalize nodelta
     118  whd in match set_arg_8'; normalize nodelta
    118119  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    119120  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
     
    132133    ∀prf:is_in ?
    133134     [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b.
    134   eject … (set_arg_8 ? (set_program_counter T ps pc) b val) =
     135  set_arg_8 ? (set_program_counter T ps pc) b val =
    135136  set_program_counter T (set_arg_8 ? ps b val) pc.
    136137  [2,3: cases b in prf; *; normalize //]
    137138  #n #l #T #ps #pc #val * *;
    138   #x try (#y #H) try #H whd in H; try cases H
    139   whd in ⊢ (??(???(%))?); whd in ⊢ (???(??(%)?)); try %
     139  #x try (#y #H) try #H whd in H; try cases H try %
     140  whd in match set_arg_8; normalize nodelta
     141  whd in match set_arg_8'; normalize nodelta
    140142  cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
    141143  cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.