From c2493dcc4dee4f5afc8247cefe53212502159ec6 Mon Sep 17 00:00:00 2001
From: Johannes Theiner <j.theiner@live.de>
Date: Sun, 10 May 2020 14:03:13 +0200
Subject: [PATCH] small change

---
 mCRL2/TrafficLights/v4/v4_spec.mcrl2 | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/mCRL2/TrafficLights/v4/v4_spec.mcrl2 b/mCRL2/TrafficLights/v4/v4_spec.mcrl2
index 00e0a77..59c2fbe 100644
--- a/mCRL2/TrafficLights/v4/v4_spec.mcrl2
+++ b/mCRL2/TrafficLights/v4/v4_spec.mcrl2
@@ -4,14 +4,9 @@ sort
 	CardinalDirection = struct north | east | south | west;
 
 map
-	oppositeDirection: CardinalDirection -> CardinalDirection;
 	nextDirection: CardinalDirection -> CardinalDirection;
 
 eqn
-	oppositeDirection(north) = south;
-	oppositeDirection(south) = north;
-	oppositeDirection(east) = west;
-	oppositeDirection(west) = east;
 
 	nextDirection(north) = east;
 	nextDirection(east) = south;