Changeset 1606 for src/ASM/Assembly.ma
 Timestamp:
 Dec 14, 2011, 1:40:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1593 r1606 679 679 [ #Hi #l normalize nodelta; cases label normalize nodelta 680 680 [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl 681 lapply ( sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr681 lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 682 682 % [ @addr  @Haddr ] 683 683  #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) Hocc; … … 686 686 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 687 687 @⊥ @(absurd … Hocc) 688  normalize nodelta lapply ( sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)688  normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?) 689 689 [ #addr #Haddr % [ @addr  <Haddr @lookup_add_miss /2/ ] 690 690  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; // … … 832 832 cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?); 833 833 [ #H @H 834  #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? ( sig2 ?? policy) i Hi))834  #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi)) 835 835 @(ex_intro … y (ex_intro … z H)) 836 836 ] 837  #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? ( sig2 ?? policy) i Hi) Hj)837  #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj) 838 838 #H elim H H; #x #H elim H H; #y #H >H in Hnone; #abs destruct (abs) 839 839 ] … … 868 868  CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 869 869  DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 870  _ ⇒ ( eject… policy)870  _ ⇒ (pi1 … policy) 871 871 ] 872 872  Call c ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 873 873  Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (prefix)) 〈0,short_jump〉 policy 874  _ ⇒ ( eject… policy)874  _ ⇒ (pi1 … policy) 875 875 ] 876 876 ) (Stub ? ?). … … 881 881 #i >append_length <commutative_plus #Hi normalize in Hi; 882 882 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 883 #Hi2 cases (le_to_or_lt_eq … Hi) Hi; #Hi @(proj1 ?? (proj1 ?? ( sig2 ?? policy)) i)883 #Hi2 cases (le_to_or_lt_eq … Hi) Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i) 884 884 [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121: 885 885 @le_S_to_le @le_S_to_le @Hi … … 895 895 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 896 896 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) 897 @(proj2 ?? (proj1 ?? ( sig2 ?? policy)) i (le_S_S_to_le … Hi))897 @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 898 898 ] 899 899 @conj >(injective_S … Hi) … … 902 902 ] 903 903 #H elim H; H; #t1 #H elim H; H #t2 #H 904 >(proj1 ?? (proj1 ?? ( sig2 ?? policy)) (prefix) (le_n (prefix)) ?) in H;904 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) in H; 905 905 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 906 906 #H destruct (H) 907 907 ] 908 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S908 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S 909 909 @le_plus_n_r 910 910 ] … … 912 912 Hi; #Hi 913 913 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55,57,59,61: 914 #Hj @(proj2 ?? ( sig2 ?? policy) i (le_S_S_to_le … Hi))914 #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi)) 915 915 >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; // 916 916 ] … … 922 922 #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss 923 923 [1,3,5,7,9,11,13,15,17,19,21: 924 @(proj1 ?? (proj1 ?? ( sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)924 @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 925 925 ] 926 926 >eq_bv_sym @bitvector_of_nat_abs 927 927 [1,4,7,10,13,16,19,22,25,28,31: 928 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S928 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S 929 929 @le_plus_n_r 930 930 2,5,8,11,14,17,20,23,26,29,32: @Hi2 … … 937 937 >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss 938 938 [1,3,5,7,9,11,13,15,17,19,21: 939 @(proj2 ?? (proj1 ?? ( sig2 ?? policy)) i (le_S_S_to_le … Hi))939 @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 940 940 ] 941 941 @bitvector_of_nat_abs … … 943 943 1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 944 944 ] 945 @(transitive_lt … ( sig2 ?? program))945 @(transitive_lt … (pi2 ?? program)) 946 946 >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 947 947 ] … … 957 957 >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss 958 958 [1,3,5,7,9,11,13,15,17,19,21: 959 @(proj2 ?? ( sig2 ?? policy) i (le_S_S_to_le … Hi) Hj)959 @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj) 960 960 ] 961 961 @bitvector_of_nat_abs … … 963 963 1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 964 964 ] 965 @(transitive_lt … ( sig2 ?? program))965 @(transitive_lt … (pi2 ?? program)) 966 966 >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r 967 967 ] … … 1028 1028 [ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi; 1029 1029 [ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr 1030 [ @(proj1 ?? (proj1 ?? ( sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)1030 [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 1031 1031  #z normalize nodelta >lookup_opt_insert_miss 1032 [ @(proj1 ?? (proj1 ?? ( sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)1032 [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2) 1033 1033  >eq_bv_sym @bitvector_of_nat_abs 1034 [ @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1034 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1035 1035 @le_S_S @le_plus_n_r 1036 1036  @Hi2 … … 1041 1041  cases (le_to_or_lt_eq … Hi) Hi; 1042 1042 [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj 1043 [ #Hj lapply (proj2 ?? (proj1 ?? ( sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc1043 [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc 1044 1044 cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y 1045 1045 [ @(proj1 ?? Hacc Hj) … … 1049 1049 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 1050 1050 ] 1051 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1051 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1052 1052 @le_S_S @le_plus_n_r 1053 1053 ] ] 1054 1054 ] 1055  lapply (proj2 ?? (proj1 ?? ( sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc1055  lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc 1056 1056 #H elim H H; #h #H elim H H; #n cases add_instr cases (lookup ??? old_policy ?) 1057 1057 normalize nodelta #x #y [2: #z] … … 1061 1061 1: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) 1062 1062 ] 1063 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1063 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1064 1064 @le_S_S @le_plus_n_r 1065 1065  @Hl … … 1071 1071 [3,5,11: #H @⊥ @H (* instr is not a jump *) 1072 1072 4,6,12: #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 1073 #x #y normalize nodelta >(proj1 ?? (proj1 ?? ( sig2 ?? policy)) (prefix) (le_n (prefix)) ?)1073 #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 1074 1074 [1,3,5: #H destruct (H)] 1075 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1075 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1076 1076 @le_S_S @le_plus_n_r 1077 1077 7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n … … 1095 1095 72,73,74: #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 1096 1096 #x #y normalize nodelta 1097 >(proj1 ?? (proj1 ?? ( sig2 ?? policy)) (prefix) (le_n (prefix)) ?)1097 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 1098 1098 [1,3,5: #H destruct (H)] 1099 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1099 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1100 1100 @le_S_S @le_plus_n_r 1101 1101 41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x 1102 1102 #H elim H H; #h #H elim H H #n cases (lookup ??? old_policy ?) 1103 1103 #x #y normalize nodelta 1104 >(proj1 ?? (proj1 ?? ( sig2 ?? policy)) (prefix) (le_n (prefix)) ?)1104 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 1105 1105 [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)] 1106 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1106 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1107 1107 @le_S_S @le_plus_n_r 1108 1108 38,39,40,43,44,70,71: #x #y #H elim H H; #h #H elim H H #n 1109 1109 cases (lookup ??? old_policy ?) #x #y normalize nodelta 1110 >(proj1 ?? (proj1 ?? ( sig2 ?? policy)) (prefix) (le_n (prefix)) ?)1110 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 1111 1111 [1,3,5,7,9,11,13: #H destruct (H)] 1112 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1112 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1113 1113 @le_S_S @le_plus_n_r 1114 1114 46,47,51,52: #id #_ // … … 1122 1122 cases (le_to_or_lt_eq … Hi) Hi; #Hi 1123 1123 [ cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 1124 #x #y @((proj2 ?? ( sig2 ?? policy)) i (le_S_S_to_le … Hi))1124 #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 1125 1125  normalize nodelta >(injective_S … Hi) 1126 1126 >lookup_opt_lookup_miss … … 1129 1129  cases (lookup ?? (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 1130 1130 #x #y normalize nodelta 1131 >(proj1 ?? (proj1 ?? ( sig2 ?? policy)) (prefix) (le_n (prefix)) ?)1131 >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (prefix) (le_n (prefix)) ?) 1132 1132 [ // 1133  @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1133  @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1134 1134 @le_S_S @le_plus_n_r 1135 1135 ] … … 1160 1160 [ cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 1161 1161 #y #z normalize nodelta normalize nodelta >lookup_insert_miss 1162 [ @((proj2 ?? ( sig2 ?? policy)) i (le_S_S_to_le … Hi))1162 [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) 1163 1163  @bitvector_of_nat_abs 1164 1164 [3: @lt_to_not_eq @(le_S_S_to_le … Hi) 1165 1165 1: @(transitive_lt ??? (le_S_S_to_le … Hi)) 1166 1166 ] 1167 @(transitive_lt … ( sig2 ?? program)) >prf >append_length normalize <plus_n_Sm1167 @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm 1168 1168 @le_S_S @le_plus_n_r 1169 1169 ] 1170  >(injective_S … Hi) elim (proj1 ?? (proj2 ?? ( sig2 ?? old_policy) (prefix) ?) ?)1170  >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (prefix) ?) ?) 1171 1171 [ #a #H elim H H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H) 1172 1172 normalize nodelta >lookup_insert_hit @jmpleq_max_length … … 1207 1207  S m ⇒ jump_expansion_step program (jump_expansion_internal program m) 1208 1208 ]. 1209 [ @(proj1 ?? ( sig2 ?? (jump_expansion_start program)))1210  @(proj1 ?? ( sig2 ?? (jump_expansion_step program (jump_expansion_internal program m))))1209 [ @(proj1 ?? (pi2 ?? (jump_expansion_start program))) 1210  @(proj1 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program m)))) 1211 1211 ] 1212 1212 qed. … … 1249 1249 [ @refl 1250 1250  @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn)) 1251 [ @(proj1 ?? ( sig2 … (jump_expansion_step program p2)))1251 [ @(proj1 ?? (pi2 … (jump_expansion_step program p2))) 1252 1252  @Hnotjmp 1253 1253 ] 1254 1254 ] 1255 1255  @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn)) 1256 [ @(proj1 ?? ( sig2 ?? (jump_expansion_step program p1)))1256 [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1))) 1257 1257  @Hnotjmp 1258 1258 ] … … 1302 1302 (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (program)) 1303 1303 [ #H elim H; H #i #Hi @(ex_intro ?? i) @Hi 1304  #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? ( sig2 ?? (jump_expansion_step program policy)) n Hn)1304  #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) n Hn) 1305 1305 [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn  @Hj ] 1306 1306  #H @H … … 1355 1355 [ #Hp #acc normalize @le_n 1356 1356  #h #t #Hind #Hp #acc 1357 cases (proj2 ?? ( sig2 ?? (jump_expansion_step program policy)) (t) ?)1357 cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (t) ?) 1358 1358 [ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?); 1359 1359 cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) … … 1453 1453 [ @(transitive_le … Hp) // 1454 1454  whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ??)?) in Hm; 1455 lapply (proj2 ?? ( sig2 ?? (jump_expansion_step program policy)) (t) ?)1455 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (t) ?) 1456 1456 [ @(lt_to_le_to_lt … (h::t)) [ //  @Hp ] 1457 1457  cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) in Hm; … … 1476 1476  #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 1477 1477 whd in match (measure_int ?(jump_expansion_step ??)?) in Hm; 1478 lapply (proj2 ?? ( sig2 ?? (jump_expansion_step program policy)) (t) ?)1478 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (t) ?) 1479 1479 [ @(lt_to_le_to_lt … (h::t)) [ //  @Hp ] 1480 1480  cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (t)) policy 〈0,short_jump〉)) in Hm; … … 1501 1501  #h #t #Hind #Hp whd in match (measure_int ???); 1502 1502 cases (dec_is_jump (nth (t) ? program 〈None ?, Comment []〉)) #Hj 1503 [ >(lookup_opt_lookup_hit … (proj2 ?? ( sig2 ?? (jump_expansion_start program)) (t) ? Hj) 〈0,short_jump〉)1503 [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (t) ? Hj) 〈0,short_jump〉) 1504 1504 [ normalize nodelta @Hind @le_S_to_le ] 1505 1505 @Hp … … 1534 1534 [ lapply (measure_full program (jump_expansion_internal program (2*program))) 1535 1535 #Hfull #i #Hi 1536 lapply (proj2 ?? ( sig2 ?? (jump_expansion_step program (jump_expansion_internal program (2*program)))) i Hi)1536 lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program (2*program)))) i Hi) 1537 1537 >(Hfull ? i Hi) 1538 1538 [ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*program))) 〈0,short_jump〉)) … … 1700 1700 match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with 1701 1701 [ None ⇒ λabs. ⊥ 1702  Some r ⇒ λ_.r] ( sig2 … policy).1702  Some r ⇒ λ_.r] (pi2 … policy). 1703 1703 cases abs /2/ 1704 1704 qed. … … 1735 1735 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None …. 1736 1736 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%); 1737 generalize in match ( sig2 ?? pol); whd in prf:(???%); <prf in pol; #pol1737 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol 1738 1738 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0; 1739 1739 normalize nodelta >sigma00_append … … 1774 1774  Some res ⇒ res ]. 1775 1775 [ @⊥ whd in p:(??%??); 1776 generalize in match ( sig2 ?? pol); whd in ⊢ (% → ?);1776 generalize in match (pi2 ?? pol); whd in ⊢ (% → ?); 1777 1777 whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ?  _ ⇒ ?])?) → ?); 1778 1778 generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉))); … … 1848 1848 = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi. 1849 1849 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3 1850 cases ( sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))1850 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3)) 1851 1851 #H1 #_ @H1 1852 1852 qed. … … 1923 1923 whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta; 1924 1924 whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %; 1925 generalize in match ( sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)1925 generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?) 1926 1926 whd in match sigma0; normalize nodelta; 1927 1927 >foldl_step … … 2004 2004 let 〈pc, costs〉 ≝ pc_costs in 2005 2005 〈labels, costs〉. 2006 [2: whd generalize in match ( sig2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH22006 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 2007 2007 generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]] 2008 2008 [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ % … … 2020 2020 <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]] 2021 2021 3: whd % [% [%]] [>sigma_0 %  %  %  #id normalize in ⊢ (% → ?); #abs @⊥ // ] 2022  generalize in match ( sig2 … result) in ⊢ ?;2022  generalize in match (pi2 … result) in ⊢ ?; 2023 2023 normalize nodelta in p ⊢ %; result; >p in ⊢ (match % with [_ ⇒ ?] → ?); 2024 2024 normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
Note: See TracChangeset
for help on using the changeset viewer.