Changeset 2210


Ignore:
Timestamp:
Jul 18, 2012, 3:03:59 PM (5 years ago)
Author:
mulligan
Message:

XOR case completely finished.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2209 r2210  
    819819      ]
    820820    |2:
    821       cases daemon (* XXX: todo *)
     821      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
     822      >EQP -P normalize nodelta
     823      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     824      whd in maps_assm:(??%%);
     825      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
     826      [2: normalize nodelta #absurd destruct(absurd) ]
     827      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
     828      [2: normalize nodelta #absurd destruct(absurd) ]
     829      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
     830      whd in ⊢ (??%?);
     831      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
     832      change with (set_arg_8 ????? = ?)
     833      @set_arg_8_status_of_pseudo_status try %
     834      >EQs >EQticks <instr_refl >addr_refl
     835      [1:
     836        @sym_eq @set_clock_status_of_pseudo_status
     837        [1:
     838          @sym_eq @set_program_counter_status_of_pseudo_status %
     839        |2:
     840          @eq_f2 %
     841        ]
     842      |2:
     843        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     844        [1: @(subaddressing_mode_elim … direct) #w % ] %
     845      |3:
     846        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     847        [1:
     848          @(subaddressing_mode_elim … direct) #w %
     849        |4:
     850          @eq_f2
     851          @(pose … (set_clock ????)) #status #status_refl
     852          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
     853          [1:
     854            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
     855            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
     856          |3:
     857            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
     858            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     859          |2:
     860            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
     861            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
     862          |4:
     863            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
     864            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
     865          ]
     866        |*:
     867          %
     868        ]
     869      ]
    822870    ]
    823871  |4,5,6,7,8,9: (* INC and DEC *)
Note: See TracChangeset for help on using the changeset viewer.