Ignore:
Timestamp:
Jun 9, 2011, 10:38:21 AM (9 years ago)
Author:
sacerdot
Message:

Type of set_code_memory generalized.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r909 r911  
    15231523qed.
    15241524*)
     1525
     1526axiom execute_1_pseudo_instruction_preserves_code_memory:
     1527 ∀ticks_of,ps.
     1528  code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.
     1529
    15251530(*
    15261531lemma execute_code_memory_unchanged:
     
    15761581  match status_of_pseudo_status ps' with [ None ⇒ True | Some s'' ⇒
    15771582  let s' ≝ execute_1 s in
    1578    s = s'']].
     1583   s' = s'']].
    15791584 #ticks_of #ps
    1580  whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     1585 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.%])
     1586 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]])
     1587 >execute_1_pseudo_instruction_preserves_code_memory
    15811588 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
     1589 change with (? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) = ?)
    15821590 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
    15831591 generalize in match (sig2 … (execute_1_pseudo_instruction' ticks_of ps))
Note: See TracChangeset for help on using the changeset viewer.