Changeset 2301


Ignore:
Timestamp:
Aug 22, 2012, 5:30:56 PM (7 years ago)
Author:
mulligan
Message:

Trying to get the big proof working again

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2285 r2301  
    591591      @set_arg_8_status_of_pseudo_status try %
    592592      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)]
    593   |(*3: (* SUBB *)
     593  |3: (* SUBB *)
    594594    (* XXX: work on the right hand side *)
    595595    (* XXX: switch to the left hand side *)
     
    597597    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    598598    whd in maps_assm:(??%%);
    599     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     599    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    600600    [2,4: normalize nodelta #absurd destruct(absurd) ]
    601     inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     601    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    602602    [2,4: normalize nodelta #absurd destruct(absurd) ]
    603603    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    611611      [1:
    612612        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
    613         @(get_arg_8_status_of_pseudo_status cm status … M')
    614         [1:
    615           >status_refl @sym_eq @set_clock_status_of_pseudo_status %
     613        @(get_arg_8_status_of_pseudo_status cm status … 〈low, high, accA〉)
     614        [1:
     615          >status_refl @set_clock_status_of_pseudo_status %
    616616        |2:
    617617          >status_refl
     
    625625      |2:
    626626        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
    627         @(get_arg_8_status_of_pseudo_status cm status … M')
    628         [1:
    629           >status_refl @sym_eq @set_clock_status_of_pseudo_status %
     627        @(get_arg_8_status_of_pseudo_status cm status … 〈low, high, accA〉)
     628        [1:
     629          >status_refl @set_clock_status_of_pseudo_status %
    630630        |2:
    631631          >status_refl
     
    638638        ]
    639639      |3:
    640         @(get_cy_flag_status_of_pseudo_status … M')
    641         @sym_eq @set_clock_status_of_pseudo_status
    642         [1:
    643           @sym_eq @set_program_counter_status_of_pseudo_status %
     640        @(get_cy_flag_status_of_pseudo_status … 〈low, high, accA〉)
     641        @set_clock_status_of_pseudo_status
     642        [1:
     643          @set_program_counter_status_of_pseudo_status %
    644644        |2:
    645645          %
     
    653653      |2:
    654654        @set_flags_status_of_pseudo_status try %
    655         @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
    656         [1:
    657           @sym_eq @set_clock_status_of_pseudo_status %
     655        @(set_arg_8_status_of_pseudo_status … (refl …))
     656        [1:
     657          @set_clock_status_of_pseudo_status %
    658658        |2:
    659659          @I
     
    672672      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    673673      whd in maps_assm:(??%%);
    674       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     674      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    675675      [2: normalize nodelta #absurd destruct(absurd) ]
    676676      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    677677      whd in ⊢ (??%?);
    678678      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    679       whd in ⊢ (??%?);
    680       inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
    681       @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
    682       [1:
    683         @eq_f2 try %
    684         @(pose … (set_clock ????)) #status #status_refl
    685         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
    686         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
    687       |2:
    688         @set_arg_8_status_of_pseudo_status try %
    689         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
    690       ]
     679      change with (set_arg_8 ??? ACC_A ? = ?)
     680      [2: @I ]
     681      @set_arg_8_status_of_pseudo_status try %
     682      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
     683      @eq_f2 try % @sym_eq
     684      @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
     685      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
    691686    |2:
    692687      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    693688      whd in maps_assm:(??%%);
    694       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     689      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    695690      [2: normalize nodelta #absurd destruct(absurd) ]
    696691      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    697692      whd in ⊢ (??%?);
    698693      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    699       whd in ⊢ (??%?);
    700       @let_pair_in_status_of_pseudo_status
    701       [1:
    702         @eq_f2 try %
    703         @(pose … (set_clock ????)) #status #status_refl
    704         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
    705         >EQs >EQticks
    706         [1:
    707           @sym_eq @set_clock_status_of_pseudo_status %
    708         |2:
    709           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
    710         |3:
    711           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) %
    712         ]
    713       |2:
    714         #carry #result
    715         @sym_eq @set_arg_8_status_of_pseudo_status try %
    716         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
    717       ]
     694      change with (set_arg_8 ??? (REGISTER w) ? = ?)
     695      [2: @I ]
     696      @set_arg_8_status_of_pseudo_status try %
     697      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1)
     698      [1: /2 by refl, eq_false_to_notb/ ] try %
     699      @eq_f2 try % @sym_eq
     700      @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
     701      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
    718702    |3:
    719703      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    720704      whd in maps_assm:(??%%);
    721       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     705      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    722706      [2: normalize nodelta #absurd destruct(absurd) ]
    723707      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    724708      whd in ⊢ (??%?);
    725709      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    726       whd in ⊢ (??%?);
    727       @let_pair_in_status_of_pseudo_status
    728       [1:
    729         @eq_f2 try %
    730         @(pose … (set_clock ????)) #status #status_refl
    731         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
    732         >EQs >EQticks
    733         [1:
    734           @sym_eq @set_clock_status_of_pseudo_status %
    735         |2:
    736           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
    737         |3:
    738           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) %
    739         ]
    740       |2:
    741         #carry #result
    742         @sym_eq @set_arg_8_status_of_pseudo_status try %
    743         @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %   
    744       ]
     710      change with (set_arg_8 ??? (DIRECT w) ? = ?)
     711      [2: /2 by refl, eq_false_to_notb/ ]
     712      @set_arg_8_status_of_pseudo_status try %
     713      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1)
     714      [1,2,3: % ]
     715      @eq_f2 try % @sym_eq
     716      @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
     717      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
    745718    |4:
    746719      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    747720      whd in maps_assm:(??%%);
    748       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     721      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    749722      [2: normalize nodelta #absurd destruct(absurd) ]
    750723      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    751724      whd in ⊢ (??%?);
    752725      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    753       whd in ⊢ (??%?);
    754       @let_pair_in_status_of_pseudo_status
    755       [1:
    756         @eq_f2 try %
    757         @(pose … (set_clock ????)) #status #status_refl
    758         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
    759         >EQs >EQticks
    760         [1:
    761           @sym_eq @set_clock_status_of_pseudo_status %
     726      change with (set_arg_8 ??? (INDIRECT w) ? = ?)
     727      [2: /2 by refl, eq_false_to_notb/ ]
     728      @set_arg_8_status_of_pseudo_status try %
     729      [1:
     730        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
     731      |2:
     732        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) try %
     733        @eq_f2 try % @sym_eq
     734        @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
     735        [1:
     736          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
    762737        |2:
    763738          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
    764         |3:
    765           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
    766         ]
    767       |2:
    768         #carry #result
    769         @sym_eq @set_arg_8_status_of_pseudo_status try %
    770         [1:
    771           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
    772         |2:
    773           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %   
    774739        ]
    775740      ]
     
    783748      [1:
    784749        @eq_f2 try %
    785         @(pose … (set_clock ????)) #status #status_refl
    786         @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
     750        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     751        @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl
    787752        >EQs >EQticks %
    788753      |2:
    789         #carry #bl
    790         @sym_eq @let_pair_in_status_of_pseudo_status
     754        #carry #bl @let_pair_in_status_of_pseudo_status
    791755        [1:
    792756          @eq_f3 try %
    793           @(pose … (set_clock ????)) #status #status_refl
    794           @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
     757          @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     758          @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl
    795759          >EQs >EQticks %
    796760        |2:
    797           #carry' #bu
    798           @sym_eq @set_8051_sfr_status_of_pseudo_status %
     761          #carry' #bu @set_8051_sfr_status_of_pseudo_status %
    799762        ]
    800763      ]
     
    806769      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    807770      whd in maps_assm:(??%%);
    808       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     771      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    809772      [2: normalize nodelta #absurd destruct(absurd) ]
    810773      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    815778      [1:
    816779        @eq_f3 try %
    817         @(pose … (set_clock ????)) #status #status_refl
    818         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     780        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     781        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
    819782        >EQs >EQticks try %
    820783        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
    821784      |2:
    822785        #result #flags
    823         @sym_eq @set_arg_8_status_of_pseudo_status try %
     786        @set_arg_8_status_of_pseudo_status try %
    824787        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
    825788      ]
     
    827790      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    828791      whd in maps_assm:(??%%);
    829       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     792      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    830793      [2: normalize nodelta #absurd destruct(absurd) ]
    831794      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    836799      [1:
    837800        @eq_f3 try %
    838         @(pose … (set_clock ????)) #status #status_refl
    839         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     801        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     802        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
    840803        >EQs >EQticks try %
    841804        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
    842805      |2:
    843806        #result #flags
    844         @sym_eq @set_arg_8_status_of_pseudo_status try %
     807        @set_arg_8_status_of_pseudo_status try %
    845808        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
    846809      ]
     
    848811      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    849812      whd in maps_assm:(??%%);
    850       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     813      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    851814      [2: normalize nodelta #absurd destruct(absurd) ]
    852815      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    857820      [1:
    858821        @eq_f3 try %
    859         @(pose … (set_clock ????)) #status #status_refl
    860         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     822        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     823        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
    861824        >EQs >EQticks try %
    862825        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
    863826      |2:
    864827        #result #flags
    865         @sym_eq @set_arg_8_status_of_pseudo_status try %
     828        @set_arg_8_status_of_pseudo_status try %
    866829        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
    867830      ]
     
    869832      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    870833      whd in maps_assm:(??%%);
    871       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     834      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    872835      [2: normalize nodelta #absurd destruct(absurd) ]
    873836      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    878841      [1:
    879842        @eq_f3 try %
    880         @(pose … (set_clock ????)) #status #status_refl
    881         @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
     843        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
     844        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
    882845        >EQs >EQticks try %
    883846        [1:
     
    888851      |2:
    889852        #result #flags
    890         @sym_eq @set_arg_8_status_of_pseudo_status try %
     853        @set_arg_8_status_of_pseudo_status try %
    891854        [1:
    892855          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
     
    902865    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    903866    whd in maps_assm:(??%%);
    904     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     867    inversion (assert_data ?????) in maps_assm;
     868    @(subaddressing_mode_elim … addr1) #addressing_mode_ok_assm_1
    905869    [2: normalize nodelta #absurd destruct(absurd) ]
    906     inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     870    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    907871    [2: normalize nodelta #absurd destruct(absurd) ]
    908872    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    915879      [1:
    916880        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    917         whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
    918         %
     881        whd in ⊢ (??%?);
     882        whd in addressing_mode_ok_assm_1:(??%?); cases accA in addressing_mode_ok_assm_1;
     883        normalize nodelta [2: * #upper_lower #address #absurd destruct(absurd) ] #_ %
    919884      |2:
    920885        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
    921886      ]
    922887    ]
    923     @sym_eq @set_8051_sfr_status_of_pseudo_status
     888    @set_8051_sfr_status_of_pseudo_status
    924889    [2:
    925       >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
     890      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … ACC_A … addressing_mode_ok_assm_1)
     891      [2: /2 by refl, eq_false_to_notb/ ]
    926892      @eq_f @eq_f2 try % @eq_f2 @eq_f
    927893      @sym_eq
    928894      [1:
    929895        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    930         whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    931       |2:
    932         @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
    933       ]
    934     ]
    935     @sym_eq @set_clock_status_of_pseudo_status
     896        whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     897        cases accA in addressing_mode_ok_assm_1;
     898        normalize nodelta [2: * #upper_lower #address #absurd destruct(absurd) ] #_ %
     899      |2:
     900        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
     901      ]
     902    ]
     903    @set_clock_status_of_pseudo_status
    936904    [2:
    937905      @eq_f %
    938906    ]
    939     @sym_eq @set_program_counter_status_of_pseudo_status %
     907    @set_program_counter_status_of_pseudo_status %
    940908  |7,8: (* DIV *)
    941909    (* XXX: work on the right hand side *)
     
    944912    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    945913    whd in maps_assm:(??%%);
    946     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     914    inversion (assert_data ?????) in maps_assm;
     915    @(subaddressing_mode_elim … addr1) #addressing_mode_ok_assm_1
    947916    [2,4: normalize nodelta #absurd destruct(absurd) ]
    948     inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     917    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    949918    [2,4: normalize nodelta #absurd destruct(absurd) ]
    950919    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    952921    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    953922    whd in ⊢ (??%?); normalize nodelta
    954     @(match_nat_status_of_pseudo_status M' cm sigma policy)
     923    @(match_nat_status_of_pseudo_status 〈low, high, accA〉 cm sigma policy)
    955924    [1,4:
    956925      @eq_f
    957926      @sym_eq @(pose … (set_clock ????)) #status #status_refl
    958       @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
     927      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl try %
    959928    |2,5:
    960929      @sym_eq @set_flags_status_of_pseudo_status %
    961930    |3,6:
    962931      #n @sym_eq @set_flags_status_of_pseudo_status try %
    963       @sym_eq @set_8051_sfr_status_of_pseudo_status
     932      @set_8051_sfr_status_of_pseudo_status
    964933      [1,3:
    965         @sym_eq @set_8051_sfr_status_of_pseudo_status try %
    966         whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
    967         @eq_f @eq_f2 try % @eq_f
    968         @(pose … (set_clock ????)) #status #status_refl
    969         @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
    970         whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     934        @set_8051_sfr_status_of_pseudo_status try %
     935        whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     936        cases accA in addressing_mode_ok_assm_1; normalize nodelta
     937        [2,4: #address_entry #absurd destruct(absurd) ] #_
     938        @eq_f @eq_f2 %
    971939      |2,4:
    972940        whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f
    973941        @(pose … (set_clock ????)) #status #status_refl
    974         @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
    975         whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     942        @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl try %
     943        whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     944        cases accA in addressing_mode_ok_assm_1; normalize nodelta
     945        [2,4: #address_entry #absurd destruct(absurd) ] #_ %
    976946      ]
    977947    ]
     
    982952    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    983953    whd in maps_assm:(??%%);
    984     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     954    inversion (assert_data ?????) in maps_assm;
     955    @(subaddressing_mode_elim … addr) #addressing_mode_ok_assm_1
    985956    [2: normalize nodelta #absurd destruct(absurd) ]
    986957    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    992963      @eq_f normalize nodelta >EQs >EQticks <instr_refl
    993964      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    994       whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     965      whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     966      cases accA in addressing_mode_ok_assm_1; normalize nodelta
     967      [2: #address_entry #absurd destruct(absurd) ] #_ %
    995968    |2:
    996969      @(pair_replace ?????????? p)
     
    1005978          |2:
    1006979            change with (get_ac_flag ??? = get_ac_flag ???)
    1007             @(get_ac_flag_status_of_pseudo_status M')
    1008             @sym_eq @set_clock_status_of_pseudo_status
     980            @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉)
     981            @set_clock_status_of_pseudo_status
    1009982            >EQs >EQticks <instr_refl %
    1010983          ]
     
    1014987          [1:
    1015988            @eq_f3 try % normalize nodelta
    1016             @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
    1017             whd in ⊢ (??%?);
    1018             >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     989            @(get_8051_sfr_status_of_pseudo_status 〈low, high, accA〉 … policy … (refl …))
     990            whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     991            cases accA in addressing_mode_ok_assm_1; normalize nodelta
     992            [2: #address_entry #absurd destruct(absurd) ] #_
     993            >EQs >EQticks <instr_refl %
    1019994          |2:
    1020995            @(pair_replace ?????????? p2) try %
     
    1023998            @(if_then_else_replace ???????? p4) try % normalize nodelta
    1024999            @(if_then_else_replace ???????? p4) try % normalize nodelta
    1025             @(pair_replace ?????????? p5) try %
    1026             @(pair_replace ?????????? p5) try %
    10271000            @set_flags_status_of_pseudo_status try %
    10281001            [1:
    1029               @eq_f @(get_ac_flag_status_of_pseudo_status M')
    1030               @sym_eq @set_8051_sfr_status_of_pseudo_status
     1002              @eq_f @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉)
     1003              @set_8051_sfr_status_of_pseudo_status
    10311004              [1:
    1032                 @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
     1005                @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
    10331006              |2:
    1034                 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1007                whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     1008                cases accA in addressing_mode_ok_assm_1; normalize nodelta
     1009                [2: #address_entry #absurd destruct(absurd) ] #_ %
    10351010              ]
    10361011            |2:
    1037               @(get_ov_flag_status_of_pseudo_status M')
    1038               @sym_eq @set_8051_sfr_status_of_pseudo_status
     1012              @(get_ov_flag_status_of_pseudo_status 〈low, high, accA〉)
     1013              @set_8051_sfr_status_of_pseudo_status
    10391014              [1:
    1040                 @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
     1015                @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
    10411016              |2:
    1042                 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1017                whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     1018                cases accA in addressing_mode_ok_assm_1; normalize nodelta
     1019                [2: #address_entry #absurd destruct(absurd) ] #_ %
    10431020              ]
    10441021            |3:
    1045               @sym_eq @set_8051_sfr_status_of_pseudo_status
     1022              @set_8051_sfr_status_of_pseudo_status
    10461023              [1:
    1047                 @sym_eq @set_clock_status_of_pseudo_status
     1024                @set_clock_status_of_pseudo_status
    10481025                [1:
    1049                   >EQs
    1050                   @sym_eq @set_program_counter_status_of_pseudo_status %
     1026                  >EQs @set_program_counter_status_of_pseudo_status %
    10511027                |2:
    10521028                  >EQs >EQticks <instr_refl %
    10531029                ]
    10541030              |2:
    1055                 whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1031                whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     1032                cases accA in addressing_mode_ok_assm_1; normalize nodelta
     1033                [2: #address_entry #absurd destruct(absurd) ] #_ %
    10561034              ]
    10571035            ]
     
    10661044    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    10671045    whd in maps_assm:(??%%);
    1068     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1046    inversion (assert_data ?????) in maps_assm;
     1047    @(subaddressing_mode_elim … addr) #addressing_mode_ok_assm_1
    10691048    [2: normalize nodelta #absurd destruct(absurd) ]
    10701049    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    10761055      @eq_f normalize nodelta >EQs >EQticks <instr_refl
    10771056      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    1078       whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1057      whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     1058      cases accA in addressing_mode_ok_assm_1; normalize nodelta
     1059      [2: #address_entry #absurd destruct(absurd) ] #_ %
    10791060    |2:
    10801061      @(pair_replace ?????????? p)
     
    10891070          |2:
    10901071            change with (get_ac_flag ??? = get_ac_flag ???)
    1091             @(get_ac_flag_status_of_pseudo_status M')
    1092             @sym_eq @set_clock_status_of_pseudo_status
     1072            @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉)
     1073            @set_clock_status_of_pseudo_status
    10931074            >EQs >EQticks <instr_refl %
    10941075          ]
     
    10981079          [1:
    10991080            @eq_f3 try % normalize nodelta
    1100             @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
    1101             whd in ⊢ (??%?);
    1102             >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1081            @(get_8051_sfr_status_of_pseudo_status 〈low, high, accA〉 … policy … (refl …))
     1082            whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     1083            cases accA in addressing_mode_ok_assm_1; normalize nodelta
     1084            [2: #address_entry #absurd destruct(absurd) ] #_ >EQs >EQticks <instr_refl %
    11031085          |2:
    11041086            @(pair_replace ?????????? p2) try %
     
    11091091            @set_clock_status_of_pseudo_status
    11101092            [1:
    1111               >EQs
    1112               @sym_eq @set_program_counter_status_of_pseudo_status %
     1093              >EQs @set_program_counter_status_of_pseudo_status %
    11131094            |2:
    11141095              >EQs >EQticks <instr_refl %
     
    11241105    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    11251106    whd in maps_assm:(??%%);
    1126     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1107    inversion (assert_data ?????) in maps_assm;
     1108    @(subaddressing_mode_elim … addr) #addressing_mode_ok_assm_1
    11271109    [2: normalize nodelta #absurd destruct(absurd) ]
    11281110    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    11341116      @eq_f normalize nodelta >EQs >EQticks <instr_refl
    11351117      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
    1136       whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
     1118      whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
     1119      cases accA in addressing_mode_ok_assm_1; normalize nodelta
     1120      [2: #address_entry #absurd destruct(absurd) ] #_ %
    11371121    |2:
    11381122      @(pair_replace ?????????? p)
     
    11471131          |2:
    11481132            change with (get_ac_flag ??? = get_ac_flag ???)
    1149             @(get_ac_flag_status_of_pseudo_status M')
    1150             @sym_eq @set_clock_status_of_pseudo_status
     1133            @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉)
     1134            @set_clock_status_of_pseudo_status
    11511135            >EQs >EQticks <instr_refl %
    11521136          ]
     
    11551139          @set_clock_status_of_pseudo_status
    11561140          [1:
    1157             >EQs
    1158             @sym_eq @set_program_counter_status_of_pseudo_status %
     1141            >EQs @set_program_counter_status_of_pseudo_status %
    11591142          |2:
    11601143            >EQs >EQticks <instr_refl %
     
    15801563    @pair_elim #sj_possible #disp #sj_possible_disp_refl
    15811564    inversion sj_possible #sj_possible_refl normalize nodelta
     1565    @(subaddressing_mode_elim … addr1) #w
    15821566    [1:
    15831567      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     
    15901574      >EQs >EQticks <instr_refl normalize nodelta
    15911575      [1:
    1592         @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉) try %
    1593         @(subaddressing_mode_elim … addr1) #w whd
     1576        @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉) try % whd
     1577        @vsplit_elim #bit_1 #seven_bits #bit_1_seven_bits_refl normalize nodelta
     1578        inversion (head' bool ??) #head_refl' normalize nodelta
     1579        @vsplit_elim #four_bits #three_bits #four_bits_three_bits_refl normalize nodelta
     1580        whd in ⊢ (??%%); cases (sfr_of_Byte ?) normalize nodelta
    15941581      |2:
    15951582        @set_program_counter_status_of_pseudo_status
     
    16371624      @(if_then_else_replace ???????? p) normalize nodelta
    16381625      [1:
     1626        @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉 … (BIT_ADDR w))
     1627     
    16391628        @eq_f >EQs
    16401629        whd in match get_cy_flag; normalize nodelta
     
    16751664      ]
    16761665    ]
    1677   |16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
     1666  |*)16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
    16781667    cases daemon
    16791668  |(*29,30: (* ANL and ORL *)
     
    16861675        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    16871676        whd in maps_assm:(??%%);
    1688         inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1677        inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    16891678        [2,4: normalize nodelta #absurd destruct(absurd) ]
    1690         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1679        inversion (assert_data ?????) #addressing_mode_ok_assm_2
    16911680        [2,4: normalize nodelta #absurd destruct(absurd) ]
    16921681        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    17361725        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    17371726        whd in maps_assm:(??%%);
    1738         inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1727        inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    17391728        [2,4: normalize nodelta #absurd destruct(absurd) ]
    1740         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1729        inversion (assert_data ?????) #addressing_mode_ok_assm_2
    17411730        [2,4: normalize nodelta #absurd destruct(absurd) ]
    17421731        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    17871776      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    17881777      whd in maps_assm:(??%%);
    1789       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1778      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    17901779      [2,4: normalize nodelta #absurd destruct(absurd) ]
    1791       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1780      inversion (assert_data ?????) #addressing_mode_ok_assm_2
    17921781      [2,4: normalize nodelta #absurd destruct(absurd) ]
    17931782      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    18061795      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    18071796      whd in maps_assm:(??%%);
    1808       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1797      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    18091798      [2: normalize nodelta #absurd destruct(absurd) ]
    1810       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1799      inversion (assert_data ?????) #addressing_mode_ok_assm_2
    18111800      [2: normalize nodelta #absurd destruct(absurd) ]
    18121801      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    18551844      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    18561845      whd in maps_assm:(??%%);
    1857       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1846      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    18581847      [2: normalize nodelta #absurd destruct(absurd) ]
    1859       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     1848      inversion (assert_data ?????) #addressing_mode_ok_assm_2
    18601849      [2: normalize nodelta #absurd destruct(absurd) ]
    18611850      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    19071896    whd in maps_assm:(??%%);
    19081897    [1,2:
    1909       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1898      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    19101899      [2,4: normalize nodelta #absurd destruct(absurd) ]
    19111900      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    19411930    whd in maps_assm:(??%%);
    19421931    [1,2:
    1943       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     1932      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    19441933      [2,4: normalize nodelta #absurd destruct(absurd) ]
    19451934      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    19891978    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    19901979    whd in maps_assm:(??%%);
    1991     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
     1980    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm
    19921981    [2,4: normalize nodelta #absurd destruct(absurd) ]
    19931982    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    20122001    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    20132002    whd in maps_assm:(??%%);
    2014     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
     2003    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm
    20152004    [2,4: normalize nodelta #absurd destruct(absurd) ]
    20162005    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    20382027    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    20392028    whd in maps_assm:(??%%);
    2040     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2029    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    20412030    [2: normalize nodelta #absurd destruct(absurd) ]
    20422031    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    20932082              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    20942083              whd in maps_assm:(??%%);
    2095               inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2084              inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    20962085              [2: normalize nodelta #absurd destruct(absurd) ]
    2097               inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2086              inversion (assert_data ?????) #addressing_mode_ok_assm_2
    20982087              [2: normalize nodelta #absurd destruct(absurd) ]
    20992088              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    21322121              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    21332122              whd in maps_assm:(??%%);
    2134               inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2123              inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    21352124              [2: normalize nodelta #absurd destruct(absurd) ]
    2136               inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2125              inversion (assert_data ?????) #addressing_mode_ok_assm_2
    21372126              [2: normalize nodelta #absurd destruct(absurd) ]
    21382127              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    21712160            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    21722161            whd in maps_assm:(??%%);
    2173             inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2162            inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    21742163            [2: normalize nodelta #absurd destruct(absurd) ]
    2175             inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2164            inversion (assert_data ?????) #addressing_mode_ok_assm_2
    21762165            [2: normalize nodelta #absurd destruct(absurd) ]
    21772166            normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    22102199          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    22112200          whd in maps_assm:(??%%);
    2212           inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2201          inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    22132202          [2: normalize nodelta #absurd destruct(absurd) ]
    2214           inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2203          inversion (assert_data ?????) #addressing_mode_ok_assm_2
    22152204          [2: normalize nodelta #absurd destruct(absurd) ]
    22162205          normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    22272216        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    22282217        whd in maps_assm:(??%%);
    2229         inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2218        inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    22302219        [2: normalize nodelta #absurd destruct(absurd) ]
    2231         inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2220        inversion (assert_data ?????) #addressing_mode_ok_assm_2
    22322221        [2: normalize nodelta #absurd destruct(absurd) ]
    22332222        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    22502239      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    22512240      whd in maps_assm:(??%%);
    2252       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2241      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    22532242      [2: normalize nodelta #absurd destruct(absurd) ]
    2254       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2243      inversion (assert_data ?????) #addressing_mode_ok_assm_2
    22552244      [2: normalize nodelta #absurd destruct(absurd) ]
    22562245      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    22862275      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    22872276      whd in maps_assm:(??%%);
    2288       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2277      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    22892278      [2: normalize nodelta #absurd destruct(absurd) ]
    2290       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2279      inversion (assert_data ?????) #addressing_mode_ok_assm_2
    22912280      [2: normalize nodelta #absurd destruct(absurd) ]
    22922281      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    23192308      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    23202309      whd in maps_assm:(??%%);
    2321       inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2310      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    23222311      [2: normalize nodelta #absurd destruct(absurd) ]
    2323       inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2312      inversion (assert_data ?????) #addressing_mode_ok_assm_2
    23242313      [2: normalize nodelta #absurd destruct(absurd) ]
    23252314      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    23562345    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    23572346    whd in maps_assm:(??%%);
    2358     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2347    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    23592348    [2: normalize nodelta #absurd destruct(absurd) ]
    23602349    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    24362425    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    24372426    whd in maps_assm:(??%%);
    2438     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2427    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    24392428    [2: normalize nodelta #absurd destruct(absurd) ]
    2440     inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2429    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    24412430    [2: normalize nodelta #absurd destruct(absurd) ]
    24422431    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     
    24872476    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    24882477    whd in maps_assm:(??%%);
    2489     inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     2478    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    24902479    [2: normalize nodelta #absurd destruct(absurd) ]
    2491     inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     2480    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    24922481    [2: normalize nodelta #absurd destruct(absurd) ]
    24932482    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
Note: See TracChangeset for help on using the changeset viewer.