Changeset 1519 for src/ASM/StatusProofs.ma

Timestamp:

Nov 21, 2011, 12:10:57 PM (8 years ago)

Author:

campbell

Message:

More syntax updates.

File:

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

src/ASM/StatusProofs.ma

@@ -41 +41 @@
   set_code_memory T U (set_bit_addressable_sfr ? ps x val) code_mem.
   #T #U #ps #code_mem #x #val
-  whd in ⊢ (??%?)
-  whd in ⊢ (???(???%?))
+  whd in ⊢ (??%?);
+  whd in ⊢ (???(???%?));
   cases (eqb ? 128) [ normalize nodelta cases not_implemented
   | normalize nodelta
@@ -115 +115 @@
   #n #l #T #U #ps #code_mem #val * *;
   #x try (#y #H) try #H whd in H; try cases H
-  whd in ⊢ (??(%)?) whd in ⊢ (???(???(%)?)) try %
+  whd in ⊢ (??(%)?); whd in ⊢ (???(???(%)?)); try %
   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
@@ -137 +137 @@
   #n #l #T #ps #pc #val * *;
   #x try (#y #H) try #H whd in H; try cases H
-  whd in ⊢ (??(%)?) whd in ⊢ (???(??(%)?)) try %
+  whd in ⊢ (??(%)?); whd in ⊢ (???(??(%)?)); try %
   cases (split bool 4 4 ?) #nu' #nl' normalize nodelta
   cases (split bool 1 3 nu') #bit1' #ignore' normalize nodelta
@@ -175 +175 @@
     special_function_registers_8051 T (write_at_stack_pointer T s x)
   = special_function_registers_8051 T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -182 +182 @@
 lemma get_8051_sfr_write_at_stack_pointer:
  ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
- #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl
+ #T #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl
 qed.
 
 lemma code_memory_write_at_stack_pointer:
  ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -229 +229 @@
 lemma external_ram_write_at_stack_pointer:
  ∀T,s,x. external_ram T (write_at_stack_pointer T s x) = external_ram T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -238 +238 @@
     special_function_registers_8052 T (write_at_stack_pointer T s x)
   = special_function_registers_8052 T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -245 +245 @@
 lemma p1_latch_write_at_stack_pointer:
  ∀T,s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -252 +252 @@
 lemma p3_latch_write_at_stack_pointer:
  ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -259 +259 @@
 lemma clock_write_at_stack_pointer:
  ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s.
- #T #s #x whd in ⊢ (??(??%)?)
+ #T #s #x whd in ⊢ (??(??%)?);
  cases (split ????) #nu #nl normalize nodelta;
  cases (get_index_v bool ????) %
@@ -269 +269 @@
 lemma get_8051_sfr_set_8051_sfr:
  ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y.
- #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?)
+ #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);
  whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index
 qed.