proposition: Theorem ails_no_conflict_tau_le0 : h intr = V -> h (tr evad) = V -> (MinDistance T <= l intr evad T)%R -> (l intr evad T <= MaxDistance T)%R -> (AlertRange < d intr evad)%R -> Omega (thetat intr 0 + beta intr evad T) = false -> (tau (measure2state intr 0) (measure2state (tr evad) 0) 0 <= 0)%R -> conflict intr evad T = false.
proof: Proof. Proof with trivial. intros; apply cos_no_conflict... apply (Alpha_d_AlertRange_3 H3)... apply R_T_d_diff_0... apply Rlt_le_trans with (MinDistance T)... apply MinDistance_pos... apply tau_le_0_diverg... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm