Do not create a DELETE as the first operation on the doc

DaveCTurner · DaveCTurner · commit 019272cc6d23 · 2018-03-23T13:50:55.000Z
diff --git a/ReplicaEngine/tla/ReplicaEngine.tla b/ReplicaEngine/tla/ReplicaEngine.tla
@@ -39,7 +39,7 @@ Request(request_count)
           }
     (* DELETE *)
     \cup  { [type |-> DELETE, seqno |-> seqno]
-          : seqno \in 1..request_count
+          : seqno \in 2..request_count
           }
 
 (* The set of sets of requests, which have distinct seqnos *)

Original file line number	Diff line number	Diff line change
`@@ -39,7 +39,7 @@ Request(request_count)`
`39`	`39`	`}`
`40`	`40`	`(* DELETE *)`
`41`	`41`	`\cup { [type \|-> DELETE, seqno \|-> seqno]`
`42`		`- : seqno \in 1..request_count`
	`42`	`+ : seqno \in 2..request_count`
`43`	`43`	`}`
`44`	`44`
`45`	`45`	`(* The set of sets of requests, which have distinct seqnos *)`