property_10.why

theory ACASXU_P10
  use ACASXU_4_5.AsTuple
  use ieee_float.Float64

  goal P10_4_5: forall x0 x1 x2 x3 x4.
     (0.2689779999999999948734341614908771589398384094238281250000000000:t) .<= x0 .<= (0.6798579999999999623483404320722911506891250610351562500000000000:t) ->
     (0.1114079999999999931459271351741335820406675338745117187500000000:t) .<= x1 .<= (0.5:t) ->
     (-0.5:t) .<= x2 .<= (-0.4933803236000000036476365039561642333865165710449218750000000000:t) ->
     (0.2272730000000000027959856652159942314028739929199218750000000000:t) .<= x3 .<= (0.5:t) ->
     (0.0:t) .<= x4 .<= (0.5:t) ->
     let (y0, y1, y2, y3, y4) = nn_apply x0 x1 x2 x3 x4 in
     y0 .<= y1 /\ y0 .<= y2 /\ y0 .<= y3 /\ y0 .<= y4
end