Changeset 2285 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Aug 2, 2012, 1:58:14 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2284 r2285 2394 2394 *: >EQs /demod nohyps/ >add_commutative % ] 2395 2395 43: (* POP *) 2396 cases daemon 2396 *: cases daemon ] 2397 >EQP P normalize nodelta lapply instr_refl 2398 @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta 2399 #sigma_increment_commutation 2400 whd in ⊢ (??%? → ?); 2401 @vsplit_elim #bit_one #seven_bits 2402 cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H bit_one 2403 cases bitone #bit_one_seven_bits_refl normalize nodelta 2404 [ @eq_bv_elim #seven_bits_refl normalize nodelta 2405 [2: inversion (lookup_from_internal_ram ??) normalize nodelta 2406 [2: #x #_ #abs destruct(abs)] #lookup_from_internal_ram_refl]] 2407 @Some_Some_elim #Mrefl <Mrefl M' #fetch_many_assm %{1} 2408 whd in ⊢ (??%?); 2409 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 2410 whd in match execute_1_0; normalize nodelta 2411 whd in match execute_1_preinstruction; normalize nodelta 2412 @(pair_replace ?????????? p) >p normalize nodelta 2413 >bit_one_seven_bits_refl 2414 [1,3,5: <p @eq_f3 try % 2415 @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … s) try % 2416 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl try % 2417 @eq_f2 try % @(subaddressing_mode_elim … addr) #y % 2418 2: @set_arg_8_status_of_pseudo_status try % 2419 [1: @set_8051_sfr_status_of_pseudo_status try % 2420 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl try % 2421 @eq_f2 try % @(subaddressing_mode_elim … addr) #y % 2422  whd in ⊢ (??%?); 2423 inversion (sfr_of_Byte ?) normalize nodelta 2424 [ #sfr_of_Byte_refl (*CSC: needs >read_at_stack_pointer_set_clock*) cases daemon 2425  * normalize nodelta * #sfr_of_Byte_refl 2426 [18: @⊥ @(absurd ?? seven_bits_refl) >bit_one_seven_bits_refl 2427 @eq_sfr_of_Byte_accA_to_eq assumption 2428 *: change with (read_at_stack_pointer ??? = ?) 2429 cases daemon (*CSC: needs >read_at_stack_pointer_set_clock*)]]] 2430 3: 2431 4: 2432 XXX 2433 ] 2397 2434 44: 2398 2435 >EQP P normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.