diff --git a/Physics/MovingParticles.mch b/Physics/MovingParticles.mch
index bcb23e6fff1b7612c894a53023d272f4a2b92b4d..f26ff2c3f21f7ee55b7481ddfacf746b3239c0d4 100644
--- a/Physics/MovingParticles.mch
+++ b/Physics/MovingParticles.mch
@@ -1,6 +1,6 @@
 MACHINE MovingParticles
 // Encoding of an n-body problem in B using the REAL datatype
-INCLUDES Vectors
+INCLUDES Vectors2
 DEFINITIONS
   "LibraryReals.def"; "SORT.def"; 
   MASS == FLOAT;
diff --git a/Physics/Vectors.mch b/Physics/Vectors.mch
index 25b6f7ec8e832c5bffc55e9de3b9779db61513c3..05ff9ddcc76992a32f44af3d2f737a15938e823a 100644
--- a/Physics/Vectors.mch
+++ b/Physics/Vectors.mch
@@ -30,7 +30,7 @@ PROPERTIES
   delta_vec = %(v1,v2).(v1:VEC & v2:VEC | %i.(i:DIM| v1(i)-v2(i))) 
                 /*@desc "difference of two vectors" */ &
   // dot_product = %(v1,v2).(v1:VEC & v2:VEC | SIGMA(i).(i:DIM| v1(i)*v2(i))) &
-  dot_product = %(v1,v2).(v1:VEC & v2:VEC | sigma_reals(%i.(i:DIM| v1(i)*v2(i))))  
+  dot_product = %(v1,v2).(v1:VEC & v2:VEC | SIGMA(i).(i:DIM| v1(i)*v2(i)))  
                 /*@desc "dot product of two vectors" */ &
   
   magnitude = %v1.(v1:VEC | RSQRT(dot_product(v1,v1))) /*@desc "Magnitude of a vector" */ &
diff --git a/Physics/Vectors2.mch b/Physics/Vectors2.mch
new file mode 100644
index 0000000000000000000000000000000000000000..825b3304b3d04332d6c2625496fc24d57848bef7
--- /dev/null
+++ b/Physics/Vectors2.mch
@@ -0,0 +1,44 @@
+MACHINE Vectors2 // an optimized instance of Vectors for n=2
+DEFINITIONS
+  "LibraryReals.def"
+ABSTRACT_CONSTANTS
+  n,
+  VEC, DIM,
+  add_vec     /*@desc "sum of two vectors" */,
+  delta_vec   /*@desc "difference of two vectors" */,
+  dot_product /*@desc "dot product of two vectors" */,
+  magnitude  /*@desc "Magnitude of a vector" */,
+  unit_vec   /*@desc "unit vector of a vector" */,
+  times_vec  /*@desc "multiply scalar by a vector" */,
+  distance   /*@desc "Eucledian distance between two vectors" */,
+  
+  sigma_vecs  /*@desc "sum of a sequence of vectors" */
+PROPERTIES
+  n:NATURAL1 & n = 2 &
+  DIM = (1..n) &
+  VEC = DIM --> REAL &
+  
+  sigma_vecs = %v.(v:seq1(VEC) | [SIGMA(i).(i:dom(v)|v(i)(1)), SIGMA(i).(i:dom(v)|v(i)(2))]) 
+               /*@desc "sum of a sequence of vectors" */&
+  
+  add_vec = %(v1,v2).(v1:VEC & v2:VEC | [v1(1)+v2(1),v1(2)+v2(2)]) 
+                /*@desc "sum of two vectors" */ &
+
+  delta_vec = %(v1,v2).(v1:VEC & v2:VEC | [v1(1)-v2(1),v1(2)-v2(2)]) 
+                /*@desc "difference of two vectors" */ &
+
+  dot_product = %(v1,v2).(v1:VEC & v2:VEC | v1(1)*v2(1) + v1(2)*v2(2))
+                /*@desc "dot product of two vectors" */ &
+  
+  magnitude = %v1.(v1:VEC | RSQRT(v1(1)**2 + v1(2)**2)) /*@desc "Magnitude of a vector" */ &
+            // alternative: RSQRT(dot_product(v1,v1)))
+  
+  unit_vec = %v1.(v1:VEC | LET m BE m=magnitude(v1) IN
+                              [v1(1)/m,v1(2)/m] END ) /*@desc "unit vector of a vector" */  &
+                              
+  times_vec = %(k,v1).(k:REAL & v1:VEC | [k*v1(1),k*v1(2)]) /*@desc "multiply scalar by a vector" */ &
+                              
+  distance = %(v1,v2).(v1:VEC & v2:VEC | magnitude(delta_vec(v1,v2)))
+    /*@desc "Eucledian distance between two vectors" */
+
+END
\ No newline at end of file