source: src/ASM/PolicyStep.ma @ 2222

Last change on this file since 2222 was 2220, checked in by sacerdot, 7 years ago

Some minor speed up and daemon-uncommenting.

File size: 56.2 KB
Line 
1include "ASM/PolicyFront.ma".
2include alias "basics/lists/list.ma".
3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
5
6lemma jump_expansion_step1:
7 ∀program : Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l.
8 ∀prefix,x,tl. pi1 … program=prefix@[x]@tl →
9 ∀labels: label_map.
10 ∀old_sigma : ppc_pc_map.
11 ∀inc_added : ℕ.
12 ∀inc_pc_sigma : ppc_pc_map.
13 ∀label : (option Identifier).
14 ∀instr : pseudo_instruction.
15 ∀inc_pc : ℕ.
16 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
17 ∀old_length : jump_length.
18 ∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉.
19 ∀policy : ppc_pc_map.
20 ∀new_length : jump_length.
21 ∀isize : ℕ.
22 let add_instr ≝ match instr with
23  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
24  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
25  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
26  | _             ⇒ None ?
27  ] in
28 ∀Heq1 :
29  match add_instr with 
30   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
31   |Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉]
32   =〈new_length,isize〉.
33 ∀Heq2 :
34   〈inc_pc+isize,
35     insert … (bitvector_of_nat … (S (|prefix|)))
36      〈inc_pc+isize, \snd  (lookup … (bitvector_of_nat … (S (|prefix|))) (\snd  old_sigma) 〈O,short_jump〉)〉
37      (insert … (bitvector_of_nat … (|prefix|)) 〈inc_pc,new_length〉 inc_sigma)〉
38   = policy.
39  not_jump_default (prefix@[〈label,instr〉]) policy.
40 #program #prefix #x #tl #prf #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
41 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
42 #i >append_length <commutative_plus #Hi normalize in Hi;
43 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
44 [ <Heq2 >lookup_insert_miss
45   [ >lookup_insert_miss
46     [ >(nth_append_first ? i prefix ?? Hi)
47       @(Hpolicy i Hi)
48     | @bitvector_of_nat_abs
49       [ @(transitive_lt ??? Hi) ]
50       [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
51         @le_plus_n_r
52       | @lt_to_not_eq @Hi
53       ]
54     ]
55   | @bitvector_of_nat_abs
56     [ @(transitive_lt ??? Hi) @le_S_to_le ]
57     [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
58       <plus_n_Sm @le_S_S @le_plus_n_r
59     | @lt_to_not_eq @le_S @Hi
60     ]
61   ]
62 | <Heq2 >Hi >lookup_insert_miss
63   [ >lookup_insert_hit cases instr in Heq1;
64     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
65     |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
66       [1,3: <minus_n_n whd in match (nth ????); %
67       |2,4: @le_n
68       ]
69     |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
70       [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:
71         [1,2,3,6,7,24,25: #x #y
72         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
73         <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
74       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
75         #_ #H @⊥ cases H #H2 @H2 %
76       ]
77     ]
78   | @bitvector_of_nat_abs
79     [ @le_S_to_le ]
80     [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S
81       >append_length <plus_n_Sm @le_S_S @le_plus_n_r
82     | @lt_to_not_eq @le_n
83     ]
84   ]
85 ]
86qed.
87
88(* One step in the search for a jump expansion fixpoint. *)
89definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
90  S (|l|) < 2^16 ∧ is_well_labelled_p l).
91  ∀labels:(Σlm:label_map.∀l.
92    occurs_exactly_once ?? l program →
93    bitvector_of_nat ? (lookup_def … lm l 0) =
94    address_of_word_labels_code_mem program l).
95  ∀old_policy:(Σpolicy:ppc_pc_map.
96    (* out_of_program_none program policy *)
97    And (And (And (And (not_jump_default program policy)
98    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
99    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
100    (sigma_compact_unsafe program labels policy))
101    (\fst policy ≤ 2^16)).
102  (Σx:bool × (option ppc_pc_map).
103    let 〈no_ch,y〉 ≝ x in
104    match y with
105    [ None ⇒ nec_plus_ultra program old_policy
106    | Some p ⇒ And (And (And (And (And (And (And
107       (not_jump_default program p)
108       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
109       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
110       (jump_increase program old_policy p))
111       (sigma_compact_unsafe program labels p))
112       (sigma_jump_equal program old_policy p → no_ch = true))
113       (no_ch = true → sigma_pc_equal program old_policy p))
114       (\fst p ≤ 2^16)
115    ])
116    ≝
117  λprogram.λlabels.λold_sigma.
118  let 〈final_added, final_policy〉 ≝
119    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
120    (λprefix.Σx:ℕ × ppc_pc_map.
121      let 〈added,policy〉 ≝ x in
122      And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
123      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
124      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
125      (jump_increase prefix old_sigma policy))
126      (sigma_compact_unsafe prefix labels policy))
127      (sigma_jump_equal prefix old_sigma policy → added = 0))
128      (added = 0 → sigma_pc_equal prefix old_sigma policy))
129      (out_of_program_none prefix policy))
130      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
131       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
132      (sigma_safe prefix labels added old_sigma policy))
133    program
134    (λprefix.λx.λtl.λprf.λacc.
135      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
136      let 〈label,instr〉 ≝ x in
137      (* Now, we must add the current ppc and its pc translation.
138       * Three possibilities:
139       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
140       *   - Instruction is a backward jump; we can use the sigma we're constructing,
141       *     since it will already know the translation of its destination;
142       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
143       *     does not know the translation yet), but compensate for the jumps we
144       *     have lengthened.
145       *)
146      let add_instr ≝ match instr with
147      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
148      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
149      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
150      | _             ⇒ None ?
151      ] in
152      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
153      let old_length ≝
154        \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
155      let old_size ≝ instruction_size_jmplen old_length instr in
156      let 〈new_length, isize〉 ≝ match add_instr with
157      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
158      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
159      ] in
160      let new_added ≝ match add_instr with
161      [ None   ⇒ inc_added
162      | Some x ⇒ plus inc_added (minus isize old_size)
163      ] in
164      let old_Slength ≝
165        \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
166      let updated_sigma ≝
167        (* we add the new PC to the next position and the new jump length to this one *)
168        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
169        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
170      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
171    ) 〈0, 〈0,
172      bvt_insert …
173        (bitvector_of_nat ? 0)
174        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
175        (Stub ??)〉〉
176    ) in
177    if gtb (\fst final_policy) 2^16 then
178      〈eqb final_added 0, None ?〉
179    else
180      〈eqb final_added 0, Some ? final_policy〉.
181[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
182  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
183  (* USE: inc_pc = fst of policy (from fold) *)
184  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
185  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
186  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
187  #Hsig #Hge
188  (* USE: added = 0 → policy_pc_equal (from fold) *)
189  lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|)))
190  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
191    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
192    cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
193    [ #Hj
194      (* USE: policy_increase (from fold) *)
195      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
196      lapply (Habs i Hi Hj)
197      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
198      #opc #oj
199      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
200      #pc #j normalize nodelta #Heq >Heq cases j
201      [1,2: #abs cases abs #abs2 try (cases abs2) @refl
202      |3: #_ @refl
203      ]
204    | #Hnj
205      (* USE: not_jump_default (from fold and old_sigma) *)
206      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi Hnj)
207      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi Hnj)
208      @refl
209    ]
210  | #abs >abs in Hsig; #Hsig
211    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
212  ]
213| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
214  >H2 in H; normalize nodelta -H2 -x #H @conj
215  [ @conj [ @conj
216  [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
217     * jump_increase, sigma_compact_unsafe (from fold) *)
218    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
219  | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
220    @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
221  ]
222  | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
223     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
224  ]
225  | @not_lt_to_le @ltb_false_to_not_lt @p1
226  ]
227|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
228  #inc_pc #inc_sigma #Hips
229  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
230  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
231  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
232  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
233  #Heq1 #Heq2
234  @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
235  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
236   * commented out for full proofs, but this needs a lot of memory and time *)
237  [ (* not_jump_default *)
238    cases (pair_destruct ?????? Heq2) -Heq2 #_ #Heq2
239    @(jump_expansion_step1 … prf … Heq1 Heq2)
240    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
241  | (* 0 ↦ 0 *)
242    <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
243    [ cases (decidable_eq_nat 0 (|prefix|))
244      [ #Heq <Heq >lookup_insert_hit
245        (* USE: inc_pc = fst policy *)
246        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
247        <Heq
248        (* USE[pass]: 0 ↦ 0 *)
249        @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
250      | #Hneq >lookup_insert_miss
251        [ (* USE[pass]: 0 ↦ 0 *) @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
252        | @bitvector_of_nat_abs
253          [3: @Hneq]
254        ]
255      ]
256    | @bitvector_of_nat_abs
257      [3: @lt_to_not_eq @lt_O_S ]
258    ]
259    [1,3: @lt_O_S
260    |2,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
261      [2: <plus_n_Sm @le_S_S]
262      @le_plus_n_r
263    ]
264  ]
265  | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
266    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
267  ]
268  | (* jump_increase *) (* cases daemon *)
269    #i >append_length >commutative_plus #Hi normalize in Hi;
270    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
271    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
272      [ (* USE[pass]: jump_increase *)
273        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i (le_S_to_le … Hi))
274        <(proj2 ?? (pair_destruct ?????? Heq2))
275        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
276        [ >lookup_insert_miss
277          [ @pair_elim #pc #j #EQ2 #X @X
278          | @bitvector_of_nat_abs
279            [ @(transitive_lt ??? Hi) ]
280            [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
281              @le_S_S @le_plus_n_r
282            | @lt_to_not_eq @Hi
283            ]
284          ]
285        | @bitvector_of_nat_abs
286          [ @(transitive_lt ??? Hi) @le_S_to_le ]
287          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
288            >append_length @le_S_S <plus_n_Sm @le_plus_n_r
289          | @lt_to_not_eq @le_S @Hi
290          ]
291        ]
292      | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >Holdeq normalize nodelta
293        >lookup_insert_miss
294        [ >lookup_insert_hit cases (dec_is_jump instr)
295          [ cases instr in Heq1; normalize nodelta
296            [ #pi cases pi
297              [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:
298                [1,2,3,6,7,24,25: #x #y
299                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
300              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
301                whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
302                #_ <(proj1 ?? (pair_destruct ?????? Heq1))
303                @jmpleq_max_length
304              ]
305            |2,3,6: #x [3: #y] #_ #Hj cases Hj
306            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
307            ]
308          | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
309            [ #pi cases pi
310              [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:
311                [1,2,3,6,7,24,25: #x #y
312                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
313                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
314                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
315                (* USE: not_jump_default (from old_sigma) *)
316                lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
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:
318                  >prf >nth_append_second
319                  [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:
320                    <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
321                  |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:
322                    @le_n
323                  ]
324                |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:
325                  >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
326                |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:
327                  >Holdeq #EQ2 >EQ2 %2 @refl
328                ]
329              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
330                #_ #_ #abs @⊥ @(absurd ? I abs)
331              ]
332            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
333              (* USE: not_jump_default (from old_sigma) *)
334              lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
335              [1,4,7: >prf >nth_append_second
336                [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
337                |2,4,6: @le_n
338                ]
339              |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
340              |3,6,9: >Holdeq #EQ2 >EQ2 %2 @refl
341              ]
342            |4,5: #x #_ #_ #abs @⊥ @(absurd ? I abs)
343            ]
344          ]
345        | @bitvector_of_nat_abs
346          [ @le_S_to_le ]
347          [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf
348            >append_length <plus_n_Sm @le_S_S @le_plus_n_r
349          | @lt_to_not_eq @le_n
350          ]
351        ]
352      ]
353    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
354      normalize nodelta
355      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
356      #a #b normalize nodelta %2 @refl
357    ]
358  ]
359  | (* sigma_compact_unsafe *)
360    #i >append_length <commutative_plus #Hi normalize in Hi;
361    <(proj2 ?? (pair_destruct ?????? Heq2))
362    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
363    [ >lookup_opt_insert_miss
364      [ >lookup_opt_insert_miss
365        [ >lookup_opt_insert_miss
366          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
367            [ >lookup_opt_insert_miss
368              [ (* USE[pass]: sigma_compact_unsafe *)
369                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
370                [ @le_S_to_le @Hi ]
371                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
372                [ normalize nodelta #X @X
373                | #x cases x -x #x1 #x2
374                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
375                  normalize nodelta
376                  [ #X @X
377                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
378                    [ #X @X
379                    | @le_S_to_le @Hi
380                    ]
381                  ]
382                ]
383              | @bitvector_of_nat_abs
384                [3: @lt_to_not_eq @Hi ]
385              ]
386            | >Hi >lookup_opt_insert_hit normalize nodelta
387              (* USE[pass]: sigma_compact_unsafe *)
388              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
389              [ <Hi @le_n
390              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
391                [ normalize nodelta #X @X
392                | #x cases x -x #x1 #x2
393                  (* USE: inc_pc = fst inc_sigma *)
394                  lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
395                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
396                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
397                  [ normalize nodelta #_  #_ #H cases H
398                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
399                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
400                      #Heq2 <Heq2 #X @X
401                    | <Hi @le_n
402                    ]
403                  ]
404                ]
405              ]
406            ]
407          ]
408        ]
409      ]
410      [3,4,5: @bitvector_of_nat_abs]
411      [ @(transitive_lt ??? (le_S_S … Hi))
412      |3: @lt_to_not_eq @le_S_S @Hi
413      |4,7,10: @(transitive_lt ??? Hi) @le_S_to_le
414      |5,11: @le_S_to_le
415      |6: @lt_to_not_eq @Hi
416      |9: @lt_to_not_eq @le_S @Hi
417      ]
418      @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
419        <plus_n_Sm @le_S_S @le_plus_n_r
420    | >Hi >lookup_opt_insert_miss
421      [2: @bitvector_of_nat_abs
422        [ @le_S_to_le ]
423        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
424          <plus_n_Sm @le_S_S @le_plus_n_r
425        | @lt_to_not_eq @le_n
426        ]
427      ]
428      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
429      (* USE: out_of_program_none ← *)
430      lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?))
431      [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r
432      | >Hi
433        (* USE: inc_pc = fst policy *)
434        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
435        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
436        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
437        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
438          [ @H %
439          | @le_to_not_lt @le_n
440          ]
441        | #x cases x -x #x1 #x2 #Heq #Hip #_ >nth_append_second
442          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
443          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
444          cases instr in Heq1;
445          [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
446            <(proj1 ?? (pair_destruct ?????? Heq1)) %
447          |4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
448            <(proj1 ?? (pair_destruct ?????? Heq1)) %
449          |1: #pi cases pi normalize nodelta
450            [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:
451              [1,2,3,6,7,24,25: #x #y
452              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
453              #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
454              <(proj1 ?? (pair_destruct ?????? Heq1)) %
455            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
456              <(proj2 ?? (pair_destruct ?????? Heq1))
457              <(proj1 ?? (pair_destruct ?????? Heq1)) %
458            ]
459          ]
460        ]
461      ]
462    ]
463  ]
464  | (* policy_jump_equal → added = 0 *)
465    <(proj2 ?? (pair_destruct ?????? Heq2))
466    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
467    (* USE[pass]: policy_jump_equal → added = 0 *)
468    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?)
469    [ cases instr in Heq1 Heq;
470      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
471      |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
472        #Heq lapply Holdeq -Holdeq
473        (* USE: inc_pc = fst inc_sigma *)
474        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
475        lapply (Heq (|prefix|) ?)
476        [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
477        -Heq >lookup_insert_miss
478        [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
479          #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
480          #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n %
481        |2,4: @bitvector_of_nat_abs
482          [1,4: @le_S_to_le]
483          [1,2,3,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
484            <plus_n_Sm @le_S_S @le_plus_n_r
485          |4,6: @lt_to_not_eq @le_n
486          ]
487        ]
488      |1: #pi cases pi normalize nodelta
489        [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:
490          [1,2,3,6,7,24,25: #x #y
491          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #_ @refl
492        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
493          <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq -Holdeq
494          (* USE: inc_pc = fst inc_sigma *)
495          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
496          lapply (Heq (|prefix|) ?)
497          [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
498          -Heq >lookup_insert_miss
499          [1,3,5,7,9,11,13,15,17: >lookup_insert_hit in ⊢ (???(???%) → ?); <(proj1 ?? (pair_destruct ?????? Heq1))
500            #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
501            #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
502          |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
503            [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
504            |1,4,7,10,13,16,19,22,25: @le_S_to_le
505            ]
506            @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S
507              >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
508          ]
509        ]
510      ]
511    | #i #Hi lapply (Heq i ?)
512      [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
513      | >lookup_insert_miss
514        [ >lookup_insert_miss
515          [ / by /
516          | @bitvector_of_nat_abs
517            [ @(transitive_lt ??? Hi) ]
518            [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
519              @le_plus_n_r
520            | @lt_to_not_eq @Hi
521            ]
522          ]
523        | @bitvector_of_nat_abs
524          [ @(transitive_lt ??? Hi) @le_S_to_le ]
525          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
526            <plus_n_Sm @le_S_S @le_plus_n_r
527          | @lt_to_not_eq @le_S @Hi
528          ]
529        ]
530      ]
531    ]
532  ]
533  | (* added = 0 → policy_pc_equal *) cases daemon
534    (* USE[pass]: added = 0 → policy_pc_equal *)
535    (* lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
536    <(proj2 ?? (pair_destruct ?????? Heq2))
537    <(proj1 ?? (pair_destruct ?????? Heq2))
538    lapply Heq1 -Heq1 lapply (refl ? instr)
539    cases instr in ⊢ (???% → % → %); normalize nodelta
540    [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
541      #Hi normalize in Hi;
542      cases (le_to_or_lt_eq … Hi) -Hi #Hi
543      [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
544        [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
545          [1,3,5: >lookup_insert_miss
546            [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
547            |2,4,6: @bitvector_of_nat_abs
548              [3,6,9: @lt_to_not_eq @Hi
549              |1,4,7: @(transitive_lt ??? Hi)
550              ]
551              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
552              @le_S_S <plus_n_Sm @le_S @le_plus_n_r
553            ]
554          |2,4,6: @bitvector_of_nat_abs
555            [3,6,9: @lt_to_not_eq @le_S @Hi
556            |1,4,7: @(transitive_lt … Hi) @le_S_to_le
557            ]
558            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
559              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
560          ]
561        |2,4,6: >Hi >lookup_insert_miss
562          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
563            @sym_eq (* USE: fst p = lookup |prefix| *)
564            @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
565          |2,4,6: @bitvector_of_nat_abs
566            [3,6,9: @lt_to_not_eq @le_n
567            |1,4,7: @le_S_to_le
568            ]
569            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
570              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
571          ]
572        ]
573      |2,4,6: >Hi >lookup_insert_hit
574        (* USE fst p = lookup |prefix| *)
575        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
576        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
577        (* USE: sigma_compact (from old_sigma) *)
578        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
579        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
580        |2,4,6:
581          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
582          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
583          [1,3,5: normalize nodelta #_ #ABS cases ABS
584          |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
585            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
586            [1,3,5: normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
587            |2,4,6: normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
588              normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
589              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
590              >prf >p1 >Hins >nth_append_second
591              [2,4,6: @(le_n (|prefix|))
592              |1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
593                 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by /
594              ]
595            ]
596          ]
597        ]
598      ]
599    |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
600       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
601       [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
602         [1,3: >lookup_insert_miss
603           [1,3: >lookup_insert_miss
604             [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded;
605               @plus_zero_zero
606             |2,4: @bitvector_of_nat_abs
607               [3,6: @lt_to_not_eq @Hi
608               |1,4: @(transitive_lt ??? Hi)
609               ]
610               @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
611               >append_length @le_plus_n_r
612             ]
613           |2,4: @bitvector_of_nat_abs
614             [3,6: @lt_to_not_eq @le_S @Hi
615             |1,4: @(transitive_lt ??? Hi) @le_S_to_le
616             ]
617             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
618             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
619           ]
620         |2,4: >Hi >lookup_insert_miss
621           [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
622             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
623             (* USE: fst p = lookup |prefix| *)
624             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
625           |2,4: @bitvector_of_nat_abs
626             [3,6: @lt_to_not_eq @le_n
627             |1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
628             ]
629             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
630             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
631           ]
632         ]
633       |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
634         elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
635         [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1))
636           @jump_length_le_max / by I/
637         |2,4: #H (* USE: fst p = lookup |prefix| *)
638           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
639           <(Hold ? (|prefix|) (le_n (|prefix|)))
640           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
641             >(jump_length_equal_max … H)
642             [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *)
643               lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
644               [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
645               |2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
646                 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
647                 [1,3: normalize nodelta #_ #_ #ABS cases ABS
648                 |2,4: normalize nodelta
649                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
650                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
651                   [1,3: #_ #x cases x -x #pc #j normalize nodelta #_ #_ #ABS cases ABS
652                   |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
653                     normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
654                     >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
655                     >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
656                     [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
657                     |2,4: @le_n
658                     ]
659                   ]
660                 ]
661               ]
662             |2,4: / by I/
663             ]
664           |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded]
665           ]
666         ]
667       ]
668     |1: #pi cases pi normalize nodelta
669      [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:
670        [1,2,3,6,7,24,25: #x #y
671        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
672        #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
673        cases (le_to_or_lt_eq … Hi) -Hi #Hi
674        [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:
675          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
676          [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:
677            <(proj2 ?? (pair_destruct ?????? Heq2))
678            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
679            [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:
680              >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma)
681              [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:
682                @(Hold Hadded i (le_S_to_le … Hi))
683              |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:
684                @bitvector_of_nat_abs
685                [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:
686                  @lt_to_not_eq @Hi
687                |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:
688                  @(transitive_lt ??? Hi)
689                ]
690                @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
691                @le_S_S <plus_n_Sm @le_S @le_plus_n_r
692              ]
693            |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:
694              @bitvector_of_nat_abs
695              [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:
696                @lt_to_not_eq @le_S @Hi
697              |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:
698                @(transitive_lt … Hi) @le_S_to_le
699              ]
700              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
701              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
702            ]
703          |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:
704            >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
705            [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:
706              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
707              (* USE: fst p = lookup |prefix| *)
708              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
709            |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:
710              @bitvector_of_nat_abs
711              [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:
712                @lt_to_not_eq @le_n
713              |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:
714                @le_S_to_le
715              ]
716              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
717                @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
718            ]
719          ]
720        |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:
721          >Hi >lookup_insert_hit
722          (* USE fst p = lookup |prefix| *)
723          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
724          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
725          (* USE: sigma_compact (from old_sigma) *)
726          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
727          [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:
728            >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
729          |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:
730            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
731            cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
732            [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:
733              normalize nodelta #_ #ABS cases ABS
734            |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:
735              lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
736              cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
737              [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:
738                normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
739              |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:
740                normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
741                normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
742                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
743                >prf >p1 >Hins >nth_append_second
744                [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:
745                  @(le_n (|prefix|))
746                |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:
747                  <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
748                  #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H
749                ]
750              ]
751            ]
752          ]
753        ]
754      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded
755        #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
756        -Hi #Hi
757        [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
758          [1,3,5,7,9,11,13,15,17:
759            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
760            [1,3,5,7,9,11,13,15,17:
761              >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc,new_length〉 16 (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i) inc_sigma)
762              [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi))
763                >commutative_plus in Hadded; @plus_zero_zero
764              |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
765                [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
766                |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi)
767                ]
768                @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
769                >append_length @le_plus_n_r
770              ]
771            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
772              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
773              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le
774              ]
775              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
776              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
777            ]
778          |2,4,6,8,10,12,14,16,18: >Hi
779            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
780            [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
781              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
782              (* USE: fst p = lookup |prefix| *)
783              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
784            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
785              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
786              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
787              ]
788              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
789              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
790            ]
791          ]
792        |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
793          elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
794          [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt
795            <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/
796          |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *)
797            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
798            <(Hold ? (|prefix|) (le_n (|prefix|)))
799            [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
800              >(jump_length_equal_max … H)
801              [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *)
802                lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
803                [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
804                |2,4,6,8,10,12,14,16,18: lapply Holdeq
805                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
806                  cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
807                  [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS
808                  |2,4,6,8,10,12,14,16,18: normalize nodelta
809                    lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
810                    cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
811                    [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta
812                      #_ #_ #ABS cases ABS
813                    |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x
814                      #pc #j #EQ
815                      normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
816                      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
817                      >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
818                      [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
819                      |2,4,6,8,10,12,14,16,18: @le_n
820                      ]
821                    ]
822                  ]
823                ]
824              |2,4,6,8,10,12,14,16,18: / by I/
825              ]
826            |2,4,6,8,10,12,14,16,18: @plus_zero_zero
827              [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded]
828            ]
829          ]
830        ]
831      ]
832    ] *)
833  ]
834  | (* out_of_program_none *) cases daemon
835    (* #i #Hi2 >append_length <commutative_plus @conj
836    [ (* → *) #Hi normalize in Hi;
837      cases instr in Heq2; normalize nodelta
838      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
839      [1,3,5,7,9,11: >lookup_opt_insert_miss
840        [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *)
841          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2))
842          @le_S_to_le @Hi
843        |2,4,6,8,10,12: @bitvector_of_nat_abs
844          [1,4,7,10,13,16: @Hi2
845          |2,5,8,11,14,17: @(transitive_lt … Hi2)
846          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
847          ] @le_S_to_le @Hi
848        ]
849      |2,4,6,8,10,12: @bitvector_of_nat_abs
850        [1,4,7,10,13,16: @Hi2
851        |2,5,8,11,14,17: @(transitive_lt … Hi2)
852        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
853        ] @Hi
854      ]
855    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
856      elim (decidable_lt i (|prefix|))
857      [ #Hi
858        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
859        #Hl2 (* USE[pass]: out_of_program_none ← *)
860        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
861        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
862      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
863        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
864          [ / by /
865          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
866          ]
867        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
868          >X >eq_bv_refl #H normalize in H; destruct (H)
869        ]
870      ]
871    ] *)
872  ]
873  | (* lookup p = lookup old_sigma + added *) cases daemon
874    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
875    >lookup_insert_hit
876    <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1;
877    [2,3,6: #x [3: #y] normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
878      (* USE: sigma_compact_unsafe (from old_sigma) *)
879      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
880      [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
881      |2,4,6: lapply Holdeq -Holdeq
882        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
883        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
884        [1,3,5: normalize nodelta #_ #_ #abs cases abs
885        |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
886          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
887          [1,3,5: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
888          |2,4,6: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
889            #H (* USE: fst p = lookup |prefix| *)
890            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
891            (* USE[pass]: lookup p = lookup old_sigma + added *)
892            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
893            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
894            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
895            [1,3,5: <minus_n_n >p1 whd in match (nth ????); >associative_plus
896              >(associative_plus pc) @plus_left_monotone >commutative_plus
897              @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
898            |2,4,6: @le_n
899            ]
900          ]
901        ]
902      ]
903    |4,5: #x normalize nodelta #p1 #Heq1
904      (* USE: sigma_compact_unsafe (from old_sigma) *)
905      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
906      [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
907      |2,4: lapply Holdeq -Holdeq
908        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
909        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
910        [1,3: normalize nodelta #_ #_ #abs cases abs
911        |2,4: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
912          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
913          [1,3: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
914          |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
915            #H (* USE: fst p = lookup |prefix| *)
916            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
917            (* USE[pass]: lookup p = lookup old_sigma + added *)
918            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
919            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
920            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
921            >(associative_plus pc) @plus_left_monotone >assoc_plus1
922            >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
923            [1,3: >(proj2 ?? (pair_destruct ?????? EQ)) >prf >nth_append_second
924              [1,3: <minus_n_n whd in match (nth ????); >p1 >commutative_plus
925                @minus_plus_m_m
926              |2,4: @le_n
927              ]
928            |2,4: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max @I
929            ]
930          ]
931        ]
932      ]
933    |1: #pi cases pi
934      [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:
935        [1,2,3,6,7,24,25: #x #y
936        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
937        normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
938        (* USE: sigma_compact_unsafe (from old_sigma) *)
939        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
940        [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:
941          >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
942        |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:
943          lapply Holdeq -Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
944          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
945          [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:
946            normalize nodelta #_ #_ #abs cases abs
947          |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:
948            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
949            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
950            [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:
951              normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
952            |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:
953              #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
954              #H (* USE: fst p = lookup |prefix| *)
955              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
956              (* USE[pass]: lookup p = lookup old_sigma + added *)
957              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
958              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
959              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
960              [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:
961                <minus_n_n >p1 whd in match (nth ????); >associative_plus
962                >(associative_plus pc) @plus_left_monotone >commutative_plus
963                @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
964              |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:
965                @le_n
966              ]
967            ]
968          ]
969        ]
970      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta #p1 #Heq1
971      (* USE: sigma_compact_unsafe (from old_sigma) *)
972        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
973        [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
974        |2,4,6,8,10,12,14,16,18: lapply Holdeq -Holdeq
975          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
976          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
977          [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs
978          |2,4,6,8,10,12,14,16,18: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
979            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
980            [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #x cases x -x #Spc #Sj
981              normalize nodelta #_ #_ #abs cases abs
982            |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j
983              #Holdeq #EQ normalize nodelta #H (* USE: fst p = lookup |prefix| *)
984              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
985              (* USE[pass]: lookup p = lookup old_sigma + added *)
986              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
987              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
988              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
989              >(associative_plus pc) @plus_left_monotone >assoc_plus1
990              >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
991              [1,3,5,7,9,11,13,15,17: >(proj2 ?? (pair_destruct ?????? EQ)) >prf
992                >nth_append_second
993                [1,3,5,7,9,11,13,15,17: <minus_n_n whd in match (nth ????); >p1
994                  >commutative_plus @minus_plus_m_m
995                |2,4,6,8,10,12,14,16,18: @le_n
996                ]
997              |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq1))
998                @jump_length_le_max @I
999              ]
1000            ]
1001          ]
1002        ]
1003      ]
1004    ] *)
1005  ]
1006  | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
1007    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
1008    [ >nth_append_first [2: @Hi]
1009      <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
1010      [ >lookup_insert_miss
1011        [ >lookup_insert_miss
1012          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
1013            [ >lookup_insert_miss
1014              [ >lookup_insert_miss
1015                [ (* USE[pass]: sigma_safe *)
1016                  lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
1017                  cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
1018                  #pc #j normalize nodelta
1019                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
1020                  #Spc #Sj normalize nodelta
1021                  cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
1022                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
1023                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
1024                    [1,4,7: *)
1025                 
1026  ]         
1027| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
1028  [ #i cases i
1029    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1030    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
1031    ]
1032  | >lookup_insert_hit @refl
1033  ]
1034  | >lookup_insert_hit @refl
1035  ]
1036  | #i #Hi <(le_n_O_to_eq … Hi)
1037    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
1038    #a #b normalize nodelta %2 @refl
1039  ]
1040  | #i cases i
1041    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1042    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1043    ]
1044  ]
1045  | #_ %
1046  ]
1047  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
1048    (* USE: 0 ↦ 0 (from old_sigma) *)
1049    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
1050  ]
1051  | #i cases i
1052    [ #Hi2 @conj
1053      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
1054      | >lookup_opt_insert_hit #H destruct (H)
1055      ]
1056    | -i #i #Hi2 @conj
1057      [ #Hi >lookup_opt_insert_miss
1058        [ / by refl/
1059        | @bitvector_of_nat_abs
1060          [ @Hi2
1061          | / by /
1062          | @sym_neq @lt_to_not_eq / by /
1063          ]
1064        ]
1065      | #_ @le_S_S @le_O_n
1066      ]
1067    ]
1068  ]
1069  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
1070    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
1071  ]
1072  | #i cases i
1073    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1074    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1075    ]
1076  ]
1077]
1078qed.
1079
Note: See TracBrowser for help on using the repository browser.