Changeset 2172 for src/ASM/StatusProofs.ma

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:

• src/ASM/StatusProofs.ma (modified) (5 diffs)

src/ASM/StatusProofs.ma

@@ -200 +200 @@
   #x try (#y #H) try #H whd in H; try cases H try %
   whd in match set_arg_8; normalize nodelta
-  whd in match set_arg_8'; normalize nodelta
-  cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta
-  cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta
-  cases (get_index_v bool 4 nu' 0 ?) normalize nodelta
-  try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*)
+  cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta
+  cases (head' bool ??) normalize nodelta
+  try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *)
 qed.
   
@@ -349 +347 @@
   #m #cm #s #addr #byte
   whd in match set_arg_8; normalize nodelta
+  cases daemon (*
   whd in match set_arg_8'; normalize nodelta
   cases addr #subaddressing_modein_proof
@@ -357 +356 @@
   cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta
   cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta
-  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try %
+  cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *)
 qed.
 
@@ -366 +365 @@
   #m #cm #s #addr #v
   whd in match set_arg_1; normalize nodelta
+  cases daemon (*
   whd in match set_arg_1'; normalize nodelta
   cases addr #subaddressing_modein_proof
@@ -376 +376 @@
   cases (get_index_v bool 4 nu ??) normalize nodelta
   (* XXX: try /demod/ try % *)
-  cases daemon
+  cases daemon *)
 qed.