%% 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) $$$eventDV.pvs % 2008/08/12 20:53:48 % event-based DV suffers from count-to-infinity % 1) if the network is stable, the distance vectors computes by the rules converges % 2) if link fails, (in a 4-node network), count-to-infinity occurs NDlogRule: THEORY BEGIN Node: TYPE = posnat Time: TYPE = nat Cost: TYPE = posnat S, D, Z: VAR Node C, MIN_C: VAR Cost period, Tc, Tp, Tl, MAX_Tc: VAR Time a, b, c, e: Node linkInput (S,D,C,Tc): INDUCTIVE bool = exists (j: posnat): (S = a and D = b and C = 1 and Tc = j*5+1) or (S = b and D = a and C = 1 and Tc = j*5+1) or (S = a and D = c and C = 1 and Tc = j*5+1) or (S = c and D = a and C = 1 and Tc = j*5+1) or (S = a and D = e and C = 1 and Tc = j*5+1) or (S = e and D = a and C = 1 and Tc = j*5+1) or (S = b and D = c and C = 1 and Tc = j*5+1) or (S = c and D = b and C = 1 and Tc = j*5+1) bestHop: [Node, Node, Node, Cost, Time -> bool] periodic (S, period, Tc): INDUCTIVE bool = EXISTS (Tc2: Time): periodic (S, period, Tc2) AND (Tc = Tc2 + period) link (S,D,C,Tp): INDUCTIVE bool = EXISTS (T: Time): linkInput (S, D, C, T) and Tp-5< T and T<= Tp hopMsg (S,D,Z,C,Tp): INDUCTIVE bool = (EXISTS (Tp2: Time): bestHop (S,D,Z,C,Tp2) and Tp = Tp2+5) hop (S, D, Z, C, Tp): INDUCTIVE bool = (link (S,D,C,Tp) and Z=D) OR (EXISTS (C1, C2: Cost) (W: Node): link (S,Z,C1,Tp) and hopMsg (Z,D,W,C2,Tp) and C=C1+C2) bestHopCost (S,D,MIN_C, Tp): INDUCTIVE bool = (EXISTS (Z: Node): hop(S, D, Z, MIN_C, Tp)) AND (FORALL (C: Cost): (EXISTS (Z: Node): hop(S, D, Z, C, Tp)) => MIN_C <= C) bestHop_refresh: Axiom forall (S,D,Z: Node) (C: Cost) (Tp: Time): bestHopCost (S,D,C,Tp) and hop (S,D,Z,C,Tp) => bestHop (S,D,Z,C,Tp) periodic_axiom: axiom forall (S: Node): periodic (S, 5, 0) 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, 5*i) link_general: Theorem forall (S,D: Node) (C: Cost) (t:Time) (i: nat): linkInput (S,D,C,t) and (5*i-5 link (S,D,C,5*i) END NDlogRule stableConvergen: THEORY BEGIN importing NDlogRule hop_ab_1: lemma linkInput (a, e, 1, 1) and linkInput (b, a, 1, 6) => hop (b, e, a, 2, 10) hopBest_be_1: lemma linkInput (a, e, 1, 1) and linkInput (b, a, 1, 6) => bestHop (b, e, a, 2, 10) node_disjoint: axiom (not (a = b)) and (not (a = c)) and (not (a = e)) and (not (b = c)) and (not (b = e)) and (not (c = e)) j: posnat stable_state: axiom bestHop (a, b, b, 1, 5*j) and bestHop (b, a, a, 1, 5*j) and bestHop (a, c, c, 1, 5*j) and bestHop (c, a, a, 1, 5*j) and bestHop (b, c, c, 1, 5*j) and bestHop (c, b, b, 1, 5*j) and bestHop (a, e, e, 1, 5*j) and bestHop (e, a, a, 1, 5*j) and bestHop (b, e, a, 2, 5*j) and bestHop (e, b, a, 2, 5*j) and bestHop (c, e, a, 2, 5*j) and bestHop (e, c, a, 2, 5*j) bestHop_primaryKey: axiom forall (S, D: Node) (Z1, Z2: Node) (C1, C2: Node) (T: Time): bestHop (S, D, Z1, C1, T) and bestHop (S, D, Z2, C2, T) => (C1 = C2 and Z1= Z2) linkInput_symmetry: axiom forall (S, D: Node) (C: Cost) (Tc: Time): linkInput (S,D,C,Tc) => linkInput (D,S,C,Tc) bestHopCost_be: lemma bestHopCost (b, e, 2, 5*j+5) bestHopCost_ab: lemma bestHopCost (a, b, 1, 5*j+5) bestHopCost_ac: lemma bestHopCost (a, c, 1, 5*j+5) bestHopCost_ae: lemma bestHopCost (a, e, 1, 5*j+5) bestHopCost_bc: lemma bestHopCost (b, c, 1, 5*j+5) bestHopCost_ce: lemma bestHopCost (c, e, 2, 5*j+5) bestHopCost_symmetry: axiom forall (S, D: Node) (C: Cost) (Tp: Time): bestHopCost (S, D, C, Tp) => bestHopCost (D, S, C, Tp) bestHopCost_step: axiom forall (S, D: Node) (C: Cost) (i: posnat): (i>=j) => bestHopCost (S, D, C, 5*i) = bestHopCost (S, D, C, 5*i+5) bestHopCost_stable: theorem forall (S, D: Node) (C: Cost) (i: posnat): (i> j) => bestHopCost (S, D, C, 5*i) = bestHopCost (S, D, C, 5*j) END stableConvergen %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DV_linkFail: THEORY BEGIN Node: TYPE = posnat Time: TYPE = nat Cost: TYPE = posnat S, D, Z: VAR Node C, MIN_C: VAR Cost period, Tc, Tp, Tl, MAX_Tc: VAR Time a, b, c, e: Node linkInput (S,D,C,Tc): INDUCTIVE bool = (exists (j: posnat): (S = a and D = b and C = 1 and Tc = j*5+1 and j<=19)) OR (exists (j: posnat): (S = b and D = a and C = 1 and Tc = j*5+1 and j<=19)) OR (exists (j: posnat): (S = a and D = c and C = 1 and Tc = j*5+1 and j<=19)) or (exists (j: posnat): (S = c and D = a and C = 1 and Tc = j*5+1 and j<=19)) or (exists (j: posnat): (S = a and D = e and C = 1 and Tc = j*5+1 and j<=19)) or (exists (j: posnat): (S = e and D = a and C = 1 and Tc = j*5+1 and j<=19)) or (exists (j: posnat): (S = b and D = c and C = 1 and Tc = j*5+1 and j<=19)) or (exists (j: posnat): (S = c and D = b and C = 1 and Tc = j*5+1 and j<=19)) or %% (exists (j: posnat): (S = a and D = b and C = 1 and Tc = j*5+1 and j>=20)) or (exists (j: posnat): (S = b and D = a and C = 1 and Tc = j*5+1 and j>=20)) or (exists (j: posnat): (S = a and D = c and C = 1 and Tc = j*5+1 and j>=20)) or (exists (j: posnat): (S = c and D = a and C = 1 and Tc = j*5+1 and j>=20)) or (exists (j: posnat): (S = b and D = c and C = 1 and Tc = j*5+1 and j>=20)) or (exists (j: posnat): (S = c and D = b and C = 1 and Tc = j*5+1 and j>=20)) % (S = a and D = e and C = 1 and Tc = j*5+1 and j<=100) or % (S = e and D = a and C = 1 and Tc = j*5+1 and j<=100) or bestHop: [Node, Node, Node, Cost, Time -> bool] periodic (S, period, Tc): INDUCTIVE bool = EXISTS (Tc2: Time): periodic (S, period, Tc2) AND (Tc = Tc2 + period) link (S,D,C,Tp): INDUCTIVE bool = EXISTS (T: Time): linkInput (S, D, C, T) and Tp-5< T and T<= Tp hopMsg (S,D,Z,C,Tp): INDUCTIVE bool = (EXISTS (Tp2: Time): bestHop (S,D,Z,C,Tp2) and Tp = Tp2+5) hop (S, D, Z, C, Tp): INDUCTIVE bool = (link (S,D,C,Tp) and Z=D) OR (EXISTS (C1, C2: Cost) (W: Node): link (S,Z,C1,Tp) and hopMsg (Z,D,W,C2,Tp) and C=C1+C2) bestHopCost (S,D,MIN_C, Tp): INDUCTIVE bool = (EXISTS (Z: Node): hop(S, D, Z, MIN_C, Tp)) AND (FORALL (C: Cost): (EXISTS (Z: Node): hop(S, D, Z, C, Tp)) => MIN_C <= C) bestHop_refresh: Axiom forall (S,D,Z: Node) (C: Cost) (Tp: Time): bestHopCost (S,D,C,Tp) and hop (S,D,Z,C,Tp) => bestHop (S,D,Z,C,Tp) bestHop_close: Axiom forall (S,D,Z: Node) (C: Cost) (Tp: Time): bestHop (S,D,Z,C,Tp) and Tp>10 => bestHopCost (S,D,C,Tp) and hop (S,D,Z,C,Tp) periodic_axiom: axiom forall (S: Node): periodic (S, 5, 0) 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, 5*i) link_general: Theorem forall (S,D: Node) (C: Cost) (t:Time) (i: nat): linkInput (S,D,C,t) and (5*i-5 link (S,D,C,5*i) END DV_linkFail diverge_linkFail: THEORY BEGIN importing DV_linkFail hopBest_be_1: lemma linkInput (a, e, 1, 1) and linkInput (b, a, 1, 6) => bestHop (b, e, a, 2, 10) node_disjoint: axiom (not (a = b)) and (not (a = c)) and (not (a = e)) and (not (b = c)) and (not (b = e)) and (not (c = e)) distanceVectorAt100: axiom bestHop (a, b, b, 1, 100) and bestHop (b, a, a, 1, 100) and bestHop (a, c, c, 1, 100) and bestHop (c, a, a, 1, 100) and bestHop (b, c, c, 1, 100) and bestHop (c, b, b, 1, 100) and bestHop (a, e, e, 1, 100) and bestHop (e, a, a, 1, 100) and bestHop (b, e, a, 2, 100) and bestHop (e, b, a, 2, 100) and bestHop (c, e, a, 2, 100) and bestHop (e, c, a, 2, 100) linkInput_symmetry: axiom forall (S, D: Node) (C: Cost) (Tc: Time): linkInput (S,D,C,Tc) => linkInput (D,S,C,Tc) bestHop_primaryKey: axiom forall (S, D: Node) (Z1, Z2: Node) (C1, C2: Node) (T: Time): bestHop (S, D, Z1, C1, T) and bestHop (S, D, Z2, C2, T) => (C1 = C2 and Z1= Z2) hop_be_3: lemma hop (b, e, c, 3, 105) hop_be_2: lemma hop (b, e, a, 2, 105) bestHop_be_2: Theorem bestHop (b, e, a, 2, 105) hop_be_2at100: lemma not hop (b, e, a, 2, 110) hop_ae_2at110: lemma not hop (a, e, e, 1, 110) hop_ae_3at110: lemma hop (a, e, b, 3, 110) bestHop_ae_3at110: Theorem bestHop (a, e, b, 3, 110) hop_contradict_link: theorem exists (t: Time): (not (link (a, e, 1, t) and link (b, e, 1, t) and link (c, e, 1, t))) and hop (a, e, b, 3, t) hop_be2ae_increase: Theorem forall (t: Time) (c: Cost): (exists (i: posnat): t = i*5 and t>100) and bestHop (b, e, a, c, t) => hop (a, e, b, c+1, t+5) hop_ae2be_increase: Theorem forall (t: Time) (c: Cost): (exists (i: posnat): t = i*5 and t>100) and bestHop (a, e, b, c, t) => hop (b, e, a, c+1, t+5) hop_ae_best: axiom forall (c: Cost) (t: Time): t>100 and hop (a, e, b, c, t) => bestHop (a, e, b, c, t) hop_be_best: axiom forall (c: Cost) (t: Time): t>100 and hop (b, e, a, c, t) => bestHop (b, e, a, c, t) bestHop_ae2be_increase: theorem forall (t: Time) (c: Cost): (exists (i: posnat): t = i*5 and t>100) and bestHop (a, e, b, c, t) => bestHop (b, e, a, c+1, t+5) bestHop_be2ae_increase: Axiom forall (t: Time) (c: Cost): (exists (i: posnat): t = i*5 and t>100) and bestHop (b, e, a, c, t) => bestHop (a, e, b, c+1, t+5) bestHop_ae_increase_to_infinity: Theorem forall (t: Time) (c: Cost): (exists (i: posnat): t = i*5 and t>100) => (bestHop (a, e, b, c, t) => bestHop (a, e, b, c+2, t+10)) bestHop_be_increase_to_infinity: Theorem forall (t: Time) (c: Cost): (exists (i: posnat): t = i*5 and t>100) => (bestHop (b, e, a, c, t) => bestHop (b, e, a, c+2, t+10)) END diverge_linkFail $$$eventDV.prf (NDlogRule (p_test_general 0 (p_test_general-1 nil 3427349645 3427468321 ("" (skolem!) (("" (skolem!) (("" (induct i) (("1" (prop) (("1" (grind) nil nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (expand periodic 1) (("2" (inst 1 "t!1 + p!1 * j!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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" NDlogRule nil) (Time type-eq-decl nil NDlogRule nil) (Node type-eq-decl nil NDlogRule 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) 344 260 t shostak)) (p_general 0 (p_general-1 nil 3427350243 3427468322 ("" (skolem!) (("" (lemma p_test_general) (("" (use periodic_axiom) (("" (grind) nil nil)) nil)) nil)) nil) proved ((p_test_general formula-decl nil NDlogRule nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Time type-eq-decl nil NDlogRule 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 NDlogRule nil) (periodic_axiom formula-decl nil NDlogRule nil)) 240 170 t shostak)) (link_general 0 (link_general-1 nil 3427350317 3427468322 ("" (skosimp*) (("" (expand link) (("" (inst 1 t!1) (("" (grind) nil nil)) nil)) nil)) nil) proved ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (link inductive-decl "bool" NDlogRule nil) (Time type-eq-decl nil NDlogRule 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)) 124 90 t shostak))) (stableConvergen (hop_ab_1 0 (hop_ab_1-1 nil 3427427434 3427468322 ("" (prop) (("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 1 e) (("1" (prop) (("1" (expand link) (("1" (inst 1 6) (("1" (grind) nil nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 5) (("2" (grind) (("2" (lemma bestHop_refresh) (("2" (instantiate -1 ("a" "e" "e" "1" "5")) (("2" (prop) (("1" (expand bestHopCost) (("1" (inst 1 e) (("1" (expand hop) (("1" (expand link) (("1" (inst 1 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hop) (("2" (expand link) (("2" (inst 1 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 1 e) (("2" (grind) (("1" (expand hopMsg) (("1" (inst 1 5) (("1" (grind) (("1" (lemma bestHop_refresh) (("1" (instantiate -1 ("a" "e" "e" "1" "5")) (("1" (prop) (("1" (expand bestHopCost) (("1" (inst 1 e) (("1" (expand hop) (("1" (expand link) (("1" (inst 1 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hop) (("2" (expand link) (("2" (inst 1 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand link) (("2" (inst 1 6) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((hop inductive-decl "bool" NDlogRule nil) (Time type-eq-decl nil NDlogRule nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (link inductive-decl "bool" NDlogRule nil) (bestHop_refresh formula-decl nil NDlogRule nil) (a const-decl "Node" NDlogRule nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hopMsg inductive-decl "bool" NDlogRule 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) (Cost type-eq-decl nil NDlogRule nil) (Node type-eq-decl nil NDlogRule nil) (e const-decl "Node" NDlogRule nil)) 514 320 t shostak)) (hopBest_be_1 0 (hopBest_be_1-1 nil 3427452244 3427468323 ("" (prop) (("" (lemma bestHop_refresh) (("" (instantiate -1 ("b" "e" "a" "2" "10")) (("" (prop) (("1" (expand bestHopCost) (("1" (prop) (("1" (inst 1 a) (("1" (lemma hop_ab_1) (("1" (grind) nil nil)) nil)) nil) ("2" (skolem!) (("2" (delete 2) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (expand link) (("1" (skosimp*) (("1" (expand linkInput) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand link) (("2" (skosimp*) (("2" (expand linkInput) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma hop_ab_1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((bestHop_refresh formula-decl nil NDlogRule 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 NDlogRule nil) (b const-decl "Node" NDlogRule nil) (e const-decl "Node" NDlogRule nil) (a const-decl "Node" NDlogRule nil) (Cost type-eq-decl nil NDlogRule nil) (Time type-eq-decl nil NDlogRule nil) (hop_ab_1 formula-decl nil stableConvergen nil) (linkInput inductive-decl "bool" NDlogRule nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (link inductive-decl "bool" NDlogRule nil) (hop inductive-decl "bool" NDlogRule nil) (bestHopCost inductive-decl "bool" NDlogRule nil)) 290 210 t shostak)) (bestHopCost_be 0 (bestHopCost_be-1 nil 3427351243 3427468324 ("" (expand bestHopCost) (("" (prop) (("1" (inst 1 a) (("1" (expand hop) (("1" (prop) (("1" (inst 2 1 1 e) (("1" (delete 1) (("1" (prop) (("1" (expand link) (("1" (inst 1 "5*j+1") (("1" (grind) (("1" (lemma linkInput_symmetry) (("1" (instantiate -1 ("a" "b" "1" "1+5*j")) (("1" (prop) (("1" (delete 2) (("1" (expand linkInput) (("1" (inst 1 "j") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 5*j) (("2" (lemma stable_state) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 1 e) (("2" (prop) (("1" (lemma link_general) (("1" (instantiate -1 ("b" "a" "1" "5*j+1" "j+1")) (("1" (prop) (("1" (grind) nil nil) ("2" (use linkInput_symmetry) (("2" (prop) (("2" (expand linkInput 1) (("2" (inst 1 j) nil nil)) nil)) nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 5*j) (("2" (lemma stable_state) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (expand hop) (("2" (prop) (("2" (expand hopMsg) (("2" (grind) (("2" (expand link) (("2" (skosimp*) (("2" (lemma linkInput_symmetry) (("2" (instantiate -1 ("b" "e" "C!1" "T!1")) (("2" (prop) (("2" (expand linkInput -1) (("2" (skosimp* -1) (("2" (prop) (("1" (lemma node_disjoint) (("1" (grind) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (grind) nil nil)) nil) ("3" (lemma node_disjoint) (("3" (grind) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (grind) nil nil)) nil) ("5" (lemma node_disjoint) (("5" (grind) nil nil)) nil) ("6" (lemma node_disjoint) (("6" (grind) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (grind) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((hop inductive-decl "bool" NDlogRule nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (link_general formula-decl nil NDlogRule nil) (e const-decl "Node" NDlogRule nil) (Cost type-eq-decl nil NDlogRule nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (j const-decl "posnat" stableConvergen nil) (posnat nonempty-type-eq-decl nil integers 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) (Time type-eq-decl nil NDlogRule nil) (linkInput_symmetry formula-decl nil stableConvergen nil) (b const-decl "Node" NDlogRule nil) (linkInput inductive-decl "bool" NDlogRule nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (link inductive-decl "bool" NDlogRule nil) (stable_state formula-decl nil stableConvergen nil) (hopMsg inductive-decl "bool" NDlogRule nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (a const-decl "Node" NDlogRule nil) (Node type-eq-decl nil NDlogRule 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) (node_disjoint formula-decl nil stableConvergen nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) 931 690 t shostak)) (bestHopCost_ab 0 (bestHopCost_ab-1 nil 3427355991 3427468324 ("" (expand bestHopCost) (("" (inst 1 b) (("" (expand hop) (("" (expand link) (("" (inst 1 5*j+1) (("" (prop) (("1" (expand linkInput) (("1" (inst 1 j) nil nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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 NDlogRule nil) (b const-decl "Node" NDlogRule nil) (link inductive-decl "bool" NDlogRule nil) (linkInput inductive-decl "bool" NDlogRule nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Time type-eq-decl nil NDlogRule nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (j const-decl "posnat" stableConvergen nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" NDlogRule nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) 179 140 t shostak)) (bestHopCost_ac 0 (bestHopCost_ac-1 nil 3427356095 3427468324 ("" (expand bestHopCost) (("" (inst 1 c) (("" (expand hop) (("" (expand link) (("" (inst 1 5*j+1) (("" (grind) (("" (expand linkInput) (("" (inst 1 j) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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 NDlogRule nil) (c const-decl "Node" NDlogRule nil) (link inductive-decl "bool" NDlogRule nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (linkInput inductive-decl "bool" NDlogRule nil) (Time type-eq-decl nil NDlogRule nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (j const-decl "posnat" stableConvergen nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" NDlogRule nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) 221 160 t shostak)) (bestHopCost_ae 0 (bestHopCost_ae-1 nil 3427356248 3427468324 ("" (expand bestHopCost) (("" (inst 1 e) (("" (expand hop) (("" (expand link) (("" (inst 1 5*j+1) (("" (grind) (("" (expand linkInput) (("" (inst 1 j) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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 NDlogRule nil) (e const-decl "Node" NDlogRule nil) (link inductive-decl "bool" NDlogRule nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (linkInput inductive-decl "bool" NDlogRule nil) (Time type-eq-decl nil NDlogRule nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (j const-decl "posnat" stableConvergen nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" NDlogRule nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) 189 160 t shostak)) (bestHopCost_bc 0 (bestHopCost_bc-1 nil 3427356329 3427468324 ("" (expand bestHopCost) (("" (inst 1 c) (("" (expand hop) (("" (expand link) (("" (inst 1 5*j+1) (("" (grind) (("" (expand linkInput) (("" (inst 1 j) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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 NDlogRule nil) (c const-decl "Node" NDlogRule nil) (link inductive-decl "bool" NDlogRule nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (linkInput inductive-decl "bool" NDlogRule nil) (Time type-eq-decl nil NDlogRule nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (j const-decl "posnat" stableConvergen nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" NDlogRule nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) 192 160 t shostak)) (bestHopCost_ce 0 (bestHopCost_ce-1 nil 3427356405 3427468325 ("" (expand bestHopCost) (("" (prop) (("1" (inst 1 a) (("1" (expand hop) (("1" (prop) (("1" (inst 2 1 1 e) (("1" (delete 1) (("1" (grind) (("1" (expand hopMsg) (("1" (inst 1 5*j) (("1" (lemma stable_state) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand link) (("2" (inst 1 5*j+1) (("2" (grind) (("2" (expand linkInput) (("2" (inst 1 j) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 1 e) (("2" (grind) (("1" (expand hopMsg) (("1" (inst 1 5*j) (("1" (lemma stable_state) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand link) (("2" (inst 1 5*j+1) (("2" (grind) (("2" (expand linkInput) (("2" (inst 1 j) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (expand hop) (("2" (expand hopMsg) (("2" (grind) (("2" (expand link) (("2" (skosimp*) (("2" (expand linkInput) (("2" (grind) (("1" (lemma node_disjoint) (("1" (grind) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (grind) nil nil)) nil) ("3" (lemma node_disjoint) (("3" (grind) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((hop inductive-decl "bool" NDlogRule nil) (e const-decl "Node" NDlogRule nil) (Cost type-eq-decl nil NDlogRule nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (j const-decl "posnat" stableConvergen nil) (posnat nonempty-type-eq-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Time type-eq-decl nil NDlogRule nil) (stable_state formula-decl nil stableConvergen nil) (hopMsg inductive-decl "bool" NDlogRule nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (linkInput inductive-decl "bool" NDlogRule nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (link inductive-decl "bool" NDlogRule nil) (a const-decl "Node" NDlogRule nil) (Node type-eq-decl nil NDlogRule 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) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (node_disjoint formula-decl nil stableConvergen nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) 1030 810 t shostak)) (bestHopCost_symmetry 0 (bestHopCost_symmetry-1 nil 3427356869 3427356941 ("" (skolem!) (("" (skolem!) (("" (skolem!) (("" (prop) (("" (postpone) nil nil)) nil)) nil)) nil)) nil) unchecked nil 71807 100 t shostak)) (bestHopCost_step 0 (bestHopCost_step-1 nil 3427360608 3427360618 ("" (postpone) nil nil) unchecked nil 9498 0 t shostak)) (bestHopCost_stable 0 (bestHopCost_stable-1 nil 3427355807 3427468326 ("" (skolem!) (("" (skolem!) (("" (induct i) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skolem!) (("3" (prop) (("1" (lemma bestHopCost_step) (("1" (instantiate -1 ("S!1" "D!1" "C!1" "j!1")) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ("2" (case "j!1=j") (("1" (replace -1) (("1" (lemma bestHopCost_step) (("1" (instantiate -1 ("S!1" "D!1" "C!1" "j")) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) proved ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (bestHopCost_step formula-decl nil stableConvergen nil) (j!1 skolem-const-decl "nat" stableConvergen nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (bestHopCost inductive-decl "bool" NDlogRule nil) (Time type-eq-decl nil NDlogRule nil) (Cost type-eq-decl nil NDlogRule nil) (Node type-eq-decl nil NDlogRule nil) (= const-decl "[T, T -> boolean]" equalities nil) (j const-decl "posnat" stableConvergen nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals 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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil)) 490 380 t shostak))) (DV_linkFail) (diverge_linkFail (hopBest_be_1 0 (hopBest_be_1-1 nil 3427453696 3427456967 ("" (prop) (("" (lemma bestHop_refresh) (("" (instantiate -1 (b e a 2 10)) (("" (prop) (("1" (delete 2) (("1" (expand bestHopCost) (("1" (prop) (("1" (inst 1 a) (("1" (expand hop) (("1" (prop) (("1" (delete 1) (("1" (inst 1 1 1 e) (("1" (grind) (("1" (expand hopMsg) (("1" (inst 1 5) (("1" (grind) (("1" (lemma bestHop_refresh) (("1" (instantiate -1 (a e e 1 5)) (("1" (prop) (("1" (delete 2) (("1" (expand bestHopCost) (("1" (inst 1 e) (("1" (expand hop) (("1" (expand link) (("1" (inst 1 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hop) (("2" (expand link) (("2" (inst 1 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand link) (("2" (inst 1 6) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 1 e) (("2" (grind) (("1" (expand hopMsg) (("1" (inst 1 5) (("1" (grind) (("1" (lemma bestHop_refresh) (("1" (instantiate -1 (a e e 1 5)) (("1" (grind) (("1" (expand hop) (("1" (expand link) (("1" (inst 1 1) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (expand bestHopCost) (("2" (inst 1 e) (("2" (expand hop) (("2" (expand link) (("2" (inst 1 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand link) (("2" (inst 1 6) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (expand link) (("1" (skosimp*) (("1" (expand linkInput) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (expand link) (("2" (skosimp*) (("2" (expand linkInput) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (expand hop) (("2" (prop) (("1" (delete 1) (("1" (inst 1 1 1 e) (("1" (prop) (("1" (expand link) (("1" (inst 1 6) (("1" (grind) nil nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 5) (("2" (grind) (("2" (use bestHop_refresh) (("2" (prop) (("1" (expand bestHopCost) (("1" (inst 1 e) (("1" (expand hop) (("1" (expand link) (("1" (inst 1 1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hop) (("2" (expand link) (("2" (inst 1 1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (ground) nil nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 1 e) (("2" (ground) (("1" (expand link) (("1" (inst 1 6) (("1" (ground) nil nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 5) (("2" (ground) (("2" (use bestHop_refresh) (("2" (prop) (("1" (expand bestHopCost) (("1" (inst 1 e) (("1" (expand hop) (("1" (expand link) (("1" (inst 1 1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hop) (("2" (expand link) (("2" (inst 1 1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((hop inductive-decl "bool" DV_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (link inductive-decl "bool" DV_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (linkInput inductive-decl "bool" DV_linkFail nil) (bestHopCost inductive-decl "bool" DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail nil) (a const-decl "Node" DV_linkFail nil) (e const-decl "Node" DV_linkFail nil) (b const-decl "Node" DV_linkFail nil) (Node type-eq-decl nil DV_linkFail 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) (bestHop_refresh formula-decl nil DV_linkFail nil)) 14005 1330 t shostak)) (hop_be_3 0 (hop_be_3-1 nil 3427455537 3427457264 ("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 2 a) (("1" (ground) (("1" (expand link) (("1" (inst 1 101) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 13 20) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 100) (("2" (ground) (("2" (use distanceVectorAt100) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 2 a) (("2" (ground) (("1" (expand link) (("1" (inst 1 101) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 13 20) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 100) (("2" (ground) (("2" (use distanceVectorAt100) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((a const-decl "Node" DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail 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) (hopMsg inductive-decl "bool" DV_linkFail nil) (distanceVectorAt100 formula-decl nil diverge_linkFail nil) (link inductive-decl "bool" DV_linkFail nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_times_even_is_even application-judgement "even_int" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (linkInput inductive-decl "bool" DV_linkFail nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (Time type-eq-decl nil DV_linkFail nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" DV_linkFail nil)) 116693 1060 t shostak)) (hop_be_2 0 (hop_be_2-1 nil 3427459779 3427459939 ("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 1 e) (("1" (prop) (("1" (expand link) (("1" (inst 1 101) (("1" (prop) (("1" (expand linkInput) (("1" (prop) (("1" (inst 10 20) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 100) (("2" (ground) (("2" (lemma distanceVectorAt100) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (ground) nil nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 1 e) (("2" (ground) (("1" (expand link) (("1" (inst 1 101) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 10 20) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 100) (("2" (ground) (("2" (lemma distanceVectorAt100) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((e const-decl "Node" DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail 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) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (distanceVectorAt100 formula-decl nil diverge_linkFail nil) (link inductive-decl "bool" DV_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_times_even_is_even application-judgement "even_int" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (linkInput inductive-decl "bool" DV_linkFail nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Time type-eq-decl nil DV_linkFail nil) (hop inductive-decl "bool" DV_linkFail nil)) 160286 980 t shostak)) (bestHop_be_2 0 (bestHop_be_2-1 nil 3427460123 3427460402 ("" (use bestHop_refresh) (("" (prop) (("1" (delete 2) (("1" (expand bestHopCost) (("1" (prop) (("1" (inst 1 a) (("1" (use hop_be_2) nil nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (expand link) (("1" (skosimp*) (("1" (expand linkInput) (("1" (prop) (("1" (skosimp*) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (ground) nil nil)) nil) ("6" (skosimp*) (("6" (ground) nil nil)) nil) ("7" (skosimp*) (("7" (ground) nil nil)) nil) ("8" (skosimp*) (("8" (ground) nil nil)) nil) ("9" (skosimp*) (("9" (ground) (("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil)) nil)) nil) ("10" (skosimp*) (("10" (ground) (("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil)) nil)) nil) ("11" (skosimp*) (("11" (lemma node_disjoint) (("11" (ground) nil nil)) nil)) nil) ("12" (skosimp*) (("12" (ground) (("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil)) nil)) nil) ("13" (skosimp*) (("13" (lemma node_disjoint) (("13" (ground) nil nil)) nil)) nil) ("14" (skosimp*) (("14" (lemma node_disjoint) (("14" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand link) (("2" (skosimp*) (("2" (expand linkInput) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma hop_be_2) (("2" (propax) nil nil)) nil)) nil)) nil) unchecked ((bestHopCost inductive-decl "bool" DV_linkFail nil) (node_disjoint formula-decl nil diverge_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (linkInput inductive-decl "bool" DV_linkFail nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (link inductive-decl "bool" DV_linkFail nil) (hop inductive-decl "bool" DV_linkFail nil) (hop_be_2 formula-decl nil diverge_linkFail 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 DV_linkFail nil) (b const-decl "Node" DV_linkFail nil) (e const-decl "Node" DV_linkFail nil) (a const-decl "Node" DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (bestHop_refresh formula-decl nil DV_linkFail nil)) 279087 2230 t shostak)) (hop_be_2at100 0 (hop_be_2at100-1 nil 3427460464 3427461588 ("" (expand hop) (("" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (delete -1) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (use bestHop_close) (("2" (prop) (("1" (expand hop) (("1" (prop) (("1" (expand link) (("1" (skosimp*) (("1" (expand linkInput) (("1" (prop) (("1" (skosimp*) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (replace -1) (("5" (delete -1) (("5" (replace -5) (("5" (delete -5) (("5" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil)) nil) ("7" (skosimp*) (("7" (lemma node_disjoint) (("7" (ground) nil nil)) nil)) nil) ("8" (skosimp*) (("8" (lemma node_disjoint) (("8" (ground) nil nil)) nil)) nil) ("9" (skosimp*) (("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil)) nil) ("10" (skosimp*) (("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil)) nil) ("11" (skosimp*) (("11" (lemma node_disjoint) (("11" (ground) nil nil)) nil)) nil) ("12" (skosimp*) (("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil)) nil) ("13" (lemma node_disjoint) (("13" (skosimp*) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand link) (("2" (skosimp*) (("2" (expand linkInput) (("2" (prop) (("1" (skosimp*) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (ground) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (skosimp*) nil nil)) nil) ("5" (skosimp*) (("5" (ground) nil nil)) nil) ("6" (lemma node_disjoint) (("6" (skosimp*) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (skosimp*) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (skosimp*) nil nil)) nil) ("9" (skosimp*) (("9" (ground) nil nil)) nil) ("10" (skosimp*) (("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil)) nil) ("11" (skosimp*) (("11" (ground) nil nil)) nil) ("12" (lemma node_disjoint) (("12" (skosimp*) nil nil)) nil) ("13" (lemma node_disjoint) (("13" (skosimp*) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((hop inductive-decl "bool" DV_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (bestHop_close formula-decl nil DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail nil) (e const-decl "Node" DV_linkFail nil) (a const-decl "Node" DV_linkFail nil) (Node type-eq-decl nil DV_linkFail 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (link inductive-decl "bool" DV_linkFail nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (linkInput inductive-decl "bool" DV_linkFail nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (node_disjoint formula-decl nil diverge_linkFail nil)) 405819 2500 t shostak)) (hop_ae_2at110 0 (hop_ae_2at110-1 nil 3427462308 3427462881 ("" (expand hop) (("" (expand link) (("" (skosimp*) (("" (expand linkInput) (("" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil) ("5" (ground) (("5" (skosimp*) (("5" (ground) nil nil)) nil)) nil) ("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (ground) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (ground) nil nil)) nil) ("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil) ("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil) ("11" (lemma node_disjoint) (("11" (ground) nil nil)) nil) ("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil) ("13" (lemma node_disjoint) (("13" (ground) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((link inductive-decl "bool" DV_linkFail nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (linkInput inductive-decl "bool" DV_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (node_disjoint formula-decl nil diverge_linkFail nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (hop inductive-decl "bool" DV_linkFail nil)) 96411 1380 t shostak)) (hop_ae_3at110 0 (hop_ae_3at110-1 nil 3427462938 3427463097 ("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 2 a) (("1" (ground) (("1" (expand link) (("1" (inst 1 106) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 9 21) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 105) (("2" (ground) (("2" (lemma bestHop_be_2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 2 a) (("2" (ground) (("1" (expand link) (("1" (inst 1 106) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 9 21) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 105) (("2" (ground) (("2" (use bestHop_be_2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((a const-decl "Node" DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail 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) (hopMsg inductive-decl "bool" DV_linkFail nil) (bestHop_be_2 formula-decl nil diverge_linkFail nil) (link inductive-decl "bool" DV_linkFail nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (linkInput inductive-decl "bool" DV_linkFail nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (Time type-eq-decl nil DV_linkFail nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" DV_linkFail nil)) 158896 1000 t shostak)) (bestHop_ae_3at110 0 (bestHop_ae_3at110-1 nil 3427463141 3427463975 ("" (use bestHop_refresh) (("" (ground) (("1" (delete 2) (("1" (expand bestHopCost) (("1" (prop) (("1" (inst 1 b) (("1" (use hop_ae_3at110) nil nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (expand link) (("1" (skosimp*) (("1" (expand linkInput) (("1" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil) ("5" (ground) (("5" (skosimp*) (("5" (ground) nil nil)) nil)) nil) ("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (ground) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (ground) nil nil)) nil) ("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil) ("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil) ("11" (lemma node_disjoint) (("11" (ground) nil nil)) nil) ("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil) ("13" (lemma node_disjoint) (("13" (ground) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand link) (("2" (skosimp*) (("2" (expand linkInput) (("2" (ground) (("1" (skosimp*) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (skosimp*) (("3" (ground) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil) ("5" (skosimp*) (("5" (ground) nil nil)) nil) ("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (ground) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (ground) nil nil)) nil) ("9" (skosimp*) (("9" (ground) (("9" (expand hopMsg) (("9" (skosimp*) (("9" (use bestHop_close) (("9" (prop) (("1" (expand hop) (("1" (prop) (("1" (replace -3) (("1" (delete -3) (("1" (replace -3) (("1" (delete -3) (("1" (expand link) (("1" (skosimp*) (("1" (expand linkInput) (("1" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil) ("5" (lemma node_disjoint) (("5" (ground) nil nil)) nil) ("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (ground) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (ground) nil nil)) nil) ("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil) ("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil) ("11" (lemma node_disjoint) (("11" (ground) nil nil)) nil) ("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil) ("13" (lemma node_disjoint) (("13" (ground) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil) ("11" (skosimp*) (("11" (replace -1) (("11" (delete -1) (("11" (ground) (("11" (expand hopMsg) (("11" (skosimp*) (("11" (use bestHop_close) (("11" (ground) (("11" (expand hop) (("11" (prop) (("11" (replace -3) (("11" (expand link) (("11" (skosimp*) (("11" (expand linkInput) (("11" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil) ("5" (lemma node_disjoint) (("5" (ground) nil nil)) nil) ("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (ground) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (ground) nil nil)) nil) ("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil) ("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil) ("11" (lemma node_disjoint) (("11" (ground) nil nil)) nil) ("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil) ("13" (lemma node_disjoint) (("13" (ground) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil) ("13" (lemma node_disjoint) (("13" (ground) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (expand hop) (("2" (prop) (("1" (delete 1) (("1" (inst 1 1 2 a) (("1" (ground) (("1" (expand link) (("1" (inst 1 106) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 9 21) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 105) (("2" (use bestHop_be_2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 2 a) (("2" (prop) (("1" (expand link) (("1" (inst 1 106) (("1" (prop) (("1" (expand linkInput) (("1" (prop) (("1" (inst 9 21) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 105) (("2" (ground) (("2" (use bestHop_be_2) nil nil)) nil)) nil)) nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((bestHopCost inductive-decl "bool" DV_linkFail nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (node_disjoint formula-decl nil diverge_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (linkInput inductive-decl "bool" DV_linkFail nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (link inductive-decl "bool" DV_linkFail nil) (c const-decl "Node" DV_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (bestHop_close formula-decl nil DV_linkFail nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (hop inductive-decl "bool" DV_linkFail nil) (hop_ae_3at110 formula-decl nil diverge_linkFail nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (bestHop_be_2 formula-decl nil diverge_linkFail 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 DV_linkFail nil) (a const-decl "Node" DV_linkFail nil) (e const-decl "Node" DV_linkFail nil) (b const-decl "Node" DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (bestHop_refresh formula-decl nil DV_linkFail nil)) 834322 6670 t shostak)) (hop_contradict_link 0 (hop_contradict_link-1 nil 3427464347 3427464530 ("" (inst 1 110) (("" (prop) (("1" (expand link -1) (("1" (skosimp*) (("1" (expand linkInput) (("1" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil) ("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil) ("5" (skosimp*) (("5" (ground) nil nil)) nil) ("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil) ("7" (lemma node_disjoint) (("7" (ground) nil nil)) nil) ("8" (lemma node_disjoint) (("8" (ground) nil nil)) nil) ("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil) ("10" (lemma node_disjoint) (("10" (ground) nil nil)) nil) ("11" (lemma node_disjoint) (("11" (ground) nil nil)) nil) ("12" (lemma node_disjoint) (("12" (ground) nil nil)) nil) ("13" (lemma node_disjoint) (("13" (ground) nil nil)) nil) ("14" (lemma node_disjoint) (("14" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use hop_ae_3at110) nil nil)) nil)) nil) unchecked ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (node_disjoint formula-decl nil diverge_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (linkInput inductive-decl "bool" DV_linkFail nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (link inductive-decl "bool" DV_linkFail nil) (hop_ae_3at110 formula-decl nil diverge_linkFail nil) (Time type-eq-decl nil DV_linkFail 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)) 91562 1450 t shostak)) (hop_be2ae_increase 0 (hop_be2ae_increase-1 nil 3427464903 3427465326 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (expand hop 1) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 c!1) (("1" (inst 1 a) (("1" (prop) (("1" (expand link) (("1" (skosimp* -1) (("1" (inst 1 i!1*5+1) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 9 i!1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 t!1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 c!1 a) (("2" (prop) (("1" (expand link) (("1" (skosimp* -1) (("1" (inst 1 i!1*5+1) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 9 i!1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 t!1) nil nil)) nil)) 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) (Cost type-eq-decl nil DV_linkFail nil) (NOT const-decl "[bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (linkInput inductive-decl "bool" DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (link inductive-decl "bool" DV_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (a const-decl "Node" DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (hop inductive-decl "bool" DV_linkFail nil)) 125874 980 t shostak)) (hop_ae2be_increase 0 (hop_ae2be_increase-1 nil 3427465449 3427465711 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (skosimp*) (("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 c!1 b) (("1" (prop) (("1" (expand link) (("1" (inst 1 i!1*5+1) (("1" (prop) (("1" (expand linkInput) (("1" (prop) (("1" (inst 9 i!1) (("1" (ground) (("1" (inst 10 i!1) (("1" (ground) nil nil)) nil) ("2" (inst 10 "i!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 t!1) nil nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 c!1 b) (("2" (prop) (("1" (expand link) (("1" (inst 1 i!1*5+1) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (ground 10 i!1) (("1" (inst 1 i!1) (("1" (inst 10 i!1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 t!1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((b const-decl "Node" DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail 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) (hopMsg inductive-decl "bool" DV_linkFail nil) (link inductive-decl "bool" DV_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (linkInput inductive-decl "bool" DV_linkFail nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Time type-eq-decl nil DV_linkFail nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" DV_linkFail nil)) 261567 1910 t shostak)) (bestHop_ae2be_increase 0 (bestHop_ae2be_increase-1 nil 3427466579 3427466874 ("" (lemma hop_ae2be_increase) (("" (lemma hop_ae_best) (("" (skolem!) (("" (skolem!) (("" (prop) (("" (instantiate -2 (t!1 c!1)) (("" (prop) (("" (delete -2) (("" (lemma hop_be_best) (("" (instantiate -1 (c!1+1 t!1+5)) (("" (prop) (("" (skosimp*) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((hop_ae_best formula-decl nil diverge_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (hop_be_best formula-decl nil diverge_linkFail nil) (Cost type-eq-decl nil DV_linkFail nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (Time type-eq-decl nil DV_linkFail 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) (hop_ae2be_increase formula-decl nil diverge_linkFail nil)) 295727 490 t shostak)) (bestHop_be2ae_increase 0 (bestHop_be2ae_increase-1 nil 3427468688 3427468693 ("" (postpone) nil nil) unchecked nil 4812 0 t shostak)) (bestHop_ae_increase_to_infinity 0 (bestHop_ae_increase_to_infinity-1 nil 3427473733 3427473976 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (skosimp*) (("" (use bestHop_be2ae_increase) (("" (prop) (("1" (grind) nil nil) ("2" (inst 1 i!1+1) (("2" (grind) nil nil)) nil) ("3" (delete 2) (("3" (use bestHop_ae2be_increase) (("3" (prop) (("1" (grind) nil nil) ("2" (inst 1 i!1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((int_plus_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posnat nonempty-type-eq-decl nil integers nil) (bestHop_ae2be_increase formula-decl nil diverge_linkFail nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "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) (Time type-eq-decl nil DV_linkFail nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Cost type-eq-decl nil DV_linkFail nil) (bestHop_be2ae_increase formula-decl nil diverge_linkFail nil)) 166265 620 t shostak)) (bestHop_be_increase_to_infinity 0 (bestHop_be_increase_to_infinity-1 nil 3427474007 3427474060 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (skosimp*) (("" (use bestHop_ae2be_increase) (("" (prop) (("1" (grind) nil nil) ("2" (inst 1 i!1+1) (("2" (grind) nil nil)) nil) ("3" (delete 2) (("3" (use bestHop_be2ae_increase) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((int_plus_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posnat nonempty-type-eq-decl nil integers nil) (bestHop_be2ae_increase formula-decl nil diverge_linkFail nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "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) (Time type-eq-decl nil DV_linkFail nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Cost type-eq-decl nil DV_linkFail nil) (bestHop_ae2be_increase formula-decl nil diverge_linkFail nil)) 52803 780 t shostak)))