Changeset 2246


Ignore:
Timestamp:
Jul 24, 2012, 5:51:11 PM (7 years ago)
Author:
sacerdot
Message:

Final technical lemma streamlined. Maybe it can be streamlined even more.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2245 r2246  
    589589    lapply Hpolicy1 <Heq2b <Heq2a lapply Heq1 -Heq1
    590590    inversion instr normalize nodelta
    591     [2,3,6: #x [3: #y] #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
    592       #Hi normalize in Hi;
    593       cases (le_to_or_lt_eq … Hi) -Hi #Hi
    594       [1,3,5: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    595         [1,3,5: <Heq2b >lookup_insert_miss
    596           [1,3,5: >lookup_insert_miss
    597             [1,3,5: @(Hold Hadded i (le_S_to_le … Hi))
    598             |*: @bitvector_of_nat_abs try assumption
    599               [2,4,6: @lt_to_not_eq @Hi
    600               |*: @(transitive_lt ??? Hi) assumption ]]
     591    [ #pi #Hins whd in match jump_expansion_step_instruction; normalize nodelta
     592      lapply (destination_of_None_to_is_jump_false pi)
     593      lapply (destination_of_Some_to_is_jump_true pi)
     594      cases (destination_of ?) normalize nodelta
     595      [ #_ #dest_None | #tgt #dest_Some #_ ]]
     596    try (#x #y #Hins #Heq1 #Hold #Hadded #i #Hi)
     597    try (#x #Hins #Heq1 #Hold #Hadded #i #Hi)
     598    try (#Heq1 #Hold #Hadded #i #Hi)
     599    >append_length in Hi; >commutative_plus #Hi normalize in Hi;
     600    cases (le_to_or_lt_eq … Hi) -Hi #Hi
     601    [1,3,5,7,9,11,13: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     602      [1,3,5,7,9,11,13: <Heq2b >lookup_insert_miss
     603        [1,3,5,7,9,11,13: >lookup_insert_miss
     604          [1,3,5,7,9,11,13:
     605            try @(Hold Hadded i (le_S_to_le … Hi))
     606            @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded; @plus_zero_zero
    601607          |*: @bitvector_of_nat_abs try assumption
    602             [2,4,6: @lt_to_not_eq @le_S @Hi
    603             |*: @(transitive_lt … Hi) assumption ]]
    604         |*: >Hi >lookup_insert_miss
    605           [1,3,5: >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|)))
    606             @sym_eq (* USE: fst p = lookup |prefix| *)
    607             @Hpolicy2
    608           |*: @bitvector_of_nat_abs try assumption
    609               @lt_to_not_eq %]]
    610       |2,4,6: >Hi >lookup_insert_hit
    611         (* USE fst p = lookup |prefix| *)
    612         >Hpolicy2
    613         <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    614         (* USE: sigma_compact (from old_sigma) *)
    615         lapply (pi2 ?? old_sigma (|prefix|) ?)
    616         [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    617         |*:
    618           inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
    619           [1,3,5: normalize nodelta #_ #ABS cases ABS
    620           |*: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
    621             [1,3,5: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS
    622             |*: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ
    623               normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
    624               >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    625               >prf >p1 >Hins >nth_append_second try %
    626               <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
    627                  #H >H @plus_left_monotone @instruction_size_irrelevant % ]]]]
    628     |4,5: #x #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus
    629        #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
    630        [1,3: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    631          [1,3: >lookup_insert_miss
    632            [1,3: >lookup_insert_miss
    633              [1,3: @(Hold ? i (le_S_to_le … Hi)) >commutative_plus in Hadded;
    634                @plus_zero_zero
    635              |2,4: @bitvector_of_nat_abs
    636                [3,6: @lt_to_not_eq @Hi
    637                |1,4: @(transitive_lt ??? Hi)
    638                ]
    639                assumption
    640              ]
    641            |2,4: @bitvector_of_nat_abs
    642              [3,6: @lt_to_not_eq @le_S @Hi
    643              |1,4: @(transitive_lt ??? Hi) assumption]
    644              assumption ]
    645          |2,4: >Hi >lookup_insert_miss
    646            [1,3: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
    647              [2,4: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
     608            [2,4,6,8,10,12,14: @lt_to_not_eq @Hi
     609            |*: @(transitive_lt ??? Hi) assumption ]]
     610        |*: @bitvector_of_nat_abs try assumption
     611          [2,4,6,8,10,12,14: @lt_to_not_eq @le_S @Hi
     612          |*: @(transitive_lt … Hi) assumption ]]
     613      |*: >Hi >lookup_insert_miss
     614        [1,3,5,7,9,11,13: >lookup_insert_hit
     615          try (>(Hold Hadded (|prefix|) (le_n (|prefix|)))
     616               @sym_eq (* USE: fst p = lookup |prefix| *)
     617               @Hpolicy2)
     618          >(Hold ? (|prefix|) (le_n (|prefix|)))
     619          [2,4,6,8: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
    648620             (* USE: fst p = lookup |prefix| *)
    649              @Hpolicy2
    650            |2,4: @bitvector_of_nat_abs try assumption
    651              @lt_to_not_eq @le_n]]
    652        |2,4: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
    653          elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
    654          [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt <(proj2 ?? (pair_destruct ?????? Heq1))
    655            @jump_length_le_max %
    656          |*: #H (* USE: fst p = lookup |prefix| *)
    657            >Hpolicy2
    658            <(Hold ? (|prefix|) (le_n (|prefix|)))
    659            [1,3: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
    660              >(jump_length_equal_max … H) try %
    661              (* USE: sigma_compact_unsafe (from old_sigma) *)
    662              lapply (pi2 ?? old_sigma (|prefix|) ?)
    663              [1,3: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    664              |2,4: inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
    665                [1,3: normalize nodelta #_ #ABS cases ABS
    666                |2,4: normalize nodelta
    667                  inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
    668                  [1,3: #_ * #pc #j normalize nodelta #_ #ABS cases ABS
    669                  |2,4: * #Spc #Sj #EQS #x cases x -x #pc #j #EQ
    670                    normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    671                    >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
    672                    >EQpair @eq_f >prf >nth_append_second try %
    673                    <minus_n_n >p1 whd in match (nth ????); >Hins
    674                    >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
    675                    >(proj2 … (pair_destruct … EQ')) % ]]]
    676            |2,4: @plus_zero_zero [2,4: >commutative_plus @Hadded |*: skip]]]]
    677      |1: #pi cases pi normalize nodelta
    678       [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:
    679         [1,2,3,6,7,24,25: #x #y
    680         |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    681         #Hins #Heq1 #Hold #Hadded #i >append_length >commutative_plus #Hi normalize in Hi;
    682         cases (le_to_or_lt_eq … Hi) -Hi #Hi
    683         [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:
    684           cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    685           [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:
    686             <(proj2 ?? (pair_destruct ?????? Heq2))
    687             >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
    688             [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:
    689               >(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)
    690               [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:
    691                 @(Hold Hadded i (le_S_to_le … Hi))
    692               |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:
    693                 @bitvector_of_nat_abs
    694                 [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:
    695                   @lt_to_not_eq @Hi
    696                 |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:
    697                   @(transitive_lt ??? Hi)
    698                 ]
    699                 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    700                 @le_S_S <plus_n_Sm @le_S @le_plus_n_r
    701               ]
    702             |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:
    703               @bitvector_of_nat_abs
    704               [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:
    705                 @lt_to_not_eq @le_S @Hi
    706               |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:
    707                 @(transitive_lt … Hi) @le_S_to_le
    708               ]
    709               @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    710               @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    711             ]
    712           |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:
    713             >Hi >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
    714             [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:
    715               >lookup_insert_hit >(Hold Hadded (|prefix|) (le_n (|prefix|))) @sym_eq
    716               (* USE: fst p = lookup |prefix| *)
    717               @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    718             |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:
    719               @bitvector_of_nat_abs
    720               [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:
    721                 @lt_to_not_eq @le_n
    722               |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:
    723                 @le_S_to_le
    724               ]
    725               @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length
    726                 @le_S_S <plus_n_Sm @le_S_S @le_plus_n_r
    727             ]
    728           ]
    729         |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56:
    730           >Hi >lookup_insert_hit
    731           (* USE fst p = lookup |prefix| *)
    732           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    733           <(Hold Hadded (|prefix|) (le_n (|prefix|)))
    734           (* USE: sigma_compact (from old_sigma) *)
    735           lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    736           [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:
    737             >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    738           |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:
    739             lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    740             cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% -> %);
    741             [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:
    742               normalize nodelta #_ #ABS cases ABS
    743             |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:
    744               lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    745               cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    746               [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55:
    747                 normalize nodelta #Hl #x cases x -x #pc #j normalize nodelta #Hl2 #ABS cases ABS
    748               |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:
    749                 normalize nodelta #x cases x -x #Spc #Sj #EQS #x cases x -x #pc #j #EQ
    750                 normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
    751                 >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    752                 >prf >p1 >Hins >nth_append_second
    753                 [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:
    754                   @(le_n (|prefix|))
    755                 |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:
    756                   <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
    757                   #H >H @plus_left_monotone @instruction_size_irrelevant @nmk #H @H
    758                 ]
    759               ]
    760             ]
    761           ]
    762         ]
    763       |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Hold #Hadded
    764         #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi)
    765         -Hi #Hi
    766         [1,3,5,7,9,11,13,15,17: cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    767           [1,3,5,7,9,11,13,15,17:
    768             >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 i))
    769             [1,3,5,7,9,11,13,15,17:
    770               >(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)
    771               [1,3,5,7,9,11,13,15,17: @(Hold ? i (le_S_to_le … Hi))
    772                 >commutative_plus in Hadded; @plus_zero_zero
    773               |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    774                 [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi
    775                 |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi)
    776                 ]
    777                 @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
    778                 >append_length @le_plus_n_r
    779               ]
    780             |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    781               [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_S @Hi
    782               |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? Hi) @le_S_to_le
    783               ]
    784               @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
    785               >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    786             ]
    787           |2,4,6,8,10,12,14,16,18: >Hi
    788             >(lookup_insert_miss (ℕ×jump_length) 〈0,short_jump〉 〈inc_pc+isize,?〉 16 (bitvector_of_nat 16 (S (|prefix|))) (bitvector_of_nat 16 (|prefix|)))
    789             [1,3,5,7,9,11,13,15,17: >lookup_insert_hit >(Hold ? (|prefix|) (le_n (|prefix|)))
    790               [2,4,6,8,10,12,14,16,18: >commutative_plus in Hadded; @plus_zero_zero] @sym_eq
    791               (* USE: fst p = lookup |prefix| *)
    792               @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    793             |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    794               [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
    795               |1,4,7,10,13,16,19,22,25: @(transitive_lt ??? (le_S_S … (le_n (|prefix|))))
    796               ]
    797               @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf
    798               >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    799             ]
    800           ]
    801         |2,4,6,8,10,12,14,16,18: >Hi >lookup_insert_hit <(proj2 ?? (pair_destruct ?????? Heq1))
    802           elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
    803           [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt
    804             <(proj2 ?? (pair_destruct ?????? Heq1)) @jump_length_le_max / by I/
    805           |2,4,6,8,10,12,14,16,18: #H (* USE: fst p = lookup |prefix| *)
    806             >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    807             <(Hold ? (|prefix|) (le_n (|prefix|)))
    808             [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq1)) in H; #H
    809               >(jump_length_equal_max … H)
    810               [1,3,5,7,9,11,13,15,17: (* USE: sigma_compact_unsafe (from old_sigma) *)
    811                 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?)
    812                 [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    813                 |2,4,6,8,10,12,14,16,18: lapply Holdeq
    814                   lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)))
    815                   cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %);
    816                   [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #ABS cases ABS
    817                   |2,4,6,8,10,12,14,16,18: normalize nodelta
    818                     lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)))
    819                     cases (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %);
    820                     [1,3,5,7,9,11,13,15,17: #_ #x cases x -x #pc #j normalize nodelta
    821                       #_ #_ #ABS cases ABS
    822                     |2,4,6,8,10,12,14,16,18: #x cases x -x #Spc #Sj #EQS #x cases x -x
    823                       #pc #j #EQ
    824                       normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
    825                       >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) #EQpair
    826                       >(proj2 ?? (pair_destruct ?????? EQpair)) >prf >nth_append_second
    827                       [1,3,5,7,9,11,13,15,17: <minus_n_n >p1 whd in match (nth ????); >Hins #H @H
    828                       |2,4,6,8,10,12,14,16,18: @le_n
    829                       ]
    830                     ]
    831                   ]
    832                 ]
    833               |2,4,6,8,10,12,14,16,18: / by I/
    834               ]
    835             |2,4,6,8,10,12,14,16,18: @plus_zero_zero
    836               [2,4,6,8,10,12,14,16,18: >commutative_plus @Hadded]
    837             ]
    838           ]
    839         ]
    840       ]
    841     ]
     621          @Hpolicy2
     622        |*: @bitvector_of_nat_abs try assumption
     623            @lt_to_not_eq %]]
     624    |*: >Hi >lookup_insert_hit
     625      (* USE fst p = lookup |prefix| *)
     626      >Hpolicy2
     627      <(Hold ? (|prefix|) (le_n (|prefix|))) try @Hadded
     628      [3,7,9: @plus_zero_zero [2,4,6: >commutative_plus @Hadded |*: skip]]
     629      (* USE: sigma_compact (from old_sigma) *)
     630      lapply (pi2 ?? old_sigma (|prefix|) ?)
     631      [1,3,5,7,9,11,13: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
     632      |*:
     633        inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))
     634        [1,3,5,7,9,11,13: normalize nodelta #_ #ABS cases ABS
     635        |*: inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))
     636          [1,3,5,7,9,11,13: normalize nodelta #Hl * #pc #j normalize nodelta #Hl2 #ABS cases ABS
     637          |*: normalize nodelta * #Spc #Sj #EQS * #pc #j #EQ
     638            normalize nodelta >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉)
     639            >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
     640            >prf >p1 >Hins >nth_append_second try %
     641            <minus_n_n whd in match (nth ????); <(proj2 ?? (pair_destruct ?????? Heq1))
     642            #H >H @plus_left_monotone
     643            [1,3,4,7: @instruction_size_irrelevant try %
     644              whd in match is_jump; normalize nodelta >dest_None %
     645            |*: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ'
     646                >(proj2 … (pair_destruct … EQ'))
     647               elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … Hadded)))
     648               [1,3,5: #H @⊥ @(absurd ? H) @le_to_not_lt
     649                 <(proj2 ?? (pair_destruct ?????? Heq1))
     650                 @jump_length_le_max try %
     651                 whd in match is_jump; normalize nodelta >dest_Some %]
     652               #EQisize >(proj2 … (pair_destruct … Heq1)) >EQisize % ]]]]]
    842653qed.
    843654
Note: See TracChangeset for help on using the changeset viewer.