%% PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul 22, 2008 3:35) %% 8.1 [Linux (x86)] (Jul 22, 2008 3:35) $$$pingPong.pvs pingPong: THEORY BEGIN Node: TYPE = posnat Time: TYPE = posnat link: [Node, Node, Time, Time -> bool] S, D: VAR Node period, Tc, T, Tl, RTT: VAR Time periodic (S, period, Tc): INDUCTIVE bool = EXISTS (Tc2: Time): periodic (S, period, Tc2) AND (Tc = Tc2 + period) now_test: Time S_test: Node periodic_axiom: axiom forall (S: Node): periodic (S, 5, 1) p_test1: Lemma periodic (S_test, 5, 1) => periodic (S_test, 5, 6) p_test2: Lemma periodic (S, 5, 6) p_test_general: Lemma forall (s: Node) (t, p: Time) (i: nat): periodic (s, p, t) => periodic (s, p, (t + p*i)) p_general: Theorem forall (i: nat): periodic (S, 5, 1+5*i) link_periodic : lemma forall (t: Time): link (S, D, t, 10) => (exists (tp: Time): periodic (S, 5, tp) and t<= tp and tp <= t+10) ping (S, D, Tc): INDUCTIVE bool = EXISTS (Tc2: Time): periodic (S, 5, Tc) AND link (S, D, Tc2, 10) AND Tc2 <= Tc AND Tc <= Tc2 + 10 pingMsg (S, D, Tc): INDUCTIVE bool = EXISTS (Tc2: Time): ping (S, D, Tc) AND link (S, D, Tc2, 10) AND Tc2 <= Tc AND Tc <= Tc2 + 10 pendingPing (S, D, T, Tc, Tl): INDUCTIVE bool = ping (S, D, Tc) and T = Tc and Tl = 10 pongMsg (S, Tc): INDUCTIVE bool = EXISTS (D: Node) (Tc2: Time): pingMsg (S, D, Tc) AND link (D, S, Tc2, 10) AND Tc2 <= Tc AND Tc <= Tc2 + 10 pingRTT (S, D, RTT, Tc, Tl): INDUCTIVE bool = EXISTS (T, Tc2: Time): pongMsg (S, Tc) and pendingPing (S, D, T, Tc2, 10) and RTT = Tc - T and Tc2 <= Tc AND Tc <= Tc2 + 10 and Tl = 10 link_refresh: Axiom forall (S, D: Node) (RTT, Tc, Tl: Time): pingRTT(S, D, RTT, Tc, Tl) => link (S, D, Tc, Tl) % invariant 2 link_ping: lemma link (S, D, Tc, 10) => (exists (Tc2: Time): ping (S, D, Tc2) and Tc<= Tc2 and Tc2 <= Tc+10) link_pingMsg: lemma link (S, D, Tc, 10) => (exists (Tp: Time): pingMsg (S, D, Tp) and Tc <= Tp and Tp <= Tc+10) link_pendingPing: lemma link (S, D, Tc, 10) => (exists (Tc2, T, Tl: Time): pendingPing (S, D, T, Tc2, Tl) and Tc<= Tc2 and Tc2 <= Tc+10 and Tl = 10) neighbor_axiom: Axiom link (S, D, Tc, 10) => link (D, S, Tc, 10) link_pongMsg: lemma link (S, D, Tc, 10) => (exists (Tp: Time): pongMsg (S, Tp) and Tc <= Tp and Tp <= Tc+10) link_pingRTT: lemma link (S, D, Tc, 10) => (exists (RTT, Tp, Tl: Time): pingRTT (S, D, RTT, Tp, Tl) and Tc <= Tp and Tp <= Tc+10) % invariant 1 pingMsg_link: lemma pingMsg (S, D, 3) => (exists (t: Time): link (S, D, t, 10) and t<= 3 and 3 <= t+10) pongMsg_link: lemma pongMsg (S, 3) => (exists (t: Time) (D: Node): link (S, D, t, 10) and t<= 3 and 3 <= t+10) pongMsg_link_general: lemma forall (Tc: Time): pongMsg (S, Tc) => (exists (t: Time) (D: Node): link (S, D, t, 10) and t<= Tc and Tc <= t+10) pingRTT_pongMst: Lemma forall (S, D: Node) (RTT, Tc, Tl: Time): pingRTT (S, D, RTT, Tc, Tl) => pongMsg (S, Tc) pingRTT_link: Theorem forall (S, D: Node) (RTT, Tc, Tl: Time): pingRTT (S, D, RTT, Tc, Tl) => (exists (t: Time) (D: Node): link (S, D, t, 10) and t<= Tc and Tc <= t+10) % pendingPing is irrelevant in this proof END pingPong $$$pingPong.prf (pingPong (p_test1 0 (p_test1-1 nil 3426107660 3426107664 ("" (expand periodic) (("" (propax) nil nil)) nil) unchecked ((periodic inductive-decl "bool" pingPong nil)) 3446 20 t shostak)) (p_test2 0 (p_test2-1 nil 3426113758 3426113791 ("" (skolem!) (("" (expand periodic) (("" (lemma periodic_axiom) (("" (inst 1 1) (("" (grind) nil nil)) nil)) nil)) nil)) nil) unchecked ((periodic inductive-decl "bool" pingPong nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Time type-eq-decl nil pingPong nil) (Node type-eq-decl nil pingPong nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (periodic_axiom formula-decl nil pingPong nil)) 32443 190 t shostak)) (p_test_general 0 (p_test_general-1 nil 3426112167 3426113243 ("" (skolem!) (("" (skolem!) (("" (induct "i") (("1" (grind) nil nil) ("2" (skolem!) (("2" (prop) (("2" (expand periodic 1) (("2" (inst 1 "j!1 * p!1 + t!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (periodic inductive-decl "bool" pingPong nil) (Time type-eq-decl nil pingPong nil) (Node type-eq-decl nil pingPong nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) 1076387 710 t shostak)) (p_general 0 (p_general-1 nil 3426113920 3426113991 ("" (skolem!) (("" (lemma p_test_general) (("" (use periodic_axiom) (("" (grind) nil nil)) nil)) nil)) nil) unchecked ((p_test_general formula-decl nil pingPong nil) (Time type-eq-decl nil pingPong nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Node type-eq-decl nil pingPong nil) (periodic_axiom formula-decl nil pingPong nil)) 71358 450 t shostak)) (link_periodic 0 (link_periodic-1 nil 3426113435 3426115790 ("" (skolem!) (("" (prop) (("" (lemma p_general) (("" (delete -2) (("" (inst 1 "(ceiling ((t!1-1)/5))*5+1") (("1" (prop) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) unchecked ((p_general formula-decl nil pingPong nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (Time type-eq-decl nil pingPong nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (Node type-eq-decl nil pingPong nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 1696289 1620 t shostak)) (link_ping 0 (link_ping-1 nil 3426121928 3426124756 ("" (skolem!) (("" (prop) (("" (lemma link_periodic) (("" (instantiate -1 ("D!1" "S!1" "Tc!1")) (("" (prop) (("" (skolem!) (("" (inst 1 "tp!1") (("" (prop) (("" (expand ping) (("" (inst 1 "Tc!1") (("" (prop) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((link_periodic formula-decl nil pingPong nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Node type-eq-decl nil pingPong nil) (Time type-eq-decl nil pingPong nil) (ping inductive-decl "bool" pingPong nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) 1035 160 t shostak)) (link_pingMsg 0 (link_pingMsg-1 nil 3426121035 3426124763 ("" (skolem!) (("" (prop) (("" (lemma link_periodic) (("" (instantiate -1 ("D!1" "S!1" "Tc!1")) (("" (prop) (("" (skolem!) (("" (prop) (("" (inst 1 tp!1) (("" (prop) (("" (expand pingMsg) (("" (inst 1 "Tc!1") (("" (prop) (("1" (expand ping) (("1" (inst 1 "Tc!1") (("1" (prop) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((link_periodic formula-decl nil pingPong nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Node type-eq-decl nil pingPong nil) (Time type-eq-decl nil pingPong nil) (ping inductive-decl "bool" pingPong nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (pingMsg inductive-decl "bool" pingPong nil)) 1030 190 t shostak)) (link_pendingPing 0 (link_pendingPing-1 nil 3426122425 3426124769 ("" (skolem!) (("" (prop) (("" (lemma link_ping) (("" (instantiate -1 ("D!1" "S!1" "Tc!1")) (("" (prop) (("" (skolem!) (("" (prop) (("" (expand pendingPing) (("" (inst 1 "Tc2!1" "Tc2!1" 10) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((link_ping formula-decl nil pingPong nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Node type-eq-decl nil pingPong nil) (Time type-eq-decl nil pingPong nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pendingPing inductive-decl "bool" pingPong nil)) 719 120 t shostak)) (link_pongMsg 0 (link_pongMsg-1 nil 3426122876 3426124779 ("" (skolem!) (("" (prop) (("" (lemma link_pingMsg) (("" (instantiate -1 ("D!1" "S!1" "Tc!1")) (("" (prop) (("" (skolem!) (("" (prop) (("" (expand pongMsg) (("" (inst 1 "Tp!1") (("" (copy -1) (("" (expand pingMsg -1) (("" (skolem!) (("" (lemma neighbor_axiom) (("" (instantiate -1 ("D!1" "S!1" "Tc2!1")) (("" (prop) (("1" (inst 1 "D!1" "Tc2!1") (("1" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((link_pingMsg formula-decl nil pingPong nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Node type-eq-decl nil pingPong nil) (Time type-eq-decl nil pingPong nil) (pingMsg inductive-decl "bool" pingPong nil) (neighbor_axiom formula-decl nil pingPong nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (pongMsg inductive-decl "bool" pingPong nil)) 1011 230 t shostak)) (link_pingRTT 0 (link_pingRTT-1 nil 3426123684 3426329967 ("" (skolem!) (("" (prop) (("" (lemma link_pongMsg) (("" (lemma link_pendingPing) (("" (instantiate -2 ("D!1" "S!1" "Tc!1")) (("" (prop) (("" (skolem!) (("" (prop) (("" (instantiate -4 ("D!1" "S!1" "Tc!1")) (("" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 204595221 110 t shostak)) (pingMsg_link 0 (pingMsg_link-1 nil 3426118834 3426118952 ("" (skolem!) (("" (prop) (("" (expand pingMsg) (("" (skolem!) (("" (prop) (("" (inst 1 Tc2!1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Time type-eq-decl nil pingPong nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pingMsg inductive-decl "bool" pingPong nil)) 118850 130 t shostak)) (pongMsg_link 0 (pongMsg_link-1 nil 3426119065 3426119141 ("" (skolem!) (("" (prop) (("" (expand pongMsg) (("" (skolem!) (("" (skosimp*) (("" (expand pingMsg) (("" (skosimp*) (("" (inst 1 "Tc2!2" "D!1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((pingMsg inductive-decl "bool" pingPong nil) (Node type-eq-decl nil pingPong nil) (Time type-eq-decl nil pingPong nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pongMsg inductive-decl "bool" pingPong nil)) 76598 190 t shostak)) (pongMsg_link_general 0 (pongMsg_link_general-1 nil 3426119777 3426119836 ("" (skolem!) (("" (prop) (("" (expand pongMsg) (("" (skosimp*) (("" (expand pingMsg) (("" (skosimp*) (("" (inst 1 "Tc2!2" "D!1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Time type-eq-decl nil pingPong nil) (Node type-eq-decl nil pingPong nil) (pingMsg inductive-decl "bool" pingPong nil) (pongMsg inductive-decl "bool" pingPong nil)) 58812 240 t shostak)) (pingRTT_pongMst 0 (pingRTT_pongMst-1 nil 3426119411 3426119428 ("" (skosimp*) (("" (expand pingRTT) (("" (grind) nil nil)) nil)) nil) unchecked ((minus_odd_is_odd application-judgement "odd_int" integers nil) (pingRTT inductive-decl "bool" pingPong nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Time type-eq-decl nil pingPong nil) (NOT const-decl "[bool -> bool]" booleans nil)) 17780 170 t shostak)) (pingRTT_link 0 (pingRTT_link-1 nil 3426119852 3426125063 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (lemma pingRTT_pongMst) (("" (lemma pongMsg_link_general) (("" (instantiate -2 ("S!1" "D!1" "RTT!1" "Tc!1" "Tl!1")) (("" (instantiate -1 ("S!1" "Tc!1")) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((pongMsg_link_general formula-decl nil pingPong nil) (Time type-eq-decl nil pingPong nil) (Node type-eq-decl nil pingPong nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (pingRTT_pongMst formula-decl nil pingPong nil)) 705 40 t shostak)))