$$$top.pvs top: THEORY BEGIN IMPORTING vertical_only, ground_speed_only, heading_only, rr3d_algo, rr3d_prop END top $$$Vectors_rew.pvs Vectors_rew : THEORY BEGIN IMPORTING Vectors v,w, v1, v2 : VAR Vect3 a,b : VAR real vr0x: LEMMA (v + w)`x = v`x + w`x vr0y: LEMMA (v + w)`y = v`y + w`y vr0z: LEMMA (v + w)`z = v`z + w`z vr1x: LEMMA (v - w)`x = v`x - w`x vr1y: LEMMA (v - w)`y = v`y - w`y vr1z: LEMMA (v - w)`z = v`z - w`z vr2: LEMMA v1 + v2 - v2 = v1 vr3: LEMMA v1 - v2 + v2 = v1 END Vectors_rew $$$Vectors_rew.prf (|Vectors_rew| (|vr0x| "" (GROUND) (("" (SKOSIMP*) (("" (GRIND) NIL NIL)) NIL)) NIL) (|vr0y| "" (SKOSIMP*) (("" (GRIND) NIL NIL)) NIL) (|vr0z| "" (SKOSIMP*) (("" (GRIND) NIL NIL)) NIL) (|vr1x| "" (GRIND) NIL NIL) (|vr1y| "" (GRIND) NIL NIL) (|vr1z| "" (GRIND) NIL NIL) (|vr2| "" (SKOSIMP*) (("" (ASSERT) (("" (EXPAND "+ ") (("" (EXPAND "-") (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|vr3| "" (SKOSIMP*) (("" (EXPAND "-") (("" (EXPAND "+ ") (("" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) $$$hd_only_prop.pvs hd_only_prop: THEORY BEGIN IMPORTING hd_only_algo, hd_only, line_line_hd_comb, line_circle_hd_comb, circle_circle_hd_comb, circle_line_hd_comb, in_circle_hd_comb, out_circle_hd_comb, Vectors_rew s : VAR Vect3 % Relative position vo : VAR Vect3 % Ownship absolute velocity vi : VAR Vect3 % Intruder absolute velocity v : VAR Vect3 % Relative velocity vv : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity voe : VAR Vect3 % Ownship escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR posreal % Recovery time te : VAR real % Escape time t : VAR real % time tpp : VAR real % time thp : VAR real % time thpp: VAR real % time m : VAR solution a : VAR real b : VAR real c : VAR real A, B, C, E, Ax, Ay, B_x, B_y, SSx, SSy: VAR real vex : VAR real vrx : VAR real vry : VAR real vrz : VAR real alpha : VAR real alpha2 : VAR real eps : VAR Sign root : VAR bool % a flag: true = x1 root, false = x2 root root2: VAR bool % a flag: true = x1 root, false = x2 root % % % ---------------------------------------------------------------- % Proofs of Line-line Components % ---------------------------------------------------------------- % % hd_solution_correct : LEMMA v = vo - vi AND sr = s + tr*v AND sq(s`x) + sq(s`y) > sq(D) AND sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND sr`y /= 0 AND alpha = alpha_calc(eps,s) AND alpha2 = alpha_calc(eps,sr) AND a = 1 + sq(alpha) AND b = 2*(vi`x + alpha * vi`y) AND c = sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y) AND discr(a, b, c) >= 0 AND (vex = x1(a, b, c) OR vex = x2(a, b, c)) AND ve = (# x:= vex, y:= alpha * vex, z:= v`z #) AND ve`y-alpha2*ve`x /= 0 AND te = tr*(v`y-alpha2*v`x)/(ve`y - alpha2*ve`x) AND tr /= te AND vrx = (tr*v`x-te*vex) / (tr - te) AND vry = alpha2 * vrx AND vrz = v`z AND member(m, hd_solution(ve, vrx, vry, vrz, te, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z line_line_root_correct : LEMMA v = vo - vi AND sr = s + tr*v AND sq(s`x) + sq(s`y) > sq(D) AND sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND sr`y /= 0 AND member(m, line_line_root(s, sr, vo, vi, tr, eps, root)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z line_line_hd_correct : LEMMA member(m, line_line_hd(s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z % % % ---------------------------------------------------------------- % Proofs of Line-circle Components % ---------------------------------------------------------------- % % c_hd_solution_prop : LEMMA v = vo - vi AND sr = s + tr*v AND member(m, c_hd_solution(s, ve, vo, vi, te, tpp, tr)) IMPLIES hor_speed_gt_0?(m`ve) AND % tau(s,m`ve) < tpp AND tpp < tr AND m`te /= tr AND 0 < m`te AND m`te < tr AND entry?(sr+(tpp-tr)*m`vr,m`vr) AND vo`z = (m`vr+vi)`z AND m`ve = ve AND m`te = te AND m`vr = (# x:= (tr*v`x-te*ve`x)/(tr-te), y:= (tr*v`y-te*ve`y)/(tr-te), z:= v`z #) line_circle_root_correct : LEMMA v = vo - vi AND sr = s + tr*v AND sq(s`x) + sq(s`y) > sq(D) AND sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND member(m, line_circle_root(s, sr, vo, vi, tr, eps, root, root2)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z line_circle_hd_correct : LEMMA member(m, line_circle_hd(s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z % % % ---------------------------------------------------------------- % Proofs of Circle-circle Components % ---------------------------------------------------------------- % % circle_circle_root2_correct : LEMMA v = vo - vi AND ve = voe - vi AND sr = s + tr*v AND v`z /= 0 AND thp = theta(-1,s`z,v`z) AND % CALCULATION SSx = s`x - thp * vi`x AND % CALCULATION SSy = s`y - thp * vi`y AND % CALCULATION A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND % CALCULATION B = 4*(s`x - thp*vi`x)*thp*E AND % CALCULATION C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND % TEST AFTER COMPUTATION sq(vo`x) + sq(vo`y) >= sq(voe`x) AND % TEST AFTER COMPUTATION ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND % COMPUTED VALUE voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND % COMPUTED VALUE voe`z = vo`z AND % COMPUTED VALUE member(m, circle_circle_root2(s, voe, vo, vi, E, thp, tr, root2)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z circle_circle_root_correct : LEMMA member(m, circle_circle_root(s, vo, vi, tr, root, root2)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z circle_circle_hd_correct : LEMMA member(m, circle_circle_hd(s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z % % % ---------------------------------------------------------------- % Proofs of Circle-line Components % ---------------------------------------------------------------- % % cl_solution_prop : LEMMA v = vo - vi AND sr = s + tr*v AND ve = voe - vi AND member(m, cl_solution(s, voe, vo, vi, E, thp, tr, eps)) IMPLIES exit?(s + thp * ve, ve) AND sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND sr`y /= 0 AND ve`y-alpha_calc(eps,sr)*ve`x /= 0 AND m`te = tr*(v`y-alpha_calc(eps,sr)*v`x)/(ve`y-alpha_calc(eps,sr)*ve`x) AND tr /= m`te AND 0 < m`te AND m`te < tr AND m`ve = ve AND m`vr = (# x:= (tr*v`x-m`te*ve`x)/(tr-m`te), y:= alpha_calc(eps,sr)*(tr*v`x-m`te*ve`x)/(tr-m`te), z:= v`z #) AND hor_speed_gt_0?(m`vr) AND vo`z = (m`vr+vi)`z circle_line_root_correct : LEMMA member(m, circle_line_root(s, vo, vi, tr, root, eps)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z circle_line_hd_correct : LEMMA member(m, circle_line_hd(s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z ic_solution_prop : LEMMA v = vo - vi AND ve = voe - vi AND te = thpp AND member(m, ic_solution(s, voe, vo, vi, thpp, tr)) IMPLIES entry?(s + thpp * ve, ve) AND 0 < m`te AND m`te < tr AND m`ve = ve AND m`te = thpp AND m`vr = (# x:= (te*voe`x - tr*vo`x)/(thpp - tr) - vi`x, y:= (te*voe`y - tr*vo`y)/(thpp - tr) - vi`y, z:= v`z #) AND vo`z = m`vr`z + vi`z in_circle_root_prop : LEMMA member(m, in_circle_root(s, vo, vi, tr,root)) IMPLIES sq(vo`x) + sq(vo`y) >= sq(m`ve`x + vi`x) AND m`ve`y + vi`y = sqrt(sq(vo`x) + sq(vo`y) - sq(m`ve`x + vi`x)) AND m`ve`z + vi`z = vo`z AND theta(1, s`z, vo`z - vi`z) = m`te AND vo`z - vi`z /= 0 AND 4 * (sq(theta(1, s`z, vo`z - vi`z)) * sq(s`x - theta(1, s`z, vo`z - vi`z) * vi`x)) + 4 * (sq(theta(1, s`z, vo`z - vi`z)) * sq(s`y - theta(1, s`z, vo`z - vi`z) * vi`y)) /= 0 AND sign(-2 * (m`ve`y * s`y * m`te) - 2 * (s`y * vi`y * m`te) + 2 * (m`ve`y * vi`y * m`te * m`te) + 2 * (vi`y * vi`y * m`te * m`te)) = sign(sq(s`x - m`te * vi`x) + sq(s`y - m`te * vi`y) + sq(m`te) * sq(vo`x) + sq(m`te) * sq(vo`y) - sq(D) - 2 * (m`ve`x * vi`x * m`te * m`te) - 2 * (vi`x * vi`x * m`te * m`te) + 2 * (m`ve`x * s`x * m`te) + 2 * (s`x * vi`x * m`te)) in_circle_root_correct : LEMMA member(m, in_circle_root(s, vo, vi, tr,root)) IMPLIES separation?(s, m`ve) AND separation_pos?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND vo`z = (m`vr+vi)`z in_circle_hd_correct : LEMMA member(m, in_circle_hd(s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation_pos?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND vo`z = (m`vr+vi)`z oc_solution_prop : LEMMA v = vo - vi AND ve = voe - vi AND te = thp AND member(m, oc_solution(s, voe, vo, vi, thp, tr)) IMPLIES exit?(s + thp * ve, m`ve) AND exit?(s + thp * ve, m`vr) AND 0 < m`te AND m`te < tr AND m`ve = ve AND m`te = thp AND m`vr = (# x:= (te*voe`x - tr*vo`x)/(thp - tr) - vi`x, y:= (te*voe`y - tr*vo`y)/(thp - tr) - vi`y, z:= v`z #) AND vo`z = m`vr`z + vi`z out_circle_root_prop : LEMMA member(m, out_circle_root(s, vo, vi, tr,root)) IMPLIES sq(vo`x) + sq(vo`y) >= sq(m`ve`x + vi`x) AND m`ve`y + vi`y = sqrt(sq(vo`x) + sq(vo`y) - sq(m`ve`x + vi`x)) AND m`ve`z + vi`z = vo`z AND theta(-1, s`z, vo`z - vi`z) = m`te AND vo`z - vi`z /= 0 AND 4 * (sq(theta(-1, s`z, vo`z - vi`z)) * sq(s`x - theta(-1, s`z, vo`z - vi`z) * vi`x)) + 4 * (sq(theta(-1, s`z, vo`z - vi`z)) * sq(s`y - theta(-1, s`z, vo`z - vi`z) * vi`y)) /= 0 AND sign(-2 * (m`ve`y * s`y * m`te) - 2 * (s`y * vi`y * m`te) + 2 * (m`ve`y * vi`y * m`te * m`te) + 2 * (vi`y * vi`y * m`te * m`te)) = sign(sq(s`x - m`te * vi`x) + sq(s`y - m`te * vi`y) + sq(m`te) * sq(vo`x) + sq(m`te) * sq(vo`y) - sq(D) - 2 * (m`ve`x * vi`x * m`te * m`te) - 2 * (vi`x * vi`x * m`te * m`te) + 2 * (m`ve`x * s`x * m`te) + 2 * (s`x * vi`x * m`te)) out_circle_root_correct : LEMMA member(m, out_circle_root(s, vo, vi, tr,root)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND vo`z = (m`vr+vi)`z out_circle_hd_correct : LEMMA member(m, out_circle_hd(s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + m`te * m`ve, m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND vo`z = (m`vr+vi)`z % % % ----------------------------------------------------------- % Proofs of Heading-Speed Only % ----------------------------------------------------------- % % % hd_only_algo_correct_alt : THEOREM % member(m, hd_only_algo(s, vo, vi, tr)) % IMPLIES % separation?(s, m`ve) AND % separation?(s + m`te * m`ve, m`vr) AND % s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND % 0 < m`te AND m`te < tr AND % heading_only?(vo, m`ve+vi) AND %% vo`z = (m`ve+vi)`z AND % vo`z = (m`vr+vi)`z hd_only_algo_correct : THEOREM member(m, hd_only_algo(s, vo, vi, tr)) IMPLIES pred_sep?(s, m`ve, m`te) AND pred_sep?(s + m`te * m`ve, m`vr, tr - m`te) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND heading_only?(vo, m`ve+vi) AND % vo`z = (m`ve+vi)`z AND vo`z = (m`vr+vi)`z END hd_only_prop $$$hd_only_prop.prf (|hd_only_prop| (|hd_solution_correct_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|hd_solution_correct_TCC2| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (MULT-CASES -2) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|hd_solution_correct_TCC3| "" (SUBTYPE-TCC) NIL NIL) (|hd_solution_correct_TCC4| "" (SUBTYPE-TCC) NIL NIL) (|hd_solution_correct| "" (SKOSIMP*) (("" (LEMMA "llhd") (("" (INST?) (("" (INST - "alpha!1" "alpha2!1" "eps!1" "s!1+tr!1*v!1" "vi!1" "vo!1" "m!1`ve + vi!1") (("" (ASSERT) (("" (CASE "m!1`ve = m!1`ve + vi!1 - vi!1") (("1" (ASSERT) (("1" (EXPAND "member") (("1" (EXPAND "hd_solution") (("1" (SPLIT -19) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "singleton") (("1" (ASSERT) (("1" (REPLACE -21) (("1" (HIDE -21) (("1" (REPLACE -21) (("1" (HIDE -21) (("1" (REPLACE -21) (("1" (HIDE -21) (("1" (REPLACE -8) (("1" (HIDE -8) (("1" (REPLACE -18) (("1" (HIDE -18) (("1" (SPLIT -17) (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "+" 5) (("1" (REPLACE -6 5) (("1" (ASSERT) (("1" (EXPAND "-" 5) (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (REPLACE -6 5) (("2" (EXPAND "+" 5) (("2" (EXPAND "-" 5) (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -3) (("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (EXPAND "+") (("2" (EXPAND "-") (("2" (APPLY-EXTENSIONALITY) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_line_root_correct_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (MULT-CASES -2) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_line_root_correct| "" (SKOSIMP*) (("" (LEMMA "hd_solution_correct") (("" (INST?) (("" (INST?) (("" (INST - "_" "alpha_calc(eps!1, s!1)" "alpha_calc(eps!1, sr!1)" "_" "_" "eps!1" "_" "_" "_" "_" "_" "_") (("1" (EXPAND "member") (("1" (EXPAND "line_line_root") (("1" (SPLIT -6) (("1" (FLATTEN) (("1" (SPLIT -2) (("1" (FLATTEN) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (CASE "root!1") (("1" (ASSERT) (("1" (INST - "x1(1 + sq(alpha_calc(eps!1, s!1)), 2 * vi!1`x + 2 * (vi!1`y * alpha_calc(eps!1, s!1)), sq(vi!1`x) + sq(vi!1`y) - sq(vo!1`x) - sq(vo!1`y))") (("1" (ASSERT) NIL NIL) ("2" (HIDE 2 3 6) (("2" (HIDE -2) (("2" (GROUND) (("2" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (ASSERT) (("2" (INST - "x2(1 + sq(alpha_calc(eps!1, s!1)), 2 * vi!1`x + 2 * (vi!1`y * alpha_calc(eps!1, s!1)), sq(vi!1`x) + sq(vi!1`y) - sq(vo!1`x) - sq(vo!1`y))") (("1" (SPLIT -3) (("1" (PROPAX) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL)) NIL) ("2" (HIDE 3 4 7 -1) (("2" (GROUND) (("2" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE 4) (("2" (GROUND) (("2" (MULT-CASES -2) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE 4) (("3" (GROUND) (("3" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_line_hd_correct| "" (SKOSIMP*) (("" (LEMMA "line_line_root_correct") (("" (INST?) (("" (INST - "_" "_" "s!1+tr!1*(vo!1-vi!1)" "vo!1-vi!1") (("" (EXPAND "member") (("" (EXPAND "line_line_hd") (("" (SPLIT -2) (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT -3) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|c_hd_solution_prop_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|c_hd_solution_prop| "" (SKOSIMP*) (("" (REPLACE -2) (("" (HIDE -2) (("" (REPLACE -1) (("" (HIDE -1) (("" (EXPAND "member") (("" (EXPAND "c_hd_solution") (("" (SPLIT -) (("1" (FLATTEN) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "singleton") (("1" (REPLACE -2) (("1" (HIDE -2) (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_circle_root_correct_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (PROP) (("" (CASE "s!1`x=0") (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (CASE "s!1`y=0") (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_circle_root_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "line_circle_root") (("" (SPLIT -4) (("1" (NAME-REPLACE "VEX" " IF root!1 THEN x1 (1 + sq (alpha_calc (eps!1, s!1)), 2 * vi!1`x + 2 * (vi!1`y * alpha_calc (eps!1, s!1)), sq(vi!1`x) + sq(vi!1`y) - sq(vo!1`x) - sq(vo!1`y)) ELSE x2 (1 + sq (alpha_calc (eps!1, s!1)), 2 * vi!1`x + 2 * (vi!1`y * alpha_calc (eps!1, s!1)), sq(vi!1`x) + sq(vi!1`y) - sq(vo!1`x) - sq(vo!1`y)) ENDIF" NIL) (("1" (EXPAND "-") (("1" (EXPAND "+") (("1" (EXPAND "*") (("1" (FLATTEN) (("1" (SPLIT -3) (("1" (FLATTEN) (("1" (NAME-REPLACE "TE1" "x1(sq(sr!1`x + theta(1, s!1`z, vo!1`z - vi!1`z) * VEX - VEX * tr!1) + sq(sr!1`y - alpha_calc(eps!1, s!1) * VEX * tr!1 + alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX) - sq(D), 2 * (sq(D) * tr!1) - 2 * (s!1`x * sr!1`x * tr!1) - 2 * (s!1`y * sr!1`y * tr!1) - 2 * (s!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) - 2 * (sr!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (sr!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) - 2 * (vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1) - 2 * (vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) - 2 * (vi!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1) - 2 * (vo!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) + 2 * (s!1`x * VEX * tr!1 * tr!1) + 2 * (sr!1`x * vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (sr!1`y * vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (s!1`y * alpha_calc(eps!1, s!1) * VEX * tr!1 * tr!1) + 2 * (vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) + 2 * (vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1) + 2 * (vi!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) + 2 * (vo!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1), sq(s!1`x + vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) + sq(s!1`y + vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) - sq(D) * sq(tr!1))" NIL) (("1" (NAME-REPLACE "TE2" "x2(sq(sr!1`x + theta(1, s!1`z, vo!1`z - vi!1`z) * VEX - VEX * tr!1) + sq(sr!1`y - alpha_calc(eps!1, s!1) * VEX * tr!1 + alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX) - sq(D), 2 * (sq(D) * tr!1) - 2 * (s!1`x * sr!1`x * tr!1) - 2 * (s!1`y * sr!1`y * tr!1) - 2 * (s!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) - 2 * (sr!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (sr!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) - 2 * (vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1) - 2 * (vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) - 2 * (vi!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1) - 2 * (vo!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) + 2 * (s!1`x * VEX * tr!1 * tr!1) + 2 * (sr!1`x * vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (sr!1`y * vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (s!1`y * alpha_calc(eps!1, s!1) * VEX * tr!1 * tr!1) + 2 * (vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) + 2 * (vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1) + 2 * (vi!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1) + 2 * (vo!1`y * alpha_calc(eps!1, s!1) * theta(1, s!1`z, vo!1`z - vi!1`z) * VEX * tr!1 * tr!1), sq(s!1`x + vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) + sq(s!1`y + vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) - sq(D) * sq(tr!1))" NIL) (("1" (LEMMA "c_hd_solution_prop") (("1" (INST?) (("1" (INST - "m!1" "s!1+tr!1*(vo!1-vi!1)" "vo!1-vi!1") (("1" (EXPAND "member") (("1" (ASSERT) (("1" (LEMMA "lchd") (("1" (ASSERT) (("1" (INST - "eps!1" "s!1" "IF root2!1 THEN TE1 ELSE TE2 ENDIF" "tr!1" "vi!1" "vo!1" "_" "m!1`vr") (("1" (INST - "m!1`ve + vi!1") (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (ASSERT) (("1" (SPLIT -2) (("1" (FLATTEN) (("1" (ASSERT) (("1" (REPLACE -7) (("1" (HIDE -7) (("1" (REPLACE -7) (("1" (HIDE -7) (("1" (REPLACE -7) (("1" (HIDE -7) (("1" (CASE "root!1") (("1" (REPLACE -1) (("1" (CASE "root2!1") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REPLACE 1) (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "root2!1") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (REPLACE 1) (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE 1) (("2" (ASSERT) (("2" (ASSERT) (("2" (REPLACE -12) (("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-9 1)) (("2" (EXPAND "sq") (("2" (GROUND) (("2" (MULT-CASES -2) NIL NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (HIDE-ALL-BUT (-8 1)) (("3" (EXPAND "sq") (("3" (GROUND) (("3" (MULT-CASES -2) NIL NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (HIDE-ALL-BUT (-7 1)) (("3" (EXPAND "sq") (("3" (GROUND) (("3" (MULT-CASES -2) NIL NIL)) NIL)) NIL)) NIL) ("4" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL) ("3" (FLATTEN) (("3" (HIDE-ALL-BUT 2) (("3" (REVEAL -5) (("3" (EXPAND "sq") (("3" (GROUND) (("3" (MULT-CASES -2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (FLATTEN) NIL NIL) ("5" (FLATTEN) (("5" (HIDE-ALL-BUT 1) (("5" (EXPAND "sq") (("5" (REVEAL -6) (("5" (EXPAND "sq") (("5" (GROUND) (("5" (MULT-CASES -2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_circle_root_correct_NEW| "" (SKOSIMP*) (("" (LEMMA "c_hd_solution_prop") (("" (ASSERT) (("" (INST -1 "m!1" "s!1" "m!1`te" "theta(1, s!1`z, vo!1`z - vi!1`z)" "tr!1" "m!1`ve" "vi!1" "vo!1") (("1" (EXPAND "member") (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "lchd") (("1" (ASSERT) (("1" (INST - "eps!1" "s!1" "m!1`te" "tr!1" "vi!1" "vo!1" "m!1`ve+vi!1" "m!1`vr") (("1" (ASSERT) (("1" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (POSTPONE) NIL NIL)) NIL)) NIL) ("2" (POSTPONE) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|line_circle_hd_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "line_circle_hd") (("" (SPLIT -1) (("1" (EXPAND "union") (("1" (EXPAND "member") (("1" (FLATTEN) (("1" (LEMMA "line_circle_root_correct") (("1" (EXPAND "member") (("1" (SPLIT -3) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL) ("5" (INST?) (("5" (ASSERT) NIL NIL)) NIL) ("6" (INST?) (("6" (ASSERT) NIL NIL)) NIL) ("7" (INST?) (("7" (ASSERT) NIL NIL)) NIL) ("8" (INST?) (("8" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_circle_root2_correct_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|circle_circle_root2_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "circle_circle_root2") (("" (ASSERT) (("" (SPLIT -16) (("1" (FLATTEN) (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (NAME-REPLACE "TE" " IF root2!1 THEN x1(sq(s!1`x + vo!1`x * tr!1 + voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - voe!1`x * tr!1) + sq(s!1`y + vo!1`y * tr!1 + voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - voe!1`y * tr!1) - sq(D), 2 * (sq(D) * tr!1) - 2 * (s!1`x * s!1`x * tr!1) - 2 * (s!1`y * s!1`y * tr!1) - 2 * (s!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`x * vo!1`x * tr!1 * tr!1) - 2 * (s!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`y * vo!1`y * tr!1 * tr!1) - 2 * (s!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vi!1`x * vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vi!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vi!1`y * vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vi!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vo!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vo!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vo!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vo!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 4 * (s!1`x * vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (s!1`x * voe!1`x * tr!1 * tr!1) + 4 * (s!1`y * vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (s!1`y * voe!1`y * tr!1 * tr!1) + 2 * (vi!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vi!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) + 2 * (vi!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vi!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vi!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) + 2 * (vi!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vo!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) + 2 * (vo!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1), sq(s!1`x + vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) + sq(s!1`y + vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) - sq(D) * sq(tr!1)) ELSE x2(sq(s!1`x + vo!1`x * tr!1 + voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - voe!1`x * tr!1) + sq(s!1`y + vo!1`y * tr!1 + voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - voe!1`y * tr!1) - sq(D), 2 * (sq(D) * tr!1) - 2 * (s!1`x * s!1`x * tr!1) - 2 * (s!1`y * s!1`y * tr!1) - 2 * (s!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`x * vo!1`x * tr!1 * tr!1) - 2 * (s!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (s!1`y * vo!1`y * tr!1 * tr!1) - 2 * (s!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vi!1`x * vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vi!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vi!1`y * vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vi!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vo!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vo!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) - 2 * (vo!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) - 2 * (vo!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 4 * (s!1`x * vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (s!1`x * voe!1`x * tr!1 * tr!1) + 4 * (s!1`y * vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (s!1`y * voe!1`y * tr!1 * tr!1) + 2 * (vi!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vi!1`x * vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) + 2 * (vi!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vi!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vi!1`y * vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) + 2 * (vi!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1) + 2 * (vo!1`x * voe!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1) + 2 * (vo!1`y * voe!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) * tr!1 * tr!1), sq(s!1`x + vo!1`x * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`x * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) + sq(s!1`y + vo!1`y * theta(1, s!1`z, vo!1`z - vi!1`z) - vi!1`y * theta(1, s!1`z, vo!1`z - vi!1`z)) * sq(tr!1) - sq(D) * sq(tr!1)) ENDIF" NIL) (("1" (LEMMA "c_hd_solution_prop") (("1" (INST?) (("1" (INST - "m!1" "sr!1" "v!1") (("1" (EXPAND "+") (("1" (EXPAND "*") (("1" (ASSERT) (("1" (EXPAND "member") (("1" (FLATTEN) (("1" (LEMMA "cchd") (("1" (INST?) (("1" (ASSERT) (("1" (INST - "TE" "tr!1" "voe!1" "m!1`vr") (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (REPLACE -20 :DIR RL) (("1" (HIDE -20) (("1" (REPLACE -20 :DIR RL) (("1" (HIDE -20) (("1" (REPLACE -20 :DIR RL) (("1" (HIDE -20) (("1" (REPLACE -20 :DIR RL) (("1" (HIDE -20) (("1" (REPLACE -20 :DIR RL) (("1" (HIDE -20) (("1" (HIDE -20) (("1" (ASSERT) (("1" (REPLACE -22) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE-ALL-BUT (-20 5 -12 -2)) (("1" (REPLACE -2) (("1" (HIDE -2) (("1" (ASSERT) (("1" (CASE-REPLACE "(# x := voe!1`x, y := voe!1`y, z := voe!1`z #) = voe!1") (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 6) (("2" (CASE "root2!1") (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "exit?") (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 5) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL) ("5" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_circle_root_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "circle_circle_root") (("" (EXPAND "+") (("" (EXPAND "-") (("" (EXPAND "*") (("" (SPLIT -1) (("1" (FLATTEN) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (SPLIT -) (("1" (NAME-REPLACE "VOEX1" "x1(4 * (sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x)) + 4 * (sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)), -4 * (s!1`x * sq(D) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * vi!1`x * theta (-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * vi!1`x * theta (-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta (-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta (-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (sq(D) * vi!1`x * theta (-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)), sq (sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) + sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) + sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`x) + sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`y) - sq(D)) - 4 * (sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)) - 4 * (sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)))" NIL) (("1" (NAME-REPLACE "VOEX2" "x2(4 * (sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x)) + 4 * (sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)), -4 * (s!1`x * sq(D) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (sq(D) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)), sq (sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) + sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) + sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`x) + sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`y) - sq(D)) - 4 * (sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)) - 4 * (sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y))) " NIL) (("1" (LEMMA "circle_circle_root2_correct") (("1" (INST?) (("1" (ASSERT) (("1" (INST - "m!1") (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (ASSERT) (("1" (REPLACE -2) (("1" (REPLACE -3) (("1" (HIDE -2 -3) (("1" (FLATTEN) (("1" (EXPAND "member") (("1" (SPLIT -1) (("1" (PROPAX) NIL NIL) ("2" (PROPAX) NIL NIL) ("3" (HIDE-ALL-BUT 1) (("3" (GROUND) (("3" (LIFT-IF) (("3" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("4" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (HIDE-ALL-BUT (-3 1)) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_circle_hd_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "circle_circle_hd") (("" (EXPAND "union") (("" (EXPAND "member") (("" (LEMMA "circle_circle_root_correct") (("" (EXPAND "member") (("" (SPLIT -2) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cl_solution_prop_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (PROP) (("" (CASE "sr!1`x=0") (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cl_solution_prop_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cl_solution_prop| "" (SKOSIMP*) (("" (REPLACE -1) (("" (HIDE -1) (("" (REPLACE -1) (("" (HIDE -1) (("" (REPLACE -1) (("" (HIDE -1) (("" (EXPAND "member") (("" (EXPAND "cl_solution") (("" (SPLIT -1) (("1" (FLATTEN) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE -5) (("1" (EXPAND "singleton") (("1" (NAME-REPLACE "ALPHA" "alpha_calc(eps!1, s!1 + tr!1 * (vo!1 - vi!1))") (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-5 1 4)) (("2" (PROP) (("2" (NAME-REPLACE "SR" "s!1 + tr!1 * (vo!1 - vi!1)") (("2" (MULT-CASES -2) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_line_root_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "circle_line_root") (("" (SPLIT -) (("1" (FLATTEN) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (ASSERT) (("1" (NAME-REPLACE "VOEX1" "x1 (4 * (sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x)) + 4 * (sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)), -4 * (s!1`x * sq(D) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * theta (-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (sq(D) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta (-1, s!1`z, vo!1`z - vi!1`z)), sq (sq (s!1`x - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) + sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) + sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`x) + sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`y) - sq(D)) - 4 * (sq(vo!1`x) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)) - 4 * (sq(vo!1`y) * sq (theta (-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta (-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)))" NIL) (("1" (NAME-REPLACE "VOEX2" "x2(4 * (sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`x - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x)) + 4 * (sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)), -4 * (s!1`x * sq(D) * theta(-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`x - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta(-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq (s!1`y - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta(-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`x) * sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta(-1, s!1`z, vo!1`z - vi!1`z)) - 4 * (sq(vo!1`y) * sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta(-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`x - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) * theta(-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq (s!1`y - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) * theta(-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`x) * sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * theta(-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (s!1`x * sq(vo!1`y) * sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * theta(-1, s!1`z, vo!1`z - vi!1`z)) + 4 * (sq(D) * vi!1`x * theta(-1, s!1`z, vo!1`z - vi!1`z) * theta(-1, s!1`z, vo!1`z - vi!1`z)), sq (sq (s!1`x - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`x) + sq (s!1`y - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y) + sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`x) + sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * sq(vo!1`y) - sq(D)) - 4 * (sq(vo!1`x) * sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)) - 4 * (sq(vo!1`y) * sq (theta(-1, s!1`z, vo!1`z - vi!1`z)) * sq (s!1`y - theta(-1, s!1`z, vo!1`z - vi!1`z) * vi!1`y)))" NIL) (("1" (SPLIT -4) (("1" (FLATTEN) (("1" (LEMMA "cl_solution_prop") (("1" (INST?) (("1" (INST - "m!1" "s!1+tr!1*(vo!1-vi!1)" "vo!1-vi!1" "(# x := IF root!1 THEN VOEX1 ELSE VOEX2 ENDIF, y := sqrt(sq(vo!1`x) + sq(vo!1`y) - IF root!1 THEN sq(VOEX1) ELSE sq(VOEX2) ENDIF), z := vo!1`z #)-vi!1") (("1" (EXPAND "member") (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (ASSERT) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (LEMMA "clhd") (("1" (INST?) (("1" (ASSERT) (("1" (INST - "eps!1" "tr!1" " (# x := IF root!1 THEN VOEX1 ELSE VOEX2 ENDIF, y := sqrt(sq(vo!1`x) + sq(vo!1`y) - IF root!1 THEN sq(VOEX1) ELSE sq(VOEX2) ENDIF) , z := vo!1`z #)" "_") (("1" (INST - "m!1`vr") (("1" (EXPAND "+") (("1" (EXPAND "-") (("1" (EXPAND "*") (("1" (ASSERT) (("1" (REPLACE -14) (("1" (REPLACE -15) (("1" (NAME-REPLACE "ALPHA" " alpha_calc(eps!1, (# x := s!1`x + vo!1`x * tr!1 - vi!1`x * tr!1, y := s!1`y + vo!1`y * tr!1 - vi!1`y * tr!1, z := s!1`z + vo!1`z * tr!1 - vi!1`z * tr!1 #))") (("1" (REPLACE -5 :DIR RL) (("1" (REPLACE -8 :DIR RL) (("1" (ASSERT) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE -1) (("1" (REPLACE -11 6) (("1" (ASSERT) (("1" (CASE "root!1") (("1" (SPLIT 6) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL) ("4" (PROPAX) NIL NIL)) NIL) ("2" (SPLIT 7) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL) ("4" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL) ("3" (PROPAX) NIL NIL) ("4" (HIDE 7) (("4" (CASE "root!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("5" (CASE "root!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL) ("6" (PROPAX) NIL NIL) ("7" (ASSERT) (("7" (CASE "root!1") (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (HIDE 8) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("8" (ASSERT) (("8" (CASE "root!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (1 2 -3)) (("2" (ASSERT) (("2" (PROP) (("2" (REPLACE -1) (("2" (ASSERT) (("2" (CASE "s!1`x + vo!1`x * tr!1 - vi!1`x * tr!1 = 0") (("1" (ASSERT) (("1" (REPLACE -1) (("1" (ASSERT) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "(s!1`x + vo!1`x * tr!1 - vi!1`x * tr!1)*(s!1`y + vo!1`y * tr!1 - vi!1`y * tr!1) = s!1`x * s!1`y - s!1`x * vi!1`y * tr!1 - s!1`y * vi!1`x * tr!1 - vi!1`x * vo!1`y * tr!1 * tr!1 - vi!1`y * vo!1`x * tr!1 * tr!1 + s!1`x * vo!1`y * tr!1 + s!1`y * vo!1`x * tr!1 + vi!1`x * vi!1`y * tr!1 * tr!1 + vo!1`x * vo!1`y * tr!1 * tr!1") (("1" (REPLACE -1) (("1" (REPLACE -1 :DIR RL) (("1" (DIV-BY -3 "s!1`x + vo!1`x * tr!1 - vi!1`x * tr!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REAL-PROPS 1) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 7) (("2" (CASE "root!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "root!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (CASE "root!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_line_hd_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "circle_line_hd") (("" (EXPAND "union") (("" (EXPAND "member") (("" (LEMMA "circle_line_root_correct") (("" (EXPAND "member") (("" (SPLIT -2) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL) ("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ic_solution_prop_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|ic_solution_prop| "" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "Vectors_rew") (("" (EXPAND "ic_solution") (("" (EXPAND "member") (("" (SPLIT -4) (("1" (FLATTEN) (("1" (ASSERT) (("1" (ASSERT) (("1" (EXPAND "singleton") (("1" (REPLACE -3) (("1" (SPLIT -2) (("1" (FLATTEN) (("1" (REPLACE -3) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|in_circle_root_prop_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|in_circle_root_prop_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|in_circle_root_prop| "" (SKOSIMP*) (("" (GRIND :EXCLUDE ("theta" "sq" "discr" "entry?" "sign" "x1" "x2")) NIL NIL)) NIL) (|in_circle_root_correct| "" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "Vectors_rew") (("" (LEMMA "in_circle_root_prop") (("" (ASSERT) (("" (INST?) (("" (ASSERT) (("" (FLATTEN) (("" (LEMMA "ic_solution_prop") (("" (INST?) (("" (INST -1 "m!1" "m!1`te" "tr!1" "vo!1-vi!1" "vi!1" "vo!1" "m!1`ve+vi!1") (("" (ASSERT) (("" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "ichd") (("1" (ASSERT) (("1" (INST?) (("1" (INST -1 "m!1`ve +vi!1" "m!1`vr +vi!1") (("1" (ASSERT) (("1" (REPLACE -10) (("1" (EXPAND "member") (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (HIDE 4) (("2" (GRIND :EXCLUDE ("theta" "sq" "discr" "entry?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL) ("3" (HIDE 4) (("3" (EXPAND "in_circle_root") (("3" (EXPAND "emptyset") (("3" (GROUND) (("3" (CASE "root!1") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (GRIND :EXCLUDE ("theta" "sq" "discr" "entry?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL) ("2" (REPLACE 1) (("2" (ASSERT) (("2" (HIDE -1 -3 -4) (("2" (GRIND :EXCLUDE ("theta" "sq" "discr" "entry?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (EXPAND "member") (("2" (EXPAND "in_circle_root") (("2" (EXPAND "emptyset") (("2" (GROUND) (("2" (HIDE -1 -3 -4) (("2" (CASE "root!1") (("1" (ASSERT) (("1" (EXPAND "ic_solution" -) (("1" (EXPAND "emptyset") (("1" (GROUND) (("1" (EXPAND "singleton") (("1" (GRIND :EXCLUDE ("theta" "sq" "discr" "entry?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE 1) (("2" (EXPAND "ic_solution" -) (("2" (EXPAND "emptyset") (("2" (GROUND) (("2" (EXPAND "singleton") (("2" (GRIND :EXCLUDE ("theta" "sq" "discr" "entry?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|in_circle_hd_correct| "" (SKOSIMP*) (("" (LEMMA "in_circle_root_correct") (("" (INST?) (("" (EXPAND "in_circle_hd") (("" (EXPAND "member") (("" (EXPAND "union") (("" (EXPAND "member") (("" (SPLIT -2) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|oc_solution_prop_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|oc_solution_prop| "" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "Vectors_rew") (("" (EXPAND "oc_solution") (("" (EXPAND "member") (("" (SPLIT -4) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "singleton") (("1" (SPLIT -3) (("1" (FLATTEN) (("1" (ASSERT) (("1" (ASSERT) (("1" (HIDE -1 -2) (("1" (REPLACE -1) (("1" (ASSERT) (("1" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (REPLACE -4) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|out_circle_root_prop_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|out_circle_root_prop_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|out_circle_root_prop| "" (SKOSIMP*) (("" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL) (|out_circle_root_correct| "" (SKOSIMP*) (("" (AUTO-REWRITE-THEORY "Vectors_rew") (("" (LEMMA "out_circle_root_prop") (("" (ASSERT) (("" (INST?) (("" (ASSERT) (("" (FLATTEN) (("" (LEMMA "oc_solution_prop") (("" (INST?) (("" (INST -1 "m!1" "m!1`te" "tr!1" "vo!1-vi!1" "vi!1" "vo!1" "m!1`ve+vi!1") (("" (ASSERT) (("" (SPLIT -1) (("1" (FLATTEN) (("1" (LEMMA "ochd") (("1" (ASSERT) (("1" (INST?) (("1" (INST -1 "m!1`ve +vi!1" "m!1`vr +vi!1") (("1" (ASSERT) (("1" (EXPAND "member") (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (HIDE 4) (("2" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL) ("3" (HIDE 4) (("3" (FLATTEN) (("3" (EXPAND "out_circle_root") (("3" (EXPAND "emptyset") (("3" (GROUND) (("3" (HIDE -1 -3 -4) (("3" (EXPAND "oc_solution" -) (("3" (EXPAND "emptyset") (("3" (GROUND) (("3" (CASE "root!1") (("1" (ASSERT) (("1" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL) ("2" (REPLACE 1) (("2" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (EXPAND "member") (("2" (EXPAND "out_circle_root") (("2" (EXPAND "emptyset") (("2" (GROUND) (("2" (HIDE -1 -3 -4) (("2" (EXPAND "oc_solution" -) (("2" (EXPAND "emptyset") (("2" (GROUND) (("2" (CASE "root!1") (("1" (ASSERT) (("1" (EXPAND "oc_solution") (("1" (EXPAND "emptyset") (("1" (GROUND) (("1" (HIDE -1 -2 -3 -4 -5 2 5) (("1" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL) ("2" (HIDE -11 5) (("2" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL) ("3" (HIDE -11 2) (("3" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE 1) (("2" (EXPAND "oc_solution") (("2" (EXPAND "emptyset") (("2" (GROUND) (("1" (HIDE -1 -2 -3 -4 -12 6) (("1" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL) ("2" (EXPAND "singleton") (("2" (HIDE -10 3 6) (("2" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL) ("3" (EXPAND "singleton") (("3" (HIDE -10 3 6) (("3" (GRIND :EXCLUDE ("theta" "sq" "discr" "exit?" "sign" "x1" "x2")) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|out_circle_hd_correct| "" (SKOSIMP*) (("" (EXPAND "out_circle_hd") (("" (EXPAND "union") (("" (LEMMA "out_circle_root_correct") (("" (EXPAND "member") (("" (SPLIT -2) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|hd_only_algo_correct| "" (SKOSIMP*) (("" (LEMMA "line_line_hd_correct") (("" (INST?) (("" (LEMMA "line_circle_hd_correct") (("" (INST?) (("" (LEMMA "circle_circle_hd_correct") (("" (INST?) (("" (LEMMA "circle_line_hd_correct") (("" (INST?) (("" (LEMMA "in_circle_hd_correct") (("" (INST?) (("" (LEMMA "out_circle_hd_correct") (("" (INST?) (("" (LEMMA "sep_connection") (("" (COPY -1) (("" (INST?) (("" (INST -2 "s!1 + m!1`te * m!1`ve" "tr!1 - m!1`te" "m!1`vr") (("" (EXPAND "hd_only_algo") (("" (EXPAND "union") (("" (EXPAND "member") (("" (GROUND) (("" (EXPAND "heading_only?") (("" (HIDE-ALL-BUT (-3 1)) (("" (EXPAND "pred_sep?") (("" (EXPAND "separation_pos?") (("" (SKOSIMP*) (("" (INST?) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$rr3d_prop.pvs rr3d_prop: THEORY BEGIN IMPORTING rr3d_algo, gs_only_prop, vert_only_prop, hd_only_prop, common_defs s : VAR Vect3 % Relative position vo : VAR Vect3 % Ownship absolute velocity vi : VAR Vect3 % Intruder absolute velocity tr : VAR posreal % Recovery time m : VAR solution % % % ----------------------------------------------------------- % Proof of RR3D Algorithm % ----------------------------------------------------------- % % rr3d_algo_correct : THEOREM hor_sep?(s) AND NOT pred_sep?(s,vo-vi,tr) AND member(m, rr3d_algo(s, vo, vi, tr)) IMPLIES pred_sep?(s, m`ve, m`te) AND pred_sep?(s + m`te * m`ve, m`vr, tr - m`te) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND ((ground_speed_only?(m`ve+vi, vo, vi) AND ground_speed_only?(m`vr+vi, vo, vi)) OR (vertical_change?(vo-vi, m`ve) AND vertical_change?(vo-vi, m`vr))) END rr3d_prop $$$rr3d_prop.prf (|rr3d_prop| (|rr3d_algo_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "rr3d_algo") (("" (EXPAND "union") (("" (LEMMA "vert_only_algo_correct") (("" (INST?) (("" (LEMMA "gs_only_algo_correct") (("" (INST?) (("" (SPLIT -4) (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$hd_only_algo.pvs hd_only_algo: THEORY BEGIN IMPORTING hd_only, criteria, common_defs, sign s : VAR Vect3 % Relative position vo : VAR Vect3 % Ownship absolute velocity vi : VAR Vect3 % Intruder absolute velocity v : VAR Vect3 % Relative velocity vv : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity voe : VAR Vect3 % Ownship escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR posreal % Recovery time te : VAR real % Escape time t : VAR real % time thp : VAR real % time thpp: VAR real % time tpp : VAR real % time m : VAR solution a : VAR real b : VAR real c : VAR real E : VAR real vrx : VAR real % x component of recovery velocity vry : VAR real % y component of recovery velocity vrz : VAR real % z component of recovery velocity eps : Var Sign root : Var bool % a flag: true = x1 root, false = x2 root root2: Var bool % a flag: true = x1 root, false = x2 root % % % ---------------------------------------------------------------- % Line-Line Algorithm % ---------------------------------------------------------------- % % hd_solution(ve, vrx, vry, vrz, te, tr) : set[solution] = LET vr = (# x:= vrx, y:= vry, z:= vrz #) IN IF hor_speed_gt_0?(ve) AND hor_speed_gt_0?(vr) AND 0 < te AND te < tr THEN LET m = (# ve:=ve, vr:=vr, te:=te #) IN singleton(m) ELSE emptyset ENDIF line_line_root(s:alpha_type, sr: alpha_type, vo, vi, tr, eps, root) : set[solution] = LET v = vo - vi, alpha = alpha_calc(eps,s), alpha2 = alpha_calc(eps,sr), a = 1 + sq(alpha), b = 2*(vi`x + alpha * vi`y), c = sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y) IN IF discr(a, b, c) >= 0 THEN LET vex = IF root THEN x1(a, b, c) ELSE x2(a, b, c) ENDIF, ve = (# x:= vex, y:= alpha * vex, z:= v`z #) IN IF ve`y-alpha2*ve`x /= 0 THEN LET te = tr*(v`y-alpha2*v`x)/(ve`y - alpha2*ve`x) IN IF tr /= te THEN LET vrx = (tr*v`x-te*vex) / (tr - te), vry = alpha2 * vrx, vrz = v`z IN hd_solution(ve, vrx, vry, vrz, te, tr) ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF line_line_hd(s, vo, vi, tr) : set[solution] = LET v = vo - vi, sr = s + tr*v IN IF sq(s`x) + sq(s`y) > sq(D) AND sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND sr`y /= 0 THEN LET m1 = line_line_root(s, sr, vo, vi, tr, -1, TRUE), m2 = line_line_root(s, sr, vo, vi, tr, -1, FALSE), m3 = line_line_root(s, sr, vo, vi, tr, 1, TRUE), m4 = line_line_root(s, sr, vo, vi, tr, 1, FALSE) IN union(m1, union(m2, union(m3, m4))) ELSE emptyset ENDIF % % % ---------------------------------------------------------------- % Line-Circle Algorithm % ---------------------------------------------------------------- % % c_hd_solution(s, ve, vo, vi, te, tpp, tr) : set[solution] = LET v = vo - vi, sr = s + tr * v IN IF hor_speed_gt_0?(ve) AND % tau(s,ve) < tpp AND tpp < tr AND te /= tr AND 0 < te AND te < tr THEN LET vr = (# x:= (tr*v`x-te*ve`x)/(tr-te), y:= (tr*v`y-te*ve`y)/(tr-te), z:= v`z #) IN IF entry?(sr+(tpp-tr)*vr,vr) THEN LET m = (# ve:=ve, vr:=vr, te:=te #) IN singleton(m) ELSE emptyset ENDIF ELSE emptyset ENDIF line_circle_root(s:alpha_type, sr, vo, vi, tr, eps, root, root2) : set[solution] = LET v = vo - vi, alpha = alpha_calc(eps,s), a = 1 + sq(alpha), b = 2*(vi`x + alpha * vi`y), c = sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y) IN IF discr(a, b, c) >= 0 AND v`z /= 0 THEN LET vex = IF root THEN x1(a, b, c) ELSE x2(a, b, c) ENDIF, ve = (# x:= vex, y:= alpha * vex, z:= v`z #), tpp = theta(1,s`z,v`z), Ax = sr`x + (tpp - tr)*ve`x, Ay = sr`y + (tpp - tr)*ve`y, B_x = (s`x+tpp*v`x), B_y = (s`y+tpp*v`y), a2 = sq(Ax) + sq(Ay) - sq(D), b2 = 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, c2 = sq(tr) * (sq(B_x) + sq(B_y) - sq(D)) IN IF a2 /= 0 AND discr(a2, b2, c2) >= 0 THEN LET te = IF root2 THEN x1(a2, b2, c2) ELSE x2(a2, b2, c2) ENDIF IN c_hd_solution(s, ve, vo, vi, te, tpp, tr) ELSE emptyset ENDIF ELSE emptyset ENDIF line_circle_hd(s, vo, vi, tr) : set[solution] = LET v = vo - vi, sr = s + tr*v IN IF sq(s`x) + sq(s`y) > sq(D) AND sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) THEN LET m1 = line_circle_root(s, sr, vo, vi, tr, -1, TRUE, TRUE), m2 = line_circle_root(s, sr, vo, vi, tr, -1, FALSE, TRUE), m3 = line_circle_root(s, sr, vo, vi, tr, 1, TRUE, TRUE), m4 = line_circle_root(s, sr, vo, vi, tr, 1, FALSE, TRUE), m5 = line_circle_root(s, sr, vo, vi, tr, -1, TRUE, FALSE), m6 = line_circle_root(s, sr, vo, vi, tr, -1, FALSE, FALSE), m7 = line_circle_root(s, sr, vo, vi, tr, 1, TRUE, FALSE), m8 = line_circle_root(s, sr, vo, vi, tr, 1, FALSE, FALSE) IN union(m1, union(m2, union(m3, union(m4, union(m5, union(m6, union(m7, m8))))))) ELSE emptyset ENDIF % % % ---------------------------------------------------------------- % Circle-Circle Algorithm % ---------------------------------------------------------------- % % circle_circle_root2(s, voe, vo, vi, E, thp, tr, root2) : set[solution] = LET v = vo - vi, sr = s + tr*v, ve = voe - vi IN IF v`z /= 0 THEN LET tpp = theta(1,s`z,v`z), Ax = sr`x + (tpp - tr)*ve`x, Ay = sr`y + (tpp - tr)*ve`y, B_x = (s`x+tpp*v`x), B_y = (s`y+tpp*v`y), a2 = sq(Ax) + sq(Ay) - sq(D), b2 = 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, c2 = sq(tr) * (sq(B_x) + sq(B_y) - sq(D)) IN IF a2 /= 0 AND discr(a2, b2, c2) >= 0 AND sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND exit?(s + thp * ve, ve) THEN LET te = IF root2 THEN x1(a2, b2, c2) ELSE x2(a2, b2, c2) ENDIF IN c_hd_solution(s, ve, vo, vi, te, tpp, tr) ELSE emptyset ENDIF ELSE emptyset ENDIF circle_circle_root(s, vo, vi, tr, root, root2) : set[solution] = LET v = vo - vi, sr = s + tr*v IN IF v`z /= 0 THEN LET thp = theta(-1,s`z,v`z), SSx = s`x - thp * vi`x, SSy = s`y - thp * vi`y, E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D), A = 4*sq(thp)*(sq(SSx) + sq(SSy)), B = 4*(s`x - thp*vi`x)*thp*E, C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) IN IF A /= 0 AND discr(A,B,C) >= 0 THEN LET voex = IF root THEN x1(A, B, C) ELSE x2(A, B, C) ENDIF IN IF sq(vo`x) + sq(vo`y) >= sq(voex) THEN LET voe = (# x:= voex, y:= sqrt(sq(vo`x) + sq(vo`y) - sq(voex)), z:= vo`z #) IN circle_circle_root2(s, voe, vo, vi, E, thp, tr, root2) ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF circle_circle_hd(s, vo, vi, tr) : set[solution] = union( circle_circle_root(s, vo, vi, tr, TRUE, TRUE), union( circle_circle_root(s, vo, vi, tr, FALSE, TRUE), union( circle_circle_root(s, vo, vi, tr, TRUE, FALSE), circle_circle_root(s, vo, vi, tr, FALSE, FALSE)))) % % % ---------------------------------------------------------------- % Circle-Line Algorithm % ---------------------------------------------------------------- % % cl_solution(s, voe, vo, vi, E, thp, tr, eps) : set[solution] = LET v = vo - vi, sr = s + tr*v, ve = voe - vi IN IF exit?(s + thp * ve, ve) AND sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND sr`y /= 0 THEN LET alpha2 = alpha_calc(eps,sr) IN IF ve`y-alpha2*ve`x /= 0 THEN LET te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) IN IF tr /= te AND 0 < te AND te < tr THEN LET vr = (# x:= (tr*v`x-te*ve`x)/(tr-te), y:= alpha2*(tr*v`x-te*ve`x)/(tr-te), z:= v`z #) IN IF hor_speed_gt_0?(vr) THEN singleton((#ve:= ve, vr:= vr, te:=te#)) ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF circle_line_root(s, vo, vi, tr, root, eps) : set[solution] = LET v = vo - vi, sr = s + tr*v IN IF v`z /= 0 THEN LET thp = theta(-1,s`z,v`z), SSx = s`x - thp * vi`x, SSy = s`y - thp * vi`y, E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D), A = 4*sq(thp)*(sq(SSx) + sq(SSy)), B = 4*(s`x - thp*vi`x)*thp*E, C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) IN IF A /= 0 AND discr(A,B,C) >= 0 THEN LET voex = IF root THEN x1(A, B, C) ELSE x2(A, B, C) ENDIF IN IF sq(vo`x) + sq(vo`y) >= sq(voex) THEN LET voe = (# x:= voex, y:= sqrt(sq(vo`x) + sq(vo`y) - sq(voex)), z:= vo`z #) IN cl_solution(s, voe, vo, vi, E, thp, tr, eps) ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF circle_line_hd(s, vo, vi, tr) : set[solution] = union( circle_line_root(s, vo, vi, tr, TRUE, -1), union( circle_line_root(s, vo, vi, tr, FALSE, -1), union( circle_line_root(s, vo, vi, tr, TRUE, 1), circle_line_root(s, vo, vi, tr, FALSE, 1)))) % % % ---------------------------------------------------------------- % In-Circle Algorithm % ---------------------------------------------------------------- % % ic_solution(s, voe, vo, vi, thpp, tr) : set[solution] = LET v = vo - vi, sr = s + tr*v, ve = voe - vi IN IF entry?(s + thpp * ve, ve) THEN LET te = thpp IN IF 0 < te AND te < tr THEN LET vorx = (te*voe`x - tr*vo`x)/(thpp - tr), vory = (te*voe`y - tr*vo`y)/(thpp - tr), vr = (# x:= vorx - vi`x, y:= vory - vi`y, z:= v`z #) IN singleton((#ve:= ve, vr:= vr, te:=te#)) ELSE emptyset ENDIF ELSE emptyset ENDIF in_circle_root(s, vo, vi, tr, root) : set[solution] = LET v = vo - vi, sr = s + tr*v IN IF v`z /= 0 THEN LET thpp = theta(1,s`z,v`z) , SSx = s`x - thpp * vi`x , SSy = s`y - thpp * vi`y , E = sq(s`x - thpp*vi`x) + sq(s`y - thpp*vi`y) + sq(thpp)*sq(vo`x) + sq(thpp)*sq(vo`y) - sq(D) , A = 4*sq(thpp)*(sq(SSx) + sq(SSy)) , B = 4*(s`x - thpp*vi`x)*thpp*E , C = sq(E) - 4*sq(s`y - thpp*vi`y)*sq(thpp)*(sq(vo`x)+sq(vo`y)) IN IF A /= 0 AND discr(A,B,C) >= 0 THEN LET voex = IF root THEN x1(A, B, C) ELSE x2(A, B, C) ENDIF IN IF sq(vo`x) + sq(vo`y) >= sq(voex) THEN LET voey = sqrt(sq(vo`x) + sq(vo`y) - sq(voex)) IN IF sign(-2 * (s`y - thpp*vi`y) * thpp * voey) = sign(E + 2 * (s`x - thpp*vi`x) * thpp * voex) THEN LET voe = (# x:= voex, y:= voey, z:= vo`z #) IN ic_solution(s, voe, vo, vi, thpp, tr) ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF in_circle_hd(s, vo, vi, tr) : set[solution] = LET v = vo - vi, m1 = in_circle_root(s, vo, vi, tr, TRUE), m2 = in_circle_root(s, vo, vi, tr, FALSE) IN union(m1, m2) % % % ---------------------------------------------------------------- % Out-Circle Algorithm % ---------------------------------------------------------------- % % oc_solution(s, voe, vo, vi, thp, tr) : set[solution] = LET v = vo - vi, sr = s + tr*v, ve = voe - vi, te = thp IN IF 0 < te AND te < tr THEN LET vorx = (te*voe`x - tr*vo`x)/(thp - tr), vory = (te*voe`y - tr*vo`y)/(thp - tr), vr = (# x:= vorx - vi`x, y:= vory - vi`y, z:= v`z #) IN IF exit?(s + thp * ve, ve) AND exit?(s + thp * ve, vr) THEN singleton((# ve:= ve, vr:= vr, te:=te #)) ELSE emptyset ENDIF ELSE emptyset ENDIF out_circle_root(s, vo, vi, tr, root) : set[solution] = LET v = vo - vi, sr = s + tr*v IN IF v`z /= 0 THEN LET thp = theta(-1,s`z,v`z) , SSx = s`x - thp * vi`x , SSy = s`y - thp * vi`y , E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) , A = 4*sq(thp)*(sq(SSx) + sq(SSy)) , B = 4*(s`x - thp*vi`x)*thp*E , C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) IN IF A /= 0 AND discr(A,B,C) >= 0 THEN LET voex = IF root THEN x1(A, B, C) ELSE x2(A, B, C) ENDIF IN IF sq(vo`x) + sq(vo`y) >= sq(voex) THEN LET voey = sqrt(sq(vo`x) + sq(vo`y) - sq(voex)) IN IF sign(-2 * (s`y - thp*vi`y) * thp * voey) = sign(E + 2 * (s`x - thp*vi`x) * thp * voex) THEN LET voe = (# x:= voex, y:= voey, z:= vo`z #) IN oc_solution(s, voe, vo, vi, thp, tr) ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF ELSE emptyset ENDIF out_circle_hd(s, vo, vi, tr) : set[solution] = union( out_circle_root(s, vo, vi, tr, TRUE), out_circle_root(s, vo, vi, tr, FALSE)) % % % ---------------------------------------------------------------- % The Heading Only Algorithm % ---------------------------------------------------------------- % % hd_only_algo(s, vo, vi, tr) : set[solution] = union( line_line_hd(s, vo, vi, tr), union( line_circle_hd(s, vo, vi, tr), union( circle_line_hd(s, vo, vi, tr), union( circle_circle_hd(s, vo, vi, tr), union( in_circle_hd(s, vo, vi, tr), out_circle_hd(s, vo, vi, tr)))))) END hd_only_algo $$$hd_only_algo.prf (|hd_only_algo| (|line_line_root_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|line_line_hd_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_line_hd_TCC2| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (MULT-CASES -2) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|c_hd_solution_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|line_circle_hd_TCC1| "" (SUBTYPE-TCC) (("" (MOVE-TERMS -3 L 1) (("" (ASSERT) (("" (CASE "s!1`y=0") (("1" (ASSERT) NIL NIL) ("2" (CASE "s!1`x=0") (("1" (ASSERT) NIL NIL) ("2" (DIV-BY -5 "s!1`x") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_circle_root_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cl_solution_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (PROP) (("" (REPLACE -1) (("" (EXPAND "sq") (("" (CASE "sr!1`x=0") (("1" (ASSERT) NIL NIL) ("2" (CASE "sr!1`y=0") (("1" (PROPAX) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cl_solution_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ic_solution_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|in_circle_root_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|oc_solution_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL)) $$$rr3d_algo.pvs rr3d_algo: THEORY BEGIN IMPORTING common_defs, gs_only_algo, vert_only_algo, hd_only_algo s : VAR Vect3 % Relative position vo : VAR Vect3 % Ownship absolute velocity vi : VAR Vect3 % Intruder absolute velocity tr : VAR posreal % Recovery time % % % ---------------------------------------------------------------- % The RR3D Algorithm % ---------------------------------------------------------------- % % rr3d_algo(s, vo, vi, tr) : set[solution] = union( vert_only_algo(s, vo, vi, tr), gs_only_algo(s, vo, vi, tr)) END rr3d_algo $$$extra_hd.pvs extra_hd: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape maneuver sr : VAR Vect3 % Relative position at the end of the escape maneuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign thpp: VAR real thpp_tr_lem: LEMMA v`z /= 0 AND thpp = theta(1,s`z,v`z) AND 0 < thpp AND thpp < tr AND sr = s + tr*v IMPLIES (H < sr`z) OR (sr`z < -H) llhd_escape_A: THEOREM % THIS C ASE WILL NOT BE USED IN ALGORITHM ve = voe - vi AND voe`x = vi`x AND % COMPUTED VALUE voe`y = vi`y AND % COMPUTED VALUE hor_speed_gt_0?(ve) % TEST AFTER COMPUTATION IMPLIES separation?(s,ve) llhd_recovery_A: THEOREM hor_speed_gt_0?(vr) AND % TEST CONDITION AFTER COMPUTATION te * ve`y = tr * v`y AND % TEST CONDITION ve`x /= 0 AND % TEST CONDITION te = tr*v`x/ve`x AND % COMPUTED VALUE vr`x = 0 AND % COMPUTED VALUE vr`y = 0 AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) END extra_hd $$$extra_hd.prf (|extra_hd| (|thpp_tr_lem| "" (SKOSIMP*) (("" (EXPAND "theta") (("" (CROSS-MULT -1) (("" (REPLACE -4) (("" (HIDE -4) (("" (CASE "v!1`z > 0") (("1" (EXPAND "sign") (("1" (ASSERT) (("1" (MULT-BY -4 "v!1`z") (("1" (GROUND) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "sign") (("2" (ASSERT) (("2" (MULT-BY -3 "-v!1`z") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_escape_A| "" (SKOSIMP*) (("" (LEMMA "separation_lem") (("" (INST -1 "s!1" "tau(s!1,ve!1)" "ve!1") (("" (ASSERT) (("" (HIDE 2) (("" (LEMMA "line_case_correctness") (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (LEMMA "tau_is_tangent_pt") (("" (INST?) (("" (EXPAND "at") (("" (HIDE 2) (("" (EXPAND "tan_condition?") (("" (CASE-REPLACE "ve!1`x = 0") (("1" (REWRITE "sq_0") (("1" (ASSERT) (("1" (REPLACE -2) (("1" (HIDE-ALL-BUT (-4 1)) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 -5 1)) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_recovery_A| "" (SKOSIMP*) (("" (NAME "SR" "s!1 + tr!1*v!1") (("" (CASE-REPLACE "s!1 + te!1*ve!1 = SR - (tr!1-te!1)*vr!1") (("1" (HIDE -1) (("1" (LEMMA "separation_lem") (("1" (INST -1 "SR - (tr!1 - te!1) * vr!1" "tr!1-te!1+tau(SR,vr!1)" "vr!1") (("1" (ASSERT) (("1" (HIDE 3) (("1" (CASE-REPLACE "SR - (tr!1 - te!1) * vr!1 + (tau(SR, vr!1) - te!1 + tr!1) * vr!1 = SR + tau(SR, vr!1) * vr!1") (("1" (HIDE -1) (("1" (LEMMA "line_case_correctness") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (LEMMA "tau_is_tangent_pt") (("1" (INST -1 "SR" "vr!1") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (HIDE 2) (("1" (EXPAND "tan_condition?") (("1" (REPLACE -5) (("1" (REPLACE -6) (("1" (EXPAND "sq") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$out_circle_hd_comb.pvs out_circle_hd_comb: THEORY BEGIN IMPORTING criteria, common_defs, out_circle_hd vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship escape velocity vor : VAR Vect3 % Ownship recovery velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thp,SSx,SSy: VAR real ochd: THEOREM v = vo - vi AND ve = voe - vi AND vr = vor - vi AND sr = s + tr*v AND v`z /= 0 AND % TEST CONDITION thp = theta(-1,s`z,v`z) AND % CALCULATION SSx = s`x - thp * vi`x AND % CALCULATION SSy = s`y - thp * vi`y AND % CALCULATION A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND % CALCULATION B = 4*(s`x - thp*vi`x)*thp*E AND % CALCULATION C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND % CALCULATION exit?(s + thp * ve, ve) AND % TEST A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND % TEST AFTER COMPUTATION sq(vo`x) + sq(vo`y) >= sq(voe`x) AND % TEST AFTER COMPUTATION ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND % COMPUTED VALUE voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND % COMPUTED VALUE voe`z = vo`z AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = % TEST AFTER COMPUTATION sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND te = thp AND % COMPUTED VALUE % 0 < thp AND % TEST AFTER COMPUTATION thp < tr AND % TEST AFTER COMPUTATION exit?(s + thp * ve, vr) AND % TEST AFTER COMPUTATION % (sr`z - (tr - te) * vr`z) * vr`z <= 0 AND % TEST AFTER COMPUTATION vor`x = (te*voe`x - tr*vo`x)/(thp - tr) AND % COMPUTED VALUE vor`y = (te*voe`y - tr*vo`y)/(thp - tr) AND % COMPUTED VALUE vr`z = v`z IMPLIES separation?(s,ve) AND separation?(s+te*ve,vr) AND heading_only?(vo,voe) AND s + tr * v = s + te*ve + (tr-te)*vr END out_circle_hd_comb $$$out_circle_hd_comb.prf (|out_circle_hd_comb| (|ochd_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ochd_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ochd| "" (SKOSIMP*) (("" (SPLIT +) (("1" (LEMMA "circle_escape") (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "ochd_recovery") (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (ASSERT) (("2" (ASSERT) (("2" (INST -1 "voe!1") (("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LEMMA "cir_hd_only") (("3" (INST?) (("3" (INST -1 "ve!1" "voe!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "basic_timeliness") (("4" (INST?) (("4" (LEMMA "vor_timeliness") (("4" (INST?) (("4" (INST?) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$in_circle_hd_comb.pvs in_circle_hd_comb: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship escape velocity vor : VAR Vect3 % Ownship recovery velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thpp,SSx,SSy: VAR real ichd: THEOREM v = vo - vi AND ve = voe - vi AND vr = vor - vi AND % sr = s + tr*v AND v`z /= 0 AND % TEST CONDITION thpp = theta(1,s`z,v`z) AND % CALCULATION SSx = s`x - thpp * vi`x AND % CALCULATION SSy = s`y - thpp * vi`y AND % CALCULATION A = 4*sq(thpp)*(sq(SSx) + sq(SSy)) AND % CALCULATION B = 4*(s`x - thpp*vi`x)*thpp*E AND % CALCULATION C = sq(E) - 4*sq(s`y - thpp*vi`y)*sq(thpp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thpp*vi`x) + sq(s`y - thpp*vi`y) + sq(thpp)*sq(vo`x) + sq(thpp)*sq(vo`y) - sq(D) AND entry?(s + thpp * ve, ve) AND % TEST A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND % TEST AFTER COMPUTATION sq(vo`x) + sq(vo`y) >= sq(voe`x) AND % TEST AFTER COMPUTATION ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND % COMPUTED VALUE voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND % COMPUTED VALUE voe`z = vo`z AND % COMPUTED VALUE % ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thpp*vi`y) * thpp * voe`y) = % TEST AFTER COMPUTATION sign(E + 2 * (s`x - thpp*vi`x) * thpp * voe`x) AND te = thpp AND % COMPUTED VALUE % 0 < thpp AND % TEST AFTER COMPUTATION thpp < tr AND % TEST AFTER COMPUTATION vor`x = (te*voe`x - tr*vo`x)/(thpp - tr) AND % COMPUTED VALUE vor`y = (te*voe`y - tr*vo`y)/(thpp - tr) AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s,ve) AND heading_only?(vo,voe) AND separation_pos?(s+te*ve,vr) AND s + tr * v = s + te*ve + (tr-te)*vr END in_circle_hd_comb $$$in_circle_hd_comb.prf (|in_circle_hd_comb| (|ichd_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ichd_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ichd| "" (SKOSIMP*) (("" (SPLIT +) (("1" (LEMMA "circle_escape") (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "cir_hd_only") (("2" (INST?) (("2" (INST -1 "ve!1" "voe!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (LEMMA "in_circle_recovery") (("3" (INST?) (("3" (INST?) (("3" (ASSERT) (("3" (REPLACE -2) (("3" (REPLACE -3) (("3" (REPLACE -1) (("3" (EXPAND "-") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "vor_timeliness") (("4" (INST?) (("4" (INST?) (("4" (INST -1 "vi!1" "vor!1") (("4" (ASSERT) (("4" (REPLACE -2) (("4" (REPLACE -1) (("4" (EXPAND "-") (("4" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$circle_circle_hd_comb.pvs circle_circle_hd_comb: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thp,tpp,SSx,SSy, Ax, Ay, B_x, B_y: VAR real %% ESCAPE same as circle_line escape case. %% CHECK INTO extra tests abs(s`z) > H or abs(sr`z) > H cchd: THEOREM v = vo - vi AND ve = voe - vi AND sr = s + tr*v AND v`z /= 0 AND % TEST CONDITION thp = theta(-1,s`z,v`z) AND % CALCULATION SSx = s`x - thp * vi`x AND % CALCULATION SSy = s`y - thp * vi`y AND % CALCULATION A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND % CALCULATION B = 4*(s`x - thp*vi`x)*thp*E AND % CALCULATION C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND exit?(s + thp * ve, ve) AND % TEST AFTER COMPUTATION A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND % TEST AFTER COMPUTATION sq(vo`x) + sq(vo`y) >= sq(voe`x) AND % TEST AFTER COMPUTATION ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND % COMPUTED VALUE voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND % COMPUTED VALUE voe`z = vo`z AND % COMPUTED VALUE % ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = % TEST AFTER COMPUTATION sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND hor_speed_gt_0?(ve) AND % TEST AFTER COMPUTATION v`z /= 0 AND % For theta TCC tpp = theta(1,s`z,v`z) AND % tau(s,ve) < tpp AND % TEST CONDITION % tpp < tr AND % TEST CONDITION Ax = sr`x + (tpp - tr)*ve`x AND % CALCULATION Ay = sr`y + (tpp - tr)*ve`y AND % CALCULATION B_x = (s`x+tpp*v`x) AND % CALCULATION B_y = (s`y+tpp*v`y) AND % CALCULATION sq(Ax) + sq(Ay) - sq(D) /= 0 AND % TEST CONDITION discr(sq(Ax) + sq(Ay) - sq(D), % TEST CONDITION 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, sq(tr) * (sq(B_x) + sq(B_y) - sq(D))) >= 0 AND ( te = x1(sq(Ax) + sq(Ay) - sq(D), % COMPUTED VALUE 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) OR te = x2(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) ) AND te /= tr AND % POST COMPUTATION TEST vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = (tr*v`y-te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z AND % COMPUTED VALUE % (sr`x + (tpp - tr) * vr`x) * vr`x + % POST COMPUTATION TEST % (sr`y + (tpp - tr) * vr`y) * vr`y <= 0 entry?(sr+(tpp-tr)*vr,vr) IMPLIES separation?(s,ve) AND heading_only?(vo,voe) AND separation?(s+te*ve,vr) AND s + tr * v = s + te*ve + (tr-te)*vr END circle_circle_hd_comb $$$circle_circle_hd_comb.prf (|circle_circle_hd_comb| (|cchd_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cchd_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cchd_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cchd| "" (SKOSIMP*) (("" (SPLIT +) (("1" (LEMMA "circle_escape") (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "cir_hd_only") (("2" (INST?) (("2" (INST -1 "ve!1" "voe!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (LEMMA "circle_recovery") (("3" (INST?) (("3" (INST?) (("3" (INST?) (("3" (INST?) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "basic_timeliness") (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$circle_line_hd_comb.pvs circle_line_hd_comb: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thp,SSx,SSy,alpha2: VAR real clhd: THEOREM v = vo - vi AND ve = voe - vi AND sr = s + tr*v AND v`z /= 0 AND % TEST CONDITION thp = theta(-1,s`z,v`z) AND % CALCULATION SSx = s`x - thp * vi`x AND % CALCULATION SSy = s`y - thp * vi`y AND % CALCULATION A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND % CALCULATION B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND exit?(s + thp * ve, ve) AND % TEST A /= 0 AND % TEST discr(A,B,C) >= 0 AND % TEST sq(vo`x) + sq(vo`y) >= sq(voe`x) AND % TEST ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND % COMPUTED VALUE voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND % COMPUTED VALUE voe`z = vo`z AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND hor_speed_gt_0?(vr) AND % TEST AFTER COMPUTATION tr /= te AND % TEST AFTER COMPUTATION sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND % TEST CONDITION sr`y /= 0 AND % TEST CONDITION alpha2 = alpha_calc(eps,sr) AND % COMPUTED VALUE ve`y-alpha2*ve`x /= 0 AND % TEST AFTER COMPUTATION te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) AND % COMPUTED VALUE vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = alpha2*vr`x AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s,ve) AND separation?(s+te*ve,vr) AND heading_only?(vo,voe) AND s + tr * v = s + te*ve + (tr-te)*vr END circle_line_hd_comb $$$circle_line_hd_comb.prf (|circle_line_hd_comb| (|clhd_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|clhd_TCC2| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|clhd_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|clhd| "" (SKOSIMP*) (("" (SPLIT +) (("1" (LEMMA "circle_escape") (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "line_recovery") (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LEMMA "cir_hd_only") (("3" (INST?) (("3" (INST -1 "ve!1" "voe!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "alpha_timeliness") (("4" (INST?) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$line_circle_hd_comb.pvs line_circle_hd_comb: THEORY BEGIN %---------------------------------------------------------------------------- % NOTE: escape lemmas same as line_line_hd %---------------------------------------------------------------------------- IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign alpha, tpp, Ax, Ay, B_x, B_y: VAR real lchd: THEOREM ve = voe - vi AND v = vo - vi AND sr = s + tr*v AND sq(s`x) + sq(s`y) > sq(D) AND % TEST CONDITION sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION hor_speed_gt_0?(ve) AND % TEST AFTER COMPUTATION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND alpha = alpha_calc(eps,s) AND % COMPUTED VALUE (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x AND % COMPUTED VALUE ve`z = v`z AND v`z /= 0 AND % For theta TCC tpp = theta(1,s`z,v`z) AND % tau(s,ve) < tpp AND % TEST CONDITION % tpp < tr AND % TEST CONDITION Ax = sr`x + (tpp - tr)*ve`x AND % CALCULATION Ay = sr`y + (tpp - tr)*ve`y AND % CALCULATION B_x = (s`x+tpp*v`x) AND % CALCULATION B_y = (s`y+tpp*v`y) AND % CALCULATION sq(Ax) + sq(Ay) - sq(D) /= 0 AND % TEST CONDITION discr(sq(Ax) + sq(Ay) - sq(D), % TEST CONDITION 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, sq(tr) * (sq(B_x) + sq(B_y) - sq(D))) >= 0 AND ( te = x1(sq(Ax) + sq(Ay) - sq(D), % COMPUTED VALUE 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) OR te = x2(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) ) AND te /= tr AND % POST COMPUTATION TEST vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = (tr*v`y-te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z AND % COMPUTED VALUE % (sr`x + (tpp - tr) * vr`x) * vr`x + % POST COMPUTATION TEST % (sr`y + (tpp - tr) * vr`y) * vr`y <= 0 entry?(sr+(tpp-tr)*vr,vr) IMPLIES separation?(s,ve) AND separation?(s+te*ve,vr) AND heading_only?(vo,voe) AND s + tr * v = s + te*ve + (tr-te)*vr %%%% THE FOLLOWING IS FOR EXPERIMENTAL PURPOSES %%%% lchd_let: THEOREM LET ve = voe - vi, v = vo - vi IN ( sq(s`x) + sq(s`y) > sq(D) AND % TEST CONDITION sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION v`z /= 0 AND % For theta TCC LET sr = s + tr*v, alpha = alpha_calc(eps,s), tpp = theta(1,s`z,v`z), Ax = sr`x + (tpp - tr)*ve`x, Ay = sr`y + (tpp - tr)*ve`y, B_x = (s`x+tpp*v`x), B_y = (s`y+tpp*v`y) IN hor_speed_gt_0?(ve) AND % TEST AFTER COMPUTATION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x AND % COMPUTED VALUE ve`z = v`z AND % tau(s,ve) < tpp AND % TEST CONDITION % tpp < tr AND % TEST CONDITION sq(Ax) + sq(Ay) - sq(D) /= 0 AND % TEST CONDITION discr(sq(Ax) + sq(Ay) - sq(D), % TEST CONDITION 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, sq(tr) * (sq(B_x) + sq(B_y) - sq(D))) >= 0 AND ( te = x1(sq(Ax) + sq(Ay) - sq(D), % COMPUTED VALUE 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) OR te = x2(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) ) AND te /= tr AND % POST COMPUTATION TEST vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = (tr*v`y-te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z AND % COMPUTED VALUE % (sr`x + (tpp - tr) * vr`x) * vr`x + % POST COMPUTATION TEST % (sr`y + (tpp - tr) * vr`y) * vr`y <= 0 entry?(sr+(tpp-tr)*vr,vr) ) IMPLIES separation?(s,ve) AND separation?(s+te*ve,vr) AND heading_only?(vo,voe) AND s + tr * v = s + te*ve + (tr-te)*vr END line_circle_hd_comb $$$line_circle_hd_comb.prf (|line_circle_hd_comb| (|lchd_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_TCC4| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd| "" (SKOSIMP*) (("" (SPLIT +) (("1" (LEMMA "line_escape") (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "circle_recovery") (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LEMMA "line_esc_hd_only") (("3" (INST?) (("3" (INST?) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "basic_timeliness") (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_let_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (EXPAND "sq") (("" (MULT-CASES -2) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_let_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_let_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_let_TCC4| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_let| "" (SKOSIMP*) (("" (ASSERT) (("" (FLATTEN) (("" (LEMMA "lchd") (("" (ASSERT) (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (REPLACE -5) (("" (ASSERT) (("" (REPLACE -9) (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$line_line_hd_comb.pvs line_line_hd_comb: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape maneuver sr : VAR Vect3 % Relative position at the end of the escape maneuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign %% SOLUTIONS THAT RESULT IN ve`x = 0 %% ESCAPE SOLUTIONS THAT RESULT IN ve'x /= 0 alpha, alpha2: VAR real llhd: THEOREM ve = voe - vi AND v = vo - vi AND sr = s + tr*v AND sq(s`x) + sq(s`y) > sq(D) AND % TEST CONDITION sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION hor_speed_gt_0?(ve) AND % TEST AFTER COMPUTATION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND alpha = alpha_calc(eps,s) AND % COMPUTED VALUE (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x AND % COMPUTED VALUE hor_speed_gt_0?(vr) AND % TEST AFTER COMPUTATION tr /= te AND % TEST AFTER COMPUTATION sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND % TEST CONDITION sr`y /= 0 AND % TEST CONDITION alpha2 = alpha_calc(eps,sr) AND % COMPUTED VALUE ve`y-alpha2*ve`x /= 0 AND % TEST AFTER COMPUTATION te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) AND % COMPUTED VALUE vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = alpha2*vr`x AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s,ve) AND separation?(s+te*ve,vr) AND heading_only?(vo,voe) AND s + tr * v = s + te*ve + (tr-te)*vr END line_line_hd_comb $$$line_line_hd_comb.prf (|line_line_hd_comb| (|llhd_TCC1| "" (SKOSIMP*) (("" (GROUND) (("" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|llhd_TCC3| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("1" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_TCC4| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|llhd| "" (SKOSIMP*) (("" (SPLIT +) (("1" (LEMMA "line_escape") (("1" (INST?) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "line_recovery") (("2" (INST?) (("2" (INST?) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (LEMMA "line_esc_hd_only") (("3" (INST?) (("3" (INST?) (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("4" (LEMMA "alpha_timeliness") (("4" (INST?) (("4" (INST?) (("4" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$out_circle_hd.pvs out_circle_hd: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship escape velocity vor : VAR Vect3 % Ownship recovery velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thp,SSx,SSy: VAR real % NOTE: same as circle_line ochd_escape: THEOREM v`z /= 0 AND thp = theta(-1,s`z,v`z) AND SSx = s`x - thp * vi`x AND SSy = s`y - thp * vi`y AND A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND exit?(s + thp * ve, ve) AND % TEST A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi AND ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) IMPLIES separation?(s,ve) ochd_hd_only: THEOREM sq(vo`x) + sq(vo`y) >= sq(voe`x) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi IMPLIES heading_only?(vo,voe) ochd_recovery: THEOREM v`z /= 0 AND thp = theta(-1,s`z,v`z) AND SSx = s`x - thp * vi`x AND SSy = s`y - thp * vi`y AND A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y-thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y-thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND A /= 0 AND % TEST AFTER COMPUTATION sr = s + tr*v AND discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND ve = voe - vi AND ve`z = v`z AND % COMPUTED VALUE te = thp AND % 0 < thp AND % thp < tr AND exit?(s + thp * ve, vr) AND % TEST vr`z = v`z IMPLIES separation?(s+te*ve,vr) END out_circle_hd $$$out_circle_hd.prf (|out_circle_hd| (|ochd_escape_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ochd_escape| "" (SKOSIMP*) (("" (LEMMA "circle_escape") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ochd_hd_only_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ochd_hd_only| "" (SKOSIMP*) (("" (LEMMA "cir_hd_only") (("" (INST?) (("" (INST -1 "ve!1" "voe!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|ochd_recovery| "" (SKOSIMP*) (("" (LEMMA "out_circle_recovery") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$in_circle_hd.pvs in_circle_hd: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship escape velocity vor : VAR Vect3 % Ownship recovery velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thpp,SSx,SSy: VAR real % NOTE: same as circle_line escape except theta^1 rather than theta^-1 % and test is for an entry_point ichd_escape: THEOREM v`z /= 0 AND thpp = theta(1,s`z,v`z) AND SSx = s`x - thpp * vi`x AND SSy = s`y - thpp * vi`y AND A = 4*sq(thpp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thpp*vi`x)*thpp*E AND C = sq(E) - 4*sq(s`y - thpp*vi`y)*sq(thpp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thpp*vi`x) + sq(s`y - thpp*vi`y) + sq(thpp)*sq(vo`x) + sq(thpp)*sq(vo`y) - sq(D) AND entry?(s + thpp * ve, ve) AND % TEST A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi AND % ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thpp*vi`y) * thpp * voe`y) = sign(E + 2 * (s`x - thpp*vi`x) * thpp * voe`x) IMPLIES separation?(s,ve) ichd_hd_only: THEOREM sq(vo`x) + sq(vo`y) >= sq(voe`x) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi IMPLIES heading_only?(vo,voe) ichd_recovery: THEOREM v`z /= 0 AND thpp = theta(1,s`z,v`z) AND ve`z = v`z AND % COMPUTED VALUE te = thpp AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation_pos?(s+te*ve,vr) ichd_timeliness: THEOREM te = thpp AND te /= tr AND vor`x = (te*voe`x - tr*vo`x)/(thpp - tr) AND vor`y = (te*voe`y - tr*vo`y)/(thpp - tr) AND vr`z = v`z AND ve`z = v`z AND v = vo - vi AND ve = voe - vi AND vr = vor - vi IMPLIES s + tr * v = s + te*ve + (tr-te)*vr END in_circle_hd $$$in_circle_hd.prf (|in_circle_hd| (|ichd_escape_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|ichd_escape| "" (SKOSIMP*) (("" (LEMMA "circle_escape") (("" (INST?) (("" (ASSERT) (("" (ASSERT) (("" (INST -1 "1" "voe!1") (("" (ASSERT) (("" (HIDE-ALL-BUT (-11 1)) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|ichd_hd_only_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|ichd_hd_only| "" (SKOSIMP*) (("" (LEMMA "cir_hd_only") (("" (INST?) (("" (INST -1 "ve!1" "voe!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|ichd_recovery| "" (SKOSIMP*) (("" (LEMMA "in_circle_recovery") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|ichd_timeliness_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|ichd_timeliness| "" (SKOSIMP*) (("" (LEMMA "vor_timeliness") (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$circle_circle_hd.pvs circle_circle_hd: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thp,tpp,SSx,SSy, Ax, Ay, B_x, B_y: VAR real %% ESCAPE same as circle_line escape case. %% CHECK INTO extra tests abs(s`z) > H or abs(sr`z) > H cchd_escape: THEOREM v`z /= 0 AND thp = theta(-1,s`z,v`z) AND SSx = s`x - thp * vi`x AND SSy = s`y - thp * vi`y AND A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND exit?(s + thp * ve, ve) AND % TEST A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi AND % ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) IMPLIES separation?(s,ve) cchd_hd_only: THEOREM sq(vo`x) + sq(vo`y) >= sq(voe`x) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi IMPLIES heading_only?(vo,voe) %% Recovery case same as line_circle except extra tests: %% 0 < theta(-1,s`z,v`z) theta(1,s`z,v`z) < tr cchd_recovery: THEOREM hor_speed_gt_0?(ve) AND ve = voe - vi AND sr = s + tr*v AND v`z /= 0 AND % For theta TCC tpp = theta(1,s`z,v`z) AND % tau(s,ve) < tpp AND % TEST CONDITION % tpp < tr AND % TEST CONDITION Ax = sr`x + (tpp - tr)*ve`x AND % CALCULATION Ay = sr`y + (tpp - tr)*ve`y AND % CALCULATION B_x = (s`x+tpp*v`x) AND % CALCULATION B_y = (s`y+tpp*v`y) AND % CALCULATION sq(Ax) + sq(Ay) - sq(D) /= 0 AND % TEST CONDITION discr(sq(Ax) + sq(Ay) - sq(D), % TEST CONDITION 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, sq(tr) * (sq(B_x) + sq(B_y) - sq(D))) >= 0 AND ( te = x1(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) OR te = x2(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) ) AND te /= tr AND % POST COMPUTATION TEST vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = (tr*v`y-te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z AND % COMPUTED VALUE % (sr`x + (tpp - tr) * vr`x) * vr`x + % POST COMPUTATION TES%% (sr`y + (tpp - tr) * vr`y) * vr`y <= 0 entry?(sr+(tpp-tr)*vr,vr) IMPLIES separation?(s+te*ve,vr) cchd_timeliness: THEOREM te /= tr AND vr`x = (tr*v`x-te*ve`x)/(tr-te) AND vr`y = (tr*v`y-te*ve`y)/(tr-te) AND ve`z = v`z AND vr`z = v`z IMPLIES s + tr * v = s + te*ve + (tr-te)*vr END circle_circle_hd $$$circle_circle_hd.prf (|circle_circle_hd| (|cchd_escape_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cchd_escape| "" (SKOSIMP*) (("" (LEMMA "circle_escape") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cchd_hd_only_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|cchd_hd_only| "" (SKOSIMP*) (("" (LEMMA "cir_hd_only") (("" (INST?) (("" (INST -1 "ve!1" "voe!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cchd_recovery_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cchd_recovery_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cchd_recovery| "" (SKOSIMP*) (("" (LEMMA "circle_recovery") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cchd_timeliness_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|cchd_timeliness| "" (SKOSIMP*) (("" (LEMMA "timeliness") (("" (INST?) (("" (ASSERT) (("" (CROSS-MULT -1) (("" (CROSS-MULT -2) (("" (PROP) (("1" (CROSS-MULT 1) (("1" (ASSERT) NIL NIL)) NIL) ("2" (CROSS-MULT 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$circle_line_hd.pvs circle_line_hd: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign A,B,C,E,thp,SSx,SSy: VAR real clhd_escape: THEOREM v`z /= 0 AND thp = theta(-1,s`z,v`z) AND SSx = s`x - thp * vi`x AND SSy = s`y - thp * vi`y AND A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND exit?(s + thp * ve, ve) AND % TEST A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi AND ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) IMPLIES separation?(s,ve) clhd_hd_only: THEOREM sq(vo`x) + sq(vo`y) >= sq(voe`x) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi IMPLIES heading_only?(vo,voe) %% RECOVERY CASE SAME AS line_line_hd recovery case alpha2: VAR real clhd_recovery_0: THEOREM %% CASE vr`x = 0 AND sq(D) = sq(sr`x) hor_speed_gt_0?(vr) AND % TEST CONDITION AFTER COMPUTATION sr = s + tr*v AND sq(D) = sq(sr`x) AND % TEST CONDITION ve`x /= 0 AND % TEST CONDITION tr /= te AND % TEST CONDITION te = tr*v`x/ve`x AND % COMPUTED VALUE vr`x = 0 AND % COMPUTED VALUE vr`y = (tr*v`y - te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) clhd_recovery: THEOREM sr = s + tr*v AND hor_speed_gt_0?(vr) AND % TEST AFTER COMPUTATION tr /= te AND % TEST AFTER COMPUTATION sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND % TEST CONDITION sr`y /= 0 AND % TEST CONDITION alpha2 = alpha_calc(eps,sr) AND % COMPUTED VALUE ve`y-alpha2*ve`x /= 0 AND % TEST AFTER COMPUTATION te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) AND % COMPUTED VALUE vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = alpha2*vr`x AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) clhd_timeliness: THEOREM te /= tr AND vr`x = (tr*v`x-te*ve`x)/(tr-te) AND vr`y = alpha2*vr`x AND ve`y-alpha2*ve`x /= 0 AND te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) AND vr`z = v`z AND ve`z = v`z IMPLIES s + tr * v = s + te*ve + (tr-te)*vr END circle_line_hd $$$circle_line_hd.prf (|circle_line_hd| (|clhd_escape_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|clhd_escape| "" (SKOSIMP*) (("" (LEMMA "circle_escape") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (ASSERT) (("" (REPLACE -11) (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|clhd_hd_only_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|clhd_hd_only| "" (SKOSIMP*) (("" (LEMMA "cir_hd_only") (("" (INST?) (("" (INST -1 "ve!1" "voe!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|clhd_recovery_0_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|clhd_recovery_0| "" (SKOSIMP*) (("" (LEMMA "line_recovery_0") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|clhd_recovery_TCC1| "" (SKOSIMP*) (("" (GROUND) (("" (MULT-CASES -2) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|clhd_recovery_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|clhd_recovery| "" (SKOSIMP*) (("" (LEMMA "line_recovery ") (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|clhd_timeliness_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|clhd_timeliness| "" (SKOSIMP*) (("" (LEMMA "alpha_timeliness") (("" (INST?) (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$line_circle_hd.pvs line_circle_hd: THEORY BEGIN %---------------------------------------------------------------------------- % NOTE: escape lemmas same as line_line_hd %---------------------------------------------------------------------------- IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign alpha, tpp, Ax, Ay, B_x, B_y: VAR real lchd_escape_0: THEOREM %% IF sq(vo`x) + sq(vo`y) >= sq(vi`x) ve = voe - vi AND sq(vo`x) + sq(vo`y) >= sq(vi`x) AND % TEST CONDITION sq(D) = sq(s`x) AND % TEST CONDITION voe`x = vi`x AND % COMPUTED VALUE voe`y = eps*sqrt(sq(vo`x)+sq(vo`y)-sq(vi`x)) AND % COMPUTED VALUE hor_speed_gt_0?(ve) % TEST AFTER COMPUTATION IMPLIES separation?(s,ve) lchd_escape: THEOREM sq(s`x) + sq(s`y) > sq(D) AND % TEST CONDITION sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION hor_speed_gt_0?(ve) AND % TEST AFTER COMPUTATION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND alpha = alpha_calc(eps,s) AND % COMPUTED VALUE (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x % COMPUTED VALUE IMPLIES separation?(s,ve) lchd_esc_hd_only: THEOREM sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x AND % COMPUTED VALUE ve = voe - vi AND v = vo - vi AND ve`z = v`z IMPLIES heading_only?(vo,voe) lchd_recovery: THEOREM hor_speed_gt_0?(ve) AND ve = voe - vi AND sr = s + tr*v AND v`z /= 0 AND % For theta TCC tpp = theta(1,s`z,v`z) AND % tau(s,ve) < tpp AND % TEST CONDITION % tpp < tr AND % TEST CONDITION Ax = sr`x + (tpp - tr)*ve`x AND % CALCULATION Ay = sr`y + (tpp - tr)*ve`y AND % CALCULATION B_x = (s`x+tpp*v`x) AND % CALCULATION B_y = (s`y+tpp*v`y) AND % CALCULATION sq(Ax) + sq(Ay) - sq(D) /= 0 AND % TEST CONDITION discr(sq(Ax) + sq(Ay) - sq(D), % TEST CONDITION 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, sq(tr) * (sq(B_x) + sq(B_y) - sq(D))) >= 0 AND ( te = x1(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) OR te = x2(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) ) AND te /= tr AND % POST COMPUTATION TEST vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = (tr*v`y-te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z AND % COMPUTED VALUE % (sr`x + (tpp - tr) * vr`x) * vr`x + % POST COMPUTATION TEST % (sr`y + (tpp - tr) * vr`y) * vr`y <= 0 entry?(sr+(tpp-tr)*vr,vr) % POST COMPUTATION TEST IMPLIES separation?(s+te*ve,vr) lchd_timeliness: THEOREM te /= tr AND vr`x = (tr*v`x-te*ve`x)/(tr-te) AND vr`y = (tr*v`y-te*ve`y)/(tr-te) AND ve`z = v`z AND vr`z = v`z IMPLIES s + tr * v = s + te*ve + (tr-te)*vr END line_circle_hd $$$line_circle_hd.prf (|line_circle_hd| (|lchd_escape_0_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|lchd_escape_0| "" (SKOSIMP*) (("" (LEMMA "line_escape_0") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_escape_TCC1| "" (SKOSIMP*) (("" (ASSERT) (("" (GROUND) (("" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_escape_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_escape| "" (SKOSIMP*) (("" (LEMMA "line_escape") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_esc_hd_only_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_esc_hd_only| "" (SKOSIMP*) (("" (LEMMA "line_esc_hd_only") (("" (INST?) (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_recovery_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_recovery_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_recovery| "" (SKOSIMP*) (("" (ASSERT) (("" (LEMMA "circle_recovery") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|lchd_timeliness_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|lchd_timeliness| "" (SKOSIMP*) (("" (LEMMA "timeliness") (("" (INST?) (("" (ASSERT) (("" (CROSS-MULT -1) (("" (CROSS-MULT -2) (("" (PROP) (("1" (CROSS-MULT 1) (("1" (ASSERT) NIL NIL)) NIL) ("2" (CROSS-MULT 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$timeliness.pvs timeliness: THEORY BEGIN IMPORTING criteria, common_defs vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship escape velocity vor : VAR Vect3 % Ownship recovery velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape maneuver sr : VAR Vect3 % Relative position at the end of the escape maneuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time alpha: VAR real alpha_timeliness: THEOREM te /= tr AND vr`x = (tr*v`x-te*ve`x)/(tr-te) AND vr`y = alpha*vr`x AND ve`y-alpha*ve`x /= 0 AND te = tr*(v`y-alpha*v`x)/(ve`y-alpha*ve`x) AND vr`z = v`z AND ve`z = v`z IMPLIES s + tr * v = s + te*ve + (tr-te)*vr basic_timeliness: THEOREM te /= tr AND vr`x = (tr*v`x-te*ve`x)/(tr-te) AND vr`y = (tr*v`y-te*ve`y)/(tr-te) AND ve`z = v`z AND vr`z = v`z IMPLIES s + tr * v = s + te*ve + (tr-te)*vr vor_timeliness: THEOREM te /= tr AND vor`x = (te*voe`x - tr*vo`x)/(te - tr) AND vor`y = (te*voe`y - tr*vo`y)/(te - tr) AND vr`z = v`z AND ve`z = v`z AND v = vo - vi AND ve = voe - vi AND vr = vor - vi IMPLIES s + tr * v = s + te*ve + (tr-te)*vr END timeliness $$$timeliness.prf (|timeliness| (|alpha_timeliness_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|alpha_timeliness| "" (SKOSIMP*) (("" (CROSS-MULT -1) (("" (CROSS-MULT -3) (("" (CASE "vr!1`y*(tr!1 - te!1) = tr!1 * v!1`y - te!1 * ve!1`y") (("1" (LEMMA "timeliness") (("1" (INST?) (("1" (ASSERT) (("1" (PROP) (("1" (CROSS-MULT 1) NIL NIL) ("2" (CROSS-MULT 1) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (MULT-BY -1 "alpha!1") (("2" (ASSERT) (("2" (ISOLATE -1 R 1) (("2" (REPLACE -1 * RL) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|basic_timeliness| "" (SKOSIMP*) (("" (LEMMA "timeliness") (("" (INST?) (("" (ASSERT) (("" (CROSS-MULT -1) (("" (CROSS-MULT -2) (("" (PROP) (("1" (CROSS-MULT 1) (("1" (ASSERT) NIL NIL)) NIL) ("2" (CROSS-MULT 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|vor_timeliness_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|vor_timeliness| "" (SKOSIMP*) (("" (LEMMA "timeliness") (("" (INST?) (("" (ASSERT) (("" (HIDE 3) (("" (ISOLATE -7 R 1) (("1" (ISOLATE -6 R 1) (("1" (ISOLATE -5 R 1) (("1" (REPLACE -5 * RL) (("1" (HIDE -5) (("1" (REPLACE -5 * RL) (("1" (HIDE -5) (("1" (REPLACE -5 * RL) (("1" (HIDE -5) (("1" (CROSS-MULT -1) (("1" (CROSS-MULT -2) (("1" (GRIND) (("1" (CROSS-MULT 1) NIL NIL) ("2" (CROSS-MULT 1) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 1)) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL) ("3" (HIDE-ALL-BUT (-1 1)) (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 1)) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL) ("3" (HIDE-ALL-BUT (-1 1)) (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 1)) (("2" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL) ("3" (HIDE-ALL-BUT (-1 1)) (("3" (APPLY-EXTENSIONALITY 1 :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$hd_only.pvs hd_only: THEORY BEGIN IMPORTING criteria, common_defs, timeliness vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship escape velocity vor : VAR Vect3 % Ownship recovery velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape maneuver sr : VAR Vect3 % Relative position at the end of the escape maneuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign alpha,alpha2,A,B,C,E,thp,thpp,SSx,SSy: VAR real ss,vv: VAR Vect3 line_escape_0: THEOREM %% IF sq(vo`x) + sq(vo`y) >= sq(vi`x) ve = voe - vi AND sq(vo`x) + sq(vo`y) >= sq(vi`x) AND % TEST CONDITION sq(D) = sq(s`x) AND % TEST CONDITION voe`x = vi`x AND % COMPUTED VALUE voe`y = eps*sqrt(sq(vo`x)+sq(vo`y)-sq(vi`x)) AND % COMPUTED VALUE hor_speed_gt_0?(ve) % TEST AFTER COMPUTATION IMPLIES separation?(s,ve) line_esc_0_hd_only: THEOREM sq(vo`x) + sq(vo`y) >= sq(vi`x) AND % TEST CONDITION voe`x = vi`x AND % COMPUTED VALUE voe`y = eps*sqrt(sq(vo`x)+sq(vo`y)-sq(vi`x))AND % COMPUTED VALUE voe`z = vo`z IMPLIES heading_only?(vo,voe) alpha_type : TYPE = {s | IF sq(D) = sq(s`x) THEN s`x*s`y /= 0 ELSE sq(s`x) + sq(s`y) - sq(D) >= 0 ENDIF} alpha_calc(eps: real, s: alpha_type): real = IF sq(D) = sq(s`x) THEN (sq(s`y) - sq(D))/(2*s`x*s`y) ELSE (-s`x*s`y+eps*D*sqrt(sq(s`x)+sq(s`y)-sq(D)))/(sq(D)-sq(s`x)) ENDIF alpha_calc_lem: LEMMA IF sq(D) = sq(ss`x) THEN ss`x * ss`y /= 0 ELSE sq(ss`x) + sq(ss`y) - sq(D) >= 0 ENDIF AND alpha = alpha_calc(eps,ss) IMPLIES sq(D)*(1+sq(alpha)) = sq(ss`x*alpha - ss`y) line_esc_lem: LEMMA IF sq(D) = sq(ss`x) THEN ss`x * ss`y /= 0 ELSE sq(ss`x) + sq(ss`y) - sq(D) >= 0 ENDIF AND alpha = alpha_calc(eps,ss) AND vv`y = alpha*vv`x AND vv`x /= 0 IMPLIES tan_condition?(ss,vv) line_escape: THEOREM sq(s`x) + sq(s`y) > sq(D) AND % TEST CONDITION sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION hor_speed_gt_0?(ve) AND % TEST AFTER COMPUTATION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND alpha = alpha_calc(eps,s) AND % COMPUTED VALUE (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x % COMPUTED VALUE IMPLIES separation?(s,ve) line_esc_hd_only: THEOREM sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x AND % COMPUTED VALUE ve = voe - vi AND v = vo - vi AND ve`z = v`z IMPLIES heading_only?(vo,voe) %% RECOVERY SOLUTION THAT RESULT IN vr`x = 0 line_recovery_0: THEOREM %% CASE vr`x = 0 AND sq(D) = sq(sr`x) hor_speed_gt_0?(vr) AND % TEST CONDITION AFTER COMPUTATION sr = s + tr*v AND sq(D) = sq(sr`x) AND % TEST CONDITION ve`x /= 0 AND % TEST CONDITION tr /= te AND % TEST CONDITION te = tr*v`x/ve`x AND % COMPUTED VALUE vr`x = 0 AND % COMPUTED VALUE vr`y = (tr*v`y - te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) %% RECOVERY SOLUTIONS THAT RESULT IN vr`x /= 0 line_recovery: THEOREM sr = s + tr*v AND hor_speed_gt_0?(vr) AND % TEST AFTER COMPUTATION tr /= te AND % TEST AFTER COMPUTATION sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND % TEST CONDITION sr`y /= 0 AND % TEST CONDITION alpha2 = alpha_calc(eps,sr) AND % COMPUTED VALUE ve`y-alpha2*ve`x /= 0 AND % TEST AFTER COMPUTATION te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) AND % COMPUTED VALUE vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = alpha2*vr`x AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) %---------------------------------------------------------------------------- cir_esc_cyl: LEMMA v`z /= 0 AND thp = theta(eps,s`z,v`z) AND SSx = s`x - thp * vi`x AND SSy = s`y - thp * vi`y AND A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND ve = voe - vi IMPLIES on_cyl?(s + thp*ve) circle_escape: THEOREM v`z /= 0 AND thp = theta(eps,s`z,v`z) AND SSx = s`x - thp * vi`x AND SSy = s`y - thp * vi`y AND A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y - thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y - thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND ( (exit?(s + thp * ve, ve) AND eps = -1) OR (entry?(s + thp * ve, ve) AND eps = 1) ) AND A /= 0 AND % TEST AFTER COMPUTATION discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi AND % ve`z = v`z AND % COMPUTED VALUE sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) IMPLIES separation?(s,ve) tpp, Ax, Ay, B_x, B_y: VAR real cir_hd_only: THEOREM sq(vo`x) + sq(vo`y) >= sq(voe`x) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND voe`z = vo`z AND v = vo - vi AND ve = voe - vi IMPLIES heading_only?(vo,voe) cir_rec_lem: LEMMA Ax = sr`x + (tpp - tr)*ve`x AND Ay = sr`y + (tpp - tr)*ve`y AND B_x = (s`x+tpp*v`x) AND B_y = (s`y+tpp*v`y) AND sq(Ax) + sq(Ay) - sq(D) /= 0 AND discr(sq(Ax) + sq(Ay) - sq(D), 2*tr * sq(D) - 2*Ax * B_x * tr - 2*(Ay*B_y*tr), sq(tr) * (sq(B_x) + sq(B_y) - sq(D))) >= 0 AND ( te = x1(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) OR te = x2(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) ) AND sr = s + tr*v AND te /= tr AND vr`x = (tr*v`x-te*ve`x)/(tr-te) AND vr`y = (tr*v`y-te*ve`y)/(tr-te) IMPLIES sq(s`x + te*ve`x + (tpp - te)*vr`x) + sq(s`y + te*ve`y + (tpp - te)*vr`y) = sq(D) circle_recovery: THEOREM hor_speed_gt_0?(ve) AND ve = voe - vi AND sr = s + tr*v AND v`z /= 0 AND % For theta TCC tpp = theta(1,s`z,v`z) AND % tau(s,ve) < tpp AND % TEST CONDITION % tpp < tr AND % TEST CONDITION Ax = sr`x + (tpp - tr)*ve`x AND % CALCULATION Ay = sr`y + (tpp - tr)*ve`y AND % CALCULATION B_x = (s`x+tpp*v`x) AND % CALCULATION B_y = (s`y+tpp*v`y) AND % CALCULATION sq(Ax) + sq(Ay) - sq(D) /= 0 AND % TEST CONDITION discr(sq(Ax) + sq(Ay) - sq(D), % TEST CONDITION 2*tr*sq(D) - 2*Ax*B_x*tr - 2*Ay*B_y*tr, sq(tr) * (sq(B_x) + sq(B_y) - sq(D))) >= 0 AND ( te = x1(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) OR te = x2(sq(Ax) + sq(Ay) - sq(D), 2*tr*(sq(D) - Ax*B_x - Ay*B_y), sq(tr)*(sq(B_x)+sq(B_y)-sq(D)) ) ) AND te /= tr AND % POST COMPUTATION TEST vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = (tr*v`y-te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z AND % COMPUTED VALUE % (sr`x + (tpp - tr) * vr`x) * vr`x + % POST COMPUTATION TEST % (sr`y + (tpp - tr) * vr`y) * vr`y <= 0 entry?(sr+(tpp-tr)*vr,vr) IMPLIES separation?(s+te*ve,vr) %---------------------------------------------------------------------------- separation_pos?(s,v): bool = (FORALL (tt: nonneg_real): hor_sep?(s+tt*v) OR vert_sep?(s+tt*v)) in_circle_recovery: THEOREM v`z /= 0 AND te = theta(1,s`z,v`z) AND ve`z = v`z AND vr`z = v`z IMPLIES separation_pos?(s+te*ve,vr) out_circle_recovery: THEOREM v`z /= 0 AND thp = theta(-1,s`z,v`z) AND SSx = s`x - thp * vi`x AND SSy = s`y - thp * vi`y AND A = 4*sq(thp)*(sq(SSx) + sq(SSy)) AND B = 4*(s`x - thp*vi`x)*thp*E AND C = sq(E) - 4*sq(s`y-thp*vi`y)*sq(thp)*(sq(vo`x)+sq(vo`y)) AND E = sq(s`x - thp*vi`x) + sq(s`y-thp*vi`y) + sq(thp)*sq(vo`x) + sq(thp)*sq(vo`y) - sq(D) AND A /= 0 AND % TEST AFTER COMPUTATION sr = s + tr*v AND discr(A,B,C) >= 0 AND sq(vo`x) + sq(vo`y) >= sq(voe`x) AND ( voe`x = x1(A,B,C) OR voe`x = x2(A,B,C) ) AND voe`y = sqrt(sq(vo`x) + sq(vo`y) - sq(voe`x)) AND sign(-2 * (s`y - thp*vi`y) * thp * voe`y) = sign(E + 2 * (s`x - thp*vi`x) * thp * voe`x) AND ve = voe - vi AND ve`z = v`z AND % COMPUTED VALUE te = thp AND % 0 < thp AND % thp < tr AND exit?(s + thp * ve, vr) AND % TEST vr`z = v`z IMPLIES separation?(s+te*ve,vr) END hd_only $$$hd_only.prf (|hd_only| (|line_escape_0_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|line_escape_0| "" (SKOSIMP*) (("" (LEMMA "separation_lem") (("" (INST -1 "s!1" "tau(s!1,ve!1)" "ve!1") (("" (ASSERT) (("" (HIDE 2) (("" (LEMMA "line_case_correctness") (("" (INST?) (("" (ASSERT) (("" (HIDE 2) (("" (LEMMA "tau_is_tangent_pt") (("" (INST?) (("" (EXPAND "at") (("" (HIDE 2) (("" (EXPAND "tan_condition?") (("" (CASE-REPLACE "ve!1`x = 0") (("1" (REWRITE "sq_0") (("1" (ASSERT) (("1" (REPLACE -4) (("1" (HIDE-ALL-BUT 1) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 -4 1)) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_esc_0_hd_only_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|line_esc_0_hd_only| "" (SKOSIMP*) (("" (EXPAND "heading_only?") (("" (ASSERT) (("" (HIDE -4) (("" (REPLACE -2) (("" (HIDE -2) (("" (TYPEPRED "eps!1") (("" (PROP) (("1" (REPLACE -1) (("1" (REPLACE -3) (("1" (ASSERT) (("1" (REWRITE "sq_times") (("1" (REWRITE "sq_sqrt") (("1" (ASSERT) (("1" (HIDE -2 -3) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REPLACE -2) (("2" (REWRITE "sq_times") (("2" (REWRITE "sq_sqrt") (("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|alpha_calc_TCC1| "" (TCC) NIL NIL) (|alpha_calc_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|alpha_calc_TCC3| "" (SUBTYPE-TCC) NIL NIL) (|alpha_calc_lem_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|alpha_calc_lem| "" (SKOSIMP*) (("" (EXPAND "alpha_calc") (("" (LIFT-IF) (("" (PROP) (("1" (CROSS-MULT -2) (("1" (GRIND) NIL))) ("2" (HIDE -3 -4 2) (("2" (CASE "(sq(D) - sq(ss!1`x))*sq(alpha!1) + 2*ss!1`x*ss!1`y * alpha!1 + (sq(D) - sq(ss!1`y)) = 0") (("1" (HIDE -2 -3) (("1" (GRIND) NIL))) ("2" (LEMMA "quadratic_eq_0") (("2" (INST?) (("1" (ASSERT) (("1" (ASSERT) (("1" (HIDE 2) (("1" (PROP) (("1" (HIDE -1) (("1" (EXPAND "discr") (("1" (EXPAND "sq") (("1" (MULT-BY -1 "4*D*D") (("1" (ASSERT) NIL))))))))) ("2" (TYPEPRED "eps!1") (("2" (EXPAND "x1") (("2" (EXPAND "x2") (("2" (CASE-REPLACE "discr((sq(D) - sq(ss!1`x)), 2 * (ss!1`x * ss!1`y), (sq(D) - sq(ss!1`y))) = 4*sq(D)*(sq(ss!1`x) + sq(ss!1`y) - sq(D))") (("1" (HIDE -1) (("1" (REWRITE "sqrt_times") (("1" (CASE-REPLACE "sqrt(4*sq(D)) = 2*D") (("1" (ASSERT) (("1" (FIELD -3) (("1" (PROP) (("1" (HIDE 3) (("1" (FIELD 2) NIL))) ("2" (HIDE 2) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (HIDE -3 4) (("2" (CROSS-MULT 2) (("2" (MULT-BY -1 "2") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (HIDE-ALL-BUT 1) (("2" (REWRITE "sqrt_times") (("2" (REWRITE "sqrt_sq") (("2" (CASE-REPLACE "4 = sq(2)") (("1" (REWRITE "sqrt_sq") NIL) ("2" (EXPAND "sq") (("2" (PROPAX) NIL))))))))))))))))) ("2" (HIDE -2 2 3) (("2" (EXPAND "discr") (("2" (ASSERT) (("2" (EXPAND "sq") (("2" (PROPAX) NIL))))))))))))))))))))))))) ("2" (ASSERT) NIL))))))))))))))))) (|line_esc_lem| "" (SKOSIMP*) (("" (LEMMA "alpha_calc_lem") (("" (INST?) (("" (EXPAND "tan_condition?") (("" (ASSERT) (("" (SPLIT -1) (("1" (HIDE -2 -3) (("1" (DIV-BY -2 "vv!1`x") (("1" (REPLACE -2 * RL) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) NIL NIL) ("3" (FLATTEN) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_escape_TCC1| "" (SKOSIMP*) (("" (HIDE -2 -3 1) (("" (PROP) (("1" (GRIND) (("1" (MULT-CASES -2) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|line_escape_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|line_escape| "" (SKOSIMP*) (("" (LEMMA "quadratic_eq_0") (("" (INST?) (("" (ASSERT) (("" (FLATTEN) (("" (HIDE -1) (("" (SPLIT -1) (("1" (CASE-REPLACE "ve!1`x = 0") (("1" (REWRITE "sq_0") (("1" (ASSERT) NIL NIL)) NIL) ("2" (LEMMA "separation_lem") (("2" (INST -1 "s!1" "tau(s!1,ve!1)" "ve!1") (("2" (ASSERT) (("2" (HIDE 4) (("2" (LEMMA "line_case_correctness") (("2" (INST?) (("2" (ASSERT) (("2" (HIDE 2) (("2" (LEMMA "tau_is_tangent_pt") (("2" (INST?) (("2" (EXPAND "at") (("2" (HIDE 2) (("2" (LEMMA "line_esc_lem") (("2" (INST?) (("2" (INST -1 "ve!1") (("2" (ASSERT) (("2" (HIDE-ALL-BUT (-2 1)) (("2" (PROP) (("2" (GRIND) (("2" (MULT-CASES -2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_esc_hd_only_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|line_esc_hd_only| "" (SKOSIMP*) (("" (EXPAND "heading_only?") (("" (LEMMA "quadratic_eq_0") (("" (INST?) (("" (REPLACE -3) (("" (ASSERT) (("" (HIDE -2 -3) (("" (CASE "sq(ve!1`x + vi!1`x) + sq(alpha!1*ve!1`x + vi!1`y) = sq(vo!1`x) + sq(vo!1`y)") (("1" (HIDE -2) (("1" (REPLACE -2 * RL) (("1" (REPLACE -3) (("1" (ASSERT) (("1" (HIDE -2 -3) (("1" (PROP) (("1" (EXPAND "sq") (("1" (GRIND) NIL NIL)) NIL) ("2" (HIDE -1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (REPLACE -2 * RL) (("2" (HIDE -2 -3 -4 -5) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_recovery_0_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|line_recovery_0| "" (SKOSIMP*) (("" (CASE-REPLACE "s!1 + te!1*ve!1 = sr!1 - (tr!1-te!1)*vr!1") (("1" (HIDE -1) (("1" (LEMMA "separation_lem") (("1" (INST -1 "sr!1 - (tr!1 - te!1) * vr!1" "tr!1-te!1+tau(sr!1,vr!1)" "vr!1") (("1" (ASSERT) (("1" (HIDE 4) (("1" (CASE-REPLACE "sr!1 - (tr!1 - te!1) * vr!1 + (tau(sr!1, vr!1) - te!1 + tr!1) * vr!1 = sr!1 + tau(sr!1, vr!1) * vr!1") (("1" (HIDE -1) (("1" (LEMMA "line_case_correctness") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (LEMMA "tau_is_tangent_pt") (("1" (INST -1 "sr!1" "vr!1") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (HIDE 2) (("1" (EXPAND "tan_condition?") (("1" (REPLACE -5) (("1" (EXPAND "sq") (("1" (HIDE-ALL-BUT (-3 1)) (("1" (REWRITE "sq_rew") (("1" (REWRITE "sq_rew") (("1" (REWRITE "sq_rew") (("1" (REPLACE -1 * RL) (("1" (HIDE -1) (("1" (CASE-REPLACE "sq(D) * vr!1`y * vr!1`y = sq(vr!1`y)*sq(D)") (("1" (HIDE -1) (("1" (EXPAND "sq") (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -3 4) (("2" (CROSS-MULT -2) (("2" (CROSS-MULT -4) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_recovery_TCC1| "" (SKOSIMP*) (("" (GROUND) (("" (MULT-CASES -2) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|line_recovery_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|line_recovery| "" (SKOSIMP*) (("" (EXPAND "alpha_calc") (("" (NAME "TR" "tr!1") (("" (CASE-REPLACE "s!1 + te!1*ve!1 = sr!1 - (tr!1-te!1)*vr!1") (("1" (HIDE -1) (("1" (LEMMA "separation_lem") (("1" (INST -1 "sr!1 - (tr!1 - te!1) * vr!1" "tr!1-te!1+tau(sr!1,vr!1)" "vr!1") (("1" (ASSERT) (("1" (HIDE 5) (("1" (CASE-REPLACE "sr!1 - (tr!1 - te!1) * vr!1 + (tau(sr!1, vr!1) - te!1 + tr!1) * vr!1 = sr!1 + tau(sr!1, vr!1) * vr!1") (("1" (HIDE -1) (("1" (LEMMA "line_case_correctness") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (LEMMA "tau_is_tangent_pt") (("1" (INST -1 "sr!1" "vr!1") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (HIDE 2) (("1" (LEMMA "alpha_calc_lem") (("1" (INST -1 "alpha2!1" "eps!1" "sr!1") (("1" (ASSERT) (("1" (SPLIT -1) (("1" (EXPAND "tan_condition?") (("1" (HIDE-ALL-BUT (-1 -9 1 3)) (("1" (MULT-BY -1 "sq(vr!1`x)") (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-5 1)) (("2" (GRIND) NIL NIL)) NIL) ("3" (PROPAX) NIL NIL) ("4" (EXPAND "alpha_calc") (("4" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1 -3 -4 -5 5) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (CROSS-MULT -1) (("2" (CROSS-MULT -2) (("2" (EXPAND "+ ") (("2" (EXPAND "-") (("2" (EXPAND "*") (("2" (MULT-BY -3 "te!1 - tr!1") (("2" (ASSERT) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (MULT-BY -2 "alpha2!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cir_esc_cyl_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cir_esc_cyl| "" (SKOSIMP*) (("" (LEMMA "quadratic_eq_0") (("" (INST?) (("1" (ASSERT) (("1" (FLATTEN) (("1" (HIDE -1) (("1" (REPLACE -12) (("1" (HIDE -12) (("1" (CASE "-2*SSy!1*thp!1*voe!1`y = sq(SSx!1) + sq(SSy!1) + 2*SSx!1*thp!1*voe!1`x +sq(thp!1)*(sq(voe!1`x) + sq(voe!1`y)) - sq(D)") (("1" (HIDE-ALL-BUT (-1 -4 -5 3)) (("1" (MOVE-TERMS -1 R 5) (("1" (MOVE-TERMS -1 L 1) (("1" (REVEAL -13) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (CASE-REPLACE "sq(voe!1`y) + sq(voe!1`x) = sq(vo!1`x) + sq(vo!1`y) ") (("1" (HIDE -1) (("1" (MOVE-TERMS 1 R 3) (("1" (REPLACE -3) (("1" (REPLACE -4) (("1" (REPLACE -8 * RL) (("1" (MOVE-TERMS 1 L 2) (("1" (REPLACE -3 * RL) (("1" (REPLACE -4 * RL) (("1" (TRANSFORM-BOTH 1 "sq(%1)") (("1" (HIDE 2) (("1" (REWRITE "sq_times") (("1" (REVEAL -3) (("1" (ISOLATE -1 L 1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (ASSERT) (("1" (EXPAND "sq" 1 7) (("1" (CASE-REPLACE "4 * (voe!1`x * voe!1`x * SSx!1 * SSx!1 * thp!1 * thp!1) = 4 * sq(voe!1`x) * sq(SSx!1) * sq(thp!1)") (("1" (ISOLATE 1 R 2) (("1" (MOVE-TERMS 1 L 3) (("1" (HIDE -1) (("1" (FACTOR -5 R) (("1" (CASE-REPLACE "4 * sq(voe!1`x) * sq(SSx!1) * sq(thp!1) + sq(voe!1`x) * sq(-2 * (SSy!1 * thp!1)) = A!1 * sq(voe!1`x)") (("1" (HIDE -1) (("1" (ISOLATE -1 L 2) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1 -2 -5) (("1" (CASE "B!1 = 4 * E!1 * SSx!1 * thp!1") (("1" (REPLACE -1) (("1" (ASSERT) (("1" (HIDE -1 -4) (("1" (REWRITE "sq_times" +) (("1" (CASE-REPLACE "sq(-2) = 4") (("1" (HIDE -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (REPLACE -1) (("1" (HIDE -1) (("1" (HIDE -2) (("1" (ASSERT) (("1" (REPLACE -1) (("1" (HIDE -1 -2) (("1" (EXPAND "sq") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (REPLACE -1) (("2" (HIDE -1) (("2" (EXPAND "sq") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (HIDE-ALL-BUT (-5 1)) (("2" (REPLACE -1) (("2" (EXPAND "sq") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (EXPAND "sq") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-1 -4 -5 1)) (("2" (REVEAL -12) (("2" (NAME "SD1" "-2 * SSy!1 * thp!1 * voe!1`y") (("2" (NAME "SD2" "E!1 + 2 * SSx!1 * thp!1 * voe!1`x") (("2" (REPLACE -1) (("2" (REPLACE -2) (("2" (REPLACE -5) (("2" (REPLACE -6) (("2" (ASSERT) (("2" (REPLACE -1) (("2" (REPLACE -2) (("2" (HIDE -3 -5 -6) (("2" (REVEAL -10) (("2" (REPLACE -2) (("2" (HIDE -2) (("2" (REPLACE -2) (("2" (HIDE -2) (("2" (LEMMA "sq_eq_abs") (("2" (INST?) (("2" (ASSERT) (("2" (HIDE -3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (HIDE 2) (("2" (HIDE-ALL-BUT (-12 1)) (("2" (TRANSFORM-BOTH -1 "sq(%1)") (("1" (HIDE -2) (("1" (REWRITE "sq_sqrt") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|circle_escape_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|circle_escape| "" (SKOSIMP*) (("" (LEMMA "circle_correctness") (("" (INST -1 "s!1" "ve!1") (("" (ASSERT) (("" (CASE "ve!1`z = v!1`z") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (FLATTEN) (("1" (LEMMA "cir_esc_cyl") (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) (("1" (EXPAND "exit_point?") (("1" (EXPAND "entry_point?") (("1" (HIDE -3 -4 -5 -6 -7 -8) (("1" (TYPEPRED "eps!1") (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2) (("2" (ASSERT) (("2" (REPLACE -15) (("2" (REPLACE -14) (("2" (EXPAND "-") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cir_hd_only_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cir_hd_only| "" (SKOSIMP*) (("" (TRANSFORM-BOTH -2 "sq(%1)") (("1" (HIDE -3) (("1" (REWRITE "sq_sqrt") (("1" (EXPAND "heading_only?") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL) ("3" (ASSERT) NIL NIL)) NIL)) NIL) (|cir_rec_lem_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cir_rec_lem_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|cir_rec_lem| "" (SKOSIMP*) (("" (LEMMA "quadratic_eq_0") (("" (INST?) (("1" (ASSERT) (("1" (ASSERT) (("1" (REPLACE -7) (("1" (ASSERT) (("1" (HIDE -6 -7) (("1" (REPLACE -6) (("1" (HIDE -6) (("1" (EXPAND "+ ") (("1" (EXPAND "*") (("1" (MULT-BY 3 "sq(tr!1-te!1)") (("1" (ASSERT) (("1" (NAME "TR_TE" "tr!1-te!1") (("1" (REPLACE -1) (("1" (CROSS-MULT -7) (("1" (CROSS-MULT -8) (("1" (REWRITE "sq_times" + :DIR RL) (("1" (REWRITE "sq_times" + :DIR RL) (("1" (REPLACE -7) (("1" (HIDE -7) (("1" (REPLACE -7) (("1" (HIDE -7) (("1" (ASSERT) (("1" (REPLACE -1 * RL) (("1" (HIDE -1) (("1" (ASSERT) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (1 3)) (("2" (LEMMA "sq_eq_0") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|circle_recovery_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|circle_recovery_TCC2| "" (SKOSIMP*) (("" (ASSERT) NIL NIL)) NIL) (|circle_recovery| "" (SKOSIMP*) (("" (LEMMA "cir_rec_lem") (("" (INST -1 "Ax!1" "Ay!1" "B_x!1" "B_y!1" "s!1" "sr!1" "te!1" "tpp!1" "tr!1" "v!1" "ve!1" "vr!1") (("" (ASSERT) (("" (SPLIT -1) (("1" (HIDE -10 -11) (("1" (CASE-REPLACE "s!1 + te!1*ve!1 = sr!1 - (tr!1-te!1)*vr!1") (("1" (HIDE -1) (("1" (LEMMA "separation_lem") (("1" (INST -1 "sr!1 - (tr!1 - te!1) * vr!1" "tpp!1-te!1" "vr!1") (("1" (HIDE -1) (("1" (LEMMA "separation_lem") (("1" (INST -1 "sr!1 - (tr!1 - te!1) * vr!1" "tpp!1-te!1" "vr!1") (("1" (ASSERT) (("1" (HIDE 5) (("1" (CASE-REPLACE "sr!1 - (tr!1 - te!1) * vr!1 + (tpp!1 - te!1) * vr!1 = sr!1 + (tpp!1 - tr!1)* vr!1") (("1" (HIDE -1) (("1" (LEMMA "ccc") (("1" (INST?) (("1" (ASSERT) (("1" (SPLIT +) (("1" (HIDE-ALL-BUT (-4 -5 -12 -13 1)) (("1" (GRIND) NIL NIL)) NIL) ("2" (FLATTEN) (("2" (HIDE 2) (("2" (EXPAND "entry_point?") (("2" (CASE "on_cyl?(sr!1 + (tpp!1 - tr!1) * vr!1)") (("1" (EXPAND "entry?") (("1" (ASSERT) (("1" (HIDE 2) (("1" (HIDE-ALL-BUT (-5 -6 -14 1)) (("1" (LEMMA "vertical_entry_exit_condition") (("1" (INST -1 "1" "s!1`z" "v!1`z") (("1" (ASSERT) (("1" (REPLACE -3 * RL) (("1" (HIDE -3) (("1" (REPLACE -2) (("1" (HIDE -2) (("1" (REPLACE -2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 2 3 4) (("2" (HIDE-ALL-BUT (-1 -4 -10 -11 -12 1)) (("2" (CROSS-MULT -3) (("2" (CROSS-MULT -4) (("2" (MOVE-TERMS -3 R 2) (("2" (MOVE-TERMS -4 R 2) (("2" (ISOLATE -3 L 3) (("2" (ISOLATE -4 L 3) (("2" (REPLACE -3) (("2" (REPLACE -4) (("2" (HIDE -3 -4) (("2" (ASSERT) (("2" (REPLACE -2) (("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT (-4 -10 -11 -12 -13 1)) (("2" (CROSS-MULT -2) (("2" (CROSS-MULT -3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|in_circle_recovery| "" (SKOSIMP*) (("" (EXPAND "separation_pos?") (("" (SKOSIMP*) (("" (HIDE 2) (("" (EXPAND "vert_sep?") (("" (EXPAND "+ ") (("" (EXPAND "*") (("" (REPLACE -2) (("" (CASE "v!1`z >= 0") (("1" (EXPAND "theta") (("1" (EXPAND "sign") (("1" (ASSERT) (("1" (CROSS-MULT -2) (("1" (MULT-BY -1 "tt!1" +) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "theta") (("2" (EXPAND "sign") (("2" (ASSERT) (("2" (CROSS-MULT -1) (("2" (MULT-BY 1 "tt!1" +) (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (CASE-REPLACE "tt!1 = 0") (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|out_circle_recovery| "" (SKOSIMP*) (("" (LEMMA "cir_esc_cyl") (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (REPLACE -12) (("" (HIDE -3 -4 -5 -6 -7 -8 -10 -11 -12 -13) (("" (LEMMA "ccc") (("" (INST?) (("" (ASSERT) (("" (SPLIT +) (("1" (LEMMA "reaching_H_theta") (("1" (INST -1 "-1" "s!1`z" "ve!1`z") (("1" (HIDE -2 -5 -9 4) (("1" (GRIND :EXCLUDE "theta") NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (HIDE 1) (("2" (EXPAND "exit_point?") (("2" (HIDE -1 4) (("2" (EXPAND "theta") (("2" (CROSS-MULT -1) (("2" (EXPAND "+ ") (("2" (CASE "v!1`z > 0") (("1" (EXPAND "sign") (("1" (EXPAND "*") (("1" (HIDE -8) (("1" (HIDE -3 -4 -5 -6 -7) (("1" (ASSERT) (("1" (MULT-BY -2 "v!1`z") (("1" (ASSERT) (("1" (ASSERT) (("1" (MULT-BY -2 "H") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "sign") (("2" (ASSERT) (("2" (EXPAND "*") (("2" (HIDE -7) (("2" (MULT-BY -1 "v!1`z") (("2" (ASSERT) (("2" (ASSERT) (("2" (MULT-BY 1 "H") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$line_line_hd.pvs line_line_hd: THEORY BEGIN IMPORTING criteria, common_defs, hd_only vo : VAR Vect3 % Ownship velocity voe : VAR Vect3 % Ownship Escape velocity vi : VAR Vect3 % Intruder velocity s : VAR Vect3 % Relative position v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape maneuver sr : VAR Vect3 % Relative position at the end of the escape maneuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time eps : VAR Sign %% SOLUTIONS THAT RESULT IN ve`x = 0 llhd_escape_0: THEOREM %% IF sq(vo`x) + sq(vo`y) >= sq(vi`x) ve = voe - vi AND sq(vo`x) + sq(vo`y) >= sq(vi`x) AND % TEST CONDITION sq(D) = sq(s`x) AND % TEST CONDITION voe`x = vi`x AND % COMPUTED VALUE voe`y = eps*sqrt(sq(vo`x)+sq(vo`y)-sq(vi`x)) AND % COMPUTED VALUE hor_speed_gt_0?(ve) % TEST AFTER COMPUTATION IMPLIES separation?(s,ve) % Note. The proof of llhd_escape_A does not use the premises that define % voe`y (i.e. premises 2 and 5). This theorem is true for all voe`y. % This particular value is chosen so that we have a manuevar that only changes % the heading. The following theorem shows this is true. llhd_esc_0_hd_only: THEOREM sq(vo`x) + sq(vo`y) >= sq(vi`x) AND % TEST CONDITION voe`x = vi`x AND % COMPUTED VALUE voe`y = eps*sqrt(sq(vo`x)+sq(vo`y)-sq(vi`x))AND % COMPUTED VALUE voe`z = vo`z IMPLIES heading_only?(vo,voe) %% ESCAPE SOLUTIONS THAT RESULT IN ve'x /= 0 alpha: VAR real % ----- defined in hd_only ----- % % alpha_calc(eps: real, s | IF sq(D) = sq(s`x) THEN s`x*s`y /= 0 ELSE % sq(s`x) + sq(s`y) - sq(D) >= 0 ENDIF): real = % IF sq(D) = sq(s`x) THEN (sq(s`y) - sq(D))/(2*s`x*s`y) % ELSE (-s`x*s`y+eps*D*sqrt(sq(s`x)+sq(s`y)-sq(D)))/(sq(D)-sq(s`x)) % ENDIF llhd_escape: THEOREM sq(s`x) + sq(s`y) > sq(D) AND % TEST CONDITION sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION hor_speed_gt_0?(ve) AND % TEST AFTER COMPUTATION discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND alpha = alpha_calc(eps,s) AND % COMPUTED VALUE (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x % COMPUTED VALUE IMPLIES separation?(s,ve) llhd_esc_hd_only: THEOREM sq(s`x) + sq(s`y) > sq(D) AND % TEST CONDITION sq(vo`x) + sq(vo`y) /= sq(vi`x)+sq(vi`y) AND % TEST CONDITION ve = voe - vi AND discr(1 + sq(alpha), 2*(vi`x + alpha * vi`y), % TEST CONDITION sq(vi`x) + sq(vi`y) - sq(vo`x) - sq(vo`y)) >= 0 AND alpha = alpha_calc(eps,s) AND % COMPUTED VALUE (ve`x = x1(1+sq(alpha), % COMPUTED VALUE 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y)) OR ve`x = x2(1+sq(alpha), 2*(vi`x+alpha*vi`y), sq(vi`x)+sq(vi`y)-sq(vo`x)-sq(vo`y))) AND ve`y = alpha*ve`x AND % COMPUTED VALUE voe`z = vo`z IMPLIES heading_only?(vo,voe) %% RECOVERY SOLUTIONS THAT RESULT IN vr`x = 0 llhd_recovery_A: THEOREM hor_speed_gt_0?(vr) AND % TEST CONDITION AFTER COMPUTATION te * ve`y = tr * v`y AND % TEST CONDITION ve`x /= 0 AND % TEST CONDITION te = tr*v`x/ve`x AND % COMPUTED VALUE vr`x = 0 AND % COMPUTED VALUE vr`y = 0 AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) llhd_recovery_0: THEOREM %% CASE vr`x = 0 AND sq(D) = sq(sr`x) hor_speed_gt_0?(vr) AND % TEST CONDITION AFTER COMPUTATION sr = s + tr*v AND sq(D) = sq(sr`x) AND % TEST CONDITION ve`x /= 0 AND % TEST CONDITION tr /= te AND % TEST CONDITION te = tr*v`x/ve`x AND % COMPUTED VALUE vr`x = 0 AND % COMPUTED VALUE vr`y = (tr*v`y - te*ve`y)/(tr-te) AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) %% RECOVERY SOLUTIONS THAT RESULT IN vr`x /= 0 alpha2: VAR real % ------- replace by alpha_calc_lem ------- % % llhd_rec_C_lem: LEMMA % sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND % TEST CONDITION % sr`y /= 0 AND % TEST CONDITION % alpha2 = alpha_calc(eps,sr) % COMPUTED VALUE % IMPLIES % sq(D)*(1+sq(alpha2)) = sq(sr`x*alpha2 - sr`y) llhd_recovery: THEOREM sr = s + tr*v AND hor_speed_gt_0?(vr) AND % TEST AFTER COMPUTATION tr /= te AND % TEST AFTER COMPUTATION sq(sr`x) + sq(sr`y) - sq(D) >= 0 AND % TEST CONDITION sr`y /= 0 AND % TEST CONDITION alpha2 = alpha_calc(eps,sr) AND % COMPUTED VALUE ve`y-alpha2*ve`x /= 0 AND % TEST AFTER COMPUTATION te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) AND % COMPUTED VALUE vr`x = (tr*v`x-te*ve`x)/(tr-te) AND % COMPUTED VALUE vr`y = alpha2*vr`x AND % COMPUTED VALUE ve`z = v`z AND % COMPUTED VALUE vr`z = v`z % COMPUTED VALUE IMPLIES separation?(s+te*ve,vr) llhd_timeliness: THEOREM te /= tr AND vr`x = (tr*v`x-te*ve`x)/(tr-te) AND vr`y = alpha2*vr`x AND ve`y-alpha2*ve`x /= 0 AND te = tr*(v`y-alpha2*v`x)/(ve`y-alpha2*ve`x) AND vr`z = v`z AND ve`z = v`z IMPLIES s + tr * v = s + te*ve + (tr-te)*vr % NOTE: Recoveries are not "heading_only", may also involve speed change END line_line_hd $$$line_line_hd.prf (|line_line_hd| (|llhd_escape_0_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|llhd_escape_0| "" (SKOSIMP*) (("" (LEMMA "line_escape_0") (("" (INST?) (("" (ASSERT) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_esc_0_hd_only_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|llhd_esc_0_hd_only| "" (SKOSIMP*) (("" (LEMMA "line_esc_0_hd_only") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|llhd_escape_TCC1| "" (SKOSIMP*) (("" (GROUND) (("" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_escape_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|llhd_escape| "" (SKOSIMP*) (("" (LEMMA "line_escape") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_esc_hd_only_TCC1| "" (SKOSIMP*) (("" (GROUND) (("" (MULT-CASES -2) (("1" (EXPAND "sq") (("1" (ASSERT) NIL NIL)) NIL) ("2" (EXPAND "sq") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_esc_hd_only_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|llhd_esc_hd_only| "" (SKOSIMP*) (("" (LEMMA "quadratic_eq_0") (("" (INST?) (("" (ASSERT) (("" (FLATTEN) (("" (HIDE -1) (("" (SPLIT -1) (("1" (HIDE -2 -4 -5 -6 -8 1) (("1" (EXPAND "heading_only?") (("1" (CASE "sq(ve!1`x + vi!1`x) + sq(alpha!1*ve!1`x+vi!1`y) = sq(vo!1`x) + sq(vo!1`y)") (("1" (HIDE -2) (("1" (REPLACE -3 * RL) (("1" (HIDE -3) (("1" (REPLACE -2) (("1" (HIDE -2) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -3 -4 2) (("2" (HIDE -2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_recovery_A| "" (SKOSIMP*) (("" (NAME "SR" "s!1 + tr!1*v!1") (("" (CASE-REPLACE "s!1 + te!1*ve!1 = SR - (tr!1-te!1)*vr!1") (("1" (HIDE -1) (("1" (LEMMA "separation_lem") (("1" (INST -1 "SR - (tr!1 - te!1) * vr!1" "tr!1-te!1+tau(SR,vr!1)" "vr!1") (("1" (ASSERT) (("1" (HIDE 3) (("1" (CASE-REPLACE "SR - (tr!1 - te!1) * vr!1 + (tau(SR, vr!1) - te!1 + tr!1) * vr!1 = SR + tau(SR, vr!1) * vr!1") (("1" (HIDE -1) (("1" (LEMMA "line_case_correctness") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (LEMMA "tau_is_tangent_pt") (("1" (INST -1 "SR" "vr!1") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (HIDE 2) (("1" (EXPAND "tan_condition?") (("1" (REPLACE -5) (("1" (REPLACE -6) (("1" (EXPAND "sq") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE-ALL-BUT 1) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2 3) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_recovery_0_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|llhd_recovery_0| "" (SKOSIMP*) (("" (LEMMA "line_recovery_0") (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_recovery_TCC1| "" (SKOSIMP*) (("" (GROUND) (("" (MULT-CASES -2) (("" (EXPAND "sq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_recovery_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|llhd_recovery| "" (SKOSIMP*) (("" (LEMMA "line_recovery") (("" (INST?) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|llhd_timeliness_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|llhd_timeliness| "" (SKOSIMP*) (("" (LEMMA "alpha_timeliness") (("" (INST?) (("" (ASSERT) (("" (INST -1 "alpha2!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$heading_only.pvs heading_only: THEORY BEGIN IMPORTING line_line_hd, line_circle_hd, circle_line_hd, circle_circle_hd, in_circle_hd, out_circle_hd, line_line_hd_comb, line_circle_hd_comb, circle_line_hd_comb, circle_circle_hd_comb, in_circle_hd_comb, out_circle_hd_comb, extra_hd END heading_only $$$gs_only_prop.pvs gs_only_prop: THEORY BEGIN IMPORTING gs_only_algo, gs_only, criteria, common_defs, sign s : VAR Vect3 % Relative position vo : VAR Vect3 % Ownship absolute velocity vi : VAR Vect3 % Intruder absolute velocity v : VAR Vect3 % Relative velocity vv : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR posreal % Recovery time te : VAR real % Escape time t : VAR real % time k, j : VAR real % scale factors for escape and recovery ground speed ss : VAR real % generic scale factor m : VAR solution a : VAR real b : VAR real c : VAR real % % % ---------------------------------------------------------------- % Proofs of Algorithm Components % ---------------------------------------------------------------- % % line_factor_is_sep : LEMMA ss = compute_line_factor(s, vo, vi, tr) AND vv = (# x:= ss*vo`x - vi`x, y:= ss*vo`y - vi`y, z:= vo`z - vi`z #) IMPLIES separation?(s, vv) OR ss = 0 line_factor_is_sep_alt : LEMMA ss = compute_line_factor_alt(s, vo, vi, tr) AND vv = (# x:= ss*vo`x - vi`x, y:= ss*vo`y - vi`y, z:= vo`z - vi`z #) IMPLIES separation?(s, vv) OR ss = 0 escape_is_oncyl : LEMMA k = compute_in_circle_factor(s, vo, vi, tr) AND ve = (# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #) AND k /= 0 IMPLIES on_cyl?(at(s, ve, theta(-1,s`z,ve`z))) escape_is_oncyl_alt : LEMMA k = compute_in_circle_factor_alt(s, vo, vi, tr) AND ve = (# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #) AND k /= 0 IMPLIES on_cyl?(at(s, ve, theta(-1,s`z,ve`z))) escape_is_exit : LEMMA k = compute_in_circle_factor(s, vo, vi, tr) AND ve = (# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #) AND k /= 0 IMPLIES exit_point?(at(s, ve, theta(-1,s`z,ve`z)), ve) AND ve`z /= 0 escape_is_exit_alt : LEMMA k = compute_in_circle_factor_alt(s, vo, vi, tr) AND ve = (# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #) AND k /= 0 IMPLIES exit_point?(at(s, ve, theta(-1,s`z,ve`z)), ve) AND ve`z /= 0 circle_escape_is_sep : LEMMA (k = compute_in_circle_factor(s, vo, vi, tr) OR k = compute_in_circle_factor_alt(s, vo, vi, tr)) AND ve = (# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #) IMPLIES separation?(s, ve) OR k = 0 recovery_is_oncyl : LEMMA j = compute_out_circle_factor(s, vo, vi, tr) AND vr = (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #) AND j /= 0 IMPLIES on_cyl?(at(s+tr*(vo-vi), vr, theta(1,s`z,vr`z) - tr)) recovery_is_oncyl_alt : LEMMA j = compute_out_circle_factor_alt(s, vo, vi, tr) AND vr = (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #) AND j /= 0 IMPLIES on_cyl?(at(s+tr*(vo-vi), vr, theta(1,s`z,vr`z) - tr)) recovery_is_entry : LEMMA j = compute_out_circle_factor(s, vo, vi, tr) AND vr = (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #) AND j /= 0 IMPLIES entry_point?(at(s+tr*(vo-vi), vr, theta(1,s`z,vr`z) - tr), vr) AND vr`z /= 0 recovery_is_entry_alt : LEMMA j = compute_out_circle_factor_alt(s, vo, vi, tr) AND vr = (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #) AND j /= 0 IMPLIES entry_point?(at(s+tr*(vo-vi), vr, theta(1,s`z,vr`z) - tr), vr) AND vr`z /= 0 circle_recovery_is_sep : LEMMA (j = compute_out_circle_factor(s, vo, vi, tr) OR j = compute_out_circle_factor_alt(s, vo, vi, tr)) AND vr = (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #) IMPLIES separation?(s + tr * (vo - vi), vr) OR j = 0 in_circle_is_sep : LEMMA k = compute_factor_for_in_circle(j, s, vo, vi, tr) AND ve = (# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #) IMPLIES separation?(s, ve) OR k = 0 out_circle_is_sep : LEMMA j = compute_factor_for_out_circle(k, s, vo, vi, tr) AND vr = (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #) IMPLIES separation?(s + tr * (vo - vi), vr) OR j = 0 sep_summary : LEMMA ss = compute_line_factor(s, vo, vi, tr) OR ss = compute_line_factor_alt(s, vo, vi, tr) OR ss = compute_in_circle_factor(s, vo, vi, tr) OR ss = compute_in_circle_factor_alt(s, vo, vi, tr) OR ss = compute_factor_for_in_circle(j, s, vo, vi, tr) IMPLIES (separation?(s, (# x:= ss*vo`x - vi`x, y:= ss*vo`y - vi`y, z:= vo`z - vi`z #)) OR ss = 0) sep_summary_rec : LEMMA ss = compute_line_factor(at(s,vo-vi,tr), vo, vi, tr) OR ss = compute_line_factor_alt(at(s,vo-vi,tr), vo, vi, tr) OR ss = compute_out_circle_factor(s, vo, vi, tr) OR ss = compute_out_circle_factor_alt(s, vo, vi, tr) OR ss = compute_factor_for_out_circle(k, s, vo, vi, tr) IMPLIES (separation?(at(s,vo-vi,tr), (# x:= ss*vo`x - vi`x, y:= ss*vo`y - vi`y, z:= vo`z - vi`z #)) OR ss = 0) % % % ----------------------------------------------------------- % Proofs of Groud-Speed Only % ----------------------------------------------------------- % % form_algo_correct : LEMMA (separation?(s,(# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #)) OR k = 0) AND (separation?(s + tr * (vo - vi), (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #)) OR j = 0) AND member(m, form_gs_solution(k, j, s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + tr * (vo - vi), m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND ground_speed_only?(m`ve+vi, vo, vi) AND ground_speed_only?(m`vr+vi, vo, vi) form_properties : LEMMA member(m, form_gs_solution(k, j, s, vo, vi, tr)) IFF m`ve = (# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #) AND m`vr = (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #) AND k > 0 AND j > 0 AND j /= k AND m`te = tr * (1 - j) / (k - j) AND 0 < tr * (1 - j) / (k - j) AND tr * (1 - j) / (k - j) < tr constant_combinations : LEMMA member(m, gs_only_algo(s, vo, vi, tr)) IMPLIES EXISTS k,j: member(m, form_gs_solution(k, j, s, vo, vi, tr)) AND ((k = compute_line_factor(s, vo, vi, tr) AND j = compute_line_factor(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_line_factor_alt(s, vo, vi, tr) AND j = compute_line_factor(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_line_factor(s, vo, vi, tr) AND j = compute_line_factor_alt(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_line_factor_alt(s, vo, vi, tr) AND j = compute_line_factor_alt(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_line_factor(s, vo, vi, tr) AND j = compute_out_circle_factor(s, vo, vi, tr)) OR (k = compute_line_factor_alt(s, vo, vi, tr) AND j = compute_out_circle_factor(s, vo, vi, tr)) OR (k = compute_line_factor(s, vo, vi, tr) AND j = compute_out_circle_factor_alt(s, vo, vi, tr)) OR (k = compute_line_factor_alt(s, vo, vi, tr) AND j = compute_out_circle_factor_alt(s, vo, vi, tr)) OR (k = compute_in_circle_factor(s, vo, vi, tr) AND j = compute_line_factor(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_in_circle_factor(s, vo, vi, tr) AND j = compute_line_factor_alt(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_in_circle_factor_alt(s, vo, vi, tr) AND j = compute_line_factor(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_in_circle_factor_alt(s, vo, vi, tr) AND j = compute_line_factor_alt(at(s, vo - vi, tr), vo, vi, tr)) OR (k = compute_in_circle_factor(s, vo, vi, tr) AND j = compute_out_circle_factor(s, vo, vi, tr)) OR (k = compute_in_circle_factor_alt(s, vo, vi, tr) AND j = compute_out_circle_factor(s, vo, vi, tr)) OR (k = compute_in_circle_factor(s, vo, vi, tr) AND j = compute_out_circle_factor_alt(s, vo, vi, tr)) OR (k = compute_in_circle_factor_alt(s, vo, vi, tr) AND j = compute_out_circle_factor_alt(s, vo, vi, tr)) OR (k = compute_factor_for_in_circle(j,s, vo, vi, tr) AND j = compute_out_circle_factor(s, vo, vi, tr)) OR (k = compute_factor_for_in_circle(j,s, vo, vi, tr) AND j = compute_out_circle_factor_alt(s, vo, vi, tr)) OR (k = compute_in_circle_factor(s, vo, vi, tr) AND j = compute_factor_for_out_circle(k,s, vo, vi, tr)) OR (k = compute_in_circle_factor_alt(s, vo, vi, tr) AND j = compute_factor_for_out_circle(k,s, vo, vi, tr))) gs_only_makes_sep : LEMMA member(m, gs_only_algo(s, vo, vi, tr)) IMPLIES EXISTS k,j: member(m, form_gs_solution(k, j, s, vo, vi, tr)) AND separation?(s,(# x:= k*vo`x - vi`x, y:= k*vo`y - vi`y, z:= vo`z - vi`z #)) AND separation?(s + tr * (vo - vi), (# x:= j*vo`x - vi`x, y:= j*vo`y - vi`y, z:= vo`z - vi`z #)) gs_only_algo_correct_alt : THEOREM FORALL m:member(m, gs_only_algo(s, vo, vi, tr)) IMPLIES separation?(s, m`ve) AND separation?(s + tr * (vo - vi), m`vr) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND ground_speed_only?(m`ve+vi, vo, vi) AND ground_speed_only?(m`vr+vi, vo, vi) gs_only_algo_correct : THEOREM FORALL m:member(m, gs_only_algo(s, vo, vi, tr)) IMPLIES pred_sep?(s, m`ve, m`te) AND pred_sep?(s + m`te * m`ve, m`vr, tr - m`te) AND s + tr * (vo - vi) = s + m`te * m`ve + (tr - m`te) * m`vr AND 0 < m`te AND m`te < tr AND ground_speed_only?(m`ve+vi, vo, vi) AND ground_speed_only?(m`vr+vi, vo, vi) END gs_only_prop $$$gs_only_prop.prf (|gs_only_prop| (|line_factor_is_sep| "" (SKOSIMP*) (("" (CASE "ground_speed_only_absolute?(vv!1, ss!1, vo!1, vi!1)") (("1" (EXPAND "compute_line_factor") (("1" (ASSERT) (("1" (LIFT-IF) (("1" (SPLIT) (("1" (FLATTEN) (("1" (LIFT-IF) (("1" (LEMMA "constant_for_line_alt") (("1" (INST?) (("1" (INST?) (("1" (INST - "s!1") (("1" (LEMMA "line_correctness") (("1" (INST?) (("1" (INST - "s!1") (("1" (ASSERT) (("1" (HIDE 2) (("1" (SPLIT -2) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT -3) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (SPLIT -3) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "ground_speed_only_absolute?") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|line_factor_is_sep_alt| "" (SKOSIMP*) (("" (EXPAND "compute_line_factor_alt") (("" (ASSERT) (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT) (("1" (FLATTEN) (("1" (LEMMA "line_correctness") (("1" (INST?) (("1" (INST - "ss!1" "vi!1" "vo!1") (("1" (ASSERT) (("1" (HIDE 3) (("1" (LEMMA "constant_for_line_alt") (("1" (INST?) (("1" (INST?) (("1" (INST - "s!1") (("1" (ASSERT) (("1" (CASE "ground_speed_only_absolute?(vv!1, ss!1, vo!1, vi!1)") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "ground_speed_only_absolute?") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|escape_is_oncyl_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|escape_is_oncyl| "" (SKOSIMP*) (("" (CASE "z(vo!1-vi!1)=ve!1`z") (("1" (EXPAND "compute_in_circle_factor") (("1" (LIFT-IF) (("1" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT) (("1" (FLATTEN) (("1" (LEMMA "constant_for_circle_alt") (("1" (INST?) (("1" (INST?) (("1" (INST - "k!1" "vi!1" "vo!1") (("1" (ASSERT) (("1" (HIDE 4) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "ground_speed_only_absolute?") (("1" (LIFT-IF) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (HIDE -2) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (SPLIT -) (("1" (FLATTEN) (("1" (EXPAND "ground_speed_only_absolute?") (("1" (HIDE -2) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (HIDE -1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (REPLACE -3 1) (("2" (ASSERT) (("2" (EXPAND "-") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "-") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|escape_is_oncyl_alt_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|escape_is_oncyl_alt| "" (SKOSIMP*) (("" (CASE "z(vo!1-vi!1)=ve!1`z") (("1" (EXPAND "compute_in_circle_factor_alt") (("1" (LIFT-IF) (("1" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (FLATTEN) (("1" (HIDE -2) (("1" (LEMMA "constant_for_circle_alt") (("1" (INST?) (("1" (INST?) (("1" (INST - "vi!1" "vo!1") (("1" (ASSERT) (("1" (EXPAND "ground_speed_only_absolute?") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "-") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|escape_is_exit| "" (SKOSIMP*) (("" (LEMMA "escape_is_oncyl") (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (EXPAND "exit_point?") (("" (HIDE -1) (("" (REPLACE -2) (("" (HIDE -2) (("" (EXPAND "compute_in_circle_factor") (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (LIFT-IF) (("1" (SPLIT) (("1" (FLATTEN) (("1" (REPLACE -3 :DIR RL) (("1" (ASSERT) (("1" (EXPAND "-") (("1" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "-") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) (("1" (REPLACE -3 :DIR RL) (("1" (EXPAND "-") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|escape_is_exit_alt| "" (SKOSIMP*) (("" (LEMMA "escape_is_oncyl_alt") (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (EXPAND "exit_point?") (("" (HIDE -1) (("" (REPLACE -2) (("" (HIDE -2) (("" (EXPAND "compute_in_circle_factor_alt") (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (FLATTEN) (("1" (REPLACE -3 :DIR RL) (("1" (EXPAND "-") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_escape_is_sep| "" (SKOSIMP*) (("" (LEMMA "escape_is_exit") (("" (INST?) (("" (INST - "ve!1") (("" (LEMMA "escape_is_exit_alt") (("" (INST?) (("" (INST - "ve!1") (("" (ASSERT) (("" (LEMMA "circle_correctness") (("" (INST - "s!1" "ve!1") (("" (ASSERT) (("" (PROP) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|recovery_is_oncyl_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|recovery_is_oncyl| "" (SKOSIMP*) (("" (EXPAND "compute_out_circle_factor") (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (NAME "THETA_DEF" "theta(1, s!1`z, (vo!1 - vi!1)`z)") (("1" (REPLACE -1) (("1" (CASE-REPLACE "theta(1,s!1`z,vr!1`z)=THETA_DEF") (("1" (CASE "THETA_DEF = theta(1, s!1`z + vo!1`z * tr!1 - vi!1`z * tr!1, vo!1`z - vi!1`z) + tr!1") (("1" (LEMMA "constant_for_circle_alt") (("1" (INST?) (("1" (INST?) (("1" (INST - "j!1" "vi!1" "vo!1") (("1" (ASSERT) (("1" (HIDE 4) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (ASSERT) (("1" (LIFT-IF) (("1" (SPLIT -1) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "ground_speed_only_absolute?") (("1" (SPLIT -) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (EXPAND "ground_speed_only_absolute?") (("2" (LIFT-IF) (("2" (SPLIT -2) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -3) (("2" (LEMMA "theta_translation") (("2" (INST - "1" "s!1" "tr!1" "vo!1-vi!1") (("2" (ASSERT) (("2" (EXPAND "at") (("2" (EXPAND "+") (("2" (EXPAND "-") (("2" (EXPAND "*") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE -3) (("3" (EXPAND "-") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (REPLACE -2 1) (("2" (ASSERT) (("2" (EXPAND "-") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE -2) (("3" (REPLACE -2 1) (("3" (ASSERT) (("3" (EXPAND "-") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE -1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|recovery_is_oncyl_alt_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|recovery_is_oncyl_alt| "" (SKOSIMP*) (("" (EXPAND "compute_out_circle_factor_alt" :ASSERT? NONE) (("" (SKOLETIN -1 1) (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (CASE "vr!1`z=v__1`z") (("1" (CASE "theta(1,s!1`z,v__1`z)=theta(1,s!1`z+tr!1*v__1`z,v__1`z)+tr!1") (("1" (LEMMA "constant_for_circle_alt") (("1" (INST?) (("1" (INST?) (("1" (INST - "vr!1") (("1" (ASSERT) (("1" (HIDE 4) (("1" (SPLIT -) (("1" (FLATTEN) (("1" (ASSERT) (("1" (EXPAND "ground_speed_only_absolute?") (("1" (SPLIT -) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE -2) (("2" (LEMMA "theta_translation") (("2" (INST - "1" "s!1" "tr!1" "vo!1-vi!1") (("2" (ASSERT) (("2" (EXPAND "at") (("2" (EXPAND "+") (("2" (EXPAND "-") (("2" (EXPAND "*") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (HIDE -2) (("3" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (HIDE -1) (("2" (REVEAL "v__1") (("2" (REPLACE -1) (("2" (EXPAND "-") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|recovery_is_entry| "" (SKOSIMP*) (("" (LEMMA "recovery_is_oncyl") (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (EXPAND "entry_point?") (("" (HIDE -1) (("" (REPLACE -2 2) (("" (HIDE -2) (("" (EXPAND "compute_out_circle_factor") (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (LIFT-IF) (("1" (SPLIT) (("1" (FLATTEN) (("1" (REPLACE -3 -2 :DIR RL) (("1" (HIDE -3 -4 -1) (("1" (EXPAND "-") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) (("2" (LIFT-IF) (("2" (SPLIT) (("1" (FLATTEN) (("1" (REPLACE -3 :DIR RL) (("1" (HIDE 1) (("1" (HIDE -3) (("1" (EXPAND "-") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|recovery_is_entry_alt| "" (SKOSIMP*) (("" (LEMMA "recovery_is_oncyl_alt") (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (EXPAND "entry_point?") (("" (HIDE -1) (("" (REPLACE -2 2) (("" (HIDE -2) (("" (EXPAND "compute_out_circle_factor_alt") (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (SPLIT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (REPLACE -3 -2 :DIR RL) (("1" (HIDE -3 -4 -1) (("1" (EXPAND "-") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_recovery_is_sep| "" (SKOSIMP*) (("" (CASE "z(vo!1-vi!1)=vr!1`z") (("1" (LEMMA "recovery_is_entry") (("1" (INST?) (("1" (INST - "vr!1") (("1" (LEMMA "recovery_is_entry_alt") (("1" (INST?) (("1" (INST - "j!1") (("1" (ASSERT) (("1" (LEMMA "circle_correctness") (("1" (INST?) (("1" (ASSERT) (("1" (HIDE 2) (("1" (LEMMA "theta_translation") (("1" (INST - "1" "s!1" "tr!1" "vo!1-vi!1") (("1" (EXPAND "at") (("1" (SPLIT -5) (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "-") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|in_circle_is_sep| "" (SKOSIMP*) (("" (EXPAND "compute_factor_for_in_circle") (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT) (("1" (FLATTEN) (("1" (LEMMA "circle_correctness") (("1" (INST?) (("1" (CASE "vo!1`z - vi!1`z = ve!1`z") (("1" (REPLACE -1) (("1" (REPLACE -1 :DIR RL) (("1" (EXPAND "-") (("1" (ASSERT) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|out_circle_is_sep| "" (SKOSIMP*) (("" (EXPAND "compute_factor_for_out_circle") (("" (LIFT-IF) (("" (SPLIT) (("1" (FLATTEN) (("1" (EXPAND "-" 1) (("1" (SPLIT) (("1" (FLATTEN) (("1" (SPLIT) (("1" (FLATTEN) (("1" (LEMMA "circle_correctness") (("1" (INST?) (("1" (CASE "vo!1`z - vi!1`z = vr!1`z") (("1" (NAME "T" "theta(-1, z(s!1 + tr!1 * (vo!1 - vi!1)), vr!1`z)") (("1" (REPLACE -1) (("1" (CASE "T + tr!1 = theta(-1, s!1`z, (vo!1 - vi!1)`z)") (("1" (REPLACE -1 :DIR RL) (("1" (EXPAND "at") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (LEMMA "theta_translation") (("2" (HIDE -6) (("2" (INST?) (("2" (EXPAND "-" -1) (("2" (ASSERT) (("2" (REPLACE -2 1 :DIR RL) (("2" (EXPAND "at") (("2" (ASSERT) (("2" (REPLACE -3) (("2" (EXPAND "-") (("2" (HIDE 2) (("2" (EXPAND "+") (("2" (EXPAND "*") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("3" (EXPAND "-") (("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sep_summary| "" (SKOSIMP*) (("" (LEMMA "line_factor_is_sep") (("" (INST?) (("" (INST - "(# x := ss!1 * vo!1`x - vi!1`x, y := ss!1 * vo!1`y - vi!1`y, z := vo!1`z - vi!1`z #)") (("" (LEMMA "line_factor_is_sep_alt") (("" (INST?) (("" (INST - "(# x := ss!1 * vo!1`x - vi!1`x, y := ss!1 * vo!1`y - vi!1`y, z := vo!1`z - vi!1`z #)") (("" (LEMMA "circle_escape_is_sep") (("" (INST?) (("" (INST - "(# x := ss!1 * vo!1`x - vi!1`x, y := ss!1 * vo!1`y - vi!1`y, z := vo!1`z - vi!1`z #)") (("" (LEMMA "in_circle_is_sep") (("" (INST?) (("" (GROUND) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sep_summary_rec| "" (SKOSIMP*) (("" (LEMMA "line_factor_is_sep") (("" (INST - "at(s!1, vo!1-vi!1, tr!1)" "ss!1" "tr!1" "vi!1" "vo!1" "_") (("" (INST?) (("" (LEMMA "line_factor_is_sep_alt") (("" (INST - "at(s!1, vo!1-vi!1, tr!1)" "ss!1" "tr!1" "vi!1" "vo!1" "_") (("" (INST?) (("" (LEMMA "circle_recovery_is_sep") (("" (INST?) (("" (INST - "(# x := ss!1 * vo!1`x - vi!1`x, y := ss!1 * vo!1`y - vi!1`y, z := vo!1`z - vi!1`z #)") (("" (LEMMA "out_circle_is_sep") (("" (INST?) (("" (INST?) (("" (EXPAND "at") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|form_algo_correct| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "form_gs_solution") (("" (SPLIT -3) (("1" (FLATTEN) (("1" (EXPAND "singleton") (("1" (LEMMA "gs_timeliness") (("1" (INST - "j!1" "k!1" "s!1" "m!1`te" "tr!1" "vo!1 - vi!1" "m!1`ve" "vi!1" "vo!1" "m!1`vr") (("1" (EXPAND "at") (("1" (EXPAND "ground_speed_only?") (("1" (EXPAND "ground_speed_only_absolute?") (("1" (ASSERT) (("1" (REPLACE -6) (("1" (ASSERT) (("1" (EXPAND "-") (("1" (EXPAND "+") (("1" (EXPAND "*") (("1" (ASSERT) (("1" (SPLIT) (("1" (INST?) NIL NIL) ("2" (INST + "j!1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|form_properties_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|form_properties| "" (SKOSIMP*) (("" (SPLIT) (("1" (FLATTEN) (("1" (EXPAND "member") (("1" (EXPAND "form_gs_solution") (("1" (SPLIT) (("1" (FLATTEN) (("1" (EXPAND "singleton") (("1" (REPLACE -5) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "emptyset") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FLATTEN) (("2" (EXPAND "member") (("2" (EXPAND "form_gs_solution") (("2" (ASSERT) (("2" (EXPAND "singleton") (("2" (APPLY-EXTENSIONALITY 2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|constant_combinations| "" (SKOSIMP*) (("" (EXPAND "member") (("" (EXPAND "gs_only_algo") (("" (EXPAND "union") (("" (EXPAND "member") (("" (APPLY (TRY (PROP) (INST?) (SKIP))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|gs_only_makes_sep| "" (SKOSIMP*) (("" (LEMMA "constant_combinations") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (INST + "k!1" "j!1") (("" (LEMMA "sep_summary") (("" (INST?) (("" (LEMMA "sep_summary_rec") (("" (INST?) (("" (LEMMA "form_properties") (("" (INST?) (("" (EXPAND "at") (("" (ASSERT) (("" (FLATTEN) (("" (ASSERT) (("" (APPLY (TRY (SPLIT -11) (TRY (FLATTEN) (ASSERT) (SKIP)) (SKIP))) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|gs_only_algo_correct_alt| "" (SKOSIMP*) (("" (LEMMA "gs_only_makes_sep") (("" (INST?) (("" (ASSERT) (("" (SKOSIMP*) (("" (LEMMA "form_algo_correct") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|gs_only_algo_correct| "" (SKOSIMP*) (("" (LEMMA "sep_connection") (("" (INST - "s!1" "m!1`te" "m!1`ve") (("" (LEMMA "sep_connection") (("" (INST - "s!1+m!1`te*m!1`ve" "tr!1-m!1`te" "m!1`vr") (("" (LEMMA "gs_only_algo_correct_alt") (("" (INST?) (("" (ASSERT) (("" (FLATTEN) (("" (ASSERT) (("" (ASSERT) (("" (HIDE 2) (("" (REPLACE -3) (("" (LEMMA "separation_lem") (("" (INST - "s!1 + m!1`te * m!1`ve" "tr!1-m!1`te" "m!1`vr") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$line_and_circle_gs_only.pvs line_and_circle_gs_only: THEORY BEGIN IMPORTING criteria, common_defs, gs_only s : VAR Vect3 % Relative position vo : VAR Vect3 % Ownship absolute velocity vi : VAR Vect3 % Intruder absolute velocity v : VAR Vect3 % Relative velocity ve : VAR Vect3 % Relative escape velocity vr : VAR Vect3 % Relative recovery velocity se : VAR Vect3 % Relative position at the end of the escape manuver sr : VAR Vect3 % Relative position at the end of the escape manuver, % which is also the final position tr : VAR real % Recovery time te : VAR real % Escape time t : VAR real % time tau_p : VAR real % time of closest approach during escape tau_pp : VAR real % time of closest approach during recovery theta_p : VAR real % time to reach top of cylinder theta_pp : VAR real % time to reach top of cylinder k, j : VAR real % scale factors for escape and recovery ground speed line_line : THEOREM RR3D_criteria?(s, v, vo, vi, tr) AND hor_speed_gt_0?(vo) AND ground_speed_only_absolute?(ve, k, vo, vi) AND ground_speed_only_absolute?(vr, j, vo, vi) AND line_case?(s, ve, 0, 0, te) AND line_case?(at(s, v, tr), vr, te, tr, tr) AND time_definition?(v, ve, vr, te, tr) IMPLIES separation?(s,ve) AND separation?(at(s,v,tr),vr) AND at(s,v,tr) = at(at(s,ve,te), vr, tr - te) circle_line : THEOREM RR3D_criteria?(s, v, vo, vi, tr) AND hor_speed_gt_0?(vo) AND ground_speed_only_absolute?(ve, k, vo, vi) AND ground_speed_only_absolute?(vr, j, vo, vi) AND in_circle_case?(s, ve) AND line_case?(at(s, v, tr), vr, te, tr, tr) AND time_definition?(v, ve, vr, te, tr) IMPLIES separation?(s,ve) AND separation?(at(s,v,tr),vr) AND at(s,v,tr) = at(at(s,ve,te), vr, tr - te) line_circle : THEOREM RR3D_criteria?(s, v, vo, vi, tr) AND hor_speed_gt_0?(vo) AND ground_speed_only_absolute?(ve, k, vo, vi) AND ground_speed_only_absolute?(vr, j, vo, vi) AND line_case?(s, ve, 0, 0, te) AND out_circle_case?(s, v, vr, tr) AND time_definition?(v, ve, vr, te, tr) IMPLIES separation?(s,ve) AND separation?(at(s,v,tr),vr) AND at(s,v,tr) = at(at(s,ve,te), vr, tr - te) circle_circle : THEOREM RR3D_criteria?(s, v, vo, vi, tr) AND hor_speed_gt_0?(vo) AND ground_speed_only_absolute?(ve, k, vo, vi) AND ground_speed_only_absolute?(vr, j, vo, vi) AND in_circle_case?(s, ve) AND out_circle_case?(s, v, vr, tr) AND time_definition?(v, ve, vr, te, tr) IMPLIES separation?(s,ve) AND separation?(at(s,v,tr),vr) AND at(s,v,tr) = at(at(s,ve,te), vr, tr - te) in_circle : THEOREM RR3D_criteria?(s, v, vo, vi, tr) AND hor_speed_gt_0?(vo) AND ground_speed_only_absolute?(ve, k, vo, vi) AND ground_speed_only_absolute?(vr, j, vo, vi) AND v`z /= 0 AND 0 < theta(1, s`z, v`z) AND theta(1, s`z, v`z) < tr AND entry_point?(at(s, ve, theta(1, s`z, v`z)), ve) AND time_definition?(v, ve, vr, te, tr) AND te = theta(1, s`z, v`z) IMPLIES separation?(s,ve) AND % separation?(at(s,v,tr),vr) AND pred_sep?(at(s,ve,te), vr, tr - te) AND at(s,v,tr) = at(at(s,ve,te), vr, tr - te) out_circle : THEOREM RR3D_criteria?(s, v, vo, vi, tr) AND hor_speed_gt_0?(vo) AND ground_speed_only_absolute?(ve, k, vo, vi) AND ground_speed_only_absolute?(vr, j, vo, vi) AND v`z /= 0 AND 0 < theta(-1, s`z, v`z) AND theta(-1, s`z, v`z) < tr AND exit_point?(at(s, ve, theta(-1, s`z, v`z)), vr) AND time_definition?(v, ve, vr, te, tr) AND te = theta(-1, s`z, v`z) AND k /= j % must be explicit IMPLIES % separation?(s,ve) AND pred_sep?(s,ve,te) AND separation?(at(s,v,tr),vr) AND at(s,v,tr) = at(at(s,ve,te), vr, tr - te) END line_and_circle_gs_only $$$line_and_circle_gs_only.prf (|line_and_circle_gs_only| (|line_line| "" (SKOSIMP*) (("" (LEMMA "line_correctness2") (("" (INST - "0" "0" "s!1" "k!1" "te!1" "ve!1" "vi!1" "vo!1") (("" (ASSERT) (("" (LEMMA "line_correctness2") (("" (INST - "tr!1" "te!1" "at(s!1, v!1, tr!1)" "j!1" "tr!1" "vr!1" "vi!1" "vo!1") (("" (ASSERT) (("" (LEMMA "constants_not_equal") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "escape_time_defined") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "gs_timeliness") (("" (INST?) (("" (INST - "j!1" "k!1" "vi!1" "vo!1") (("" (ASSERT) (("" (EXPAND "RR3D_criteria?") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_line| "" (SKOSIMP*) (("" (LEMMA "circle_correctness") (("" (INST - "s!1" "ve!1") (("" (EXPAND "in_circle_case?") (("" (FLATTEN) (("" (ASSERT) (("" (LEMMA "line_correctness2") (("" (INST - "tr!1" "te!1" "at(s!1, v!1, tr!1)" "j!1" "tr!1" "vr!1" "vi!1" "vo!1") (("" (ASSERT) (("" (LEMMA "constants_not_equal") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "escape_time_defined") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "gs_timeliness") (("" (INST?) (("" (INST - "j!1" "k!1" "vi!1" "vo!1") (("" (ASSERT) (("" (EXPAND "RR3D_criteria?") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|line_circle| "" (SKOSIMP*) (("" (LEMMA "line_correctness2") (("" (INST - "0" "0" "s!1" "k!1" "te!1" "ve!1" "vi!1" "vo!1") (("" (ASSERT) (("" (LEMMA "constants_not_equal") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "escape_time_defined") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "gs_timeliness") (("" (INST?) (("" (INST - "j!1" "k!1" "vi!1" "vo!1") (("" (EXPAND "RR3D_criteria?") (("" (FLATTEN) (("" (ASSERT) (("" (LEMMA "circle_correctness") (("" (INST - "at(s!1, v!1, tr!1)" "vr!1") (("" (EXPAND "out_circle_case?") (("" (LEMMA "vert_speeds_equal") (("" (INST?) (("" (INST - "j!1" "s!1" "tr!1" "v!1" "vr!1") (("" (ASSERT) (("" (FLATTEN) (("" (ASSERT) (("" (FLATTEN) (("" (HIDE 1) (("" (LEMMA "theta_translation") (("" (INST - "1" "s!1" "tr!1" "v!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|circle_circle| "" (SKOSIMP*) (("" (LEMMA "circle_correctness") (("" (INST?) (("" (ASSERT) (("" (EXPAND "in_circle_case?") (("" (FLATTEN) (("" (ASSERT) (("" (LEMMA "constants_not_equal") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "escape_time_defined") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "gs_timeliness") (("" (INST?) (("" (INST - "j!1" "k!1" "vi!1" "vo!1") (("" (EXPAND "RR3D_criteria?") (("" (FLATTEN) (("" (ASSERT) (("" (LEMMA "circle_correctness") (("" (INST - "at(s!1, v!1, tr!1)" "vr!1") (("" (LEMMA "vert_speeds_equal") (("" (INST?) (("" (INST - "j!1" "s!1" "tr!1" "v!1" "vr!1") (("" (ASSERT) (("" (FLATTEN) (("" (ASSERT) (("" (LEMMA "theta_translation") (("" (INST - "1" "s!1" "tr!1" "vr!1") (("" (ASSERT) (("" (EXPAND "out_circle_case?") (("" (FLATTEN) (("" (EXPAND "at") (("" (EXPAND "+ ") (("" (EXPAND "*") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|in_circle| "" (SKOSIMP*) (("" (LEMMA "vert_speeds_equal") (("" (INST?) (("" (INST - "j!1" "k!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "circle_correctness") (("" (INST?) (("" (FLATTEN) (("" (ASSERT) (("" (LEMMA "constants_not_equal") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "escape_time_defined") (("" (INST?) (("" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("" (ASSERT) (("" (LEMMA "gs_timeliness") (("" (INST?) (("" (INST - "j!1" "k!1" "vi!1" "vo!1") (("" (ASSERT) (("" (SPLIT -) (("1" (ASSERT) (("1" (REPLACE -16) (("1" (HIDE -16) (("1" (EXPAND "pred_sep?") (("1" (SKOSIMP*) (("1" (HIDE 3) (("1" (EXPAND "vert_sep?") (("1" (LEMMA "vertical_criterion_sz_vz_ge_0") (("1" (INST - "s!1 + theta(1,s!1`z, vr!1`z) * vr!1" "vr!1") (("1" (EXPAND "vert_sep?") (("1" (EXPAND "at") (("1" (EXPAND "+ ") (("1" (EXPAND "*") (("1" (REPLACE -5) (("1" (HIDE -5) (("1" (REPLACE -5) (("1" (HIDE -5) (("1" (ASSERT) (("1" (SPLIT -) (("1" (INST - "t!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (LEMMA "reaching_H_theta") (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("3" (HIDE-ALL-BUT (1 3)) (("3" (LEMMA "vertical_entry_exit_condition") (("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "RR3D_criteria?") (("2" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|out_circle| "" (SKOSIMP*) (("" (LEMMA "vert_speeds_equal") (("" (INST?) (("" (INST - "j!1" "k!1" "ve!1" "vr!1") (("" (ASSERT) (("" (CASE "pred_sep?(s!1, ve!1, te!1)") (("1" (ASSERT) (("1" (LEMMA "escape_time_defined") (("1" (INST?) (("1" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("1" (ASSERT) (("1" (LEMMA "gs_timeliness") (("1" (INST?) (("1" (INST - "j!1" "k!1" "vi!1" "vo!1") (("1" (ASSERT) (("1" (SPLIT) (("1" (ASSERT) (("1" (LEMMA "circle_correctness") (("1" (INST - "at(s!1, v!1, tr!1)" "vr!1") (("1" (ASSERT) (("1" (FLATTEN) (("1" (ASSERT) (("1" (FLATTEN) (("1" (REPLACE -1 1) (("1" (LEMMA "theta_translation") (("1" (INST - "-1" "s!1" "tr!1" "vr!1") (("1" (ASSERT) (("1" (EXPAND "at") (("1" (EXPAND "+ ") (("1" (EXPAND "*") (("1" (HIDE 2) (("1" (REPLACE -6) (("1" (REPLACE -16) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (EXPAND "RR3D_criteria?") (("2" (FLATTEN) NIL NIL)) NIL) ("3" (LEMMA "escape_time_defined") (("3" (INST?) (("3" (INST - "j!1" "k!1" "te!1" "ve!1" "vr!1") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (HIDE 4) (("2" (EXPAND "pred_sep?") (("2" (SKOSIMP*) (("2" (HIDE 1) (("2" (LEMMA "vertical_criterion_sz_vz_le_0") (("2" (INST - "s!1 + theta(-1, z(s!1), z(v!1))*ve!1" "ve!1") (("2" (EXPAND "vert_sep?") (("2" (EXPAND "+ ") (("2" (EXPAND "*") (("2" (REPLACE -4) (("2" (HIDE -4) (("2" (REPLACE -4) (("2" (HIDE -4) (("2" (LEMMA "reaching_H_theta") (("2" (INST?) (("1" (ASSERT) (("1" (LEMMA "vertical_entry_exit_condition") (("1" (INST?) (("1" (ASSERT) (("1" (INST - "t!1 - theta(-1, z(s!1), vr!1`z)") (("1"