include "ASM/PolicyFront.ma".
include alias "basics/lists/list.ma".
include alias "arithmetics/nat.ma".
include alias "basics/logic.ma".

lemma not_is_jump_to_destination_of_None:
 ∀pi. ¬is_jump (Instruction pi) → destination_of pi = None ….
 * try (#x #y #H) try (#y #H) try #H cases H %
qed.

lemma destination_of_None_to_is_jump_false:
 ∀instr. destination_of instr = None … → is_jump' instr = false.
 * normalize // try (#H1 #H2 #abs) try (#H1 #abs) destruct(abs)
qed.

lemma destination_of_Some_to_is_jump_true:
 ∀instr,dst. destination_of instr = Some … dst → is_jump' instr = true.
 #instr #dst cases instr normalize // try (#H1 #H2 #abs) try (#H1 #abs) try #abs
 destruct(abs)
qed.

lemma jump_expansion_step1:
 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
 ∀labels: label_map.
 ∀old_sigma : ppc_pc_map.
 ∀inc_added : ℕ.
 ∀inc_pc_sigma : ppc_pc_map.
 ∀label : (option Identifier).
 ∀instr : pseudo_instruction.
 ∀inc_pc : ℕ.
 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
 ∀old_length : jump_length.
 ∀Hpolicy : not_jump_default prefix 〈inc_pc,inc_sigma〉.
 ∀policy : ppc_pc_map.
 ∀new_length : jump_length.
 ∀isize : ℕ.
 let add_instr ≝ match instr with
  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
  | _             ⇒ None ? 
  ] in
 ∀Heq1 :
  match add_instr with 
   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
   |Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉]
   =〈new_length,isize〉.
 ∀Heq2 :
   〈inc_pc+isize,
     insert … (bitvector_of_nat … (S (|prefix|)))
      〈inc_pc+isize, \snd  (lookup … (bitvector_of_nat … (S (|prefix|))) (\snd  old_sigma) 〈O,short_jump〉)〉
      (insert … (bitvector_of_nat … (|prefix|)) 〈inc_pc,new_length〉 inc_sigma)〉
   = policy.
  not_jump_default (prefix@[〈label,instr〉]) policy.
 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_added #inc_pc_sigma #label #instr #inc_pc
 #inc_sigma #old_length #Hpolicy #policy #new_length #isize #Heq1 #Heq2
 #i >append_length <commutative_plus #Hi normalize in Hi;
 cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
 [ <Heq2 >lookup_insert_miss
   [ >lookup_insert_miss
     [ >(nth_append_first ? i prefix ?? Hi)
       @(Hpolicy i Hi)
     | @bitvector_of_nat_abs try assumption
       [ @(transitive_lt ??? Hi) assumption ]
       @lt_to_not_eq @Hi
     ]
   | @bitvector_of_nat_abs try assumption
     [ @(transitive_lt ??? Hi) assumption ]
     @lt_to_not_eq @le_S @Hi
   ]
 | <Heq2 >Hi >lookup_insert_miss
   [ >lookup_insert_hit cases instr in Heq1;
     [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl
     |4,5: #x normalize nodelta #Heq1 >nth_append_second try %
           <minus_n_n #abs cases abs
     |1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????);
         #H #non_jump whd in match (jump_expansion_step_instruction ??????) in H;
         >not_is_jump_to_destination_of_None in H; normalize nodelta // ]         
   | @bitvector_of_nat_abs [3: // | @le_S_to_le ] assumption ]]
qed.

lemma jump_expansion_step2:
 ∀prefix: list labelled_instruction. S (|prefix|) < 2^16 → |prefix| < 2^16 → (*redundant*)
 ∀labels : label_map.
 ∀old_sigma : ppc_pc_map.
 ∀inc_pc : ℕ.
 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
 ∀Hpolicy1 :
  \fst  (lookup … (bitvector_of_nat … O) inc_sigma 〈O,short_jump〉) = O.
 ∀Hpolicy2:
   inc_pc =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
 ∀policy : ppc_pc_map.
 ∀new_length : jump_length.
 ∀isize : ℕ.
 ∀Heq2 :
  〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   = policy.
 \fst  (lookup … (bitvector_of_nat … O) (\snd  policy) 〈O,short_jump〉) = O.
 #prefix #prefix_ok1 #prefix_ok #labels #old_sigma #inc_pc
 #inc_sigma #Hpolicy1 #Hpolicy2 #policy #new_length #isize #Heq2
 <Heq2 >lookup_insert_miss
 [ cases (decidable_eq_nat 0 (|prefix|))
   [ #Heq <Heq >lookup_insert_hit >Hpolicy2 <Heq @Hpolicy1
   | #Hneq >lookup_insert_miss
     [ @Hpolicy1
     | @bitvector_of_nat_abs try assumption @lt_O_S ]]
 | @bitvector_of_nat_abs [ @lt_O_S | @prefix_ok1 | 3: @lt_to_not_eq @lt_O_S ] ]
qed.

lemma jump_expansion_step3:
 ∀program.
 ∀labels : label_map.
 ∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy.
 ∀prefix,x,tl. program=prefix@[x]@tl →
 ∀inc_added : ℕ.
 ∀inc_pc_sigma : ppc_pc_map.
 ∀label : option Identifier.
 ∀instr : pseudo_instruction.
 ∀p1 : x≃〈label,instr〉.
 ∀inc_pc : ℕ.
 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).
 ∀old_pc : ℕ.
 ∀old_length : jump_length.
 ∀Holdeq :
  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
   〈O,short_jump〉 =〈old_pc,old_length〉.
 ∀Hpolicy : jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉.
 ∀policy : ppc_pc_map.
 ∀new_length : jump_length.
 ∀isize : ℕ.
 ∀Heq1 :
   match 
   match instr
    in pseudo_instruction
    return λ_:pseudo_instruction.(option jump_length)
    with 
   [Instruction (i:(preinstruction Identifier))⇒
    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    (|prefix|) i
   |Comment (_:String)⇒None jump_length
   |Cost (_:costlabel)⇒None jump_length
   |Jmp (j:Identifier)⇒
    Some jump_length
    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
   |Call (c:Identifier)⇒
    Some jump_length
    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
   |Mov (_:[[dptr]]) (_:Identifier)⇒None jump_length]
    in option
    return λ_:(option jump_length).(jump_length×ℕ)
    with 
   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
   |Some (pl:jump_length)⇒
    〈max_length old_length pl,
    instruction_size_jmplen (max_length old_length pl) instr〉]
   =〈new_length,isize〉.
 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
 ∀prefix_ok : |prefix|< 2 \sup 16.
 ∀Heq2b :
  〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   =policy.
 jump_increase (prefix@[〈label,instr〉]) old_sigma policy.
 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label
 #instr #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy #policy #new_length
 #isize #Heq1 #prefix_ok1 #prefix_ok #Heq2
    #i >append_length >commutative_plus #Hi normalize in Hi;
    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    [ cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
      [ (* USE[pass]: jump_increase *)
        lapply (Hpolicy i (le_S_to_le … Hi))
        <Heq2
        @pair_elim #opc #oj #EQ1 >lookup_insert_miss
        [ >lookup_insert_miss
          [ @pair_elim #pc #j #EQ2 #X @X
          | @bitvector_of_nat_abs
            [ @(transitive_lt ??? Hi) ]
            [1,2: assumption
            | @lt_to_not_eq @Hi
            ]
          ]
        | @bitvector_of_nat_abs
          [ @(transitive_lt ??? Hi) @le_S_to_le ]
          [1,2: assumption
          | @lt_to_not_eq @le_S @Hi
          ]
        ]
      | >Hi <Heq2 >Holdeq normalize nodelta
        cut (|prefix| < |program|)
        [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program
        >lookup_insert_miss
        [ >lookup_insert_hit normalize nodelta
          inversion instr in Heq1; normalize nodelta
          [4,5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
          | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta
            lapply (destination_of_None_to_is_jump_false pi)
            lapply (destination_of_Some_to_is_jump_true pi)
            cases (destination_of ?) normalize nodelta
            [ #tgt #Hx
            | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length
            ]
          |2,3,6: #x [3: #y] #Heqi ]
          #Hj <(proj1 ?? (pair_destruct ?????? Hj))
          lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption
          [1,3,5,7: >prf >nth_append_second try @le_n
            <minus_n_n whd in match (nth ????); >p1 >Heqi
            whd in match is_jump; normalize nodelta try % >Hx %
          |*: >Holdeq #EQ2 >EQ2 %2 %]
        | @bitvector_of_nat_abs
          [ @le_S_to_le ]
          [1,2: assumption
          | @lt_to_not_eq @le_n
          ]
        ]
      ]
    | <Heq2 >Hi >lookup_insert_hit
      normalize nodelta
      cases (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma) 〈0,short_jump〉)
      #a #b normalize nodelta %2 @refl
    ]
qed.

lemma jump_expansion_step4:
 ∀labels : label_map.
 ∀old_sigma : ppc_pc_map.
 ∀prefix : list (option Identifier×pseudo_instruction).
 ∀inc_added : ℕ.
 ∀inc_pc_sigma : ppc_pc_map.
 ∀label : option Identifier.
 ∀instr : pseudo_instruction.
 ∀inc_pc : ℕ.
 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
 ∀old_length : jump_length.
 ∀Hpolicy1 : sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉.
 ∀Hpolicy2: inc_pc
    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma
                 〈O,short_jump〉).
 ∀Hpolicy3: out_of_program_none prefix 〈inc_pc,inc_sigma〉.
 ∀policy : ppc_pc_map.
 ∀new_length : jump_length.
 ∀isize : ℕ.
 ∀Heq1 :
  match 
   match instr
    in pseudo_instruction
    return λ_:pseudo_instruction.(option jump_length)
    with 
   [Instruction (i:(preinstruction Identifier))⇒
    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    (|prefix|) i
   |Comment (_:String)⇒None jump_length
   |Cost (_:costlabel)⇒None jump_length
   |Jmp (j:Identifier)⇒
    Some jump_length
    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
   |Call (c:Identifier)⇒
    Some jump_length
    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
   |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
    in option
    return λ_:(option jump_length).(jump_length×ℕ)
    with 
   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
   |Some (pl:jump_length)⇒
    〈max_length old_length pl,
    instruction_size_jmplen (max_length old_length pl) instr〉]
   =〈new_length,isize〉.
 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
 ∀prefix_ok : |prefix|< 2 \sup 16.
 ∀Heq2b :
   〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   =policy.
 sigma_compact_unsafe (prefix@[〈label,instr〉]) labels policy.
 #labels #old_sigma #prefix #inc_added #inc_pc_sigma #label #instr #inc_pc #inc_sigma
 #old_length #Hpolicy1 #Hpolicy2 #Hpolicy3 #policy #new_length #isize
 #Heq1 #prefix_ok1 #prefix_ok #Heq2b
    #i >append_length <commutative_plus #Hi normalize in Hi;
    <Heq2b
    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    [ >lookup_opt_insert_miss
      [ >lookup_opt_insert_miss
        [ >lookup_opt_insert_miss
          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
            [ >lookup_opt_insert_miss
              [ (* USE[pass]: sigma_compact_unsafe *)
                lapply (Hpolicy1 i ?)
                [ @le_S_to_le @Hi ]
                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
                [ normalize nodelta #X @X
                | #x cases x -x #x1 #x2
                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
                  normalize nodelta
                  [ #X @X
                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
                    [ #X @X
                    | @le_S_to_le @Hi
                    ]
                  ]
                ]
              | @bitvector_of_nat_abs
                [3: @lt_to_not_eq @Hi ]
              ]
            | >Hi >lookup_opt_insert_hit normalize nodelta
              (* USE[pass]: sigma_compact_unsafe *)
              lapply (Hpolicy1 i ?)
              [ <Hi @le_n
              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
                [ normalize nodelta #X @X
                | #x cases x -x #x1 #x2
                  (* USE: inc_pc = fst inc_sigma *)
                  lapply Hpolicy2
                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
                  [ normalize nodelta #_  #_ #H cases H
                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
                      #Heq2 <Heq2 #X @X
                    | <Hi @le_n]]]]]]]]
      [3,4,5: @bitvector_of_nat_abs]
      [ @(transitive_lt ??? (le_S_S … Hi))
      |3: @lt_to_not_eq @le_S_S @Hi
      |4,7,10: @(transitive_lt ??? Hi) assumption
      |5,11: @le_S_to_le
      |6: @lt_to_not_eq @Hi
      |9: @lt_to_not_eq @le_S @Hi
      ]
      assumption
    | >Hi >lookup_opt_insert_miss
      [2: @bitvector_of_nat_abs try assumption @lt_to_not_eq % ]
      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
      (* USE: out_of_program_none ← *)
      lapply (Hpolicy3 i ?)
      [ >Hi assumption
      | >Hi
        (* USE: inc_pc = fst policy *)
        lapply Hpolicy2
        inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma)
        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
          [ cases H #_ #X @X %
          | @le_to_not_lt @le_n]
        | * #x1 #x2 #Heq #Hip #_ >nth_append_second
          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
          cases instr in Heq1; normalize nodelta
          [1: #pi cases (jump_expansion_step_instruction ??????) normalize nodelta]
          try (#x #y #Heq1) try (#x #Heq1) try #Heq1
          @eq_f <(proj2 ?? (pair_destruct ?????? Heq1))
          try % <(proj1 ?? (pair_destruct ?????? Heq1)) %]]]
qed.

lemma jump_expansion_step5:
 ∀labels : label_map.
 ∀old_sigma : ppc_pc_map.
 ∀prefix : list (option Identifier×pseudo_instruction).
 ∀inc_added : ℕ.
 ∀inc_pc_sigma : ppc_pc_map.
 ∀label : option Identifier.
 ∀instr : pseudo_instruction.
 ∀inc_pc : ℕ.
 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
 ∀old_pc : ℕ.
 ∀old_length : jump_length.
 ∀Holdeq :
  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
   〈O,short_jump〉
   =〈old_pc,old_length〉.
 ∀Hpolicy1 : sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O.
 ∀Hpolicy2: inc_pc
    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
 ∀added : ℕ.
 ∀policy : ppc_pc_map.
 ∀new_length : jump_length.
 ∀isize : ℕ.
 let add_instr ≝ match instr with
  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
  | _             ⇒ None ? 
  ] in
 ∀Heq1 :
  match add_instr with 
   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
   |Some (pl:jump_length)⇒
    〈max_length old_length pl,
    instruction_size_jmplen (max_length old_length pl) instr〉]
   =〈new_length,isize〉.
 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
 ∀prefix_ok : |prefix|< 2 \sup 16.
 ∀Heq2a :
  match add_instr with 
   [None⇒inc_added
   |Some (x0:jump_length)⇒
    inc_added+(isize-instruction_size_jmplen old_length instr)]
   =added.
 ∀Heq2b :
  〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   =policy.
 sigma_jump_equal (prefix@[〈label,instr〉]) old_sigma policy→added=O.
 #labels #old_sigma #prefix #inc_added #inc_pc #label #instr #inc_pc #inc_sigma
 #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added #policy #new_length #isize
 #Heq1 #prefix_ok1 #prefix_ok #Heq2a #Heq2b
    <Heq2b #Heq <Heq2a
    (* USE[pass]: policy_jump_equal → added = 0 *)
    >Hpolicy1
    [ cases instr in Heq1 Heq;
      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
      |1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
          normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]]
      #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
      #Heq (*CSC: make a lemma here!*) lapply Holdeq -Holdeq
      (* USE: inc_pc = fst inc_sigma *)
      >Hpolicy2
      lapply (Heq (|prefix|) ?)
      [1,3,5: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
      -Heq >lookup_insert_miss
      [1,3,5: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
        #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
        #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n %
      |*: @bitvector_of_nat_abs try assumption @lt_to_not_eq %]
    | #i #Hi lapply (Heq i ?)
      [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
      | >lookup_insert_miss
        [ >lookup_insert_miss
          [ #X @X
          | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
            @lt_to_not_eq @Hi]
        | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
          @lt_to_not_eq @le_S @Hi ]]]
qed.

lemma jump_expansion_step6:
(*
 program :
  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)
 labels :
  (Σlm:label_map
   .(∀l:identifier ASMTag
     .occurs_exactly_once ASMTag pseudo_instruction l program
      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
       =address_of_word_labels_code_mem program l))*)
 ∀old_sigma : ppc_pc_map.(*
  (Σpolicy:ppc_pc_map
   .not_jump_default program policy
    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
                 〈O,short_jump〉)
     =O
    ∧\fst  policy
     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
                  (\snd  policy) 〈O,short_jump〉)
    ∧sigma_compact_unsafe program labels policy
    ∧\fst  policy≤ 2 \sup 16 )*)
 ∀prefix : list (option Identifier×pseudo_instruction).(*
 x : (option Identifier×pseudo_instruction)
 tl : (list (option Identifier×pseudo_instruction))
 prf : (program=prefix@[x]@tl)
 acc :
  (Σx0:ℕ×ppc_pc_map
   .(let 〈added,policy〉 ≝x0 in 
     not_jump_default prefix policy
     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
                  〈O,short_jump〉)
      =O
     ∧\fst  policy
      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
                   (\snd  policy) 〈O,short_jump〉)
     ∧jump_increase prefix old_sigma policy
     ∧sigma_compact_unsafe prefix labels policy
     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     ∧out_of_program_none prefix policy
     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
                  (\snd  policy) 〈O,short_jump〉)
      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
                   (\snd  old_sigma) 〈O,short_jump〉)
       +added
     ∧sigma_safe prefix labels added old_sigma policy))
 inc_added : ℕ
 inc_pc_sigma : ppc_pc_map
 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
 ∀label : option Identifier.
 ∀instr : pseudo_instruction.(*
 p1 : (x≃〈label,instr〉)
 add_instr ≝
  match instr
   in pseudo_instruction
   return λ_:pseudo_instruction.(option jump_length)
   with 
  [Instruction (i:(preinstruction Identifier))⇒
   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
   (|prefix|) i
  |Comment (_:String)⇒None jump_length
  |Cost (_:costlabel)⇒None jump_length
  |Jmp (j:Identifier)⇒
   Some jump_length
   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
  |Call (c:Identifier)⇒
   Some jump_length
   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
 inc_pc : ℕ
 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
 old_pc : ℕ
 old_length : jump_length
 Holdeq :
  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
   〈O,short_jump〉
   =〈old_pc,old_length〉)
 Hpolicy :
  (not_jump_default prefix 〈inc_pc,inc_sigma〉
   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
                〈O,short_jump〉)
    =O
   ∧inc_pc
    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
                 〈O,short_jump〉)
   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
                〈O,short_jump〉)
    =old_pc+inc_added
   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
 ∀added : ℕ.
 ∀policy : ppc_pc_map.(*
 new_length : jump_length
 isize : ℕ
 Heq1 :
  (match 
   match instr
    in pseudo_instruction
    return λ_:pseudo_instruction.(option jump_length)
    with 
   [Instruction (i:(preinstruction Identifier))⇒
    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    (|prefix|) i
   |Comment (_:String)⇒None jump_length
   |Cost (_:costlabel)⇒None jump_length
   |Jmp (j:Identifier)⇒
    Some jump_length
    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
   |Call (c:Identifier)⇒
    Some jump_length
    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    in option
    return λ_0:(option jump_length).(jump_length×ℕ)
    with 
   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
   |Some (pl:jump_length)⇒
    〈max_length old_length pl,
    instruction_size_jmplen (max_length old_length pl) instr〉]
   =〈new_length,isize〉)
 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
 prefix_ok : (|prefix|< 2 \sup 16 )
 Heq2a :
  (match 
   match instr
    in pseudo_instruction
    return λ_0:pseudo_instruction.(option jump_length)
    with 
   [Instruction (i:(preinstruction Identifier))⇒
    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    (|prefix|) i
   |Comment (_0:String)⇒None jump_length
   |Cost (_0:costlabel)⇒None jump_length
   |Jmp (j:Identifier)⇒
    Some jump_length
    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
   |Call (c:Identifier)⇒
    Some jump_length
    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
    in option
    return λ_0:(option jump_length).ℕ
    with 
   [None⇒inc_added
   |Some (x0:jump_length)⇒
    inc_added+(isize-instruction_size_jmplen old_length instr)]
   =added)
 Heq2b :
  (〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   =policy)
*)
 added=O→sigma_pc_equal (prefix@[〈label,instr〉]) old_sigma policy.
cases daemon(*
    (* USE[pass]: added = 0 → policy_pc_equal *)
     lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    <(proj2 ?? (pair_destruct ?????? Heq2))
    <(proj1 ?? (pair_destruct ?????? Heq2))
    lapply Heq1 -Heq1 lapply (refl ? instr)
    cases instr in ⊢ (???% → % → %); normalize nodelta
    [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
      #Hi normalize in Hi;
      cases (le_to_or_lt_eq … Hi) -Hi #Hi
      [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
        [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss
          [1,3,5: >lookup_insert_miss
            [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
            |2,4,6: @bitvector_of_nat_abs
              [3,6,9: @lt_to_not_eq @Hi
              |1,4,7: @(transitive_lt ??? Hi)
              ]
              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
              @le_S_S <plus_n_Sm @le_S @le_plus_n_r
            ]
          |2,4,6: @bitvector_of_nat_abs
            [3,6,9: @lt_to_not_eq @le_S @Hi
            |1,4,7: @(transitive_lt … Hi) @le_S_to_le
            ]
            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
          ]
        |2,4,6: >Hi >lookup_insert_miss
          [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
            @sym_eq (* USE: fst p = lookup |prefix| *)
            @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
          |2,4,6: @bitvector_of_nat_abs
            [3,6,9: @lt_to_not_eq @le_n
            |1,4,7: @le_S_to_le
            ]
            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
          ]
        ]
      |2,4,6: >Hi >lookup_insert_hit
        (* USE fst p = lookup |prefix| *)
        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
        <(Hold Hadded (|prefix|) (le_n (|prefix|)))
        (* USE: sigma_compact (from old_sigma) *)
        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
        |2,4,6: 
          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
          cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
          [1,3,5: normalize nodelta #_ #ABS cases ABS
          |2,4,6: lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
            cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
            [1,3,5: normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
            |2,4,6: normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
              normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
              >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
              >prf >p1 >Hins >nth_append_second 
              [2,4,6: @(le_n (|prefix|))
              |1,3,5: <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
                 #H >H @plus_left_monotone @instruction_size_irrelevant @nmk / by /
              ]
            ]
          ] 
        ]
      ]
    |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
       #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
       [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
         [1,3: >lookup_insert_miss
           [1,3: >lookup_insert_miss
             [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded;
               @plus_zero_zero
             |2,4: @bitvector_of_nat_abs
               [3,6: @lt_to_not_eq @Hi
               |1,4: @(transitive_lt ??? Hi)
               ]
               @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
               >append_length @le_plus_n_r
             ]
           |2,4: @bitvector_of_nat_abs
             [3,6: @lt_to_not_eq @le_S @Hi
             |1,4: @(transitive_lt ??? Hi) @le_S_to_le
             ]
             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
           ]
         |2,4: >Hi >lookup_insert_miss
           [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
             [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
             (* USE: fst p = lookup |prefix| *)
             @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
           |2,4: @bitvector_of_nat_abs
             [3,6: @lt_to_not_eq @le_n
             |1,4: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
             ]
             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
             >append_length <plus_n_Sm @le_S_S @le_plus_n_r
           ]
         ]
       |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
         elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
         [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1))
           @jump_length_le_max / by I/
         |2,4: #H (* USE: fst p = lookup |prefix| *)
           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
           <(Hold ? (|prefix|) (le_n (|prefix|)))
           [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
             >(jump_length_equal_max … H)
             [1,3: (* USE: sigma_compact_unsafe (from old_sigma) *)
               lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
               [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
               |2,4: lapply Holdeq lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
                 cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
                 [1,3: normalize nodelta #_ #_ #ABS cases ABS
                 |2,4: normalize nodelta
                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
                   [1,3: #_ #x cases x -x #pc #j normalize nodelta #_ #_ #ABS cases ABS
                   |2,4: #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
                     normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
                     >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
                     >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
                     [1,3: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
                     |2,4: @le_n
                     ]
                   ]
                 ]
               ]
             |2,4: / by I/
             ]
           |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded]
           ]
         ]
       ]
     |1: #pi cases pi normalize nodelta
      [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:
        [1,2,3,6,7,24,25: #x #y
        |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
        #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
        cases (le_to_or_lt_eq … Hi) -Hi #Hi
        [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:
          cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
          [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:
            <(proj2 ?? (pair_destruct ?????? Heq2))
            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
            [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:
              >(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)
              [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:
                @(Hold Hadded i (le_S_to_le … Hi))
              |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:
                @bitvector_of_nat_abs
                [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:
                  @lt_to_not_eq @Hi
                |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:
                  @(transitive_lt ??? Hi)
                ]
                @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
                @le_S_S <plus_n_Sm @le_S @le_plus_n_r
              ]
            |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:
              @bitvector_of_nat_abs
              [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:
                @lt_to_not_eq @le_S @Hi
              |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:
                @(transitive_lt … Hi) @le_S_to_le
              ]
              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
              @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
            ]
          |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:
            >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
            [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:
              >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
              (* USE: fst p = lookup |prefix| *)
              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
            |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:
              @bitvector_of_nat_abs
              [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:
                @lt_to_not_eq @le_n
              |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:
                @le_S_to_le
              ]
              @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
                @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
            ]
          ]
        |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:
          >Hi >lookup_insert_hit
          (* USE fst p = lookup |prefix| *)
          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
          <(Hold Hadded (|prefix|) (le_n (|prefix|)))
          (* USE: sigma_compact (from old_sigma) *)
          lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
          [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:
            >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
          |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: 
            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
            cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
            [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:
              normalize nodelta #_ #ABS cases ABS
            |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:
              lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
              cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
              [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:
                normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
              |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:
                normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
                normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
                >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
                >prf >p1 >Hins >nth_append_second 
                [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:
                  @(le_n (|prefix|))
                |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:
                  <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
                  #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H
                ]
              ]
            ] 
          ]
        ]
      |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded
        #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
        -Hi #Hi
        [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
          [1,3,5,7,9,11,13,15,17:
            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
            [1,3,5,7,9,11,13,15,17:
              >(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)
              [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi))
                >commutative_plus in Hadded; @plus_zero_zero
              |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
                [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
                |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi)
                ]
                @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
                >append_length @le_plus_n_r
              ]
            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le
              ]
              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
            ]
          |2,4,6,8,10,12,14,16,18: >Hi
            >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
            [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
              [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
              (* USE: fst p = lookup |prefix| *)
              @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
            |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
              [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
              |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
              ]
              @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
              >append_length <plus_n_Sm @le_S_S @le_plus_n_r
            ]
          ]
        |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
          elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
          [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt
            <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/
          |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *)
            >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
            <(Hold ? (|prefix|) (le_n (|prefix|)))
            [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
              >(jump_length_equal_max … H)
              [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *)
                lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
                [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
                |2,4,6,8,10,12,14,16,18: lapply Holdeq
                  lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
                  cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
                  [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS
                  |2,4,6,8,10,12,14,16,18: normalize nodelta
                    lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
                    cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
                    [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta
                      #_ #_ #ABS cases ABS
                    |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x
                      #pc #j #EQ
                      normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
                      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
                      >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
                      [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
                      |2,4,6,8,10,12,14,16,18: @le_n
                      ]
                    ]
                  ]
                ]
              |2,4,6,8,10,12,14,16,18: / by I/
              ]
            |2,4,6,8,10,12,14,16,18: @plus_zero_zero
              [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded]
            ]
          ]
        ]
      ]
    ]*)
qed.

lemma jump_expansion_step7:
 ∀old_sigma : ppc_pc_map.
 ∀prefix : list (option Identifier×pseudo_instruction).
 ∀label : option Identifier.
 ∀instr : pseudo_instruction.
 ∀inc_pc : ℕ.
 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
 ∀Hpolicy1 : out_of_program_none prefix 〈inc_pc,inc_sigma〉.
 ∀policy : ppc_pc_map.
 ∀new_length : jump_length.
 ∀isize : ℕ.
 ∀Heq2b :
  〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   =policy.
 out_of_program_none (prefix@[〈label,instr〉]) policy.
 #old_sigma #prefix #label #instr #inc_pc #inc_sigma #Hpolicy1 #policy #new_length
 #isize #Heq2b
    #i #Hi2 >append_length <commutative_plus @conj
    [ (* → *) #Hi normalize in Hi; <Heq2b >lookup_opt_insert_miss
      [ >lookup_opt_insert_miss
        [ cases (Hpolicy1 i Hi2) #X #_ @X @le_S_to_le @Hi
        | @bitvector_of_nat_abs try assumption
          [ @(transitive_lt … Hi2) @le_S_to_le assumption
          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n (S i)))
            @(transitive_le … abs) %2 % ]]
      | @bitvector_of_nat_abs try assumption
          [ @(transitive_lt … Hi2) assumption
          | % #EQ <EQ in Hi; #abs @(absurd ?? (not_le_Sn_n i)) assumption ]]
    | (* ← *) <Heq2b #Hl normalize
      @(leb_elim (S i) (|prefix|))
      [ #Hi
        lapply (proj2 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
        #Hl2 (* USE[pass]: out_of_program_none ← *)
        cases (Hpolicy1 i Hi2) #_
        #Hi3 @⊥ @(absurd ? Hi) @le_to_not_lt @le_S_to_le @Hi3 assumption
      | #Hi elim (le_to_or_lt_eq … (not_lt_to_le … Hi))
        [ #Hi3 elim (le_to_or_lt_eq … Hi3)
          [ #X @X
          | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? Hl)) >X >eq_bv_refl #H normalize in H; destruct (H)
          ]
        | #X lapply (proj1 ?? (insert_lookup_opt_miss ?????? (proj2 ?? (insert_lookup_opt_miss ?????? Hl))))
          >X >eq_bv_refl #H normalize in H; destruct (H)]]]
qed.

lemma jump_expansion_step8:
 ∀program : list labelled_instruction.
 ∀labels : label_map.
 ∀old_sigma :
  Σpolicy:ppc_pc_map.sigma_compact_unsafe program labels policy ∧\fst  policy≤ 2 \sup 16.
 ∀prefix : list (option Identifier×pseudo_instruction).
 ∀x : option Identifier×pseudo_instruction.
 ∀tl : list (option Identifier×pseudo_instruction).
 ∀prf : program=prefix@[x]@tl.
 ∀inc_added : ℕ.
 ∀inc_pc_sigma : ppc_pc_map.
 ∀label : option Identifier.
 ∀instr : pseudo_instruction.
 ∀p1 : x≃〈label,instr〉.
 ∀inc_pc : ℕ.
 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
 ∀old_pc : ℕ.
 ∀old_length : jump_length.
 ∀Holdeq :
  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
   〈O,short_jump〉
   =〈old_pc,old_length〉.
 ∀Hpolicy1 : inc_pc
    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
 ∀Hpolicy2: \fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉)
    =old_pc+inc_added.
 ∀added : ℕ.
 ∀policy : ppc_pc_map.
 ∀new_length : jump_length.
 ∀isize : ℕ.
 let add_instr ≝ match instr with
  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
  | _             ⇒ None ? 
  ] in 
 ∀Heq1 :
  match add_instr with 
   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
   |Some (pl:jump_length)⇒
    〈max_length old_length pl,
    instruction_size_jmplen (max_length old_length pl) instr〉]
   =〈new_length,isize〉.
 ∀Heq2a :
  match add_instr with
   [None⇒inc_added
   |Some (x0:jump_length)⇒
    inc_added+(isize-instruction_size_jmplen old_length instr)]
   =added.
 ∀Heq2b :
  〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   =policy.
   \fst  (lookup (ℕ×jump_length) 16
              (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  policy)
              〈O,short_jump〉)
  =\fst  (lookup (ℕ×jump_length) 16
               (bitvector_of_nat 16 (|(prefix@[〈label,instr〉])|)) (\snd  old_sigma)
               〈O,short_jump〉)
   +added.
 #program #labels #old_sigma #prefix #x #tl #prf #inc_added #inc_pc_sigma #label #instr
 #p1 #inc_pc #inc_sigma #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added
 #policy #new_length #isize #Heq1 #Heq2a #Heq2b
    <Heq2b >append_length <plus_n_Sm <plus_n_O
    >lookup_insert_hit
    <Heq2a cases instr in p1 Heq1;
    [1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
        normalize nodelta lapply (destination_of_None_to_is_jump_false pi)
        lapply (destination_of_Some_to_is_jump_true pi)
        cases (destination_of ?) normalize nodelta ]
    try (#x #y #z #p1 #Heq1) try (#x #y #p1 #Heq1) try (#x #p1 #Heq1) try (#p1 #Heq1)
    <(proj2 ?? (pair_destruct ?????? Heq1))
    (* USE: sigma_compact_unsafe (from old_sigma) *)
    lapply (proj1 ?? (pi2 ?? old_sigma) (|prefix|) ?)
    [1,3,5,7,9,11,13,15: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
    lapply Holdeq -Holdeq
    inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
    [1,3,5,7,9,11,13,15: normalize nodelta #_ #_ #abs cases abs]
    inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
    [1,3,5,7,9,11,13,15: normalize nodelta #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs]
    * #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta
    #H (* USE: fst p = lookup |prefix| *) (*CSC: This part of the proof is repeated somewhere else*)
    >Hpolicy1
    (* USE[pass]: lookup p = lookup old_sigma + added *)
    >Hpolicy2
    [1,3,4,7:
      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ;
      -Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ))
      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H >prf >nth_append_second try %
      <minus_n_n >p1 whd in match (nth ????); >associative_plus
      >(associative_plus pc) @plus_left_monotone >commutative_plus
      @plus_right_monotone @instruction_size_irrelevant try %
      whd in match is_jump; normalize nodelta >y %
    |2,5,6:
      >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H
      >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ
      -Holdeq <(proj1 ?? (pair_destruct ?????? EQ))
      >associative_plus
      >(associative_plus pc) @plus_left_monotone >assoc_plus1
      >(associative_plus inc_added) @plus_left_monotone >plus_minus_commutative
      [1,3,5: >(proj2 ?? (pair_destruct ?????? EQ)) >prf in old_sigma; #old_sigma
        >nth_append_second try %
        <minus_n_n whd in match (nth ????); >p1 in old_sigma; #old_sigma
        >commutative_plus @minus_plus_m_m
      |*: <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max try %
        whd in match is_jump; normalize nodelta >y %]]
qed.

lemma jump_expansion_step9:
(*
 program :
  (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*)
 ∀labels : label_map.(*
  (Σlm:label_map
   .(∀l:identifier ASMTag
     .occurs_exactly_once ASMTag pseudo_instruction l program
      →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O)
       =address_of_word_labels_code_mem program l))*)
 ∀old_sigma : ppc_pc_map.(*
  (Σpolicy:ppc_pc_map
   .not_jump_default program policy
    ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
                 〈O,short_jump〉)
     =O
    ∧\fst  policy
     =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|))
                  (\snd  policy) 〈O,short_jump〉)
    ∧sigma_compact_unsafe program labels policy
    ∧\fst  policy≤ 2 \sup 16 )*)
 ∀prefix : list (option Identifier×pseudo_instruction).(*
 x : (option Identifier×pseudo_instruction)
 tl : (list (option Identifier×pseudo_instruction))
 prf : (program=prefix@[x]@tl)
 acc :
  (Σx0:ℕ×ppc_pc_map
   .(let 〈added,policy〉 ≝x0 in 
     not_jump_default prefix policy
     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd  policy)
                  〈O,short_jump〉)
      =O
     ∧\fst  policy
      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
                   (\snd  policy) 〈O,short_jump〉)
     ∧jump_increase prefix old_sigma policy
     ∧sigma_compact_unsafe prefix labels policy
     ∧(sigma_jump_equal prefix old_sigma policy→added=O)
     ∧(added=O→sigma_pc_equal prefix old_sigma policy)
     ∧out_of_program_none prefix policy
     ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
                  (\snd  policy) 〈O,short_jump〉)
      =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
                   (\snd  old_sigma) 〈O,short_jump〉)
       +added
     ∧sigma_safe prefix labels added old_sigma policy))
 inc_added : ℕ
 inc_pc_sigma : ppc_pc_map
 p : (acc≃〈inc_added,inc_pc_sigma〉)*)
 ∀label : option Identifier.
 ∀instr : pseudo_instruction.(*
 p1 : (x≃〈label,instr〉)
 add_instr ≝
  match instr
   in pseudo_instruction
   return λ_:pseudo_instruction.(option jump_length)
   with 
  [Instruction (i:(preinstruction Identifier))⇒
   jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
   (|prefix|) i
  |Comment (_:String)⇒None jump_length
  |Cost (_:costlabel)⇒None jump_length
  |Jmp (j:Identifier)⇒
   Some jump_length
   (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
  |Call (c:Identifier)⇒
   Some jump_length
   (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
  |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
 inc_pc : ℕ
 inc_sigma : (BitVectorTrie (ℕ×jump_length) 16)
 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)
 old_pc : ℕ
 old_length : jump_length
 Holdeq :
  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
   〈O,short_jump〉
   =〈old_pc,old_length〉)
 Hpolicy :
  (not_jump_default prefix 〈inc_pc,inc_sigma〉
   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma
                〈O,short_jump〉)
    =O
   ∧inc_pc
    =\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
                 〈O,short_jump〉)
   ∧jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉
   ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉
   ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O)
   ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉)
   ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉
   ∧\fst  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma
                〈O,short_jump〉)
    =old_pc+inc_added
   ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*)
 ∀added : ℕ.
 ∀policy : ppc_pc_map.(*
 new_length : jump_length
 isize : ℕ
 Heq1 :
  (match 
   match instr
    in pseudo_instruction
    return λ_:pseudo_instruction.(option jump_length)
    with 
   [Instruction (i:(preinstruction Identifier))⇒
    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    (|prefix|) i
   |Comment (_:String)⇒None jump_length
   |Cost (_:costlabel)⇒None jump_length
   |Jmp (j:Identifier)⇒
    Some jump_length
    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
   |Call (c:Identifier)⇒
    Some jump_length
    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
   |Mov (_:[[dptr]])   (_0:Identifier)⇒None jump_length]
    in option
    return λ_0:(option jump_length).(jump_length×ℕ)
    with 
   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
   |Some (pl:jump_length)⇒
    〈max_length old_length pl,
    instruction_size_jmplen (max_length old_length pl) instr〉]
   =〈new_length,isize〉)
 prefix_ok1 : (S (|prefix|)< 2 \sup 16 )
 prefix_ok : (|prefix|< 2 \sup 16 )
 Heq2a :
  (match 
   match instr
    in pseudo_instruction
    return λ_0:pseudo_instruction.(option jump_length)
    with 
   [Instruction (i:(preinstruction Identifier))⇒
    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
    (|prefix|) i
   |Comment (_0:String)⇒None jump_length
   |Cost (_0:costlabel)⇒None jump_length
   |Jmp (j:Identifier)⇒
    Some jump_length
    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
   |Call (c:Identifier)⇒
    Some jump_length
    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
   |Mov (_0:[[dptr]])   (_00:Identifier)⇒None jump_length]
    in option
    return λ_0:(option jump_length).ℕ
    with 
   [None⇒inc_added
   |Some (x0:jump_length)⇒
    inc_added+(isize-instruction_size_jmplen old_length instr)]
   =added)
 Heq2b :
  (〈inc_pc+isize,
   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
   〈inc_pc+isize,
   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
               (\snd  old_sigma) 〈O,short_jump〉)〉
   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
    〈inc_pc,new_length〉 inc_sigma)〉
   =policy)
*)
 sigma_safe (prefix@[〈label,instr〉]) labels added old_sigma policy.
cases daemon(*
    #i >append_length >commutative_plus #Hi normalize in Hi;
    elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    [ >nth_append_first [2: @Hi]
      <Heq2b >lookup_insert_miss
      [ >lookup_insert_miss
        [ >lookup_insert_miss
          [ elim (le_to_or_lt_eq … Hi) -Hi #Hi
            [ >lookup_insert_miss
              [ (* USE[pass]: sigma_safe *)
                lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
                cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
                #pc #j normalize nodelta
                cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
                #Spc #Sj normalize nodelta
                cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
                #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj
                lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|))))
                cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %); #H
                [ cases (le_to_or_lt_eq … (leb_true_to_le … H)) -H #H
                  [ >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
                    >lookup_insert_miss
                    [ cases (le_to_or_lt_eq … (le_S_S_to_le … H)) -H #H
                      [ >lookup_insert_miss
                        [ #H2 @H2
                        | @bitvector_of_nat_abs
                          [3: @lt_to_not_eq @H
                          |1: @(transitive_lt ??? H)
                          ]
                          @prefix_ok
                        ]
                      | >H >lookup_insert_hit
                        (* USE: inc_pc = lookup |prefix| *)
                        >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
                        #H2 @H2
                      ]
                    | @bitvector_of_nat_abs
                      [3: @lt_to_not_eq @H
                      |1: @(transitive_lt ??? H)
                      ]
                      @prefix_ok1
                    ]
                  | >H >lookup_insert_hit normalize nodelta
                    >(not_le_to_leb_false … (lt_to_not_le ?? (le_S_S ?? (le_n (|prefix|)))))
                    normalize nodelta
                    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
                    #H2 >(proj2 ?? (proj1 ?? Hpolicy))
                  ]
                |
                        
                        
                        
                [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
                  [1,4,7: cases (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) #H
                    [1,3,5: >(le_to_leb_true … H) normalize nodelta cases (le_to_or_lt_eq … H) -H #H
                      [1,3,5: >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta
                        >lookup_insert_miss
                        [2,4,6: @bitvector_of_nat_abs
                          [3,6,9: @lt_to_not_eq @H
                          |1,4,7: @(transitive_lt ??? H)
                          ]
                          @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
                          @le_S_S >append_length <plus_n_Sm @le_S_S @le_plus_n_r
                        ]
                        cases (le_to_or_lt_eq … H) -H #H
                        [1,3,5: >lookup_insert_miss
                          [1,3,5: #H @H
                          |2,4,6: @bitvector_of_nat_abs
                            [3,6,9: @lt_to_not_eq @(le_S_S_to_le … H)
                            |1,4,7: @(transitive_lt ??? (le_S_S_to_le … H))
                            ]
                            @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf
                            >append_length @le_S_S @le_plus_n_r
                          ]
                        |2,4,6: >(injective_S … H) >lookup_insert_hit
                          (* USE: blerp *)
                          >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
                          #H @H
                        ]
                      |2,4,6: >H >lookup_insert_hit >(not_le_to_leb_false)
                        [2,4,6: @le_to_not_lt @le_n]
                        normalize nodelta
                        lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
                        [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
                         lapply (refl ? (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
                          cases (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
                          [1,3,5: normalize nodelta #_ #abs cases abs
                          |2,4,6: #x cases x -x #ppc #pj normalize nodelta #PEQ
                            lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
                            cases (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
                            [1,3,5: normalize nodelta #_ #abs cases abs
                            |2,4,6: #x cases x -x #Sppc #Spj normalize nodelta #SPEQ #Pcompact
                              >(lookup_opt_lookup_hit … SPEQ 〈0,short_jump〉)
                              >(lookup_opt_lookup_hit … PEQ 〈0,short_jump〉) in Holdeq;
                              #H >Pcompact >(proj1 ?? (pair_destruct ?????? H))
                              >commutative_plus >assoc_plus1 <(proj2 ?? (proj1 ?? Hpolicy))
                              <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
                              >prf >nth_append_second
                              [1,3,5: <minus_n_n whd in match (nth ????); >p1
                                cases daemon (* to be lemmatized *)
                              |2,4,6: @le_n
                              ]
                            ]
                          ]
                        ]
                      |2,4,6: >(not_le_to_leb_false … H)
                        >not_le_to_leb_false
                        [2,4,6: @lt_to_not_le @le_S_to_le @not_le_to_lt @H
                        |1,3,5: normalize nodelta #H @H
                        ]
                      ]
                    |2,5,8: cases daemon (* like previous case *)
                    |3,6,9: cases daemon (* like previous case *)
                    ]
                  |4,5: #x normalize nodelta cases daemon (* blerp *)
                  |1: cases daemon (* blerp *)
                  ]
                
                               
                          

   (*(\fst  (short_jump_cond (bitvector_of_nat 16 Spc)
              (bitvector_of_nat 16
               (inc_pc
                +instruction_size_jmplen
                 (max_length old_length
                  (select_jump_length labels old_sigma inc_pc_sigma inc_added
                   (|prefix|) xx)) (Jmp xx))))
  =true                   *)
                        
                  
  ]       
              [ >lookup_insert_miss
                [ (* USE[pass]: sigma_safe *)
                  lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi))
                  cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉)
                  #pc #j normalize nodelta
                  cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉)
                  #Spc #Sj normalize nodelta
                  cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta
                  #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr
                  [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta
                    [1,4,7: *)
qed.

(* One step in the search for a jump expansion fixpoint. *)
definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
  S (|l|) < 2^16 ∧ is_well_labelled_p l).
  ∀labels:(Σlm:label_map.∀l.
    occurs_exactly_once ?? l program →
    bitvector_of_nat ? (lookup_def … lm l 0) =
    address_of_word_labels_code_mem program l).
  ∀old_policy:(Σpolicy:ppc_pc_map.
    (* out_of_program_none program policy *)
    And (And (And (And (not_jump_default program policy)
    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd policy) 〈0,short_jump〉)))
    (sigma_compact_unsafe program labels policy))
    (\fst policy ≤ 2^16)).
  (Σx:bool × (option ppc_pc_map).
    let 〈no_ch,y〉 ≝ x in
    match y with
    [ None ⇒ nec_plus_ultra program old_policy
    | Some p ⇒ And (And (And (And (And (And (And
       (not_jump_default program p)
       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
       (jump_increase program old_policy p))
       (sigma_compact_unsafe program labels p))
       (sigma_jump_equal program old_policy p → no_ch = true))
       (no_ch = true → sigma_pc_equal program old_policy p))
       (\fst p ≤ 2^16)
    ])
    ≝
  λprogram.λlabels.λold_sigma.
  let 〈final_added, final_policy〉 ≝
    pi1 ?? (foldl_strong (option Identifier × pseudo_instruction)
    (λprefix.Σx:ℕ × ppc_pc_map.
      let 〈added,policy〉 ≝ x in
      And (And (And (And (And (And (And (And (And (not_jump_default prefix policy)
      (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
      (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
      (jump_increase prefix old_sigma policy))
      (sigma_compact_unsafe prefix labels policy))
      (sigma_jump_equal prefix old_sigma policy → added = 0))
      (added = 0 → sigma_pc_equal prefix old_sigma policy))
      (out_of_program_none prefix policy))
      (\fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉) =
       \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) + added))
      (sigma_safe prefix labels added old_sigma policy))
    program
    (λprefix.λx.λtl.λprf.λacc.
      let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in
      let 〈label,instr〉 ≝ x in
      (* Now, we must add the current ppc and its pc translation.
       * Three possibilities:
       *   - Instruction is not a jump; i.e. constant size whatever the sigma we use;
       *   - Instruction is a backward jump; we can use the sigma we're constructing,
       *     since it will already know the translation of its destination;
       *   - Instruction is a forward jump; we must use the old sigma (the new sigma
       *     does not know the translation yet), but compensate for the jumps we
       *     have lengthened.
       *)
      let add_instr ≝ match instr with
      [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
      | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
      | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
      | _             ⇒ None ? 
      ] in
      let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in
      let old_length ≝
        \snd (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
      let old_size ≝ instruction_size_jmplen old_length instr in
      let 〈new_length, isize〉 ≝ match add_instr with
      [ None    ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉
      | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉
      ] in
      let new_added ≝ match add_instr with
      [ None   ⇒ inc_added
      | Some x ⇒ plus inc_added (minus isize old_size)
      ] in
      let old_Slength ≝
        \snd (bvt_lookup … (bitvector_of_nat ? (S (|prefix|))) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉) in
      let updated_sigma ≝ 
        (* we add the new PC to the next position and the new jump length to this one *)
        bvt_insert … (bitvector_of_nat ? (S (|prefix|))) 〈inc_pc + isize, old_Slength〉
        (bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma) in
      〈new_added, 〈plus inc_pc isize, updated_sigma〉〉
    ) 〈0, 〈0,
      bvt_insert …
        (bitvector_of_nat ? 0)
        〈0, \snd (bvt_lookup … (bitvector_of_nat ? 0) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)〉
        (Stub ??)〉〉
    ) in
    if gtb (\fst final_policy) 2^16 then
      〈eqb final_added 0, None ?〉
    else
      〈eqb final_added 0, Some ? final_policy〉.
[ normalize nodelta @nmk #Habs lapply p -p cases (foldl_strong ? (λ_.Σx.?) ???)
  #x #H #Heq >Heq in H; normalize nodelta -Heq -x #Hind
  (* USE: inc_pc = fst of policy (from fold) *)
  >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) in p1;
  (* USE: fst policy < 2^16, inc_pc = fst of policy (old_sigma) *)
  lapply (proj2 ?? (pi2 ?? old_sigma)) >(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))
  #Hsig #Hge
  (* USE: added = 0 → policy_pc_equal (from fold) *)
  lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))) ? (|program|) (le_n (|program|)))
  [ (* USE: policy_jump_equal → added = 0 (from fold) *)
    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi
    inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    [ #Hj
      (* USE: policy_increase (from fold) *)
      lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))) i (le_S_to_le … Hi))
      lapply (Habs i Hi ?) [ >Hj %]
      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd old_sigma) 〈0,short_jump〉)
      #opc #oj
      cases (bvt_lookup … (bitvector_of_nat ? i) (\snd final_policy) 〈0,short_jump〉)
      #pc #j normalize nodelta #Heq >Heq cases j
      [1,2: #abs cases abs #abs2 try (cases abs2) @refl
      |3: #_ @refl
      ]
    | #Hnj
      (* USE: not_jump_default (from fold and old_sigma) *)
      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind)))))))) i Hi ?)
      [2: >Hnj %]
      >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))) i Hi ?) try %
      >Hnj %
    ]
  | #abs >abs in Hsig; #Hsig
    @(absurd ? Hsig) @lt_to_not_le @ltb_true_to_lt @Hge
  ]
| normalize nodelta lapply p -p cases (foldl_strong ? (λ_.Σx.?)???) in ⊢ (% → ?); #x #H #H2
  >H2 in H; normalize nodelta -H2 -x #H @conj
  [ @conj [ @conj 
  [ (* USE[pass]: not_jump_default, 0 ↦ 0, inc_pc = fst policy,
     * jump_increase, sigma_compact_unsafe (from fold) *) 
    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))))
  | #H2 (* USE[pass]: sigma_jump_equal → added = 0 (from fold) *)
    @eq_to_eqb_true @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) @H2
  ]
  | (* USE[pass]: added = 0 → sigma_pc_equal (from fold) *)
     #H2 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) @eqb_true_to_eq @H2
  ]
  | @not_lt_to_le @ltb_false_to_not_lt @p1
  ]
|4: lapply (pi2 ?? acc) >p lapply (refl ? (inc_pc_sigma)) cases inc_pc_sigma in ⊢ (???% → %);
  #inc_pc #inc_sigma #Hips
  inversion (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd (pi1 ?? old_sigma)) 〈0,short_jump〉)
  #old_pc #old_length #Holdeq #Hpolicy normalize nodelta in Hpolicy; @pair_elim
  #added #policy normalize nodelta @pair_elim #new_length #isize normalize nodelta
  #Heq1 #Heq2
 cut (S (|prefix|) < 2^16)
 [ @(transitive_lt … (proj1 … (pi2 ?? program))) @le_S_S >prf >append_length
   <plus_n_Sm @le_S_S @le_plus_n_r ] #prefix_ok1
 cut (|prefix| < 2^16) [ @(transitive_lt … prefix_ok1) %] #prefix_ok
 cases (pair_destruct ?????? Heq2) -Heq2 #Heq2a #Heq2b
  % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
  (* NOTE: to save memory and speed up work, there's cases daemon here. They can be
   * commented out for full proofs, but this needs a lot of memory and time *)
  [ (* not_jump_default *)
    @(jump_expansion_step1 … Heq1 Heq2b) try assumption
    @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
  | (* 0 ↦ 0 *)
    @(jump_expansion_step2 … Heq2b) try assumption
    [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))))
    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) ]
  | (* inc_pc = fst of policy *)
    <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
  | (* jump_increase *)
    @(jump_expansion_step3 … (pi1 ?? old_sigma) … prf … p1 ??? old_length Holdeq
      … Heq1 prefix_ok1 prefix_ok Heq2b)
    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
  | (* sigma_compact_unsafe *)
    @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))
    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
  | (* policy_jump_equal → added = 0 *)
    @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
  | (* added = 0 → policy_pc_equal *) cases daemon (*
    @(jump_expansion_step6 … Heq1 … Heq2b) try assumption
    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))
    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    *)
  | (* out_of_program_none *)
    @(jump_expansion_step7 … Heq2b)
    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
  | (* lookup p = lookup old_sigma + added *)
    @(jump_expansion_step8 (pi1 ?? program) (pi1 ?? labels) (pi1 ?? old_sigma) … Holdeq … Heq1 Heq2a Heq2b) try assumption
    [ cases (pi2 … old_sigma) * #_ #H1 #H2 % assumption
    | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    | @(proj2 ?? (proj1 ?? Hpolicy)) ]
  | (* sigma_safe *) cases daemon (*
    @jump_expansion_step9 try assumption
    @(proj2 ?? Hpolicy) *)
  ]      
| normalize nodelta % [ % [ % [ % [ % [ % [ % [ % [ % ]]]]]]]]
  [ #i cases i
    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 
    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
    ]
  | >lookup_insert_hit @refl 
  | >lookup_insert_hit @refl
  | #i #Hi <(le_n_O_to_eq … Hi)
    >lookup_insert_hit cases (bvt_lookup … (bitvector_of_nat ? 0) (\snd old_sigma) 〈0,short_jump〉)
    #a #b normalize nodelta %2 @refl
  | #i cases i
    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 
    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    ]
  | #_ %
  | #_ #i #Hi <(le_n_O_to_eq … Hi) >lookup_insert_hit
    (* USE: 0 ↦ 0 (from old_sigma) *)
    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma)))))
  | #i cases i
    [ #Hi2 @conj
      [ #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
      | >lookup_opt_insert_hit #H destruct (H)
      ]
    | -i #i #Hi2 @conj
      [ #Hi >lookup_opt_insert_miss
        [ / by refl/
        | @bitvector_of_nat_abs
          [ @Hi2
          | / by /
          | @sym_neq @lt_to_not_eq / by /
          ]
        ]
      | #_ @le_S_S @le_O_n
      ]
    ]
  | >lookup_insert_hit (* USE: 0 ↦ 0 (from old_sigma) *)
    >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? old_sigma))))) <plus_n_O %
  | #i cases i
    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O 
    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
    ]
  ]
]
qed.