Ignore:
Timestamp:
Jul 10, 2012, 2:39:38 PM (8 years ago)
Author:
mulligan
Message:

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofsSplit.ma

    r2170 r2172  
    113113  ∀b: Bit.
    114114    program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s.
    115   #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta
     115  #M #cm #s whd in match set_arg_1; cases daemon (* whd in match set_arg_1'; normalize nodelta
    116116  #addr #b
    117117  @(subaddressing_mode_elim … addr)
     
    127127  |2:
    128128    cases (vsplit ????) //
    129   ]
     129  ] *)
    130130qed.
    131131
     
    551551  #M #cm #ps #addr1 #result
    552552  @(subaddressing_mode_elim … addr1) try #w try %
    553   whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
     553  whd in ⊢ (??(???%)?); cases daemon (*whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)
    554554  [1:
    555555    cases (vsplit bool ???) #nu #nl normalize nodelta
     
    561561    cases (vsplit bool ???) #ignore #three_bits normalize nodelta
    562562    cases (get_index_v bool ????) normalize nodelta %
    563   ]
     563  ] *)
    564564qed.
    565565
     
    612612  |2:
    613613    #addressing_mode_ok_refl whd in ⊢ (??%?);
    614     @pair_elim #nu #nl #nu_nl_refl normalize nodelta
     614    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
    615615    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
    616616    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
     
    737737      ]
    738738    ]
    739   ]
     739  ] *)
    740740qed.
    741741
Note: See TracChangeset for help on using the changeset viewer.