Changeset 2239


Ignore:
Timestamp:
Jul 24, 2012, 11:09:29 AM (7 years ago)
Author:
sacerdot
Message:

One more lemma polished.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyStep.ma

    r2238 r2239  
    232232qed.
    233233
     234lemma jump_expansion_step4:
     235 ∀labels : label_map.
     236 ∀old_sigma : ppc_pc_map.
     237 ∀prefix : list (option Identifier×pseudo_instruction).
     238 ∀inc_added : ℕ.
     239 ∀inc_pc_sigma : ppc_pc_map.
     240 ∀label : option Identifier.
     241 ∀instr : pseudo_instruction.
     242 ∀inc_pc : ℕ.
     243 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
     244 ∀old_length : jump_length.
     245 ∀Hpolicy1 : sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉.
     246 ∀Hpolicy2: inc_pc
     247    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma
     248                 〈O,short_jump〉).
     249 ∀Hpolicy3: out_of_program_none prefix 〈inc_pc,inc_sigma〉.
     250 ∀policy : ppc_pc_map.
     251 ∀new_length : jump_length.
     252 ∀isize : ℕ.
     253 ∀Heq1 :
     254  match 
     255   match instr
     256    in pseudo_instruction
     257    return λ_:pseudo_instruction.(option jump_length)
     258    with 
     259   [Instruction (i:(preinstruction Identifier))⇒
     260    jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added
     261    (|prefix|) i
     262   |Comment (_:String)⇒None jump_length
     263   |Cost (_:costlabel)⇒None jump_length
     264   |Jmp (j:Identifier)⇒
     265    Some jump_length
     266    (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     267   |Call (c:Identifier)⇒
     268    Some jump_length
     269    (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     270   |Mov (_:[[dptr]])   (_:Identifier)⇒None jump_length]
     271    in option
     272    return λ_:(option jump_length).(jump_length×ℕ)
     273    with 
     274   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     275   |Some (pl:jump_length)⇒
     276    〈max_length old_length pl,
     277    instruction_size_jmplen (max_length old_length pl) instr〉]
     278   =〈new_length,isize〉.
     279 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
     280 ∀prefix_ok : |prefix|< 2 \sup 16.
     281 ∀Heq2b :
     282   〈inc_pc+isize,
     283   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     284   〈inc_pc+isize,
     285   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     286               (\snd  old_sigma) 〈O,short_jump〉)〉
     287   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     288    〈inc_pc,new_length〉 inc_sigma)〉
     289   =policy.
     290 sigma_compact_unsafe (prefix@[〈label,instr〉]) labels policy.
     291 #labels #old_sigma #prefix #inc_added #inc_pc_sigma #label #instr #inc_pc #inc_sigma
     292 #old_length #Hpolicy1 #Hpolicy2 #Hpolicy3 #policy #new_length #isize
     293 #Heq1 #prefix_ok1 #prefix_ok #Heq2b
     294    #i >append_length <commutative_plus #Hi normalize in Hi;
     295    <Heq2b
     296    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
     297    [ >lookup_opt_insert_miss
     298      [ >lookup_opt_insert_miss
     299        [ >lookup_opt_insert_miss
     300          [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
     301            [ >lookup_opt_insert_miss
     302              [ (* USE[pass]: sigma_compact_unsafe *)
     303                lapply (Hpolicy1 i ?)
     304                [ @le_S_to_le @Hi ]
     305                cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     306                [ normalize nodelta #X @X
     307                | #x cases x -x #x1 #x2
     308                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
     309                  normalize nodelta
     310                  [ #X @X
     311                  | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
     312                    [ #X @X
     313                    | @le_S_to_le @Hi
     314                    ]
     315                  ]
     316                ]
     317              | @bitvector_of_nat_abs
     318                [3: @lt_to_not_eq @Hi ]
     319              ]
     320            | >Hi >lookup_opt_insert_hit normalize nodelta
     321              (* USE[pass]: sigma_compact_unsafe *)
     322              lapply (Hpolicy1 i ?)
     323              [ <Hi @le_n
     324              | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
     325                [ normalize nodelta #X @X
     326                | #x cases x -x #x1 #x2
     327                  (* USE: inc_pc = fst inc_sigma *)
     328                  lapply Hpolicy2
     329                  <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
     330                  cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
     331                  [ normalize nodelta #_  #_ #H cases H
     332                  | #y cases y -y #y1 #y2 #Heq >nth_append_first
     333                    [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
     334                      #Heq2 <Heq2 #X @X
     335                    | <Hi @le_n]]]]]]]]
     336      [3,4,5: @bitvector_of_nat_abs]
     337      [ @(transitive_lt ??? (le_S_S … Hi))
     338      |3: @lt_to_not_eq @le_S_S @Hi
     339      |4,7,10: @(transitive_lt ??? Hi) assumption
     340      |5,11: @le_S_to_le
     341      |6: @lt_to_not_eq @Hi
     342      |9: @lt_to_not_eq @le_S @Hi
     343      ]
     344      assumption
     345    | >Hi >lookup_opt_insert_miss
     346      [2: @bitvector_of_nat_abs try assumption @lt_to_not_eq % ]
     347      >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
     348      (* USE: out_of_program_none ← *)
     349      lapply (Hpolicy3 i ?)
     350      [ >Hi assumption
     351      | >Hi
     352        (* USE: inc_pc = fst policy *)
     353        lapply Hpolicy2
     354        inversion (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma)
     355        [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
     356          [ cases H #_ #X @X %
     357          | @le_to_not_lt @le_n]
     358        | * #x1 #x2 #Heq #Hip #_ >nth_append_second
     359          [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
     360          >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
     361          cases instr in Heq1; normalize nodelta
     362          [1: #pi cases (jump_expansion_step_instruction ??????) normalize nodelta]
     363          try (#x #y #Heq1) try (#x #Heq1) try #Heq1
     364          @eq_f <(proj2 ?? (pair_destruct ?????? Heq1))
     365          try % <(proj1 ?? (pair_destruct ?????? Heq1)) %]]]
     366qed.
     367
     368lemma jump_expansion_step5:
     369 ∀labels : label_map.
     370 ∀old_sigma : ppc_pc_map.
     371 ∀prefix : list (option Identifier×pseudo_instruction).
     372 ∀inc_added : ℕ.
     373 ∀inc_pc_sigma : ppc_pc_map.
     374 ∀label : option Identifier.
     375 ∀instr : pseudo_instruction.
     376 ∀inc_pc : ℕ.
     377 ∀inc_sigma : BitVectorTrie (ℕ×jump_length) 16.
     378 ∀old_pc : ℕ.
     379 ∀old_length : jump_length.
     380 ∀Holdeq :
     381  lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd  old_sigma)
     382   〈O,short_jump〉
     383   =〈old_pc,old_length〉.
     384 ∀Hpolicy1 : sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O.
     385 ∀Hpolicy2: inc_pc
     386    =\fst  (lookup … (bitvector_of_nat … (|prefix|)) inc_sigma 〈O,short_jump〉).
     387 ∀added : ℕ.
     388 ∀policy : ppc_pc_map.
     389 ∀new_length : jump_length.
     390 ∀isize : ℕ.
     391 let add_instr ≝ match instr with
     392  [ Jmp  j        ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j)
     393  | Call c        ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c)
     394  | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i
     395  | _             ⇒ None ?
     396  ] in
     397 ∀Heq1 :
     398  match add_instr with 
     399   [None⇒〈short_jump,instruction_size_jmplen short_jump instr〉
     400   |Some (pl:jump_length)⇒
     401    〈max_length old_length pl,
     402    instruction_size_jmplen (max_length old_length pl) instr〉]
     403   =〈new_length,isize〉.
     404 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16.
     405 ∀prefix_ok : |prefix|< 2 \sup 16.
     406 ∀Heq2a :
     407  match add_instr with 
     408   [None⇒inc_added
     409   |Some (x0:jump_length)⇒
     410    inc_added+(isize-instruction_size_jmplen old_length instr)]
     411   =added.
     412 ∀Heq2b :
     413  〈inc_pc+isize,
     414   insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     415   〈inc_pc+isize,
     416   \snd  (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (S (|prefix|)))
     417               (\snd  old_sigma) 〈O,short_jump〉)〉
     418   (insert (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|))
     419    〈inc_pc,new_length〉 inc_sigma)〉
     420   =policy.
     421 sigma_jump_equal (prefix@[〈label,instr〉]) old_sigma policy→added=O.
     422 #labels #old_sigma #prefix #inc_added #inc_pc #label #instr #inc_pc #inc_sigma
     423 #old_pc #old_length #Holdeq #Hpolicy1 #Hpolicy2 #added #policy #new_length #isize
     424 #Heq1 #prefix_ok1 #prefix_ok #Heq2a #Heq2b
     425    <Heq2b #Heq <Heq2a
     426    (* USE[pass]: policy_jump_equal → added = 0 *)
     427    >Hpolicy1
     428    [ cases instr in Heq1 Heq;
     429      [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
     430      |1: #pi normalize nodelta whd in match jump_expansion_step_instruction;
     431          normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]]
     432      #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
     433      #Heq (*CSC: make a lemma here!*) lapply Holdeq -Holdeq
     434      (* USE: inc_pc = fst inc_sigma *)
     435      >Hpolicy2
     436      lapply (Heq (|prefix|) ?)
     437      [1,3,5: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
     438      -Heq >lookup_insert_miss
     439      [1,3,5: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
     440        #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
     441        #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n %
     442      |*: @bitvector_of_nat_abs try assumption @lt_to_not_eq %]
     443    | #i #Hi lapply (Heq i ?)
     444      [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
     445      | >lookup_insert_miss
     446        [ >lookup_insert_miss
     447          [ #X @X
     448          | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
     449            @lt_to_not_eq @Hi]
     450        | @bitvector_of_nat_abs [ @(transitive_lt ??? Hi) ] try assumption
     451          @lt_to_not_eq @le_S @Hi ]]]
     452qed.
     453
    234454(* One step in the search for a jump expansion fixpoint. *)
    235455definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.
     
    400620    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))
    401621    cases (pi2 … old_sigma) * * * #H #_ #_ #_ #_ @H
    402   | (* sigma_compact_unsafe *) cases daemon (*
    403     #i >append_length <commutative_plus #Hi normalize in Hi;
    404     <(proj2 ?? (pair_destruct ?????? Heq2))
    405     cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
    406     [ >lookup_opt_insert_miss
    407       [ >lookup_opt_insert_miss
    408         [ >lookup_opt_insert_miss
    409           [ cases (le_to_or_lt_eq … Hi) -Hi #Hi
    410             [ >lookup_opt_insert_miss
    411               [ (* USE[pass]: sigma_compact_unsafe *)
    412                 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    413                 [ @le_S_to_le @Hi ]
    414                 cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
    415                 [ normalize nodelta #X @X
    416                 | #x cases x -x #x1 #x2
    417                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma)
    418                   normalize nodelta
    419                   [ #X @X
    420                   | #y cases y -y #y1 #y2 normalize nodelta >nth_append_first
    421                     [ #X @X
    422                     | @le_S_to_le @Hi
    423                     ]
    424                   ]
    425                 ]
    426               | @bitvector_of_nat_abs
    427                 [3: @lt_to_not_eq @Hi ]
    428               ]
    429             | >Hi >lookup_opt_insert_hit normalize nodelta
    430               (* USE[pass]: sigma_compact_unsafe *)
    431               lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i ?)
    432               [ <Hi @le_n
    433               | cases (bvt_lookup_opt … (bitvector_of_nat ? i) inc_sigma)
    434                 [ normalize nodelta #X @X
    435                 | #x cases x -x #x1 #x2
    436                   (* USE: inc_pc = fst inc_sigma *)
    437                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    438                   <Hi lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma))
    439                   cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) inc_sigma) in ⊢ (???% → %);
    440                   [ normalize nodelta #_  #_ #H cases H
    441                   | #y cases y -y #y1 #y2 #Heq >nth_append_first
    442                     [ normalize nodelta >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
    443                       #Heq2 <Heq2 #X @X
    444                     | <Hi @le_n
    445                     ]
    446                   ]
    447                 ]
    448               ]
    449             ]
    450           ]
    451         ]
    452       ]
    453       [3,4,5: @bitvector_of_nat_abs]
    454       [ @(transitive_lt ??? (le_S_S … Hi))
    455       |3: @lt_to_not_eq @le_S_S @Hi
    456       |4,7,10: @(transitive_lt ??? Hi) @le_S_to_le
    457       |5,11: @le_S_to_le
    458       |6: @lt_to_not_eq @Hi
    459       |9: @lt_to_not_eq @le_S @Hi
    460       ]
    461       @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
    462         <plus_n_Sm @le_S_S @le_plus_n_r
    463     | >Hi >lookup_opt_insert_miss
    464       [2: @bitvector_of_nat_abs
    465         [ @le_S_to_le ]
    466         [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    467           <plus_n_Sm @le_S_S @le_plus_n_r
    468         | @lt_to_not_eq @le_n
    469         ]
    470       ]
    471       >lookup_opt_insert_hit >lookup_opt_insert_hit normalize nodelta
    472       (* USE: out_of_program_none ← *)
    473       lapply (proj2 ?? (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i ?))
    474       [ >Hi @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S @le_plus_n_r
    475       | >Hi
    476         (* USE: inc_pc = fst policy *)
    477         lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    478         lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma))
    479         cases (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) inc_sigma) in ⊢ (???% → %);
    480         [ #Heq #_ #H @⊥ @(absurd (|prefix| > |prefix|))
    481           [ @H %
    482           | @le_to_not_lt @le_n
    483           ]
    484         | #x cases x -x #x1 #x2 #Heq #Hip #_ >nth_append_second
    485           [2: @le_n] <minus_n_n whd in match (nth ????); normalize nodelta
    486           >Hip >(lookup_opt_lookup_hit … Heq 〈0,short_jump〉)
    487           cases instr in Heq1;
    488           [2,3,6: #x [3: #y] #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    489             <(proj1 ?? (pair_destruct ?????? Heq1)) %
    490           |4,5: #x #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    491             <(proj1 ?? (pair_destruct ?????? Heq1)) %
    492           |1: #pi cases pi normalize nodelta
    493             [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:
    494               [1,2,3,6,7,24,25: #x #y
    495               |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
    496               #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    497               <(proj1 ?? (pair_destruct ?????? Heq1)) %
    498             |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
    499               <(proj2 ?? (pair_destruct ?????? Heq1))
    500               <(proj1 ?? (pair_destruct ?????? Heq1)) %
    501             ]
    502           ]
    503         ]
    504       ]
    505     ]
    506   ] *)
    507   | (* policy_jump_equal → added = 0 *) cases daemon (*
    508     <(proj2 ?? (pair_destruct ?????? Heq2))
    509     #Heq <(proj1 ?? (pair_destruct ?????? Heq2))
    510     (* USE[pass]: policy_jump_equal → added = 0 *)
    511     >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) ?)
    512     [ cases instr in Heq1 Heq;
    513       [2,3,6: #x [3: #y] normalize nodelta #_ #_ %
    514       |4,5: #x normalize nodelta #Heq1 <(proj2 ?? (pair_destruct ?????? Heq1))
    515         #Heq lapply Holdeq -Holdeq
    516         (* USE: inc_pc = fst inc_sigma *)
    517         >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    518         lapply (Heq (|prefix|) ?)
    519         [1,3: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
    520         -Heq >lookup_insert_miss
    521         [1,3: >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1))
    522           #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
    523           #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n %
    524         |2,4: @bitvector_of_nat_abs
    525           [1,4: @le_S_to_le]
    526           [1,2,3,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
    527             <plus_n_Sm @le_S_S @le_plus_n_r
    528           |4,6: @lt_to_not_eq @le_n
    529           ]
    530         ]
    531       |1: #pi cases pi normalize nodelta
    532         [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:
    533           [1,2,3,6,7,24,25: #x #y
    534           |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #_ @refl
    535         |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Heq1
    536           <(proj2 ?? (pair_destruct ?????? Heq1)) #Heq lapply Holdeq -Holdeq
    537           (* USE: inc_pc = fst inc_sigma *)
    538           >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    539           lapply (Heq (|prefix|) ?)
    540           [1,3,5,7,9,11,13,15,17: >append_length <plus_n_Sm @le_S_S @le_plus_n_r]
    541           -Heq >lookup_insert_miss
    542           [1,3,5,7,9,11,13,15,17: >lookup_insert_hit in ⊢ (???(???%) → ?); <(proj1 ?? (pair_destruct ?????? Heq1))
    543             #Heq <Heq cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)
    544             #y #z #Hyz >(proj2 ?? (pair_destruct ?????? Hyz)) <minus_n_n / by /
    545           |2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs
    546             [3,6,9,12,15,18,21,24,27: @lt_to_not_eq @le_n
    547             |1,4,7,10,13,16,19,22,25: @le_S_to_le
    548             ]
    549             @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S
    550               >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r
    551           ]
    552         ]
    553       ]
    554     | #i #Hi lapply (Heq i ?)
    555       [ >append_length <plus_n_Sm @le_S <plus_n_O @Hi
    556       | >lookup_insert_miss
    557         [ >lookup_insert_miss
    558           [ / by /
    559           | @bitvector_of_nat_abs
    560             [ @(transitive_lt ??? Hi) ]
    561             [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    562               @le_plus_n_r
    563             | @lt_to_not_eq @Hi
    564             ]
    565           ]
    566         | @bitvector_of_nat_abs
    567           [ @(transitive_lt ??? Hi) @le_S_to_le ]
    568           [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
    569             <plus_n_Sm @le_S_S @le_plus_n_r
    570           | @lt_to_not_eq @le_S @Hi
    571           ]
    572         ]
    573       ]
    574     ]
    575   ] *)
     622  | (* sigma_compact_unsafe *)
     623    @(jump_expansion_step4 … Heq1 … Heq2b) try assumption
     624    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ??  (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
     625    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))
     626    @(proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)))
     627  | (* policy_jump_equal → added = 0 *)
     628    @(jump_expansion_step5 … Holdeq … Heq1 … Heq2b) try assumption
     629    try @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))
     630    @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))))))
    576631  | (* added = 0 → policy_pc_equal *) cases daemon
    577632    (* USE[pass]: added = 0 → policy_pc_equal *)
Note: See TracChangeset for help on using the changeset viewer.