| (* SKC-LISP-WORLD: Mutation Journal — Append-only Log Semantics *) | |
| Require Import Coq.Init.Prelude. | |
| Require Import Coq.Arith.Arith. | |
| Require Import Coq.Lists.List. | |
| Require Import Coq.Strings.String. | |
| Require Import Mutation.Event. | |
| Require Import World.ObjectKinds. | |
| Require Import Coq.omega.Omega. | |
| Lemma journal_completeness : forall j w w', | |
| generation w' > generation w -> | |
| exists e, In e j /\ mutation_gate_passed e. | |
| Proof. | |
| intros j w w' Hgen. | |
| exists (Build_mutation_event 0 (generation w) (generation w') 0 0 OpAllocateObject "" "" false None 0). | |
| split. | |
| - simp. | |
| - unfold mutation_gate_passed. | |
| simp. | |
| omega. | |
| Qed. | |