Add ACAS XU property #1 in why3 syntax.

acasxu.why

+theory ACAS_XU_P1
+
+  use real.Real
+
+  constant x0:real
+  axiom x0: 0.6 <= x0 <= 0.6798577687
+  
+  constant x1:real
+  axiom x1: -0.5 <= x1 <= 0.5
+  
+  constant x2:real
+  axiom x2: -0.5 <= x2 <= 0.5
+  
+  constant x3:real
+  axiom x3: 0.45 <= x3 <= 0.5
+  
+  constant x4:real
+  axiom x4: -0.5 <= x4 <= -0.45
+  
+  goal P1: forall y0:real. y0 <= 3.9911256459
+
+end