Changeset 2109
 Timestamp:
 Jun 26, 2012, 2:47:56 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2108 r2109 904 904 cases daemon 905 905 2,4: 906 XXX: here 907 >EQppc 906 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 907 [2, 4: 908 cases daemon (* XXX: !!! *) 909 ] 910 normalize nodelta >EQppc 908 911 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 909 912 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' … … 917 920 >EQstatus_after_1 in ⊢ (???%); 918 921 whd in ⊢ (???%); 919 [1: exists_labelled_instruction id instr_list →922 [1: 920 923 <fetch_refl in ⊢ (???%); 921 924 2: … … 971 974 (* XXX: switch to the right hand side *) 972 975 normalize nodelta >EQs s >EQticks ticks 973 cases (¬ eq_bv ???) normalize nodelta 974 whd in ⊢ (??%%); 976 normalize nodelta whd in ⊢ (??%%); 975 977 ] 976 978 (* XXX: finally, prove the equality using sigma commutation *) … … 988 990 989 991 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 990 whd in match (expand_relative_jump ????);991 992 <EQppc in fetch_many_assm; 993 whd in match (short_jump_cond ??); 994 @pair_elim #sj_possible #disp 992 995 @pair_elim #result #flags #sub16_refl 993 996 @pair_elim #upper #lower #vsplit_refl 994 inversion (eq_bv ???) #upper_vsplit_refl normalize nodelta 997 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 998 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta 995 999 [1,3: 996 1000 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 1001 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 1002 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 997 1003 whd in ⊢ (??%?); 998 1004 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); … … 1019 1025 ] 1020 1026 2,4: 1021 >EQppc 1027 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 1028 [2, 4: 1029 cases daemon (* XXX: !!! *) 1030 ] 1031 normalize nodelta >EQppc 1022 1032 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1023 1033 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' … … 1090 1100 1091 1101 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1092 whd in match (expand_relative_jump ????);1093 1102 <EQppc in fetch_many_assm; 1103 whd in match (short_jump_cond ??); 1104 @pair_elim #sj_possible #disp 1094 1105 @pair_elim #result #flags #sub16_refl 1095 1106 @pair_elim #upper #lower #vsplit_refl 1096 cases (eq_bv ???) normalize nodelta 1107 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 1108 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta 1097 1109 [1,3,5,7,9,11,13,15,17,19,21,23,25,27: 1098 1110 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 1111 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 1112 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 1099 1113 whd in ⊢ (??%?); 1100 1114 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); … … 1111 1125 cases daemon 1112 1126 2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1113 >EQppc 1127 >(? : eq_v bool 9 eq_b upper (zero 9) = false) 1128 [2,4,6,8,10,12,14,16,18,20,22,24,26,28: 1129 cases daemon (* XXX: !!! *) 1130 ] 1131 normalize nodelta >EQppc 1114 1132 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl 1115 1133 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl' … … 1241 1259 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1242 1260 whd in ⊢ (??%?); 1261 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 1243 1262 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1244 1263 (* XXX: work on the left hand side *) … … 1409 1428 ] 1410 1429 qed. 1411 *)
Note: See TracChangeset
for help on using the changeset viewer.