Changeset 2141 for src/ASM/PolicyStep.ma
 Timestamp:
 Jun 28, 2012, 8:08:58 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2102 r2141 5 5 6 6 (* One step in the search for a jump expansion fixpoint. *) 7 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (l) < 2^16). 7 definition jump_expansion_step: ∀program:(Σl:list labelled_instruction. 8 S (l) < 2^16 ∧ is_well_labelled_p l). 8 9 ∀labels:(Σlm:label_map.∀l. 9 10 occurs_exactly_once ?? l program → … … 11 12 address_of_word_labels_code_mem program l). 12 13 ∀old_policy:(Σpolicy:ppc_pc_map. 13 And (And (And (And (out_of_program_none program policy)14 (not_jump_default program policy))14 (* out_of_program_none program policy *) 15 And (And (And (And (not_jump_default program policy) 15 16 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 16 17 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd policy) 〈0,short_jump〉))) 18 (sigma_compact_unsafe program labels policy)) 17 19 (\fst policy < 2^16)). 18 20 (Σx:bool × (option ppc_pc_map). … … 22 24  Some p ⇒ And (And (And (And (And (And (And (And (out_of_program_none program p) 23 25 (not_jump_default program p)) 24 (jump_increase program old_policy p))25 (no_ch = true → sigma_compact program labels p))26 26 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 27 27 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 28 (jump_increase program old_policy p)) 29 (sigma_compact_unsafe program labels p)) 28 30 (no_ch = true → sigma_pc_equal program old_policy p)) 29 31 (sigma_jump_equal program old_policy p → no_ch = true)) … … 36 38 (λprefix.Σx:ℕ × ppc_pc_map. 37 39 let 〈added,policy〉 ≝ x in 38 And (And (And (And (And (And (And (And ( out_of_program_none prefix policy)40 And (And (And (And (And (And (And (And (And (out_of_program_none prefix policy) 39 41 (not_jump_default prefix policy)) 42 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 43 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 40 44 (jump_increase prefix old_sigma policy)) 41 45 (sigma_compact_unsafe prefix labels policy)) 46 (sigma_jump_equal prefix old_sigma policy → added = 0)) 47 (added = 0 → sigma_pc_equal prefix old_sigma policy)) 48 (\fst (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd policy) 〈0,short_jump〉) = 49 \fst (bvt_lookup … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma) 〈0,short_jump〉) + added)) 42 50 (sigma_safe prefix labels added old_sigma policy)) 43 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))44 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉)))45 (added = 0 → sigma_pc_equal prefix old_sigma policy))46 (sigma_jump_equal prefix old_sigma policy → added = 0))47 51 program 48 52 (λprefix.λx.λtl.λprf.λacc. … … 96 100 #x #H #Heq >Heq in H; normalize nodelta Heq x #Hind 97 101 (* USE: inc_pc = fst of policy (from fold) *) 98 >(proj2 ?? (proj1 ?? (proj1 ?? Hind))) in p1;102 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) in p1; 99 103 (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *) 100 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (p i2 ?? old_sigma)))104 lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) 101 105 #Hsig #Hge 102 106 (* USE: added = 0 → policy_pc_equal (from fold) *) 103 lapply ((proj2 ?? (proj1 ?? Hind)) ? (program) (le_n (program))) 104 [ @(proj2 ?? Hind) #i #Hi 107 lapply ((proj2 ?? (proj1 ?? (proj1 ?? Hind))) ? (program) (le_n (program))) 108 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 109 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) #i #Hi 105 110 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 106 111 [ #Hj 107 112 (* USE: policy_increase (from fold) *) 108 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))113 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) i (le_S_to_le … Hi)) 109 114 lapply (Habs i Hi Hj) 110 115 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉) … … 117 122  #Hnj 118 123 (* USE: not_jump_default (from fold and old_sigma) *) 119 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))))) i Hi Hnj)120 >(proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)124 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj) 125 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj) 121 126 @refl 122 127 ] … … 126 131  normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 127 132 >H2 in H; normalize nodelta H2 x #H @conj 128 [ @conj [ @conj [ @conj [ @conj [ @conj 129 [ (* USE[pass]: out_of_program_none, not_jump_default, policy_increase (from fold) *) 130 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))) 131  (* policy_compact_unsafe → policy_compact (in the end) *) 132 #Hch #i #Hi 133 (* USE: policy_compact_unsafe (from fold) *) 134 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) i Hi) 135 (* USE: policy_safe (from fold) *) 136 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) i Hi) 137 lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy))) 138 cases (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)) in ⊢ (???% → %); 139 [ / by / 140  #x cases x x #x1 #x2 #EQ 141 cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd final_policy)) 142 [ / by / 143  #y cases y y #y1 #y2 normalize nodelta #H #H2 144 cut (instruction_size_jmplen x2 145 (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) = 146 instruction_size … (bitvector_of_nat ? i) 147 (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉))) 148 [5: #H3 <H3 @H2 149 4: whd in match (instruction_size_jmplen ??); 150 whd in match (instruction_size …); 151 whd in match (assembly_1_pseudoinstruction …); 152 whd in match (expand_pseudo_instruction …); 153 normalize nodelta whd in match (append …) in H; 154 cases (nth i ? (pi1 ?? program) 〈None ?,Comment []〉) in H; 155 #lbl #instr cases instr 156 [2,3,6: #x [3: #y] normalize nodelta #H @refl 157 4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj 158 lapply (Hj x (refl ? x)) Hj normalize nodelta 159 >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O 160 cases x2 normalize nodelta 161 [1,4: whd in match short_jump_cond; normalize nodelta 162 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 163 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 164 normalize nodelta 165 (* USE: added = 0 → policy_pc_equal *) 166 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 167 [2,4,6,8: @(label_in_program program labels x) 168 cases daemon (* XXX this has to come from somewhere else *) 169 ] 170 [1,5: >(eqb_true_to_eq … Hch) <plus_n_O] 171 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 172 #result #flags normalize nodelta 173 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 174 cases (get_index' bool 2 0 flags) normalize nodelta 175 [1,3,5,7: cases (eq_bv 9 upper ?) 176 2,4,6,8: cases (eq_bv 9 upper (zero 9))] 177 [2,4,6,8,10,12,14,16: #H lapply (proj1 ?? H) #H3 destruct (H3) 178 5,7,13,15: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ 179 1,3,9,11: #_ normalize nodelta @refl 180 ] 181 2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; 182 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 183 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 184 normalize nodelta 185 (* USE: added = 0 → policy_pc_equal *) 186 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 187 [2,4,6,8: @(label_in_program program labels x) 188 cases daemon (* XXX this has to come from somewhere else *)] 189 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 190 normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 191 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 192 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 193 #result #flags normalize nodelta 194 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 195 cases (get_index' bool 2 0 flags) normalize nodelta 196 #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl 197 3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; 198 lapply (refl ? (leb i (lookup_def ?? labels x 0))) 199 cases (leb i (lookup_def ?? labels x 0)) in ⊢ (???% → %); #Hlab 200 normalize nodelta 201 >(proj2 ?? (proj1 ?? H) (eqb_true_to_eq … Hch) (lookup_def ?? labels x 0) ?) 202 [2,4,6,8: @(label_in_program program labels x) 203 cases daemon (* XXX this has to come from somewhere else *)] 204 [1,3: >(eqb_true_to_eq … Hch) <plus_n_O] 205 normalize nodelta 206 cases (vsplit bool 5 11 ?) #addr1 #addr2 207 cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta 208 cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) 209 #result #flags normalize nodelta 210 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 211 cases (get_index' bool 2 0 flags) normalize nodelta 212 #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl 213 ] 214 1: #pi cases pi 215 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 216 [1,2,3,6,7,24,25: #x #y 217 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 218 normalize nodelta #H @refl 219 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 220 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 221 #Hj lapply (Hj x (refl ? x)) Hj 222 whd in match expand_relative_jump; normalize nodelta 223 whd in match expand_relative_jump_internal; normalize nodelta 224 whd in match expand_relative_jump_unsafe; normalize nodelta 225 whd in match expand_relative_jump_internal_unsafe; 226 normalize nodelta >(add_bitvector_of_nat_plus ? i 1) 227 <(plus_n_Sm i 0) <plus_n_O 228 cases daemon (* XXX this needs subadressing mode magic, see above *) 229 ] 230 ] 231 ] 232 ] 233 ] 234 ] 235  (* USE: 0 ↦ 0 (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 236 ] 237  (* USE: inc_pc = fst of policy (from fold) *) @(proj2 ?? (proj1 ?? (proj1 ?? H))) 238 ] 239  #H2 (* USE: added = 0 → policy_pc_equal (from fold) *) 240 @(proj2 ?? (proj1 ?? H)) @eqb_true_to_eq @H2 241 ] 242  #H2 (* USE: policy_jump_equal → added = 0 (from fold *) 243 @eq_to_eqb_true @(proj2 ?? H) @H2 244 ] 245  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 246 ] 247 4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma 133 [ @conj [ @conj 134 [ (* USE[pass]: out_of_program_none, not_jump_default, 0 ↦ 0, inc_pc = fst policy, 135 * jump_increase, sigma_compact_unsafe (from fold) *) 136 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 137  (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *) 138 #H2 @(proj2 ?? (proj1 ?? (proj1 ?? H))) @eqb_true_to_eq @H2 139 ] 140  #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *) 141 @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @H2 142 ] 143  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 144 ] 145 4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %); 146 #inc_pc #inc_sigma #Hips 248 147 lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)) 249 148 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %); 250 #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta 251 @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2 252 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 253 [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj 149 #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim 150 #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta 151 #Heq1 #Heq2 152 @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 153 (* NOTE: to save memory and speed up work, there's cases daemon here. They can be 154 * commented out for full proofs, but this needs a lot of memory and time *) 155 [ (* out_of_program_none *) (* cases daemon *) 156 #i #Hi2 >append_length <commutative_plus @conj 254 157 [ (* → *) #Hi normalize in Hi; 255 158 cases instr in Heq2; normalize nodelta 256 159 #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss 257 160 [1,3,5,7,9,11: >lookup_opt_insert_miss 258 [1,3,5,7,9,11: (* USE : out_of_program_none → *)259 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2))161 [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *) 162 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2)) 260 163 @le_S_to_le @Hi 261 164 2,4,6,8,10,12: @bitvector_of_nat_abs … … 275 178 [ #Hi 276 179 lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl)))) 277 #Hl2 (* USE : out_of_program_none ← *)278 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi2) Hl2)180 #Hl2 (* USE[pass]: out_of_program_none ← *) 181 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2) 279 182 #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 280 183  #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi)) … … 287 190 ] 288 191 ] 289 ] 290  (* not_jump_default *) #i >append_length <commutative_plus #Hi normalize in Hi; 192 ] 193  (* not_jump_default *) (* cases daemon *) 194 #i >append_length <commutative_plus #Hi normalize in Hi; 291 195 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 292 196 [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 293 197 [ >lookup_insert_miss 294 198 [ >(nth_append_first ? i prefix ?? Hi) 295 (* USE : not_jump_default *)296 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i Hi)199 (* USE[pass]: not_jump_default *) 200 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi) 297 201  @bitvector_of_nat_abs 298 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm 299 >commutative_plus @le_plus_a @Hi 300  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S 202 [ @(transitive_lt ??? Hi) ] 203 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 301 204 @le_plus_n_r 302 205  @lt_to_not_eq @Hi … … 304 207 ] 305 208  @bitvector_of_nat_abs 306 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm 307 >commutative_plus @le_plus_a @Hi 308  @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm 309 @le_S_S @le_plus_n_r 209 [ @(transitive_lt ??? Hi) @le_S_to_le ] 210 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 211 <plus_n_Sm @le_S_S @le_plus_n_r 310 212  @lt_to_not_eq @le_S @Hi 311 213 ] … … 328 230 ] 329 231  @bitvector_of_nat_abs 330 [ @ (transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r331  @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm332 @le_S_S @le_plus_n_r232 [ @le_S_to_le ] 233 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S 234 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 333 235  @lt_to_not_eq @le_n 334 ] 335 ] 336 ] 337 ] 338  (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; 236 ] 237 ] 238 ] 239 ] 240  (* 0 ↦ 0 *) (* cases daemon *) 241 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 242 [ cases (decidable_eq_nat 0 (prefix)) 243 [ #Heq <Heq >lookup_insert_hit 244 (* USE: inc_pc = fst policy *) 245 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 246 (* USE[pass]: 0 ↦ 0 *) 247 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 248 <Heq #ONE #TWO >TWO >ONE @refl 249  #Hneq >lookup_insert_miss 250 [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 251  @bitvector_of_nat_abs 252 [3: @Hneq] 253 ] 254 ] 255  @bitvector_of_nat_abs 256 [3: @lt_to_not_eq / by / ] 257 ] 258 [1,3: / by / 259 2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 260 [2: <plus_n_Sm @le_S_S] 261 @le_plus_n_r 262 ] 263 ] 264  (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2)) 265 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 266 ] 267  (* jump_increase *) (* cases daemon *) 268 #i >append_length >commutative_plus #Hi normalize in Hi; 339 269 cases (le_to_or_lt_eq … Hi) Hi; #Hi 340 270 [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 341 [ (* USE : policy_increase *)342 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))271 [ (* USE[pass]: jump_increase *) 272 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) 343 273 <(proj2 ?? (pair_destruct ?????? Heq2)) 344 274 @pair_elim #opc #oj #EQ1 >lookup_insert_miss … … 346 276 [ @pair_elim #pc #j #EQ2 / by / 347 277  @bitvector_of_nat_abs 348 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S349 >commutative_plus @le_plus_a @Hi350  @(transitive_lt … (pi2 ?? program)) >prf >append_length@le_S_S @le_plus_n_r278 [ @(transitive_lt ??? Hi) ] 279 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 280 @le_S_S @le_plus_n_r 351 281  @lt_to_not_eq @Hi 352 282 ] 353 283 ] 354 284  @bitvector_of_nat_abs 355 [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus356 @le_plus_a @Hi357  @(transitive_lt … (pi2 ?? program)) >prf>append_length @le_S_S <plus_n_Sm @le_plus_n_r285 [ @(transitive_lt ??? Hi) @le_S_to_le ] 286 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 287 >append_length @le_S_S <plus_n_Sm @le_plus_n_r 358 288  @lt_to_not_eq @le_S @Hi 359 289 ] … … 384 314 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 385 315 (* USE: not_jump_default (from old_sigma) *) 386 lapply (proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??)316 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 387 317 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 388 318 >prf >nth_append_second … … 404 334 2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) 405 335 (* USE: not_jump_default (from old_sigma) *) 406 lapply (proj 2?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??)336 lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (prefix) ??) 407 337 [1,4,7: >prf >nth_append_second 408 338 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj … … 418 348 ] 419 349  @bitvector_of_nat_abs 420 [ @ (transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r421  @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm422 @le_S_S @le_plus_n_r350 [ @le_S_to_le ] 351 [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf 352 >append_length <plus_n_Sm @le_S_S @le_plus_n_r 423 353  @lt_to_not_eq @le_n 424 354 ] … … 431 361 ] 432 362 ] 433  (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; 363  (* sigma_compact_unsafe *) (* cases daemon *) 364 #i >append_length <commutative_plus #Hi normalize in Hi; 434 365 <(proj2 ?? (pair_destruct ?????? Heq2)) 435 366 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi … … 439 370 [ cases (le_to_or_lt_eq … Hi) Hi #Hi 440 371 [ >lookup_opt_insert_miss 441 [ (* USE : policy_compact_unsafe *)442 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)372 [ (* USE[pass]: sigma_compact_unsafe *) 373 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?) 443 374 [ @le_S_to_le @Hi ] 444 375 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 458 389 ] 459 390  >Hi >lookup_opt_insert_hit normalize nodelta 460 (* USE : policy_compact_unsafe *)461 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)391 (* USE[pass]: sigma_compact_unsafe *) 392 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?) 462 393 [ <Hi @le_n 463 394  cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma) … … 465 396  #x cases x x #x1 #x2 466 397 (* USE: inc_pc = fst inc_sigma *) 467 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Hi468 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))398 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 399 <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)) 469 400 cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %); 470 401 [ normalize nodelta #_ #_ #H cases H … … 482 413 ] 483 414 [3,4,5: @bitvector_of_nat_abs] 484 [1: (* Si < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 485 >commutative_plus @le_plus_a @Hi 486 2,8: (* Spref < 2*16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 415 [ @(transitive_lt ??? (le_S_S … Hi)) 416 3: @lt_to_not_eq @le_S_S @Hi 417 4,7,10: @(transitive_lt ??? Hi) @le_S_to_le 418 5,11: @le_S_to_le 419 6: @lt_to_not_eq @Hi 420 9: @lt_to_not_eq @le_S @Hi 421 ] 422 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 487 423 <plus_n_Sm @le_S_S @le_plus_n_r 488  (* Si ≠ Spref *) @lt_to_not_eq @le_S_S @Hi489 4,7: (* i < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length490 >commutative_plus @le_plus_a @le_S_to_le @Hi491 5,11: (* pref < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length492 @le_plus_n_r493  @lt_to_not_eq @Hi494  @lt_to_not_eq @le_S_to_le @le_S_S @Hi495  @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm496 >commutative_plus @le_plus_a @Hi497 ]498 424  >Hi >lookup_opt_insert_miss 499 425 [2: @bitvector_of_nat_abs 500 [ @ (transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r501  @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S426 [ @le_S_to_le ] 427 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 502 428 <plus_n_Sm @le_S_S @le_plus_n_r 503 429  @lt_to_not_eq @le_n … … 506 432 >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta 507 433 (* USE: out_of_program_none ← *) 508 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) i ?))509 [ >Hi @(transitive_lt … (p i2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r434 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i ?)) 435 [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r 510 436  >Hi 511 437 (* USE: inc_pc = fst policy *) 512 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))438 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 513 439 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma)) 514 440 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) inc_sigma) in ⊢ (???% → %); … … 522 448 cases instr in Heq1; 523 449 [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 524 / by refl/450 <(proj1 ?? (pair_destruct ?????? Heq1)) % 525 451 4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 526 <(proj1 ?? (pair_destruct ?????? Heq1)) @refl452 <(proj1 ?? (pair_destruct ?????? Heq1)) % 527 453 1: #pi cases pi normalize nodelta 528 454 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: … … 530 456 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 531 457 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 532 / by /458 <(proj1 ?? (pair_destruct ?????? Heq1)) % 533 459 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1 534 460 <(proj2 ?? (pair_destruct ?????? Heq1)) 535 <(proj1 ?? (pair_destruct ?????? Heq1)) 536 / by / 537 ] 538 ] 539 ] 461 <(proj1 ?? (pair_destruct ?????? Heq1)) % 462 ] 463 ] 464 ] 540 465 ] 541 466 ] 542 467 ] 543  (* policy_safe *) cases daemon 544 (* #i >append_length >commutative_plus #Hi normalize in Hi; 545 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 546 [ >nth_append_first 547 [2: @Hi] 548 <(proj2 ?? (pair_destruct ?????? Heq2)) 549 >lookup_insert_miss 550 [ >lookup_insert_miss 468  (* policy_jump_equal → added = 0 *) (* cases daemon *) 469 <(proj2 ?? (pair_destruct ?????? Heq2)) 470 #Heq <(proj1 ?? (pair_destruct ?????? Heq2)) 471 (* USE[pass]: policy_jump_equal → added = 0 *) 472 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) ?) 473 [ cases instr in Heq1 Heq; 474 [2,3,6: #x [3: #y] normalize nodelta #_ #_ % 475 4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1)) 476 #Heq lapply Holdeq Holdeq 477 (* USE: inc_pc = fst inc_sigma *) 478 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 479 lapply (Heq (prefix) ?) 480 [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 481 Heq >lookup_insert_miss 482 [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 483 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 484 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by / 485 2,4: @bitvector_of_nat_abs 486 [1,4: @le_S_to_le] 487 [1,2,3,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length 488 <plus_n_Sm @le_S_S @le_plus_n_r 489 4,6: @lt_to_not_eq @le_n 490 ] 491 ] 492 1: #pi cases pi normalize nodelta 493 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 494 [1,2,3,6,7,24,25: #x #y 495 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #_ @refl 496 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1 497 <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq Holdeq 498 (* USE: inc_pc = fst inc_sigma *) 499 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 500 lapply (Heq (prefix) ?) 501 [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 502 Heq >lookup_insert_miss 503 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 504 #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd old_sigma) 〈0,short_jump〉) 505 #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by / 506 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 507 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n 508 1,4,7,10,13,16,19,22,25: @le_S_to_le 509 ] 510 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S 511 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 512 ] 513 ] 514 ] 515  #i #Hi lapply (Heq i ?) 516 [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi 517  >lookup_insert_miss 551 518 [ >lookup_insert_miss 552 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi) 553 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 554 #pc #j cases (nth i ? prefix 〈None ?, Comment []〉) #label #instr cases j 555 normalize nodelta 556 [ #H cases (le_to_or_lt_eq … Hi) Hi #Hi 557 [ >lookup_insert_miss 558 [ #dest #Hjmp <(proj1 ?? (pair_destruct ?????? Heq2)) 519 [ / by / 520  @bitvector_of_nat_abs 521 [ @(transitive_lt ??? Hi) ] 522 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 523 @le_plus_n_r 524  @lt_to_not_eq @Hi 525 ] 526 ] 527  @bitvector_of_nat_abs 528 [ @(transitive_lt ??? Hi) @le_S_to_le ] 529 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S 530 <plus_n_Sm @le_S_S @le_plus_n_r 531  @lt_to_not_eq @le_S @Hi 532 ] 533 ] 534 ] 535 ] *) 536 ] 537  (* added = 0 → policy_pc_equal *) (* cases daemon *) 538 (* USE: added = 0 → policy_pc_equal *) 539 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 540 <(proj2 ?? (pair_destruct ?????? Heq2)) 541 <(proj1 ?? (pair_destruct ?????? Heq2)) 542 lapply Heq1 Heq1 lapply (refl ? instr) 543 cases instr in ⊢ (???% → % → %); normalize nodelta 544 [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 545 #Hi normalize in Hi; 546 cases (le_to_or_lt_eq … Hi) Hi #Hi 547 [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 548 [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 549 [1,3,5: >lookup_insert_miss 550 [1,3,5: @(Hold Hadded i (le_S_to_le … Hi)) 551 2,4,6: @bitvector_of_nat_abs 552 [3,6,9: @lt_to_not_eq @Hi 553 1,4,7: @(transitive_lt ??? Hi) 554 ] 555 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 556 @le_S_S <plus_n_Sm @le_S @le_plus_n_r 557 ] 558 2,4,6: @bitvector_of_nat_abs 559 [3,6,9: @lt_to_not_eq @le_S @Hi 560 1,4,7: @(transitive_lt … Hi) @le_S_to_le 561 ] 562 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 563 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 564 ] 565 2,4,6: >Hi >lookup_insert_miss 566 [1,3,5: >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) 567 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 568 2,4,6: @bitvector_of_nat_abs 569 [3,6,9: @lt_to_not_eq @le_n 570 1,4,7: @le_S_to_le 571 ] 572 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length 573 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 574 ] 575 ] 576 2,4,6: >Hi >lookup_insert_hit 577 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 578 <(Hold Hadded (prefix) (le_n (prefix))) 579 (*<(proj2 ?? (pair_destruct ?????? Heq1))*) 580 (* USE: sigma_compact (from old_sigma) *) 581 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (prefix) ?) 582 [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 583 2,4,6: 584 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma))) 585 cases (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) in ⊢ (???% > %); 586 [1,3,5: normalize nodelta #_ #ABS cases ABS 587 2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma))) 588 cases (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) in ⊢ (???% → %); 589 [1,3,5: normalize nodelta #Hl #x cases x x #pc #j normalize nodelta #Hl2 #ABS cases ABS 590 2,4,6: normalize nodelta #x cases x x #Spc #Sj #EQS #x cases x x #pc #j #EQ 591 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) 592 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 593 >prf >p1 >Hins >nth_append_second 594 [2,4,6: @(le_n (prefix)) 595 1,3,5: <minus_n_n whd in match (nth ????); 596 559 597 560  561 ] 562  563 ] *) 564 ] 565  (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 566 [ cases (decidable_eq_nat 0 (prefix)) 567 [ #Heq <Heq >lookup_insert_hit 568 (* USE: inc_pc = fst policy *) 569 lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) 570 (* USE: 0 ↦ 0 *) 571 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) <Heq 572 #ONE #TWO >TWO >ONE @refl 573  #Hneq >lookup_insert_miss 574 [ (* USE: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) 575  @bitvector_of_nat_abs 576 [3: @Hneq] 577 ] 578 ] 579  @bitvector_of_nat_abs 580 [3: @lt_to_not_eq / by / ] 581 ] 582 [1,3: / by / 583 2,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S 584 [2: <plus_n_Sm @le_S_S] 585 @le_plus_n_r 586 ] 587 ] 588  (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2)) 589 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 590 ] 591  (* added = 0 → policy_pc_equal *) 592 (* USE: added = 0 → policy_pc_equal *) 593 lapply (proj2 ?? (proj1 ?? Hpolicy)) 594 lapply Heq2 Heq2 lapply Heq1 Heq1 lapply (refl ? instr) 595 cases daemon 596 (*cases instr in ⊢ (???% → % → % → %); normalize nodelta 597 [ #pi cases pi normalize nodelta 598 599 ] 600 ] 601 4,5: cases daemon 602 1: cases daemon 603 ] (* 4,5 and 1 are equal to 2,3,6, but casesdaemon'd for the moment because of 604 * memory constraints *) 605 (*#x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus 606 #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi #Hi 607 [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 608 [1,3: >lookup_insert_miss 609 [1,3: >lookup_insert_miss 610 [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; 611 @plus_zero_zero 612 2,4: @bitvector_of_nat_abs 613 [1,4: @(transitive_lt ??? Hi)] 614 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 615 @le_plus_n_r 616 4,6: @lt_to_not_eq @Hi 617 ] 618 ] 619 2,4: @bitvector_of_nat_abs 620 [1,4: @(transitive_lt ??? Hi) @le_S_to_le] 621 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 622 <plus_n_Sm @le_S_S @le_plus_n_r 623 4,6: @lt_to_not_eq @le_S @Hi 624 ] 625 ] 626 2,4: >Hi >lookup_insert_miss 627 [1,3: >lookup_insert_hit >(Hold ? (prefix) (le_n (prefix))) 628 [2,4: >commutative_plus in Hadded; @plus_zero_zero] 629 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 630 2,4: @bitvector_of_nat_abs 631 [1,4: @(transitive_lt ??? (le_S_S … (le_n (prefix))))] 632 [1,2,3,5: @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length 633 <plus_n_Sm @le_S_S @le_plus_n_r 634 4,6: @lt_to_not_eq @le_n 635 ] 636 ] 637 ] 638 2,4: >Hi >lookup_insert_hit 639 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded))) 640 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1)) 641 @etblorp / by I/ 642 2,4: #H >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 643 <(Hold ? (prefix) (le_n (prefix))) 644 <(proj2 ?? (pair_destruct ?????? Heq1)) 645 (* USE: sigma_compact (from old_sigma) *) 646 cases daemon (* XXX add policy_compact_unsafe to old_sigma *) 647 ] 648 ] 649 1: #pi cases pi normalize nodelta 598 650 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 599 651 [1,2,3,6,7,24,25: #x #y 600 652 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 601 #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded 602 #i >append_length >commutative_plus #Hi normalize in Hi; 653 #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; 603 654 cases (le_to_or_lt_eq … Hi) Hi #Hi 604 655 [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: 605 <(proj2 ?? (pair_destruct ?????? Heq2)) 606 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 607 (bitvector_of_nat 16 (S (prefix))) 608 (bitvector_of_nat 16 i)) 656 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 609 657 [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: 610 (* le_to_or_lt_eq, part 2 *) 611 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16 612 (bitvector_of_nat 16 (prefix)) (bitvector_of_nat 16 i)) 613 [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: 614 @(Hold Hadded i (le_S_S_to_le … Hi)) 615 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 616 @bitvector_of_nat_abs 617 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 618 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 619 @le_S_S @le_plus_a @(le_S_S_to_le … Hi) 620 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 621 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S 622 @le_plus_n_r 623 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 624 @lt_to_not_eq @(le_S_to_le … Hi) 658 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 659 [1,3,5: >lookup_insert_miss 660 [1,3,5: @(Hold Hadded i (le_S_to_le … Hi)) 661 2,4,6: @bitvector_of_nat_abs 662 [1,4,7: @(transitive_lt ??? Hi) ] 663 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 664 @le_S_S @le_plus_n_r 665 5,7,9: @lt_to_not_eq @Hi 625 666 ] 626 667 ] 627 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 628 @bitvector_of_nat_abs 629 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 630 @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus 631 @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi) 632 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 633 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 634 @le_S_S @le_plus_n_r 635 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 636 @lt_to_not_eq @le_S_to_le @Hi 637 ] 638 ] 639 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 640 <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi) 641 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 642 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat ? (prefix))) 643 [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: 644 >lookup_insert_hit 645 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 646 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 647 >prf >nth_append_second 648 [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: 649 <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H 650 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 651 @le_n 652 ] 653 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 654 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 655 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 656 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 657 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 658 ] 659 2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: 660 @bitvector_of_nat_abs 661 [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: 662 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r 663 2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: 664 @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm 665 @le_S_S @le_plus_n_r 666 3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: 667 @lt_to_not_eq @le_n 668 ] 669 ] 670 ] 671 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold 672 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 673 #H #i >append_length >commutative_plus #Hi normalize in Hi; 674 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 675 [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2)) 676 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 677 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 i)) 678 [1,3,5,7,9,11,13,15,17: 679 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16 680 (bitvector_of_nat 16 (prefix)) (bitvector_of_nat 16 i)) 681 [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi) 682 [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 683 ] 684 @bitvector_of_nat_abs 685 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 686 >append_length >commutative_plus @le_S @le_plus_a @Hi 687 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 688 >append_length @le_S <plus_n_Sm @le_S_S @le_plus_n_r 689 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi 690 ] 691 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 692 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 693 >append_length >commutative_plus @le_S @le_plus_a @Hi 694 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 695 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 696 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi 697 ] 698 ] 699 2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi 700 >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16 701 (bitvector_of_nat 16 (S (prefix))) (bitvector_of_nat 16 (prefix))) 702 [1,3,5,7,9,11,13,15,17: >lookup_insert_hit 703 <(proj1 ?? (pair_destruct ?????? Heq1)) 704 >Holdeq normalize nodelta @sym_eq @blerpque 705 [3,6,9,12,15,18,21,24,27: 706 elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) 707 [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp 708 2,4,6,8,10,12,14,16,18: #H @H 709 ] 710 / by I/ 711 2,5,8,11,14,17,20,23,26: / by I/ 712 ] 713 2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs 714 [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf 715 >append_length @le_S_S @le_plus_n_r 716 2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf 717 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 718 3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S_S @le_n 719 ] 720 ] 721 ] 722 ] 723 2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) 724 #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; 725 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 726 [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 727 [1,3,5: >lookup_insert_miss 728 [1,3,5: @(Hold Hadded i Hi) 729 2,4,6: @bitvector_of_nat_abs 730 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length 731 >commutative_plus @le_S @le_plus_a @Hi 732 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 733 @le_S <plus_n_Sm @le_S_S @le_plus_n_r 734 3,6,9: @lt_to_not_eq @Hi 735 ] 736 ] 737 2,4,6: @bitvector_of_nat_abs 738 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length 739 >commutative_plus @le_S @le_plus_a @Hi 740 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 741 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 742 3,6,9: @lt_to_not_eq @le_S @Hi 743 ] 744 ] 745 2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss 746 [1,3,5: >lookup_insert_hit 747 lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (prefix) ??) 748 [1,4,7: >prf >nth_append_second 749 [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H 750 2,4,6: @le_n 751 ] 752 2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 753 3,6,9: 754 cases (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) 755 #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl 756 ] 757 2,4,6: @bitvector_of_nat_abs 758 [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf 759 >append_length @le_S_S @le_plus_n_r 760 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf 761 >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 762 3,6,9: @lt_to_not_eq @le_S_S @le_n 763 ] 764 ] 765 ] 766 4,5: #x #Hins #Heq1 #Heq2 #Hold 767 <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) 768 #H #i >append_length >commutative_plus #Hi normalize in Hi; 769 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 770 [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 771 [1,3: >lookup_insert_miss 772 [1,3: @(Hold ? i Hi) 773 [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] 774 ] 775 @bitvector_of_nat_abs 776 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length 777 >commutative_plus @le_S @le_plus_a @Hi 778 2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length 779 @le_S_S @le_plus_n_r 780 3,6: @lt_to_not_eq @Hi 781 ] 782 2,4: @bitvector_of_nat_abs 783 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length 784 >commutative_plus @le_S @le_plus_a @Hi 785 2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length 786 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 787 3,6: @lt_to_not_eq @le_S @Hi 788 ] 789 ] 790 2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss 791 [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) 792 >Holdeq normalize nodelta @sym_eq @blerpque 793 [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) 794 [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp 795 2,4: #H @H 796 ] 797 / by I/ 798 2,5: / by I/ 799 ] 800 2,4: @bitvector_of_nat_abs 801 [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length 802 @le_S_S @le_plus_n_r 803 2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 804 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 805 3,6,9: @lt_to_not_eq @le_S_S @le_n 806 ] 807 ] 808 ] 809 ]*) 810 ] 811  (* policy_jump_equal → added = 0 *) 812 cases daemon 813 ] 814  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 668 2,4,6: @bitvector_of_nat_abs 669 [1,4,7: @(transitive_lt … Hi) @le_S_to_le] 670 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 671 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 672 5,7,9: @lt_to_not_eq @le_S @Hi 673 ] 674 ] 675 2,4,6: >Hi >lookup_insert_miss 676 [1,3,5: >lookup_insert_hit >(Hold Hadded (prefix) (le_n (prefix))) 677 @sym_eq @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 678 2,4,6: @bitvector_of_nat_abs 679 [1,4,7: @(transitive_lt ??? (le_S_S … (le_n (prefix))))] 680 [1,2,3,4,6,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length 681 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r 682 5,7,9: @lt_to_not_eq @le_n 683 ] 684 ] 685 ] 686 2,4,6: >Hi >lookup_insert_hit 687 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 688 <(Hold Hadded (prefix) (le_n (prefix))) 689 <(proj2 ?? (pair_destruct ?????? Heq1)) 690 (* USE: sigma_compact (from old_sigma) *) 691 cases daemon (* XXX add policy_compact_unsafe to old_sigma *) 692 ]*) 693 ] 694  (* lookup p = lookup old_sigma + added *) 695 cases daemon 696 ] 697  (* sigma_safe *) (* cases daemon *) 698 #i >append_length >commutative_plus #Hi normalize in Hi; 699 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 700 [ >nth_append_first [2: @Hi] 701 <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss 702 [ >lookup_insert_miss 703 [ >lookup_insert_miss 704 [ elim (le_to_or_lt_eq … Hi) Hi #Hi 705 [ >lookup_insert_miss 706 [ (* USE[pass]: sigma_safe *) 707 lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi)) 708 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 709 #pc #j cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉) 710 #pc_plus_jmp_length #_ cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins 711 normalize nodelta #Hind #dest #Hj lapply (Hind dest Hj) Hind 712 lapply (refl ? (leb (lookup_def … labels dest 0) (S (prefix)))) 713 cases (leb (lookup_def … labels dest 0) (S (prefix))) in ⊢ (???% → %); 714 normalize nodelta 715 [ #Hle elim (le_to_or_lt_eq … (leb_true_to_le … Hle)) Hle #Hle 716 [ >(le_to_leb_true … (le_S_S_to_le … Hle)) normalize nodelta 717 >lookup_insert_miss 718 [ elim (le_to_or_lt_eq … (le_S_S_to_le … Hle)) Hle #Hle 719 [ >lookup_insert_miss 720 [ cases j / by / 721  @bitvector_of_nat_abs 722 [ @(transitive_lt ??? Hle) ] 723 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) 724 >prf @le_S_S >append_length @le_plus_n_r 725  @lt_to_not_eq @Hle 726 ] 727 ] 728  >Hle >lookup_insert_hit 729 (* USE: inc_pc = fst policy *) 730 <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))) 731 cases j / by / 732 ] 733  @bitvector_of_nat_abs 734 [ @(transitive_lt ??? Hle) ] 735 [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) 736 @le_S_S >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 737  @lt_to_not_eq @Hle 738 ] 739 ] 740  >Hle >lookup_insert_hit >(not_le_to_leb_false (S (prefix)) (prefix)) 741 [2: @le_to_not_lt @le_n ] normalize nodelta 742 (* USE: lookup p = lookup old_sigma + added *) 743 <(proj2 ?? (proj1 ?? Hpolicy)) cases daemon (* use compactness here *) 744 ] 745  (* same, but with forward jump *) cases daemon 746 ] 747  @bitvector_of_nat_abs cases daemon (* trivial, see above *) 748 ] 749  >Hi >lookup_insert_hit cases daemon 750 ] 751  @bitvector_of_nat_abs cases daemon (* see above *) 752 ] 753  @bitvector_of_nat_abs cases daemon 754 ] 755  @bitvector_of_nat_abs cases daemon 756 ] 757  >Hi cases daemon 758 ] *) 759 ] 760  normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj 815 761 [ #i cases i 816 762 [ #Hi2 @conj … … 829 775  #_ @le_S_S @le_O_n 830 776 ] 831 ] 777 ] 832 778  #i cases i 833 779 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 835 781 ] 836 782 ] 783  >lookup_insert_hit @refl 784 ] 785  >lookup_insert_hit @refl 786 ] 837 787  #i #Hi <(le_n_O_to_eq … Hi) 838 788 >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉) … … 844 794 ] 845 795 ] 796  #_ % 797 ] 798  #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit 799 (* USE: 0 ↦ 0 (from old_sigma) *) 800 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) 801 ] 802  cases daemon (* empty program here *) 803 ] 846 804  #i cases i 847 805 [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O … … 849 807 ] 850 808 ] 851  >lookup_insert_hit @refl852 ]853  >lookup_insert_hit @refl854 ]855  #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit856 (* USE: 0 ↦ 0 (from old_sigma *)857 @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))858 ]859  #_ @refl860 ]861 809 ] 862 810 qed.
Note: See TracChangeset
for help on using the changeset viewer.