property_10.why

theory ACASXU_P10
  use ieee_float.Float64
  use int.Int
  use interpretation.Vector
  use interpretation.NeuralNetwork

  constant nn_4_5: nn = read_neural_network "nets/onnx/ACASXU_4_5.onnx" ONNX

  predicate valid_input (i: vector t) =
    (0.2689779999999999948734341614908771589398384094238281250000000000:t) .<= i[0] .<= (0.6798579999999999623483404320722911506891250610351562500000000000:t)
    /\ (0.1114079999999999931459271351741335820406675338745117187500000000:t) .<= i[1] .<= (0.5:t)
    /\ (-0.5:t) .<= i[2] .<= (-0.4933803236000000036476365039561642333865165710449218750000000000:t)
    /\ (0.2272730000000000027959856652159942314028739929199218750000000000:t) .<= i[3] .<= (0.5:t)
    /\ (0.0:t) .<= i[4] .<= (0.5:t)

  predicate is_min (o: vector t) (i: int) =
    forall j: int. 0 <= j < 5 -> i <> j -> o[i] .<= o[j]

  goal P10_4_5:
    forall i: vector t. has_length i 5 -> valid_input i -> is_min (nn_4_5@@i) 0
end