Commit 93b40629 authored by Björn Brandenburg's avatar Björn Brandenburg

add trivial replace_at definition rewriting lemma

parent 87f6ec3c
...@@ -25,8 +25,16 @@ Section ReplaceAtFacts. ...@@ -25,8 +25,16 @@ Section ReplaceAtFacts.
t'. *) t'. *)
Let sched' := replace_at sched t' nstate. Let sched' := replace_at sched t' nstate.
(** We begin with the trivial observation that the schedule doesn't change at (** We begin with the trivial observation that [replace_at sched t' nstate]
other times. *) indeed returns [nstate] at time [t']. *)
Lemma replace_at_def:
sched' t' = nstate.
Proof.
rewrite /sched' /replace_at.
now apply ifT.
Qed.
(** Equally trivially, the schedule doesn't change at other times. *)
Lemma rest_of_schedule_invariant: Lemma rest_of_schedule_invariant:
forall t, t <> t' -> sched' t = sched t. forall t, t <> t' -> sched' t = sched t.
Proof. Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment