source: src/ASM/PolicyStep.ma @ 2215

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

Some speed up.

File size: 56.8 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 / by /
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)) @pair_elim #opc #oj #EQ1
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)) >Holdeq in EQ1; normalize nodelta
303                #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
304              ]
305            |2,3,6: #x [3: #y] #_ #Hj cases Hj
306            |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq in EQ1;
307              normalize nodelta #H42 >(proj2 ?? (pair_destruct ?????? H42)) @jmpleq_max_length
308            ]
309          | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
310            [ #pi cases pi
311              [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:
312                [1,2,3,6,7,24,25: #x #y
313                |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
314                whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
315                #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
316                (* USE: not_jump_default (from old_sigma) *)
317                lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
318                [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:
319                  >prf >nth_append_second
320                  [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:
321                    <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
322                  |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:
323                    @le_n
324                  ]
325                |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:
326                  >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
327                |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:
328                  cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
329                  #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2
330                  %2 @refl
331                ]
332              |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
333                #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
334              ]
335            |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
336              (* USE: not_jump_default (from old_sigma) *)
337              lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) (|prefix|) ??)
338              [1,4,7: >prf >nth_append_second
339                [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
340                |2,4,6: @le_n
341                ]
342              |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
343              |3,6,9:
344                cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in EQ1;
345                #a #b #EQ1 >(proj2 ?? (pair_destruct ?????? EQ1)) #EQ2 >EQ2 %2 @refl
346              ]
347            |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
348            ]
349          ]
350        | @bitvector_of_nat_abs
351          [ @le_S_to_le ]
352          [1,2: @(transitive_lt … (proj1 ?? (pi2 … program))) @le_S_S >prf
353            >append_length <plus_n_Sm @le_S_S @le_plus_n_r
354          | @lt_to_not_eq @le_n
355          ]
356        ]
357      ]
358    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit
359      normalize nodelta
360      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
361      #a #b normalize nodelta %2 @refl
362    ] *)
363  ]
364  | (* sigma_compact_unsafe *) cases daemon
365    (* #i >append_length <commutative_plus #Hi normalize in Hi;
366    <(proj2 ?? (pair_destruct ?????? Heq2))
367    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
368    [ >lookup_opt_insert_miss
369      [ >lookup_opt_insert_miss
370        [ >lookup_opt_insert_miss
371          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
372            [ >lookup_opt_insert_miss
373              [ (* USE[pass]: sigma_compact_unsafe *)
374                lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
375                [ @le_S_to_le @Hi ]
376                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
377                [ normalize nodelta / by /
378                | #x cases x -x #x1 #x2
379                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
380                  normalize nodelta
381                  [ / by /
382                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
383                    [ / by /
384                    | @le_S_to_le @Hi
385                    ]
386                  ]
387                ]
388              | @bitvector_of_nat_abs
389                [3: @lt_to_not_eq @Hi ]
390              ]
391            | >Hi >lookup_opt_insert_hit normalize nodelta
392              (* USE[pass]: sigma_compact_unsafe *)
393              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
394              [ <Hi @le_n
395              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
396                [ normalize nodelta / by /
397                | #x cases x -x #x1 #x2
398                  (* USE: inc_pc = fst inc_sigma *)
399                  lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
400                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
401                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
402                  [ normalize nodelta #_  #_ #H cases H
403                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
404                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
405                      #Heq2 <Heq2 / by /
406                    | <Hi @le_n
407                    ]
408                  ]
409                ]
410              ]
411            ]
412          ]
413        ]
414      ]
415      [3,4,5: @bitvector_of_nat_abs]
416      [ @(transitive_lt ??? (le_S_S … Hi))
417      |3: @lt_to_not_eq @le_S_S @Hi
418      |4,7,10: @(transitive_lt ??? Hi) @le_S_to_le
419      |5,11: @le_S_to_le
420      |6: @lt_to_not_eq @Hi
421      |9: @lt_to_not_eq @le_S @Hi
422      ]
423      @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
424        <plus_n_Sm @le_S_S @le_plus_n_r
425    | >Hi >lookup_opt_insert_miss
426      [2: @bitvector_of_nat_abs
427        [ @le_S_to_le ]
428        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
429          <plus_n_Sm @le_S_S @le_plus_n_r
430        | @lt_to_not_eq @le_n
431        ]
432      ]
433      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
434      (* USE: out_of_program_none ← *)
435      lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?))
436      [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r
437      | >Hi
438        (* USE: inc_pc = fst policy *)
439        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
440        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
441        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
442        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
443          [ @H %
444          | @le_to_not_lt @le_n
445          ]
446        | #x cases x -x #x1 #x2 #Heq #Hip #_ >nth_append_second
447          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
448          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
449          cases instr in Heq1;
450          [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
451            <(proj1 ?? (pair_destruct ?????? Heq1)) %
452          |4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
453            <(proj1 ?? (pair_destruct ?????? Heq1)) %
454          |1: #pi cases pi normalize nodelta
455            [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:
456              [1,2,3,6,7,24,25: #x #y
457              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
458              #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
459              <(proj1 ?? (pair_destruct ?????? Heq1)) %
460            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
461              <(proj2 ?? (pair_destruct ?????? Heq1))
462              <(proj1 ?? (pair_destruct ?????? Heq1)) %
463            ]
464          ]
465        ]
466      ]
467    ] *)
468  ]
469  | (* policy_jump_equal → added = 0 *) cases daemon
470    (* <(proj2 ?? (pair_destruct ?????? Heq2))
471    #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
472    (* USE[pass]: policy_jump_equal → added = 0 *)
473    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?)
474    [ cases instr in Heq1 Heq;
475      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
476      |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
477        #Heq lapply Holdeq -Holdeq
478        (* USE: inc_pc = fst inc_sigma *)
479        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
480        lapply (Heq (|prefix|) ?)
481        [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
482        -Heq >lookup_insert_miss
483        [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
484          #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
485          #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
486        |2,4: @bitvector_of_nat_abs
487          [1,4: @le_S_to_le]
488          [1,2,3,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
489            <plus_n_Sm @le_S_S @le_plus_n_r
490          |4,6: @lt_to_not_eq @le_n
491          ]
492        ]
493      |1: #pi cases pi normalize nodelta
494        [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:
495          [1,2,3,6,7,24,25: #x #y
496          |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #_ @refl
497        |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
498          <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq -Holdeq
499          (* USE: inc_pc = fst inc_sigma *)
500          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
501          lapply (Heq (|prefix|) ?)
502          [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
503          -Heq >lookup_insert_miss
504          [1,3,5,7,9,11,13,15,17: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
505            #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
506            #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
507          |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
508            [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
509            |1,4,7,10,13,16,19,22,25: @le_S_to_le
510            ]
511            @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S
512              >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
513          ]
514        ]
515      ]
516    | #i #Hi lapply (Heq i ?)
517      [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
518      | >lookup_insert_miss
519        [ >lookup_insert_miss
520          [ / by /
521          | @bitvector_of_nat_abs
522            [ @(transitive_lt ??? Hi) ]
523            [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
524              @le_plus_n_r
525            | @lt_to_not_eq @Hi
526            ]
527          ]
528        | @bitvector_of_nat_abs
529          [ @(transitive_lt ??? Hi) @le_S_to_le ]
530          [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
531            <plus_n_Sm @le_S_S @le_plus_n_r
532          | @lt_to_not_eq @le_S @Hi
533          ]
534        ]
535      ]
536    ] *)
537  ]
538  | (* added = 0 → policy_pc_equal *) cases daemon
539    (* USE[pass]: added = 0 → policy_pc_equal *)
540    (* lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
541    <(proj2 ?? (pair_destruct ?????? Heq2))
542    <(proj1 ?? (pair_destruct ?????? Heq2))
543    lapply Heq1 -Heq1 lapply (refl ? instr)
544    cases instr in ⊢ (???% → % → %); normalize nodelta
545    [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
546      #Hi normalize in Hi;
547      cases (le_to_or_lt_eq … Hi) -Hi #Hi
548      [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
549        [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
550          [1,3,5: >lookup_insert_miss
551            [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
552            |2,4,6: @bitvector_of_nat_abs
553              [3,6,9: @lt_to_not_eq @Hi
554              |1,4,7: @(transitive_lt ??? Hi)
555              ]
556              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
557              @le_S_S <plus_n_Sm @le_S @le_plus_n_r
558            ]
559          |2,4,6: @bitvector_of_nat_abs
560            [3,6,9: @lt_to_not_eq @le_S @Hi
561            |1,4,7: @(transitive_lt … Hi) @le_S_to_le
562            ]
563            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
564              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
565          ]
566        |2,4,6: >Hi >lookup_insert_miss
567          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
568            @sym_eq (* USE: fst p = lookup |prefix| *)
569            @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
570          |2,4,6: @bitvector_of_nat_abs
571            [3,6,9: @lt_to_not_eq @le_n
572            |1,4,7: @le_S_to_le
573            ]
574            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
575              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
576          ]
577        ]
578      |2,4,6: >Hi >lookup_insert_hit
579        (* USE fst p = lookup |prefix| *)
580        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
581        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
582        (* USE: sigma_compact (from old_sigma) *)
583        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
584        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
585        |2,4,6:
586          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
587          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
588          [1,3,5: normalize nodelta #_ #ABS cases ABS
589          |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
590            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
591            [1,3,5: normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
592            |2,4,6: normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
593              normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
594              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
595              >prf >p1 >Hins >nth_append_second
596              [2,4,6: @(le_n (|prefix|))
597              |1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
598                 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by /
599              ]
600            ]
601          ]
602        ]
603      ]
604    |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
605       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
606       [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
607         [1,3: >lookup_insert_miss
608           [1,3: >lookup_insert_miss
609             [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded;
610               @plus_zero_zero
611             |2,4: @bitvector_of_nat_abs
612               [3,6: @lt_to_not_eq @Hi
613               |1,4: @(transitive_lt ??? Hi)
614               ]
615               @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
616               >append_length @le_plus_n_r
617             ]
618           |2,4: @bitvector_of_nat_abs
619             [3,6: @lt_to_not_eq @le_S @Hi
620             |1,4: @(transitive_lt ??? Hi) @le_S_to_le
621             ]
622             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
623             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
624           ]
625         |2,4: >Hi >lookup_insert_miss
626           [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
627             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
628             (* USE: fst p = lookup |prefix| *)
629             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
630           |2,4: @bitvector_of_nat_abs
631             [3,6: @lt_to_not_eq @le_n
632             |1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
633             ]
634             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
635             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
636           ]
637         ]
638       |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
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           @jump_length_le_max / by I/
642         |2,4: #H (* USE: fst p = lookup |prefix| *)
643           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
644           <(Hold ? (|prefix|) (le_n (|prefix|)))
645           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
646             >(jump_length_equal_max … H)
647             [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *)
648               lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
649               [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
650               |2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
651                 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
652                 [1,3: normalize nodelta #_ #_ #ABS cases ABS
653                 |2,4: normalize nodelta
654                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
655                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
656                   [1,3: #_ #x cases x -x #pc #j normalize nodelta #_ #_ #ABS cases ABS
657                   |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
658                     normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
659                     >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
660                     >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
661                     [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
662                     |2,4: @le_n
663                     ]
664                   ]
665                 ]
666               ]
667             |2,4: / by I/
668             ]
669           |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded]
670           ]
671         ]
672       ]
673     |1: #pi cases pi normalize nodelta
674      [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:
675        [1,2,3,6,7,24,25: #x #y
676        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
677        #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
678        cases (le_to_or_lt_eq … Hi) -Hi #Hi
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          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
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            <(proj2 ?? (pair_destruct ?????? Heq2))
683            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
684            [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:
685              >(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)
686              [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:
687                @(Hold Hadded i (le_S_to_le … Hi))
688              |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:
689                @bitvector_of_nat_abs
690                [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:
691                  @lt_to_not_eq @Hi
692                |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:
693                  @(transitive_lt ??? Hi)
694                ]
695                @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
696                @le_S_S <plus_n_Sm @le_S @le_plus_n_r
697              ]
698            |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:
699              @bitvector_of_nat_abs
700              [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:
701                @lt_to_not_eq @le_S @Hi
702              |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:
703                @(transitive_lt … Hi) @le_S_to_le
704              ]
705              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
706              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
707            ]
708          |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:
709            >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
710            [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:
711              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
712              (* USE: fst p = lookup |prefix| *)
713              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
714            |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:
715              @bitvector_of_nat_abs
716              [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:
717                @lt_to_not_eq @le_n
718              |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:
719                @le_S_to_le
720              ]
721              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
722                @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
723            ]
724          ]
725        |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:
726          >Hi >lookup_insert_hit
727          (* USE fst p = lookup |prefix| *)
728          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
729          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
730          (* USE: sigma_compact (from old_sigma) *)
731          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
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            >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
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 ? (|prefix|)) (\snd old_sigma)))
736            cases (bvt_lookup_opt … (bitvector_of_nat ? (|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 #_ #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              lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
741              cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
742              [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:
743                normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
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                normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
746                normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
747                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
748                >prf >p1 >Hins >nth_append_second
749                [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:
750                  @(le_n (|prefix|))
751                |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:
752                  <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
753                  #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H
754                ]
755              ]
756            ]
757          ]
758        ]
759      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded
760        #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
761        -Hi #Hi
762        [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
763          [1,3,5,7,9,11,13,15,17:
764            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
765            [1,3,5,7,9,11,13,15,17:
766              >(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)
767              [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi))
768                >commutative_plus in Hadded; @plus_zero_zero
769              |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
770                [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
771                |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi)
772                ]
773                @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
774                >append_length @le_plus_n_r
775              ]
776            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
777              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
778              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le
779              ]
780              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
781              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
782            ]
783          |2,4,6,8,10,12,14,16,18: >Hi
784            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
785            [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
786              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
787              (* USE: fst p = lookup |prefix| *)
788              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
789            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
790              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
791              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
792              ]
793              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
794              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
795            ]
796          ]
797        |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
798          elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
799          [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt
800            <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/
801          |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *)
802            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
803            <(Hold ? (|prefix|) (le_n (|prefix|)))
804            [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
805              >(jump_length_equal_max … H)
806              [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *)
807                lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
808                [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
809                |2,4,6,8,10,12,14,16,18: lapply Holdeq
810                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
811                  cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
812                  [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS
813                  |2,4,6,8,10,12,14,16,18: normalize nodelta
814                    lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
815                    cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
816                    [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta
817                      #_ #_ #ABS cases ABS
818                    |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x
819                      #pc #j #EQ
820                      normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
821                      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
822                      >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
823                      [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
824                      |2,4,6,8,10,12,14,16,18: @le_n
825                      ]
826                    ]
827                  ]
828                ]
829              |2,4,6,8,10,12,14,16,18: / by I/
830              ]
831            |2,4,6,8,10,12,14,16,18: @plus_zero_zero
832              [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded]
833            ]
834          ]
835        ]
836      ]
837    ] *)
838  ]
839  | (* out_of_program_none *) cases daemon
840    (* #i #Hi2 >append_length <commutative_plus @conj
841    [ (* → *) #Hi normalize in Hi;
842      cases instr in Heq2; normalize nodelta
843      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
844      [1,3,5,7,9,11: >lookup_opt_insert_miss
845        [1,3,5,7,9,11: (* USE[pass]: out_of_program_none → *)
846          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2))
847          @le_S_to_le @Hi
848        |2,4,6,8,10,12: @bitvector_of_nat_abs
849          [1,4,7,10,13,16: @Hi2
850          |2,5,8,11,14,17: @(transitive_lt … Hi2)
851          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
852          ] @le_S_to_le @Hi
853        ]
854      |2,4,6,8,10,12: @bitvector_of_nat_abs
855        [1,4,7,10,13,16: @Hi2
856        |2,5,8,11,14,17: @(transitive_lt … Hi2)
857        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
858        ] @Hi
859      ]
860    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
861      elim (decidable_lt i (|prefix|))
862      [ #Hi
863        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
864        #Hl2 (* USE[pass]: out_of_program_none ← *)
865        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) i Hi2) Hl2)
866        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
867      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
868        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
869          [ / by /
870          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
871          ]
872        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
873          >X >eq_bv_refl #H normalize in H; destruct (H)
874        ]
875      ]
876    ] *)
877  ]
878  | (* lookup p = lookup old_sigma + added *) cases daemon
879    (* <(proj2 ?? (pair_destruct ?????? Heq2)) >append_length <plus_n_Sm <plus_n_O
880    >lookup_insert_hit
881    <(proj1 ?? (pair_destruct ?????? Heq2)) cases instr in p1 Heq1;
882    [2,3,6: #x [3: #y] normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
883      (* USE: sigma_compact_unsafe (from old_sigma) *)
884      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
885      [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
886      |2,4,6: lapply Holdeq -Holdeq
887        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
888        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
889        [1,3,5: normalize nodelta #_ #_ #abs cases abs
890        |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
891          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
892          [1,3,5: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
893          |2,4,6: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
894            #H (* USE: fst p = lookup |prefix| *)
895            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
896            (* USE[pass]: lookup p = lookup old_sigma + added *)
897            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
898            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
899            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
900            [1,3,5: <minus_n_n >p1 whd in match (nth ????); >associative_plus
901              >(associative_plus pc) @plus_left_monotone >commutative_plus
902              @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
903            |2,4,6: @le_n
904            ]
905          ]
906        ]
907      ]
908    |4,5: #x normalize nodelta #p1 #Heq1
909      (* USE: sigma_compact_unsafe (from old_sigma) *)
910      lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
911      [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
912      |2,4: lapply Holdeq -Holdeq
913        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
914        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
915        [1,3: normalize nodelta #_ #_ #abs cases abs
916        |2,4: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
917          cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
918          [1,3: normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
919          |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
920            #H (* USE: fst p = lookup |prefix| *)
921            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
922            (* USE[pass]: lookup p = lookup old_sigma + added *)
923            >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
924            -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
925            >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
926            >(associative_plus pc) @plus_left_monotone >assoc_plus1
927            >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
928            [1,3: >(proj2 ?? (pair_destruct ?????? EQ)) >prf >nth_append_second
929              [1,3: <minus_n_n whd in match (nth ????); >p1 >commutative_plus
930                @minus_plus_m_m
931              |2,4: @le_n
932              ]
933            |2,4: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max @I
934            ]
935          ]
936        ]
937      ]
938    |1: #pi cases pi
939      [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:
940        [1,2,3,6,7,24,25: #x #y
941        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
942        normalize nodelta #p1 #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
943        (* USE: sigma_compact_unsafe (from old_sigma) *)
944        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
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          >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
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 Holdeq -Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
949          cases (bvt_lookup_opt … (bitvector_of_nat ? (|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 #_ #_ #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            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
954            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
955            [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:
956              normalize nodelta #_ #x cases x -x #Spc #Sj normalize nodelta #_ #_ #abs cases abs
957            |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:
958              #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #Holdeq #EQ normalize nodelta
959              #H (* USE: fst p = lookup |prefix| *)
960              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
961              (* USE[pass]: lookup p = lookup old_sigma + added *)
962              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
963              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
964              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second
965              [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:
966                <minus_n_n >p1 whd in match (nth ????); >associative_plus
967                >(associative_plus pc) @plus_left_monotone >commutative_plus
968                @plus_right_monotone @instruction_size_irrelevant @nmk #H @H
969              |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:
970                @le_n
971              ]
972            ]
973          ]
974        ]
975      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta #p1 #Heq1
976      (* USE: sigma_compact_unsafe (from old_sigma) *)
977        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
978        [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
979        |2,4,6,8,10,12,14,16,18: lapply Holdeq -Holdeq
980          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
981          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
982          [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs
983          |2,4,6,8,10,12,14,16,18: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
984            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
985            [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #x cases x -x #Spc #Sj
986              normalize nodelta #_ #_ #abs cases abs
987            |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j
988              #Holdeq #EQ normalize nodelta #H (* USE: fst p = lookup |prefix| *)
989              >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
990              (* USE[pass]: lookup p = lookup old_sigma + added *)
991              >(proj2 ?? (proj1 ?? Hpolicy)) >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
992              -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
993              >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >associative_plus
994              >(associative_plus pc) @plus_left_monotone >assoc_plus1
995              >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
996              [1,3,5,7,9,11,13,15,17: >(proj2 ?? (pair_destruct ?????? EQ)) >prf
997                >nth_append_second
998                [1,3,5,7,9,11,13,15,17: <minus_n_n whd in match (nth ????); >p1
999                  >commutative_plus @minus_plus_m_m
1000                |2,4,6,8,10,12,14,16,18: @le_n
1001                ]
1002              |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq1))
1003                @jump_length_le_max @I
1004              ]
1005            ]
1006          ]
1007        ]
1008      ]
1009    ] *)
1010  ]
1011  | (* sigma_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
1012    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
1013    [ >nth_append_first [2: @Hi]
1014      <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
1015      [ >lookup_insert_miss
1016        [ >lookup_insert_miss
1017          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
1018            [ >lookup_insert_miss
1019              [ >lookup_insert_miss
1020                [ (* USE[pass]: sigma_safe *)
1021                  lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
1022                  cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
1023                  #pc #j normalize nodelta
1024                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
1025                  #Spc #Sj normalize nodelta
1026                  cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
1027                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
1028                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
1029                    [1,4,7: *)
1030                 
1031  ]         
1032| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
1033  [ #i cases i
1034    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1035    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
1036    ]
1037  | >lookup_insert_hit @refl
1038  ]
1039  | >lookup_insert_hit @refl
1040  ]
1041  | #i #Hi <(le_n_O_to_eq … Hi)
1042    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
1043    #a #b normalize nodelta %2 @refl
1044  ]
1045  | #i cases i
1046    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1047    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1048    ]
1049  ]
1050  | #_ %
1051  ]
1052  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
1053    (* USE: 0 ↦ 0 (from old_sigma) *)
1054    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
1055  ]
1056  | #i cases i
1057    [ #Hi2 @conj
1058      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
1059      | >lookup_opt_insert_hit #H destruct (H)
1060      ]
1061    | -i #i #Hi2 @conj
1062      [ #Hi >lookup_opt_insert_miss
1063        [ / by refl/
1064        | @bitvector_of_nat_abs
1065          [ @Hi2
1066          | / by /
1067          | @sym_neq @lt_to_not_eq / by /
1068          ]
1069        ]
1070      | #_ @le_S_S @le_O_n
1071      ]
1072    ]
1073  ]
1074  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
1075    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
1076  ]
1077  | #i cases i
1078    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1079    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
1080    ]
1081  ]
1082]
1083qed.
1084
Note: See TracBrowser for help on using the repository browser.