From 31fbbc4d951b23f9e6b4f2a6772e9a3531081e77 Mon Sep 17 00:00:00 2001
From: hellerve <veit@veitheller.de>
Date: Mon, 14 Jan 2019 16:17:07 +0100
Subject: [PATCH] remove: add simple remove model

---
 Remove.tla | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 Remove.tla

diff --git a/Remove.tla b/Remove.tla
new file mode 100644
index 0000000..8f27ec1
--- /dev/null
+++ b/Remove.tla
@@ -0,0 +1,12 @@
+------------------------------- MODULE Remove -------------------------------
+
+EXTENDS Integers, Sequences
+
+Remove(i, seq) == 
+  [j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j] 
+                                      ELSE seq[j+1]]
+
+=============================================================================
+\* Modification History
+\* Last modified Mon Jan 14 16:12:46 CET 2019 by veitheller
+\* Created Mon Jan 14 16:12:39 CET 2019 by veitheller