Theorem "TAP23/Theorem 2: Opposite Longitudinal Safety" Citation "M. Strauss, S. Mitsch. Slow Down, Move Over: A Case Study in Formal Verification, Refinement, and Testing of the Responsibility-Sensitive Safety Model for Self-Driving Cars. In 17th International Conference on Tests and Proofs (TAP 2023), Proceedings, Leicester, UK, Springer, 2023.". Author "Megan Strauss and Stefan Mitsch". Definitions import kyx.math.{abs,max}; Real aMinBrakeCorrect; /* Braking constant in correct direction*/ Real aMinBrake; /* Minimum braking constant */ Real aMaxAccel; /* Maximum acceleration constant */ Real aMaxBrake; /* Maximum braking constant */ Real rho; /* Response time */ /* Safe distance as defined for opposite direction */ Real safeDist(Real v1p, Real v2p) = (rho*(v1p+v1p + rho*aMaxAccel)/2 + ((v1p + rho*aMaxAccel)^2)/(2*aMinBrakeCorrect) + rho*((-v2p) + (-v2p) + rho*aMaxAccel)/2 + (((-v2p) + rho*aMaxAccel)^2)/(2*aMinBrake)); /* Control program when distance is safe */ HP control ::= { /*Set acceleration and check that it is within bounds*/ a1 := *; a2 := *; ?(a1<=aMaxAccel & a1>=-aMaxBrake & a2>=-aMaxAccel & a2<=aMaxBrake); }; /* Proper response program */ HP longProperResponseOpposite ::= { /*Change acceleration to correct unsafe distance*/ a1 := *; ?(a1<=-aMinBrakeCorrect); a2 := *; ?(a2>=aMinBrake); }; End. ProgramVariables Real v1; /*longitudinal velocity of car 1*/ Real v2; /*longitudinal velocity of car 2*/ Real a1; /*longitudinal acceleration of car 1*/ Real a2; /*longitudinal acceleration of car 2*/ Real x1; /*longitudinal position of car 1*/ Real x2; /*longitudinal position of car 2*/ Real t; /*Time parameter for proper response*/ End. Problem aMaxAccel>0 & aMaxBrake > 0 & rho>0 & aMinBrakeCorrect > 0 & aMinBrake>0 & aMinBrake=x1 & v2=0 & v1=0 -> [{ /*Choose which controller to use based on distance*/ { {?safeDist(v1, v2)<=x2-x1; control;} ++ {?safeDist(v1, v2)>=x2-x1; longProperResponseOpposite;}}; t := 0; {v1' = a1, x1' = v1, v2' = a2, x2' = v2, t' = 1 & t <= rho& (v1>=0 & v2<=0)} }*@invariant( v1>=0 & v2<=0 & x2 - (v2^2)/(2*aMinBrake)>= x1 - (v1^2)/(-2*aMinBrakeCorrect) & x1<=x2 )] x1<=x2 /* Cars have not collided */ End. Tactic "Manual Proof" implyR('R=="aMaxAccel()>0&aMaxBrake()>0&rho()>0&aMinBrakeCorrect()>0&aMinBrake()>0&aMinBrake() < aMaxBrake()&aMinBrakeCorrect() < aMaxBrake()&x2>=x1&v2=0&v1=0->[{{?safeDist(v1,v2)<=x2-x1;control{|^@|};++?safeDist(v1,v2)>=x2-x1;longProperResponseOpposite{|^@|};}t:=0;{v1'=a1,x1'=v1,v2'=a2,x2'=v2,t'=1&t<=rho()&v1>=0&v2<=0}}*]x1<=x2"); loop("v1>=0&v2<=0&x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())&x1<=x2", 'R=="[{{?safeDist(v1,v2)<=x2-x1;control{|^@|};++?safeDist(v1,v2)>=x2-x1;longProperResponseOpposite{|^@|};}t:=0;{v1'=a1,x1'=v1,v2'=a2,x2'=v2,t'=1&t<=rho()&v1>=0&v2<=0}}*]x1<=x2"); <( "Init": QE, "Post": QE, "Step": composeb('R=="[{?safeDist(v1,v2)<=x2-x1;control{|^@|};++?safeDist(v1,v2)>=x2-x1;longProperResponseOpposite{|^@|};}t:=0;{v1'=a1,x1'=v1,v2'=a2,x2'=v2,t'=1&t<=rho()&v1>=0&v2<=0}](v1>=0&v2<=0&x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())&x1<=x2)"); unfold; <( "[?safeDist(v1,v2)<=x2-x1;control{|^@|};][t:=0;{v1'=a1,x1'=v1,v2'=a2,x2'=v2,t'=1&t<=rho()&v1>=0&v2<=0}](v1>=0&v2<=0&x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())&x1<=x2)": expand("control"); unfold; solve('R=="[{v1'=a1,x1'=v1,v2'=a2,x2'=v2,t'=1&t<=rho()&v1>=0&v2<=0}](v1>=0&v2<=0&x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())&x1<=x2)"); allR('R=="\forall t_ (t_>=0->\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)->a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2)"); implyR('R=="t_>=0->\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)->a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); implyR('R=="\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)->a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); andR('R=="a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); <( "a1*t_+v1>=0": QE, "a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2": andR('R=="a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); <( "a2*t_+v2<=0": QE, "a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2": andR('R=="a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); <( "a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())": allL("t_", 'L=="\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)"); implyL('L=="0<=t_&t_<=t_->t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); <( "0<=t_&t_<=t_": QE, "t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0": expand("safeDist"); cut("t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1"); <( "Use": hideL('L=="rho()*(v1+v1+rho()*aMaxAccel())/2+(v1+rho()*aMaxAccel())^2/(2*aMinBrakeCorrect())+rho()*(-v2+-v2+rho()*aMaxAccel())/2+(-v2+rho()*aMaxAccel())^2/(2*aMinBrake())<=x2-x1"); andL('L=="t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); hideL('L=="t_+t<=rho()"); edit("t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=x2-(t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake()))", 'L=="t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1"); andL('L=="a1*t_+v1>=0&a2*t_+v2<=0"); edit("x2+a2*(t_^2/2)+v2*t_-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())", 'R=="a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); hideL('L=="rho()>0"); edit("abbrv(x2+a2*(t_^2/2)+v2*t_)-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())", 'R=="x2+a2*(t_^2/2)+v2*t_-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); edit("t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=x2-t_*(-v2+-v2+t_*aMaxAccel())/2-(-v2+t_*aMaxAccel())^2/(2*aMinBrake())", 'L=="t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=x2-(t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake()))"); edit("t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=abbrv(x2-t_*(-v2+-v2+t_*aMaxAccel())/2)-(-v2+t_*aMaxAccel())^2/(2*aMinBrake())", 'L=="t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=x2-t_*(-v2+-v2+t_*aMaxAccel())/2-(-v2+t_*aMaxAccel())^2/(2*aMinBrake())"); cut("abbrv>=abbrv_0"); <( "Use": edit("abbrv-abbrv((a2*t_+v2)^2/(2*aMinBrake()))>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())", 'R=="abbrv-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); edit("t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=abbrv_0-abbrv((-v2+t_*aMaxAccel())^2/(2*aMinBrake()))", 'L=="t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=abbrv_0-(-v2+t_*aMaxAccel())^2/(2*aMinBrake())"); cut("abbrv_2>=abbrv_1"); <( "Use": edit("abbrv-abbrv_1>=abbrv(a1*(t_^2/2)+v1*t_+x1)-abbrv((a1*t_+v1)^2/((-2)*aMinBrakeCorrect()))", 'R=="abbrv-abbrv_1>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); edit("abbrv(x1+t_*(v1+v1+t_*aMaxAccel())/2)+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())<=abbrv_0-abbrv_2", 'L=="t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+x1<=abbrv_0-abbrv_2"); edit("abbrv_5+abbrv((v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect()))<=abbrv_0-abbrv_2", 'L=="abbrv_5+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())<=abbrv_0-abbrv_2"); cut("abbrv_3<=abbrv_5"); <( "Use": allL2R('L=="abbrv_4=(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); edit("abbrv-abbrv_1>=abbrv_3+(a1*t_+v1)^2/(2*aMinBrakeCorrect())", 'R=="abbrv-abbrv_1>=abbrv_3-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); edit("abbrv-abbrv_1>=abbrv_3+abbrv((a1*t_+v1)^2/(2*aMinBrakeCorrect()))", 'R=="abbrv-abbrv_1>=abbrv_3+(a1*t_+v1)^2/(2*aMinBrakeCorrect())"); hideL('L=="abbrv_4=(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); cut("abbrv_7<=abbrv_6"); <( "Use": QE using "abbrv_5+abbrv_6<=abbrv_0-abbrv_2 :: abbrv>=abbrv_0 :: abbrv_2>=abbrv_1 :: abbrv_3<=abbrv_5 :: abbrv_7<=abbrv_6 :: abbrv-abbrv_1>=abbrv_3+abbrv_7 :: nil", "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v1>=0 :: a1<=aMaxAccel() :: a1>=-aMaxBrake() :: t_>=0 :: a1*t_+v1>=0 :: abbrv_6=(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect()) :: abbrv_7=(a1*t_+v1)^2/(2*aMinBrakeCorrect()) :: abbrv_7<=abbrv_6 :: nil" ), "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v1>=0 :: a1<=aMaxAccel() :: a1>=-aMaxBrake() :: t_>=0 :: a1*t_+v1>=0 :: abbrv_2>=abbrv_1 :: abbrv_3=a1*(t_^2/2)+v1*t_+x1 :: abbrv_5=x1+t_*(v1+v1+t_*aMaxAccel())/2 :: abbrv_3<=abbrv_5 :: nil" ), "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v2<=0 :: t=0 :: a2>=-aMaxAccel() :: a2<=aMaxBrake() :: t_>=0 :: a2*t_+v2<=0 :: abbrv_1=(a2*t_+v2)^2/(2*aMinBrake()) :: abbrv_2=(-v2+t_*aMaxAccel())^2/(2*aMinBrake()) :: abbrv_2>=abbrv_1 :: nil" ), "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v2<=0 :: a2>=-aMaxAccel() :: a2<=aMaxBrake() :: t_>=0 :: a2*t_+v2<=0 :: abbrv=x2+a2*(t_^2/2)+v2*t_ :: abbrv_0=x2-t_*(-v2+-v2+t_*aMaxAccel())/2 :: abbrv>=abbrv_0 :: nil" ), "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: rho()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: rho()*(v1+v1+rho()*aMaxAccel())/2+(v1+rho()*aMaxAccel())^2/(2*aMinBrakeCorrect())+rho()*(-v2+-v2+rho()*aMaxAccel())/2+(-v2+rho()*aMaxAccel())^2/(2*aMinBrake())<=x2-x1 :: v1>=0 :: v2<=0 :: x1<=x2 :: t=0 :: t_>=0 :: t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0 :: t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1 :: nil" ) ), "a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2": allL("t_", 'L=="\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)"); implyL('L=="0<=t_&t_<=t_->t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); <( "0<=t_&t_<=t_": QE, "t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0": andL('L=="t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); expand("safeDist"); cut("t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1"); <( "Use": andL('L=="a1*t_+v1>=0&a2*t_+v2<=0"); hideL('L=="rho()*(v1+v1+rho()*aMaxAccel())/2+(v1+rho()*aMaxAccel())^2/(2*aMinBrakeCorrect())+rho()*(-v2+-v2+rho()*aMaxAccel())/2+(-v2+rho()*aMaxAccel())^2/(2*aMinBrake())<=x2-x1"); edit("abbrv(a1*(t_^2/2)+v1*t_)+x1<=a2*(t_^2/2)+v2*t_+x2", 'R=="a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); edit("abbrv(t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect()))+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1", 'L=="t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1"); cut("abbrv<=abbrv_0"); <( "Use": edit("abbrv+x1<=abbrv(a2*(t_^2/2)+v2*t_)+x2", 'R=="abbrv+x1<=a2*(t_^2/2)+v2*t_+x2"); edit("abbrv_0-abbrv(-(t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())))<=x2-x1", 'L=="abbrv_0+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1"); cut("abbrv_1>=abbrv_2"); <( "Use": QE using "x1<=x2 :: abbrv_0-abbrv_2<=x2-x1 :: abbrv<=abbrv_0 :: abbrv_1>=abbrv_2 :: abbrv+x1<=abbrv_1+x2 :: nil", "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v2<=0 :: x1<=x2 :: a2>=-aMaxAccel() :: a2<=aMaxBrake() :: abbrv_0-abbrv_2<=x2-x1 :: a2*t_+v2<=0 :: abbrv=a1*(t_^2/2)+v1*t_ :: abbrv_0=t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect()) :: abbrv<=abbrv_0 :: abbrv_1=a2*(t_^2/2)+v2*t_ :: abbrv_2=-(t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())) :: abbrv_1>=abbrv_2 :: nil" ), "Show": hideL('L=="t_+t<=rho()"); hideL('L=="rho()>0"); QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v1>=0 :: a1<=aMaxAccel() :: a1>=-aMaxBrake() :: t_>=0 :: a1*t_+v1>=0 :: abbrv=a1*(t_^2/2)+v1*t_ :: abbrv_0=t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect()) :: abbrv<=abbrv_0 :: nil" ), "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: rho()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: rho()*(v1+v1+rho()*aMaxAccel())/2+(v1+rho()*aMaxAccel())^2/(2*aMinBrakeCorrect())+rho()*(-v2+-v2+rho()*aMaxAccel())/2+(-v2+rho()*aMaxAccel())^2/(2*aMinBrake())<=x2-x1 :: v1>=0 :: v2<=0 :: t=0 :: a1<=aMaxAccel() :: a1>=-aMaxBrake() :: a2>=-aMaxAccel() :: a2<=aMaxBrake() :: t_>=0 :: t_+t<=rho() :: a1*t_+v1>=0&a2*t_+v2<=0 :: t_*(v1+v1+t_*aMaxAccel())/2+(v1+t_*aMaxAccel())^2/(2*aMinBrakeCorrect())+t_*(-v2+-v2+t_*aMaxAccel())/2+(-v2+t_*aMaxAccel())^2/(2*aMinBrake())<=x2-x1 :: nil" ) ) ) ) ), "[?safeDist(v1,v2)>=x2-x1;longProperResponseOpposite{|^@|};][t:=0;{v1'=a1,x1'=v1,v2'=a2,x2'=v2,t'=1&t<=rho()&v1>=0&v2<=0}](v1>=0&v2<=0&x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())&x1<=x2)": unfold; expand("longProperResponseOpposite"); unfold; solve('R=="[{v1'=a1,x1'=v1,v2'=a2,x2'=v2,t'=1&t<=rho()&v1>=0&v2<=0}](v1>=0&v2<=0&x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())&x1<=x2)"); allR('R=="\forall t_ (t_>=0->\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)->a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2)"); implyR('R=="t_>=0->\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)->a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); implyR('R=="\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)->a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); andR('R=="a1*t_+v1>=0&a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); <( "a1*t_+v1>=0": QE, "a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2": andR('R=="a2*t_+v2<=0&a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); <( "a2*t_+v2<=0": QE, "a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2": expand("safeDist"); allL("t_", 'L=="\forall s_ (0<=s_&s_<=t_->s_+t<=rho()&a1*s_+v1>=0&a2*s_+v2<=0)"); andR('R=="a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())&a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); <( "a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())": implyL('L=="0<=t_&t_<=t_->t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); <( "0<=t_&t_<=t_": QE, "t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0": hideL('L=="rho()*(v1+v1+rho()*aMaxAccel())/2+(v1+rho()*aMaxAccel())^2/(2*aMinBrakeCorrect())+rho()*(-v2+-v2+rho()*aMaxAccel())/2+(-v2+rho()*aMaxAccel())^2/(2*aMinBrake())>=x2-x1"); andL('L=="t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); andL('L=="a1*t_+v1>=0&a2*t_+v2<=0"); edit("a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=abbrv(a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect()))", 'R=="a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect())"); edit("x2-v2^2/(2*aMinBrake())>=abbrv(x1-v1^2/((-2)*aMinBrakeCorrect()))", 'L=="x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())"); cut("abbrv<=abbrv_0"); <( "Use": edit("abbrv(a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake()))>=abbrv", 'R=="a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=abbrv"); edit("abbrv(x2-v2^2/(2*aMinBrake()))>=abbrv_0", 'L=="x2-v2^2/(2*aMinBrake())>=abbrv_0"); cut("abbrv_1>=abbrv_2"); <( "Use": QE using "abbrv_2>=abbrv_0 :: abbrv<=abbrv_0 :: abbrv_1>=abbrv_2 :: abbrv_1>=abbrv :: nil", "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v2<=0 :: a2>=aMinBrake() :: t_>=0 :: a2*t_+v2<=0 :: abbrv<=abbrv_0 :: abbrv_1=a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake()) :: abbrv_2=x2-v2^2/(2*aMinBrake()) :: abbrv_1>=abbrv_2 :: nil" ), "Show": hideL('L=="rho()>0") using "aMaxAccel()>0 :: aMaxBrake()>0 :: rho()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v1>=0 :: v2<=0 :: x2-v2^2/(2*aMinBrake())>=abbrv_0 :: x1<=x2 :: a1<=-aMinBrakeCorrect() :: a2>=aMinBrake() :: t=0 :: t_>=0 :: t_+t<=rho() :: a1*t_+v1>=0 :: a2*t_+v2<=0 :: abbrv=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect()) :: abbrv_0=x1-v1^2/((-2)*aMinBrakeCorrect()) :: abbrv<=abbrv_0 :: nil"; QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v1>=0 :: a1<=-aMinBrakeCorrect() :: t=0 :: t_>=0 :: a1*t_+v1>=0 :: abbrv=a1*(t_^2/2)+v1*t_+x1-(a1*t_+v1)^2/((-2)*aMinBrakeCorrect()) :: abbrv_0=x1-v1^2/((-2)*aMinBrakeCorrect()) :: a2*(t_^2/2)+v2*t_+x2-(a2*t_+v2)^2/(2*aMinBrake())>=abbrv :: abbrv<=abbrv_0 :: nil" ) ), "a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2": implyL('L=="0<=t_&t_<=t_->t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); <( "0<=t_&t_<=t_": QE, "t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0": hideL('L=="rho()*(v1+v1+rho()*aMaxAccel())/2+(v1+rho()*aMaxAccel())^2/(2*aMinBrakeCorrect())+rho()*(-v2+-v2+rho()*aMaxAccel())/2+(-v2+rho()*aMaxAccel())^2/(2*aMinBrake())>=x2-x1"); andL('L=="t_+t<=rho()&a1*t_+v1>=0&a2*t_+v2<=0"); andL('L=="a1*t_+v1>=0&a2*t_+v2<=0"); edit("a1*(t_^2/2)+v1*t_+x1<=abbrv(a2*(t_^2/2)+v2*t_+x2)", 'R=="a1*(t_^2/2)+v1*t_+x1<=a2*(t_^2/2)+v2*t_+x2"); edit("abbrv(x2-v2^2/(2*aMinBrake()))>=x1-v1^2/((-2)*aMinBrakeCorrect())", 'L=="x2-v2^2/(2*aMinBrake())>=x1-v1^2/((-2)*aMinBrakeCorrect())"); edit("abbrv(a1*(t_^2/2)+v1*t_+x1)<=abbrv", 'R=="a1*(t_^2/2)+v1*t_+x1<=abbrv"); edit("abbrv_0>=abbrv(x1-v1^2/((-2)*aMinBrakeCorrect()))", 'L=="abbrv_0>=x1-v1^2/((-2)*aMinBrakeCorrect())"); cut("abbrv>=abbrv_0"); <( "Use": cut("abbrv_1<=abbrv_2"); <( "Use": QE using "abbrv_0>=abbrv_2 :: abbrv>=abbrv_0 :: abbrv_1<=abbrv_2 :: abbrv_1<=abbrv :: nil", "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v1>=0 :: a1<=-aMinBrakeCorrect() :: t_>=0 :: a1*t_+v1>=0 :: abbrv_1=a1*(t_^2/2)+v1*t_+x1 :: abbrv_2=x1-v1^2/((-2)*aMinBrakeCorrect()) :: abbrv>=abbrv_0 :: abbrv_1<=abbrv_2 :: nil" ), "Show": QE using "aMaxAccel()>0 :: aMaxBrake()>0 :: aMinBrakeCorrect()>0 :: aMinBrake()>0 :: aMinBrake() < aMaxBrake() :: aMinBrakeCorrect() < aMaxBrake() :: v2<=0 :: a2>=aMinBrake() :: t_>=0 :: a2*t_+v2<=0 :: abbrv=a2*(t_^2/2)+v2*t_+x2 :: abbrv_0=x2-v2^2/(2*aMinBrake()) :: abbrv>=abbrv_0 :: nil" ) ) ) ) ) ) ) End. End.