Changeset 2172 for src/ASM/StatusProofsSplit.ma
 Timestamp:
 Jul 10, 2012, 2:39:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/StatusProofsSplit.ma
r2170 r2172 113 113 ∀b: Bit. 114 114 program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s. 115 #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta115 #M #cm #s whd in match set_arg_1; cases daemon (* whd in match set_arg_1'; normalize nodelta 116 116 #addr #b 117 117 @(subaddressing_mode_elim … addr) … … 127 127 2: 128 128 cases (vsplit ????) // 129 ] 129 ] *) 130 130 qed. 131 131 … … 551 551 #M #cm #ps #addr1 #result 552 552 @(subaddressing_mode_elim … addr1) try #w try % 553 whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)553 whd in ⊢ (??(???%)?); cases daemon (*whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *) 554 554 [1: 555 555 cases (vsplit bool ???) #nu #nl normalize nodelta … … 561 561 cases (vsplit bool ???) #ignore #three_bits normalize nodelta 562 562 cases (get_index_v bool ????) normalize nodelta % 563 ] 563 ] *) 564 564 qed. 565 565 … … 612 612 2: 613 613 #addressing_mode_ok_refl whd in ⊢ (??%?); 614 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 614 @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (* 615 615 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 616 616 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta … … 737 737 ] 738 738 ] 739 ] 739 ] *) 740 740 qed. 741 741
Note: See TracChangeset
for help on using the changeset viewer.