source: src/ASM/PolicyStep.ma @ 2034

Last change on this file since 2034 was 2034, checked in by boender, 8 years ago
  • split Policy into three separate files for ease (and indeed possibility) of compilation
File size: 43.1 KB
Line 
1include "ASM/PolicyFront.ma".
2
3include alias "basics/lists/list.ma".
4include alias "arithmetics/nat.ma".
5include alias "basics/logic.ma".
6
7(* One step in the search for a jump expansion fixpoint. *)
8definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
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    And (And (And (out_of_program_none program policy)
15    (jump_not_in_policy program policy))
16    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
17    (\fst policy < 2^16)).
18  (Σx:bool × (option ppc_pc_map).
19    let 〈no_ch,y〉 ≝ x in
20    match y with
21    [ None ⇒ nec_plus_ultra program old_policy
22    | Some p ⇒ And (And (And (And (And (And (And (out_of_program_none program p)
23       (jump_not_in_policy program p))
24       (policy_increase program old_policy p))
25       (policy_compact program labels 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       (no_ch = true → policy_equal program old_policy p))
29       (\fst p < 2^16)
30    ])
31    ≝
32  λprogram.λlabels.λold_sigma.
33  let 〈final_added, final_policy〉 ≝
34    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
35    (λprefix.Σx:ℕ × ppc_pc_map.
36      let 〈added,policy〉 ≝ x in
37      And (And (And (And (And (And (And (out_of_program_none prefix policy)
38      (jump_not_in_policy prefix policy))
39      (policy_increase prefix old_sigma policy))
40      (policy_compact_unsafe prefix labels policy))
41      (policy_safe prefix labels policy))
42      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
43      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
44      (added = 0 → policy_equal prefix old_sigma policy))
45    program
46    (λprefix.λx.λtl.λprf.λacc.
47      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
48      let 〈label,instr〉 ≝ x in
49      (* Now, we must add the current ppc and its pc translation.
50       * Three possibilities:
51       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
52       *   - Instruction is a backward jump; we can use the sigma we're constructing,
53       *     since it will already know the translation of its destination;
54       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
55       *     does not know the translation yet), but compensate for the jumps we
56       *     have lengthened.
57       *)
58      let add_instr ≝ match instr with
59      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
60      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
61      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
62      | _             ⇒ None ?
63      ] in
64      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
65      let old_length ≝
66        \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
67      let old_size ≝ instruction_size_jmplen old_length instr in
68      let 〈new_length, isize〉 ≝ match add_instr with
69      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
70      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
71      ] in
72      let new_added ≝ match add_instr with
73      [ None   ⇒ inc_added
74      | Some x ⇒ plus inc_added (minus isize old_size)
75      ] in
76      let updated_sigma ≝
77        (* we add the new PC to the next position and the new jump length to this one *)
78        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, short_jump〉
79        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
80      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
81    ) 〈0, 〈0, bvt_insert … (bitvector_of_nat 16 0) 〈0, short_jump〉 (Stub ??)〉〉) in
82    if geb (\fst final_policy) 2^16 then
83      〈eqb final_added 0, None ?〉
84    else
85      〈eqb final_added 0, Some ? final_policy〉.
86[ normalize nodelta cases daemon (* XXX nec_plus_ultra *)
87| normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2
88  >H2 in H; normalize nodelta -H2 -x #H @conj
89  [ @conj
90    [ @conj
91      [ @conj
92        [ @conj
93          [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
94          | (* policy_compact_unsafe → policy_compact (in the end) *)
95            #i #Hi
96            lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) i Hi)
97            lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))) i Hi)
98            lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)))
99            cases (lookup_opt … (bitvector_of_nat ? i) (\snd final_policy)) in ⊢ (???% → %);
100            [ / by /
101            | #x cases x -x #x1 #x2 #EQ
102              cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd final_policy))
103              [ / by /
104              | #y cases y -y #y1 #y2 normalize nodelta #H #H2
105                cut (
106                  instruction_size_jmplen x2
107                  (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉)) =
108                  instruction_size … (bitvector_of_nat ? i)
109                  (\snd (nth i ? (pi1 ?? program) 〈None ?, Comment []〉))
110                 )
111                [5: #H3 <H3 @H2
112                |4: whd in match (instruction_size_jmplen ??);
113                    whd in match (instruction_size …);
114                    whd in match (assembly_1_pseudoinstruction …);
115                    whd in match (expand_pseudo_instruction …);
116                    normalize nodelta whd in match (append …) in H;
117                    cases (nth i ? (pi1 ?? program) 〈None ?,Comment []〉) in H;
118                    #lbl #instr cases instr
119                    [2,3,6: #x [3: #y] normalize nodelta #H @refl
120                    |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
121                      #Hj lapply (Hj x (refl ? x)) -Hj
122                      normalize nodelta >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
123                      cases x2 normalize nodelta
124                      [1,4:
125                        whd in match short_jump_cond; normalize nodelta
126                        cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
127                        #result #flags normalize nodelta
128                        cases (split bool 8 8 result)
129                        #upper #lower normalize nodelta
130                        cases (eq_bv 8 upper (zero 8))
131                        [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
132                        |1: #_ normalize @refl
133                        |3: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
134                        ]
135                      |2,5: whd in match short_jump_cond; whd in match medium_jump_cond;
136                        normalize nodelta
137                        cases (split bool 5 11 ?) #addr1 #addr2
138                        cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
139                        cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
140                        #result #flags normalize nodelta
141                        cases (split bool 8 8 result)
142                        #upper #lower normalize nodelta
143                        #H >(not_true_is_false ? (proj2 ?? (proj1 ?? H)))
144                        >(proj1 ?? (proj1 ?? H)) normalize @refl
145                      |3,6: whd in match short_jump_cond; whd in match medium_jump_cond;
146                        normalize nodelta
147                        cases (split bool 5 11 ?) #addr1 #addr2
148                        cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
149                        cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
150                        #result #flags normalize nodelta
151                        cases (split bool 8 8 result)
152                        #upper #lower normalize nodelta
153                        #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H))
154                        normalize nodelta normalize @refl
155                      ]
156                    |1: #pi cases pi
157                      [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:
158                        [1,2,3,6,7,24,25: #x #y
159                        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
160                        normalize nodelta #H @refl
161                      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
162                        >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj
163                        [1,2,3,4,5: lapply (Hj y (refl ? y)) | 6,7,8,9: lapply (Hj x (refl ? x))] -Hj
164                        whd in match expand_relative_jump; normalize nodelta
165                        whd in match expand_relative_jump_internal; normalize nodelta
166                        whd in match expand_relative_jump_unsafe; normalize nodelta
167                        whd in match expand_relative_jump_internal_unsafe;
168                        normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
169                        <(plus_n_Sm i 0) <plus_n_O cases x2 normalize nodelta
170                        [1,4,7,10,13,16,19,22,25:
171                          whd in match short_jump_cond; normalize nodelta
172                          cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
173                          #result #flags normalize nodelta
174                          cases (split bool 8 8 result)
175                          #upper #lower normalize nodelta
176                          cases (eq_bv 8 upper (zero 8))
177                          [2,4,6,8,10,12,14,16,18: #H lapply (proj1 ?? H) #H3 destruct (H3)
178                          |1,3,5,7,9,11,13,15,17: #_ normalize nodelta
179                            [6,7,8,9: normalize @refl]
180                            whd in match (map ????);
181                            whd in match (map ??? []);
182                            whd in match (map ????);
183                            whd in match (map ??? []);
184                            normalize cases x
185                            [1,2,3,6: #am cases am normalize nodelta
186                              [1,2,3,4,8,9,16,17,18,19: #z #Ham cases Ham
187                              |5,6,7,10,11,12,13,14: #Ham cases Ham
188                              |15: #z #Ham normalize @refl
189                              |20,21,22,23,27,28,35,36,37,38: #z #Ham cases Ham
190                              |24,25,26,29,30,31,32,33: #Ham cases Ham
191                              |34: #z #Ham normalize @refl
192                              |39,40,41,42,46,47,54,55,56,57: #z #Ham cases Ham
193                              |43,44,45,48,49,50,51,52: #Ham cases Ham
194                              |53: #z #Ham normalize @refl
195                              |59,60,65,66,72,73,74,75,76: #z #Ham cases Ham
196                              |62,63,64,67,68,69,70,71: #Ham cases Ham
197                              |58,61: #z #Ham normalize @refl
198                              ]
199                            ]
200                            #w cases w #w1 #w2 cases w2 #am cases am normalize nodelta
201                            [1,2,3,4,8,9,15,16,17,18,19: #z #Ham @refl
202                            |5,6,7,10,11,12,13,14: #Ham @refl
203                            |20,21,22,23,28: #z #Ham cases Ham
204                            |24,25,26: #Ham cases Ham
205                            |27: #z #Ham cases w1 #am cases am normalize nodelta
206                               [1,2,3,4,8,9,15,16,17,18,19: #z #Ham @refl
207                               |5,6,7,10,11,12,13,14: #Ham @refl
208                               ]
209                            |34,35,36,37,38: #z #Ham cases Ham
210                            |29,30,31,32,33: #Ham cases Ham
211                            ]
212                          ]
213                        |2,5,8,11,14,17,20,23,26:
214                          whd in match short_jump_cond; whd in match medium_jump_cond;
215                          normalize nodelta
216                          cases (split bool 5 11 ?) #addr1 #addr2
217                          cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
218                          cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
219                          #result #flags normalize nodelta
220                          cases (split bool 8 8 result)
221                          #upper #lower normalize nodelta
222                          #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/
223                        |3,6,9,12,15,18,21,24,27:
224                          whd in match short_jump_cond; whd in match medium_jump_cond;
225                          normalize nodelta
226                          cases (split bool 5 11 ?) #addr1 #addr2
227                          cases (split bool 5 11 ?) #pc1 #pc2 normalize nodelta
228                          cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
229                          #result #flags normalize nodelta
230                          cases (split bool 8 8 result)
231                          #upper #lower normalize nodelta
232                          #H >(not_true_is_false ? (proj1 ?? H)) >(not_true_is_false ? (proj2 ?? H))
233                          [6,7,8,9: normalize @refl]
234                          cases x normalize nodelta
235                          [1,2,3,6: #am cases am normalize nodelta
236                            [1,2,3,4,8,9,16,17,18,19: #z #Ham cases Ham
237                            |5,6,7,10,11,12,13,14: #Ham cases Ham
238                            |15: #z #Ham @refl
239                            |20,21,22,23,27,28,35,36,37,38: #z #Ham cases Ham
240                            |24,25,26,29,30,31,32,33: #Ham cases Ham
241                            |34: #z #Ham @refl
242                            |39,40,41,42,46,47,54,55,56,57: #z #Ham cases Ham
243                            |43,44,45,48,49,50,51,52: #Ham cases Ham
244                            |53: #z #Ham @refl
245                            |59,60,65,66,72,73,74,75,76: #z #Ham cases Ham
246                            |62,63,64,67,68,69,70,71: #Ham cases Ham
247                            |58,61: #z #Ham @refl
248                            ]
249                          ]
250                          #w cases w normalize nodelta #w1 #w2 cases w2 normalize nodelta
251                          #am cases am normalize nodelta
252                          [2,3,4,9,15,16,17,18,19: #z #Ham cases Ham
253                          |5,6,7,10,11,12,13,14: #Ham cases Ham
254                          |1,8: #z #Ham @refl
255                          |20,21,22,23,28: #z #Ham cases Ham
256                          |24,25,26: #Ham cases Ham
257                          |27: #z #Ham cases w1 normalize nodelta #am cases am normalize nodelta
258                            [1,3,8,9,15,16,17,18,19: #z #Ham cases Ham
259                            |5,6,7,10,11,12,13,14: #Ham cases Ham
260                            |2,4: #z #Ham @refl
261                            ]
262                          |34,35,36,37,38: #z #Ham cases Ham
263                          |29,30,31,32,33: #Ham cases Ham
264                          ]
265                        ]
266                      ]
267                    ]
268                  ]
269                ]
270              ]
271            ]
272            | @(proj2 ?? (proj1 ?? (proj1 ?? H)))
273          ]
274        | @(proj2 ?? (proj1 ?? H))
275        ]
276      | #H2 @(proj2 ?? H) @eqb_true_to_eq @H2
277      ]
278    | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1
279    ]
280|4: lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma
281  lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉))
282  cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in ⊢ (???% → %);
283  #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta
284  @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2
285  @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
286  [ (* out_of_program_none *) #i #Hi2 >append_length <commutative_plus @conj
287    [ (* → *) #Hi normalize in Hi;
288      cases instr in Heq2; normalize nodelta
289      #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss
290      [1,3,5,7,9,11: >lookup_opt_insert_miss
291        [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi2))
292          @le_S_to_le @Hi
293        |2,4,6,8,10,12: @bitvector_of_nat_abs
294          [1,4,7,10,13,16: @Hi2
295          |2,5,8,11,14,17: @(transitive_lt … Hi2)
296          |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
297          ] @le_S_to_le @Hi
298        ]
299      |2,4,6,8,10,12: @bitvector_of_nat_abs
300        [1,4,7,10,13,16: @Hi2
301        |2,5,8,11,14,17: @(transitive_lt … Hi2)
302        |3,6,9,12,15,18: @sym_neq @lt_to_not_eq
303        ] @Hi
304      ]
305    | (* ← *) <(proj2 ?? (pair_destruct ?????? Heq2)) #Hl
306      elim (decidable_lt i (|prefix|))
307      [ #Hi
308        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
309        #Hl2
310        lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi2) Hl2)
311        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3
312      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
313        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
314          [ / by /
315          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
316          ]
317        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
318          >X >eq_bv_refl #H normalize in H; destruct (H)
319        ]
320      ]
321    ]
322  | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi;
323    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
324    [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
325      [ >lookup_insert_miss
326        [ >(nth_append_first ? i prefix ?? Hi)
327          @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i Hi)
328        | @bitvector_of_nat_abs
329          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
330            >commutative_plus @le_plus_a @Hi
331          | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
332            @le_plus_n_r
333          | @lt_to_not_eq @Hi
334          ]
335        ]
336      | @bitvector_of_nat_abs
337        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
338          >commutative_plus @le_plus_a @Hi
339        | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm
340          @le_S_S @le_plus_n_r
341        | @lt_to_not_eq @le_S @Hi
342        ]
343      ]
344    | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
345      [ >lookup_insert_hit cases instr in Heq1;
346        [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
347        |4,5: #x normalize nodelta #Heq1 #H @⊥ cases H #H @H >nth_append_second
348          [1,3: <minus_n_n whd in match (nth ????); / by I/
349          |2,4: @le_n
350          ]
351        |1: #pi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); cases pi
352          [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:
353            [1,2,3,6,7,24,25: #x #y
354            |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] normalize nodelta #Heq1
355            <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
356          |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] normalize nodelta
357            #_ #H @⊥ cases H #H2 @H2 / by I/
358          ]
359        ]
360      | @bitvector_of_nat_abs
361        [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r
362        | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
363          @le_S_S @le_plus_n_r
364        | @lt_to_not_eq @le_n
365        ]
366      ]
367    ]
368  ]
369  | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi;
370    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi
371    [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i Hi)
372      <(proj2 ?? (pair_destruct ?????? Heq2))     
373      @pair_elim #opc #oj #EQ1 >lookup_insert_miss
374      [ >lookup_insert_miss
375        [ @pair_elim #pc #j #EQ2 / by /
376        | @bitvector_of_nat_abs
377          [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S <commutative_plus
378            @le_plus_a @Hi
379          | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
380          | @lt_to_not_eq @Hi
381          ]
382        ]
383      | @bitvector_of_nat_abs
384        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S >commutative_plus
385          @le_plus_a @Hi
386        | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm @le_plus_n_r
387        | @lt_to_not_eq @le_S @Hi
388        ]
389      ]
390    | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
391      [ >lookup_insert_hit
392        cases (dec_is_jump instr)
393        [ cases instr in Heq1; normalize nodelta
394          [ #pi cases pi
395            [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:
396              [1,2,3,6,7,24,25: #x #y
397              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj
398            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
399              whd in match jump_expansion_step_instruction; normalize nodelta #Heq1
400              <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta
401              @jmpleq_max_length
402            ]
403          |2,3,6: #x [3: #y] #_ #Hj cases Hj
404          |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta
405            @jmpleq_max_length
406          ]
407        | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta
408          [ #pi cases pi
409            [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:
410              [1,2,3,6,7,24,25: #x #y
411              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
412              whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1
413              #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
414              lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
415              [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:
416                >prf >nth_append_second
417                [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:
418                  <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
419                |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:
420                  @le_n
421                ]
422              |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:
423                >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
424              |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:
425                cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
426                #a #b #H >H normalize nodelta %2 @refl
427              ]
428            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
429              #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
430            ]
431          |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1))
432            lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
433            [1,4,7: >prf >nth_append_second
434              [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj
435              |2,4,6: @le_n
436              ]
437            |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
438            |3,6,9: cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
439              #a #b #H >H normalize nodelta %2 @refl
440            ]
441          |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/
442          ]
443        ]
444      | @bitvector_of_nat_abs
445        [ @(transitive_lt … (pi2 … program)) >prf @le_S_S >append_length @le_plus_n_r
446        | @(transitive_lt … (pi2 … program)) @le_S_S >prf >append_length <plus_n_Sm
447          @le_S_S @le_plus_n_r
448        | @lt_to_not_eq @le_n
449        ]
450      ]
451    ]
452  ]
453  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
454    <(proj2 ?? (pair_destruct ?????? Heq2))
455    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
456    [ >lookup_opt_insert_miss
457      [ >lookup_opt_insert_miss
458        [ >lookup_opt_insert_miss
459          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
460            [ >lookup_opt_insert_miss
461              [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
462                [ @le_S_to_le @Hi ]
463                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
464                [ normalize nodelta / by /
465                | #x cases x -x #x1 #x2
466                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
467                  normalize nodelta
468                  [ / by /
469                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
470                    [ / by /
471                    | @le_S_to_le @Hi
472                    ]
473                  ]
474                ]
475              | @bitvector_of_nat_abs
476                [3: @lt_to_not_eq @Hi ]
477              ]
478            | >Hi >lookup_opt_insert_hit normalize nodelta
479              lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i ?)
480              [ <Hi @le_n
481              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
482                [ normalize nodelta / by /
483                | #x cases x -x #x1 #x2
484                  lapply (proj2 ?? (proj1 ?? Hpolicy)) <Hi
485                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
486                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
487                  [ normalize nodelta #_  #_ #H cases H
488                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
489                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
490                      #Heq2 <Heq2 / by /
491                    | <Hi @le_n
492                    ]
493                  ]
494                ]
495              ]
496            ]
497          ]
498        ]
499      ]
500      [3,4,5: @bitvector_of_nat_abs]
501      [1: (* Si < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
502        >commutative_plus @le_plus_a @Hi
503      |2,8: (* Spref < 2*16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
504        <plus_n_Sm @le_S_S @le_plus_n_r
505      | (* Si ≠ Spref *) @lt_to_not_eq @le_S_S @Hi
506      |4,7: (* i < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
507        >commutative_plus @le_plus_a @le_S_to_le @Hi
508      |5,11: (* pref < 2^16 *) @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length
509        @le_plus_n_r
510      | @lt_to_not_eq @Hi
511      | @lt_to_not_eq @le_S_to_le @le_S_S @Hi
512      | @(transitive_lt … (pi2 ?? program)) >prf >append_length >plus_n_Sm
513        >commutative_plus @le_plus_a @Hi
514      ]
515    | >Hi >lookup_opt_insert_miss
516      [2: @bitvector_of_nat_abs
517        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
518        | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
519          <plus_n_Sm @le_S_S @le_plus_n_r
520        | @lt_to_not_eq @le_n
521        ]
522      ]
523      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
524      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) i ?))
525      [ >Hi @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
526      | >Hi
527        lapply (proj2 ?? (proj1 ?? Hpolicy))
528        lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
529        cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
530        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
531          [ @H @refl
532          | @le_to_not_lt @le_n
533          ]
534        | #x cases x -x #x1 #x2 #Heq #Hip #_ >nth_append_second
535          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
536          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
537          cases instr in Heq1;
538          [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
539            / by refl/
540          |4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
541            <(proj1 ?? (pair_destruct ?????? Heq1)) @refl
542          |1: #pi cases pi normalize nodelta
543            [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:
544              [1,2,3,6,7,24,25: #x #y
545              |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
546              #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
547              / by /
548            |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
549              <(proj2 ?? (pair_destruct ?????? Heq1))
550              <(proj1 ?? (pair_destruct ?????? Heq1))
551              / by /
552            ]
553          ]
554        ]   
555      ]
556    ]
557  ]
558  | (* policy_safe *) cases daemon (*#i >append_length >commutative_plus #Hi normalize in Hi;
559    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
560    [ >nth_append_first
561      [2: @Hi]
562      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi)
563      <(proj2 ?? (pair_destruct ?????? Heq2))
564      >lookup_insert_miss
565      [
566      |
567      ]
568    |
569    ] *)
570  ]
571  | (* 0 ↦ 0 *) <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
572    [ cases (decidable_eq_nat 0 (|prefix|))
573      [ #Heq <Heq >lookup_insert_hit
574        lapply (proj2 ?? (proj1 ?? Hpolicy))
575        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) <Heq
576        #ONE #TWO >TWO >ONE @refl
577      | #Hneq >lookup_insert_miss
578        [ @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
579        | @bitvector_of_nat_abs
580          [3: @Hneq]
581        ]
582      ]
583    | @bitvector_of_nat_abs
584      [3: @lt_to_not_eq / by / ]
585    ]     
586    [1,3: / by /
587    |2,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
588      [2: <plus_n_Sm @le_S_S]
589      @le_plus_n_r
590    ]
591  ]
592  | (* inc_pc = fst of policy *) <(proj2 ?? (pair_destruct ?????? Heq2))
593    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
594  ]
595  | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy)
596    lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr)
597    cases instr in ⊢ (???% → % → % → %); normalize nodelta
598    [ #pi cases pi normalize nodelta
599      [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:
600        [1,2,3,6,7,24,25: #x #y
601        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
602        #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded
603        #i >append_length >commutative_plus #Hi normalize in Hi;
604        cases (le_to_or_lt_eq … Hi) -Hi #Hi
605        [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:
606          <(proj2 ?? (pair_destruct ?????? Heq2))
607          >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
608            (bitvector_of_nat 16 (S (|prefix|)))
609            (bitvector_of_nat 16 i))
610          [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:
611            >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
612              (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
613            [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
614              @(Hold Hadded i (le_S_S_to_le … Hi))
615            |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
616              @bitvector_of_nat_abs
617              [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
618                @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
619                @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi)
620              |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
621                @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S
622                @le_plus_n_r
623              |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
624                @lt_to_not_eq @(le_S_S_to_le … Hi)
625              ]
626            ]
627          |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
628            @bitvector_of_nat_abs
629            [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
630              @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus
631              @le_S_S @le_plus_a @le_S_to_le @(le_S_S_to_le … Hi)
632            |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
633              @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
634              @le_S_S @le_plus_n_r
635            |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
636              @lt_to_not_eq @le_S_to_le @Hi
637            ]
638          ]
639        |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
640           <(proj2 ?? (pair_destruct ?????? Heq2)) >(injective_S … Hi)
641           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
642             (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat ? (|prefix|)))
643           [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
644             >lookup_insert_hit
645             lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
646             [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
647               >prf >nth_append_second
648               [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
649                 <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
650               |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
651                 @le_n
652               ]
653             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
654               >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
655             |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
656               cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
657               #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
658             ]
659           |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
660             @bitvector_of_nat_abs
661             [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82:
662               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S @le_plus_n_r
663             |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83:
664               @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
665               @le_S_S @le_plus_n_r
666             |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84:
667               @lt_to_not_eq @le_n
668             ]
669           ]
670         ]
671       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold
672         <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
673         #H #i >append_length >commutative_plus #Hi normalize in Hi;
674         cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
675         [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2))
676           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
677              (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
678           [1,3,5,7,9,11,13,15,17:
679             >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc,new_length〉 16
680               (bitvector_of_nat 16 (|prefix|)) (bitvector_of_nat 16 i))
681             [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi)
682             [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
683             ]
684             @bitvector_of_nat_abs
685             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
686               >append_length >commutative_plus @le_S @le_plus_a @Hi
687             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
688               >append_length @le_S <plus_n_Sm @le_S_S @le_plus_n_r
689             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
690             ]
691           |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
692             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
693               >append_length >commutative_plus @le_S @le_plus_a @Hi
694             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
695               >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
696             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
697             ]
698           ]
699         |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi
700           >(lookup_insert_miss ? 〈0,short_jump〉 〈inc_pc+isize,short_jump〉 16
701              (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
702           [1,3,5,7,9,11,13,15,17: >lookup_insert_hit
703             <(proj1 ?? (pair_destruct ?????? Heq1))
704             >Holdeq normalize nodelta @sym_eq @blerpque
705             [3,6,9,12,15,18,21,24,27:
706               elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
707               [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
708               |2,4,6,8,10,12,14,16,18: #H @H
709               ]
710               / by I/
711             |2,5,8,11,14,17,20,23,26: / by I/
712             ]
713           |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
714             [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf
715               >append_length @le_S_S @le_plus_n_r
716             |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf
717               >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
718             |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S_S @le_n
719             ]
720           ]
721         ]
722       ]
723     |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2))
724       #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
725       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
726       [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
727         [1,3,5: >lookup_insert_miss
728           [1,3,5: @(Hold Hadded i Hi)
729           |2,4,6: @bitvector_of_nat_abs
730             [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
731               >commutative_plus @le_S @le_plus_a @Hi
732             |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
733               @le_S <plus_n_Sm @le_S_S @le_plus_n_r
734             |3,6,9: @lt_to_not_eq @Hi
735             ]
736           ]
737         |2,4,6: @bitvector_of_nat_abs
738           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length
739             >commutative_plus @le_S @le_plus_a @Hi
740           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
741             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
742           |3,6,9: @lt_to_not_eq @le_S @Hi
743           ]
744         ]
745       |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
746         [1,3,5: >lookup_insert_hit
747           lapply (proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))) (|prefix|) ??)
748           [1,4,7: >prf >nth_append_second
749             [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H
750             |2,4,6: @le_n
751             ]
752           |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
753           |3,6,9:
754             cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
755             #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl
756           ]
757         |2,4,6: @bitvector_of_nat_abs
758           [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf
759             >append_length @le_S_S @le_plus_n_r
760           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf
761             >append_length @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
762           |3,6,9: @lt_to_not_eq @le_S_S @le_n
763           ]
764         ]
765       ]
766     |4,5: #x #Hins #Heq1 #Heq2 #Hold
767       <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1))
768       #H #i >append_length >commutative_plus #Hi normalize in Hi;
769       cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
770       [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
771         [1,3: >lookup_insert_miss
772           [1,3: @(Hold ? i Hi)
773           [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r]
774           ]
775           @bitvector_of_nat_abs
776           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
777             >commutative_plus @le_S @le_plus_a @Hi
778           |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
779             @le_S_S @le_plus_n_r
780           |3,6: @lt_to_not_eq @Hi
781           ]
782         |2,4: @bitvector_of_nat_abs
783           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
784             >commutative_plus @le_S @le_plus_a @Hi
785           |2,5: @(transitive_lt … (pi2 ?? program)) >prf >append_length
786             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
787           |3,6: @lt_to_not_eq @le_S @Hi
788           ]
789         ]
790       |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_miss
791         [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
792           >Holdeq normalize nodelta @sym_eq @blerpque
793           [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H)))
794             [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp
795             |2,4: #H @H
796             ]
797             / by I/
798           |2,5: / by I/
799           ]
800         |2,4: @bitvector_of_nat_abs
801           [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length
802             @le_S_S @le_plus_n_r
803           |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length
804             @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
805           |3,6,9: @lt_to_not_eq @le_S_S @le_n
806           ]
807         ]
808       ]
809     ]
810   ]
811| normalize nodelta @conj [ @conj [ @conj [ @conj [ @conj [ @conj [ @conj
812  [ #i cases i
813    [ #Hi2 @conj
814      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
815      | >lookup_opt_insert_hit #H destruct (H)
816      ]
817    | -i #i #Hi2 @conj
818      [ #Hi >lookup_opt_insert_miss
819        [ / by refl/
820        | @bitvector_of_nat_abs
821          [ @Hi2
822          | / by /
823          | @sym_neq @lt_to_not_eq / by /
824          ]
825        ]
826      | #_ @le_S_S @le_O_n
827      ]
828    ] 
829  | #i cases i
830    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
831    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
832    ]
833  ]
834  | #i cases i
835    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
836    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
837    ]
838  ]
839  | #i cases i
840    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
841    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
842    ]
843  ]
844  | #i cases i
845    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
846    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
847    ]
848  ]
849  | >lookup_insert_hit @refl
850  ]
851  | >lookup_insert_hit @refl
852  ]
853  | #_ #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
854  ]
855]
856qed.
Note: See TracBrowser for help on using the repository browser.