source: src/ASM/PolicyStep.ma @ 2173

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