File size: 648 Bytes
119e586 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 | (* SKC-LISP-WORLD: Mutation Validation Gate *)
Require Import Coq.Init.Prelude.
Require Import Coq.Arith.Arith.
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Machine.State.
Require Import Mutation.Event.
Require Import World.ObjectKinds.
Require Import Coq.omega.Omega.
Lemma generation_monotonicity : forall e,
mutation_gate_valid e = true ->
generation_before e < generation_after e.
Proof.
intros e Hvalid.
unfold mutation_gate_valid in Hvalid.
simp in Hvalid.
unfold generation_advances in *.
cases (generation_after e > generation_before e); try discriminate.
omega.
Qed.
|