Changeset 2272 for src/ASM/StatusProofs.ma
 Timestamp:
 Jul 27, 2012, 5:53:25 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/StatusProofs.ma
r2172 r2272 27 27 #m #s #v 28 28 whd in match write_at_stack_pointer; normalize nodelta 29 cases(vsplit … 4 4 ?) #nu #nlnormalize nodelta30 cases (get_index_v … 4 nu 0 ?)//29 cases(vsplit … 1 7 ?) #bit_one #seven_bits normalize nodelta 30 cases (head' bool ??) normalize nodelta // 31 31 qed. 32 32 … … 236 236 = special_function_registers_8051 T cm s. 237 237 #T #cm #s #x whd in ⊢ (??(???%)?); 238 cases (vsplit ????) # nu #nl normalize nodelta;239 cases (get_index_v bool ????)%238 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 239 cases (head' bool ??) normalize nodelta % 240 240 qed. 241 241 … … 297 297 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s. 298 298 #T #cm #s #x whd in ⊢ (??(???%)?); 299 cases (vsplit ????) # nu #nl normalize nodelta;300 cases ( get_index_v bool ????) %299 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 300 cases (head' bool ??) % 301 301 qed. 302 302 … … 306 306 = special_function_registers_8052 T cm s. 307 307 #T #cm #s #x whd in ⊢ (??(???%)?); 308 cases (vsplit ????) # nu #nl normalize nodelta;309 cases ( get_index_v bool ????) %308 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 309 cases (head' bool ??) % 310 310 qed. 311 311 … … 313 313 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s. 314 314 #T #cm #s #x whd in ⊢ (??(???%)?); 315 cases (vsplit ????) # nu #nl normalize nodelta;316 cases ( get_index_v bool ????) %315 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 316 cases (head' bool ??) % 317 317 qed. 318 318 … … 320 320 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s. 321 321 #T #cm #s #x whd in ⊢ (??(???%)?); 322 cases (vsplit ????) # nu #nl normalize nodelta;323 cases ( get_index_v bool ????) %322 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 323 cases (head' bool ??) % 324 324 qed. 325 325 … … 412 412 #m #cm #s #v 413 413 whd in match write_at_stack_pointer; normalize nodelta 414 cases (vsplit bool 4 4 ?) #nu #nlnormalize nodelta415 cases (get_index_v bool 4 nu ??) normalize nodelta /demod/%414 cases (vsplit ????) #bit_one #seven_bits normalize nodelta 415 cases (head' bool ??) % 416 416 qed. 417 417
Note: See TracChangeset
for help on using the changeset viewer.