(* Generated by the EML-lang Coq backend *)
(* Source module: vibration_rms *)
(* Source file:   /home/monogate/monogate/forge/examples/vibration_rms.eml *)
(* Verified fns:  vibration_rms *)

Require Import Reals.
Require Import Lra.
Open Scope R_scope.

Definition NOISE_FLOOR : R := 0.25.
Definition RMS_MAX : R := 50.0.

(* ── vibration_rms ── *)

Definition vibration_rms (ax : R) (ay : R) : R :=
  let mag := sqrt (((ax * ax) + (ay * ay)) + NOISE_FLOOR) in
  Rmin RMS_MAX (Rmax 0.0 mag).

(* source obligations for vibration_rms: {O1, O2} *)
(*   O1 [8a3ee29c2e2b] -> PRESERVED (equivalent)  theorem vibration_rms_within_range -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
(*   O2 [95ead1d1c41e] -> PRESERVED (equivalent)  theorem vibration_rms_within_range -- the statement is checked for well-formedness; whether it is discharged depends on the proof body *)
(*        build: unconditional -- the theorem STATEMENT is in the artifact unconditionally; whether it is PROVED is a separate axis -- this checker rejects an undischarged theorem unless cheating is explicitly enabled *)
Theorem vibration_rms_within_range (ax : R) (ay : R)
    (h_ax : (- 30.0 <= ax /\ ax <= 30.0))
    (h_ay : (- 30.0 <= ay /\ ay <= 30.0)) :
    (((vibration_rms ax ay) >= 0.0)) /\ (((vibration_rms ax ay) <= RMS_MAX)).
Proof.
  unfold vibration_rms, NOISE_FLOOR, RMS_MAX, Rmin, Rmax.
  repeat destruct (Rle_dec _ _); lra.
Qed.