Changeset 1606 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Dec 14, 2011, 1:40:08 PM (8 years ago)
Author:
sacerdot
Message:

Porting to last library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1593 r1606  
    679679  [ #Hi #l normalize nodelta; cases label normalize nodelta
    680680    [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl
    681       lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
     681      lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 
    682682      % [ @addr | @Haddr ]
    683683    | #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) -Hocc;
     
    686686        >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 
    687687        @⊥ @(absurd … Hocc)
    688       | normalize nodelta lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
     688      | normalize nodelta lapply (pi2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)
    689689        [ #addr #Haddr % [ @addr | <Haddr @lookup_add_miss /2/ ]
    690690        | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; //
     
    832832   cases (lookup_opt … (bitvector_of_nat 16 i) policy) in ⊢ (???% → ?);
    833833   [ #H @H
    834    | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (sig2 ?? policy) i Hi))
     834   | #x cases x #y #z #H @⊥ @(absurd ? ? Hnotjmp) @(proj2 ?? (proj2 ?? (pi2 ?? policy) i Hi))
    835835     @(ex_intro … y (ex_intro … z H))
    836836   ]
    837  | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (sig2 ?? policy) i Hi) Hj)
     837 | #Hnone @nmk #Hj lapply (proj1 ?? (proj2 ?? (pi2 ?? policy) i Hi) Hj)
    838838   #H elim H -H; #x #H elim H -H; #y #H >H in Hnone; #abs destruct (abs)
    839839 ] 
     
    868868     | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    869869     | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    870      | _ ⇒ (eject … policy)
     870     | _ ⇒ (pi1 … policy)
    871871     ]
    872872   | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    873873   | Jmp j  ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈0,short_jump〉 policy
    874    | _      ⇒ (eject … policy)
     874   | _      ⇒ (pi1 … policy)
    875875   ]
    876876  ) (Stub ? ?).
     
    881881  #i >append_length <commutative_plus #Hi normalize in Hi;
    882882  [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,57,59,61:
    883    #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i)
     883   #Hi2 cases (le_to_or_lt_eq … Hi) -Hi; #Hi @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i)
    884884   [1,5,9,13,17,21,25,29,33,37,41,45,49,53,57,61,65,69,73,77,81,85,89,93,97,101,105,109,113,117,121:
    885885     @le_S_to_le @le_S_to_le @Hi
     
    895895  [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,57,59,61:
    896896    >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi))
    897     @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     897    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    898898  ]
    899899  @conj >(injective_S … Hi)
     
    902902   ]
    903903   #H elim H; -H; #t1 #H elim H; -H #t2 #H
    904    >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
     904   >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?) in H;
    905905   [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,57,59,61:
    906906     #H destruct (H)
    907907   ]
    908    @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
     908   @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    909909   @le_plus_n_r
    910910 ]
     
    912912 -Hi; #Hi
    913913 [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,57,59,61:
    914   #Hj @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi))
     914  #Hj @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi))
    915915  >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) in Hj; //
    916916 ]
     
    922922    #i >append_length <commutative_plus #Hi #Hi2 normalize in Hi; >lookup_opt_insert_miss
    923923   [1,3,5,7,9,11,13,15,17,19,21:
    924      @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     924     @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    925925   ]
    926926   >eq_bv_sym @bitvector_of_nat_abs
    927927   [1,4,7,10,13,16,19,22,25,28,31:
    928      @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
     928     @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm @le_S_S
    929929     @le_plus_n_r
    930930   |2,5,8,11,14,17,20,23,26,29,32: @Hi2
     
    937937   >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) >lookup_opt_insert_miss
    938938   [1,3,5,7,9,11,13,15,17,19,21:
    939     @(proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     939    @(proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    940940   ]
    941941   @bitvector_of_nat_abs
     
    943943   |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    944944   ]
    945    @(transitive_lt … (sig2 ?? program))
     945   @(transitive_lt … (pi2 ?? program))
    946946   >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    947947  ]
     
    957957  >(nth_append_first ?? prefix ?? (le_S_S_to_le … Hi)) #Hj >lookup_opt_insert_miss
    958958  [1,3,5,7,9,11,13,15,17,19,21:
    959    @(proj2 ?? (sig2 ?? policy) i (le_S_S_to_le … Hi) Hj)
     959   @(proj2 ?? (pi2 ?? policy) i (le_S_S_to_le … Hi) Hj)
    960960  ]
    961961  @bitvector_of_nat_abs
     
    963963  |1,4,7,10,13,16,19,22,25,28,31: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    964964  ]
    965   @(transitive_lt … (sig2 ?? program))
     965  @(transitive_lt … (pi2 ?? program))
    966966  >prf >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r
    967967 ]
     
    10281028[ @conj [ @conj #i >append_length <commutative_plus #Hi normalize in Hi;
    10291029[ #Hi2 cases (lookup ??? old_policy ?) #h #n cases add_instr
    1030   [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     1030  [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    10311031  | #z normalize nodelta >lookup_opt_insert_miss
    1032     [ @(proj1 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_to_le … Hi) Hi2)
     1032    [ @(proj1 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_to_le … Hi) Hi2)
    10331033    | >eq_bv_sym @bitvector_of_nat_abs
    1034       [ @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1034      [ @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10351035        @le_S_S @le_plus_n_r
    10361036      | @Hi2
     
    10411041| cases (le_to_or_lt_eq … Hi) -Hi;
    10421042  [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) @conj
    1043     [ #Hj lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
     1043    [ #Hj lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    10441044      cases add_instr cases (lookup ??? old_policy ?) normalize nodelta #x #y
    10451045      [ @(proj1 ?? Hacc Hj)
     
    10491049        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    10501050        ]
    1051         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1051        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10521052        @le_S_S @le_plus_n_r
    10531053        ] ]
    10541054      ]
    1055     | lapply (proj2 ?? (proj1 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
     1055    | lapply (proj2 ?? (proj1 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi)) #Hacc
    10561056      #H elim H -H; #h #H elim H -H; #n cases add_instr cases (lookup ??? old_policy ?)
    10571057      normalize nodelta #x #y [2: #z]
     
    10611061        |1: @(transitive_lt ??? (le_S_S_to_le ?? Hi))
    10621062        ]
    1063         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1063        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10641064        @le_S_S @le_plus_n_r
    10651065      | @Hl
     
    10711071     [3,5,11: #H @⊥ @H (* instr is not a jump *)
    10721072     |4,6,12: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    1073        #x #y normalize nodelta >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1073       #x #y normalize nodelta >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    10741074       [1,3,5: #H destruct (H)]
    1075        @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1075       @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    10761076       @le_S_S @le_plus_n_r
    10771077     |7,9: (* instr is a jump *) #_ cases (lookup ??? old_policy ?) #h #n
     
    10951095       |72,73,74: #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    10961096        #x #y normalize nodelta
    1097         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1097        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    10981098        [1,3,5: #H destruct (H)]
    1099         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1099        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11001100        @le_S_S @le_plus_n_r     
    11011101       |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: #x
    11021102        #H elim H -H; #h #H elim H -H #n cases (lookup ??? old_policy ?)
    11031103        #x #y normalize nodelta
    1104         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1104        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11051105        [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35: #H destruct (H)]
    1106         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1106        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11071107        @le_S_S @le_plus_n_r
    11081108       |38,39,40,43,44,70,71: #x #y #H elim H -H; #h #H elim H -H #n
    11091109        cases (lookup ??? old_policy ?) #x #y normalize nodelta
    1110         >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1110        >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11111111        [1,3,5,7,9,11,13: #H destruct (H)]
    1112         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1112        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11131113        @le_S_S @le_plus_n_r             
    11141114       |46,47,51,52: #id #_ //
     
    11221122    cases (le_to_or_lt_eq … Hi) -Hi; #Hi
    11231123    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    1124       #x #y @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     1124      #x #y @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    11251125    | normalize nodelta >(injective_S … Hi)
    11261126      >lookup_opt_lookup_miss
     
    11291129        | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    11301130          #x #y normalize nodelta
    1131           >(proj1 ?? (proj1 ?? (sig2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
     1131          >(proj1 ?? (proj1 ?? (pi2 ?? policy)) (|prefix|) (le_n (|prefix|)) ?)
    11321132          [ //
    1133           | @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1133          | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11341134            @le_S_S @le_plus_n_r
    11351135          ]
     
    11601160    [ cases (lookup … (bitvector_of_nat ? (|prefix|)) old_policy 〈0,short_jump〉)
    11611161      #y #z normalize nodelta normalize nodelta >lookup_insert_miss
    1162       [ @((proj2 ?? (sig2 ?? policy)) i (le_S_S_to_le … Hi))
     1162      [ @((proj2 ?? (pi2 ?? policy)) i (le_S_S_to_le … Hi))
    11631163      | @bitvector_of_nat_abs
    11641164        [3: @lt_to_not_eq @(le_S_S_to_le … Hi)
    11651165        |1: @(transitive_lt ??? (le_S_S_to_le … Hi))
    11661166        ]
    1167         @(transitive_lt … (sig2 ?? program)) >prf >append_length normalize <plus_n_Sm
     1167        @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm
    11681168        @le_S_S @le_plus_n_r
    11691169      ]
    1170     | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (sig2 ?? old_policy) (|prefix|) ?) ?)
     1170    | >(injective_S … Hi) elim (proj1 ?? (proj2 ?? (pi2 ?? old_policy) (|prefix|) ?) ?)
    11711171      [ #a #H elim H -H; #b #H >H >(lookup_opt_lookup_hit … 〈a,b〉 H)
    11721172        normalize nodelta >lookup_insert_hit @jmpleq_max_length
     
    12071207  | S m ⇒ jump_expansion_step program (jump_expansion_internal program m)
    12081208  ].
    1209 [ @(proj1 ?? (sig2 ?? (jump_expansion_start program)))
    1210 | @(proj1 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program m))))
     1209[ @(proj1 ?? (pi2 ?? (jump_expansion_start program)))
     1210| @(proj1 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program m))))
    12111211]
    12121212qed.
     
    12491249     [ @refl
    12501250     | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p2)) n Hn))
    1251        [ @(proj1 ?? (sig2 … (jump_expansion_step program p2)))
     1251       [ @(proj1 ?? (pi2 … (jump_expansion_step program p2)))
    12521252       | @Hnotjmp
    12531253       ]
    12541254     ]
    12551255   | @(proj1 ?? (jump_not_in_policy program (eject … (jump_expansion_step program p1)) n Hn))
    1256      [ @(proj1 ?? (sig2 ?? (jump_expansion_step program p1)))
     1256     [ @(proj1 ?? (pi2 ?? (jump_expansion_step program p1)))
    12571257     | @Hnotjmp
    12581258     ]
     
    13021302   (\snd (bvt_lookup ?? (bitvector_of_nat ? n) (jump_expansion_step program policy) 〈0,short_jump〉))) ? (|program|))
    13031303 [ #H elim H; -H #i #Hi @(ex_intro ?? i) @Hi
    1304  | #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) n Hn)
     1304 | #abs @⊥ @(absurd ?? Hp) #n #Hn cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) n Hn)
    13051305   [ #Hj @⊥ @(absurd ?? abs) @(ex_intro ?? n) @conj [ @Hn | @Hj ]
    13061306   | #H @H
     
    13551355  [ #Hp #acc normalize @le_n
    13561356  | #h #t #Hind #Hp #acc
    1357     cases (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1357    cases (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
    13581358    [ whd in match (measure_int ???); whd in match (measure_int ?(jump_expansion_step ??)?);
    13591359      cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉))
     
    14531453     [ @(transitive_le … Hp) //
    14541454     | whd in match (measure_int ???) in Hm; whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
    1455        lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1455       lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
    14561456       [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    14571457       | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
     
    14761476   | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; 
    14771477     whd in match (measure_int ?(jump_expansion_step ??)?) in Hm;
    1478      lapply (proj2 ?? (sig2 ?? (jump_expansion_step program policy)) (|t|) ?)
     1478     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program policy)) (|t|) ?)
    14791479     [ @(lt_to_le_to_lt … (|h::t|)) [ // | @Hp ]
    14801480     | cases (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) policy 〈0,short_jump〉)) in Hm;
     
    15011501 | #h #t #Hind #Hp whd in match (measure_int ???);
    15021502   cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj
    1503    [ >(lookup_opt_lookup_hit … (proj2 ?? (sig2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,short_jump〉)
     1503   [ >(lookup_opt_lookup_hit … (proj2 ?? (pi2 ?? (jump_expansion_start program)) (|t|) ? Hj) 〈0,short_jump〉)
    15041504     [ normalize nodelta @Hind @le_S_to_le ]
    15051505     @Hp
     
    15341534   [ lapply (measure_full program (jump_expansion_internal program (2*|program|)))
    15351535     #Hfull #i #Hi
    1536      lapply (proj2 ?? (sig2 ?? (jump_expansion_step program (jump_expansion_internal program (2*|program|)))) i Hi)
     1536     lapply (proj2 ?? (pi2 ?? (jump_expansion_step program (jump_expansion_internal program (2*|program|)))) i Hi)
    15371537     >(Hfull ? i Hi)
    15381538     [ cases (\snd (bvt_lookup ?? (bitvector_of_nat 16 i) (jump_expansion_step program (jump_expansion_internal program (2*|program|))) 〈0,short_jump〉))
     
    17001700  match sigma_safe p (eject … policy) return λr:option (Word → Word). r ≠ None … → Word → Word with
    17011701   [ None ⇒ λabs. ⊥
    1702    | Some r ⇒ λ_.r] (sig2 … policy).
     1702   | Some r ⇒ λ_.r] (pi2 … policy).
    17031703 cases abs /2/
    17041704qed.
     
    17351735   sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None ….
    17361736 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%);
    1737  generalize in match (sig2 ?? pol); whd in prf:(???%); <prf in pol; #pol
     1737 generalize in match (pi2 ?? pol); whd in prf:(???%); <prf in pol; #pol
    17381738 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0;
    17391739 normalize nodelta >sigma00_append
     
    17741774    | Some res ⇒ res ].
    17751775 [ @⊥ whd in p:(??%??);
    1776    generalize in match (sig2 ?? pol); whd in ⊢ (% → ?);
     1776   generalize in match (pi2 ?? pol); whd in ⊢ (% → ?);
    17771777   whd in ⊢ (?(??%?) → ?); change with (sigma00 ????) in ⊢ (?(??(match % with [_ ⇒ ? | _ ⇒ ?])?) → ?);
    17781778   generalize in match (refl … (sigma00 program pol (\snd program) (Some ? 〈O,〈O,Stub (BitVector 16) 16〉〉)));
     
    18481848   = assembly_1_pseudoinstruction_safe program pol ppc (sigma program pol ppc) lookup_labels lookup_datalabels pi.
    18491849 #program #pol #ppc #lookup_labels #lookup_datalabels #pi #prf1 #prf2 #prf3
    1850  cases (sig2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
     1850 cases (pi2 … (assembly_1_pseudoinstruction' program pol ppc lookup_labels lookup_datalabels pi prf1 prf2 prf3))
    18511851 #H1 #_ @H1
    18521852qed.
     
    19231923  whd in match tech_pc_sigma00 in ⊢ %; normalize nodelta;
    19241924  whd in match sigma00 in ⊢ %; normalize nodelta in ⊢ %;
    1925   generalize in match (sig2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
     1925  generalize in match (pi2 … pol) whd in ⊢ (% → ?) whd in ⊢ (?(??%?) → ?)
    19261926  whd in match sigma0; normalize nodelta;
    19271927  >foldl_step
     
    20042004      let 〈pc, costs〉 ≝ pc_costs in
    20052005        〈labels, costs〉.
    2006  [2: whd generalize in match (sig2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
     2006 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    20072007   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
    20082008   [ <(construct_costs_sigma … costs i1 IHn1) change with (? = ?(\fst construct)) >JMEQ %
     
    20202020          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 assumption ]]]
    20212021 |3: whd % [% [%]] [>sigma_0 % | % | % | #id normalize in ⊢ (% → ?); #abs @⊥ // ]
    2022  | generalize in match (sig2 … result) in ⊢ ?;
     2022 | generalize in match (pi2 … result) in ⊢ ?;
    20232023   normalize nodelta in p ⊢ %; -result; >p in ⊢ (match % with [_ ⇒ ?] → ?);
    20242024   normalize nodelta; >p1 normalize nodelta; >p2; normalize nodelta; * #_; #H @H]
Note: See TracChangeset for help on using the changeset viewer.