fact: Definition measure2state (tr : Trajectory) (t : R) : State := mkState (x tr t) (y tr t) (toDeg (theta tr t)) (mkBank (toDeg (phi tr t)) (cond1_sty tr t) (cond2_sty tr t)).
imports: Reals trajectory_const trajectory_def constants ails_def Omega