%% 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 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)) 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 and (not W=S)) 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 converge_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_primaryKey: axiom forall (S, D, Z: Node) (T: Time) (C1, C2: Cost): (hop (S, D, Z, C1, T) and hop (S, D, Z, C2, T)) => C1=C2 link_e: lemma forall (i: posnat): i>=21 => not (exists (c: Cost) (z: Node): link (z, e, c, 5*i)) link_e_out: lemma forall (i: posnat): i>=21 => not (exists (c: Cost) (z: Node): link (e, z, c, 5*i)) %%%% at time 105 hop_be_2: lemma hop (b, e, a, 2, 105) bestHop_be_105: lemma bestHop (b, e, a, 2, 105) %%%% bestHop of b and e to destination e at 105 bestHop_105: axiom bestHop (b, e, a, 2, 105) and bestHop (c, e, a, 2, 105) hop_ae_110_2: lemma forall (c: Cost) (z: Node): not hop (a, e, z, c, 105) bestHop_ae_110_2: Theorem forall (c: Cost) (z: Node): not bestHop (a, e, z, c, 105) % hop_no_ae: THEOREM % forall (c: Cost) (z: Node) (t: Time): % (t>=110 and (exists (i: posnat): t = 5*i)) % => not hop (a, e, z, c, t) %%%% at time 110 hop_be_110_3: lemma hop (b, e, c, 3, 110) bestHop_be_110: lemma (forall (z: Node): z=a or z=b or z=c or z=e) => bestHop (b, e, c, 3, 110) bestHop_ceNbe_110: axiom bestHop (b, e, c, 3, 110) and bestHop (c, e, b, 3, 110) hop_ae_110: Theorem forall (z: Node): (z=b or z=c or z=e) => not (exists (c: Cost): hop (a, e, z, c, 110)) %%%% at time t>110 link_abc: axiom forall (t: Time): (exists (i: posnat): t=i*5) => link (a, b, 1, t) and link (a, c, 1, t) and link (b, a, 1, t) and link (c, a, 1, t) and link (b, c, 1, t) and link (c, b, 1, t) hop_ae_exist: Theorem forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (b, e, c, C, T-5) => hop (a, e, b, C+1, T) hop_ae_exist2: Axiom forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (c, e, b, C, T-5) => hop (a, e, c, C+1, T) link_close: Axiom forall (t: Time) (S, D: Node) (C: Cost): (t>110 and (exists (i: posnat): t=5*i)) and link (S, D, C, t) => C=1 and ((S=a and D=b) or (S=b and D=a) or (S=b and D=c) or (S=c and D=b) or (S=a and D=c) or (S=c and D=a)) bestHop_ae_t: Theorem forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (b, e, c, C, T-5) and bestHop (c, e, b, C, T-5) => bestHop (a, e, c, C+1, T) hop_be_exist: Theorem forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (a, e, c, C, T-5) => hop (b, e, a, C+1, T) hop_ce_exist: Axiom forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (a, e, b, C, T-5) => hop (c, e, a, C+1, T) bestHop_ce_exist: Theorem forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (a, e, b, C, T-5) and bestHop (a, e, c, C, T-5) and (forall (z: Node) (c: Cost): not (bestHop (b, e, z, c, T-5) or (bestHop (c, e, z, c, T-5)))) => bestHop (c, e, a, C+1, T) hop_be_exist2: Theorem forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (b, e, a, C, T-5) => hop (c, e, b, C+1, T) hop_ce_exist2: Axiom forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (c, e, a, C, T-5) => hop (b, e, c, C+1, T) bestHop_ce_exist2: Theorem forall (T: Time) (C: Cost): T>110 and (exists (i: posnat): T=i*5) and bestHop (c, e, a, C, T-5) and bestHop (b, e, a, C, T-5) and (forall (z: Node) (c: Cost): not bestHop (a, e, z, c, T-5)) => bestHop (c, e, b, C+1, T) END converge_linkFail $$$eventDV.prf (DV_linkFail) (converge_linkFail (hop_primaryKey 0 (hop_primaryKey-1 nil 3427563610 3427563615 ("" (postpone) nil nil) unchecked nil 5244 0 t shostak)) (link_e 0 (link_e-1 nil 3427583576 3427650453 ("" (skolem!) (("" (prop) (("" (skosimp*) (("" (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" (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)) nil)) nil)) nil) unchecked ((real_le_is_total_order name-judgement "(total_order?[real])" real_props 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (node_disjoint formula-decl nil converge_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (linkInput inductive-decl "bool" DV_linkFail nil) (link 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)) 2593 780 t shostak)) (link_e_out 0 (link_e_out-1 nil 3427584904 3427585764 ("" (skolem!) (("" (prop) (("" (skosimp*) (("" (lemma link_e) (("" (instantiate -1 i!1) (("" (prop) (("" (inst 1 c!1 z!1) (("" (expand link) (("" (skosimp*) (("" (inst 1 T!1) (("" (ground) (("" (use linkInput_symmetry) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((Node type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail nil) (real_ge_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) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (e const-decl "Node" DV_linkFail nil) (linkInput_symmetry formula-decl nil converge_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (link 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) (posnat nonempty-type-eq-decl nil integers 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) (link_e formula-decl nil converge_linkFail nil)) 869 160 t shostak)) (hop_be_2 0 (hop_be_2-1 nil 3427560615 3427561054 ("" (expand hop) (("" (flatten) (("" (delete 1) (("" (inst 1 1 1 e) (("" (split) (("1" (expand link) (("1" (inst 1 101) (("1" (grind) (("1" (expand linkInput) (("1" (flatten) (("1" (inst 10 20) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 100) (("2" (grind) (("2" (use distanceVectorAt100) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (grind) nil nil) ("4" (lemma node_disjoint) (("4" (ground) 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) (node_disjoint formula-decl nil converge_linkFail nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (distanceVectorAt100 formula-decl nil converge_linkFail nil) (link inductive-decl "bool" DV_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) (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) (Time type-eq-decl nil DV_linkFail nil) (hop inductive-decl "bool" DV_linkFail nil)) 438218 800 t shostak)) (bestHop_be_105 0 (bestHop_be_105-1 nil 3427650188 3427650718 ("" (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" (lemma link_e) (("1" (instantiate -1 (21)) (("1" (prop) (("1" (inst 1 C!1 b) (("1" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (use bestHop_close) (("2" (prop) (("1" (expand hop) (("1" (prop) (("1" (replace -2) (("1" (delete -2) (("1" (lemma link_e) (("1" (instantiate -1 Tp2!1/5) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use hop_be_2) nil nil)) nil)) nil) unchecked ((bestHop_refresh formula-decl nil 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) (hop_be_2 formula-decl nil converge_linkFail nil) (hop inductive-decl "bool" DV_linkFail nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bestHop_close formula-decl nil DV_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (link_e formula-decl nil converge_linkFail nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bestHopCost inductive-decl "bool" DV_linkFail nil)) 255664 820 t shostak)) (hop_ae_110_2 0 (hop_ae_110_2-1 nil 3427562027 3427571309 ("" (skolem!) (("" (skolem!) (("" (expand hop) (("" (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" (grind) nil nil) ("6" (grind) nil nil) ("7" (grind) nil nil) ("8" (grind) nil nil) ("9" (lemma node_disjoint) (("9" (ground) nil nil)) nil) ("10" (skosimp*) (("10" (lemma node_disjoint) (("10" (ground) nil 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" (prop) (("1" (skosimp*) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil) ("6" (grind) nil nil) ("7" (grind) nil nil) ("8" (grind) nil nil) ("9" (skosimp*) (("9" (replace -1) (("9" (delete -1) (("9" (replace -1) (("9" (delete -1) (("9" (expand hopMsg) (("9" (skosimp*) (("9" (use distanceVectorAt100) (("9" (prop) (("9" (delete (-1 -2 -3 -4 -5 -6 -7 -8 -10 -11 -12)) (("9" (assert) (("9" (use bestHop_primaryKey) (("9" (lemma bestHop_primaryKey) (("9" (instantiate -1 ("b" "e" "a" "W!1" "2" "C2!1" "Tp2!1")) (("9" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" (replace -1) (("11" (delete -1) (("11" (expand hopMsg) (("11" (skosimp*) (("11" (use bestHop_close) (("11" (prop) (("1" (expand hop) (("1" (prop) (("1" (replace -2) (("1" (delete -2) (("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) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (expand bestHopCost) (("2" (skosimp*) (("2" (instantiate -6 2) (("2" (prop) (("1" (use distanceVectorAt100) (("1" (prop) (("1" (delete (-1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -12)) (("1" (lemma bestHop_primaryKey) (("1" (instantiate -1 (c e W!1 a C2!1 2 100)) (("1" (prop) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 1 Z!1) (("2" (use distanceVectorAt100) (("2" (prop) (("2" (delete (-1 -2 -3 -4 -5 -6 -7 -8 -9 10 -12)) (("2" (lemma bestHop_primaryKey) (("2" (instantiate -1 (c e a W!1 2 C2!1 100)) (("2" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) 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) unchecked ((hop inductive-decl "bool" DV_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (distanceVectorAt100 formula-decl nil converge_linkFail nil) (bestHop_primaryKey formula-decl nil converge_linkFail nil) (Time 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) (Cost type-eq-decl nil DV_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bestHop_close formula-decl nil DV_linkFail nil) (c const-decl "Node" DV_linkFail nil) (bestHopCost inductive-decl "bool" DV_linkFail nil) (int_minus_int_is_int application-judgement "int" integers 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals 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) (> 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (node_disjoint formula-decl nil converge_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)) 10325 2860 t shostak)) (bestHop_ae_110_2 0 (bestHop_ae_110_2-1 nil 3427650050 3427650102 ("" (skolem!) (("" (skolem!) (("" (use bestHop_close) (("" (prop) (("1" (use hop_ae_110_2) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil) unchecked ((hop_ae_110_2 formula-decl nil converge_linkFail nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (Cost type-eq-decl nil DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (bestHop_close formula-decl nil DV_linkFail nil)) 51120 60 t shostak)) (hop_be_110_3 0 (hop_be_110_3-1 nil 3427571181 3427649865 ("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 2 a) (("1" (prop) (("1" (expand link) (("1" (inst 1 106) (("1" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 13 21) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 105) (("2" (ground) (("2" (use bestHop_105) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (ground) nil nil) ("4" (lemma node_disjoint) (("4" (ground) 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" (ground) (("1" (expand linkInput) (("1" (prop) (("1" (inst 13 21) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 105) (("2" (ground) (("2" (use bestHop_105) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (ground) nil nil) ("4" (lemma node_disjoint) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((hop inductive-decl "bool" DV_linkFail nil) (Time type-eq-decl nil 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) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (link inductive-decl "bool" DV_linkFail nil) (bestHop_105 formula-decl nil converge_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (node_disjoint formula-decl nil converge_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) (Cost type-eq-decl nil DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (a const-decl "Node" DV_linkFail nil)) 39019 530 t shostak)) (bestHop_be_110 0 (bestHop_be_110-1 nil 3427651154 3427652467 ("" (use bestHop_refresh) (("" (prop) (("1" (delete 2) (("1" (expand bestHopCost) (("1" (prop) (("1" (inst 1 c) (("1" (use hop_be_110_3) nil nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (lemma link_e) (("1" (instantiate -1 22) (("1" (ground) (("1" (inst 1 C!1 b) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (lemma bestHop_ae_110_2) (("2" (instantiate -1 (C2!1 W!1)) (("2" (use bestHop_105) (("2" (prop) (("2" (case "Z!1=a") (("1" (replace -1) (("1" (delete -1) (("1" (ground) nil nil)) nil)) nil) ("2" (case "Z!1=b") (("1" (replace -1) (("1" (delete -1) (("1" (lemma bestHop_primaryKey) (("1" (instantiate -1 (b e W!1 a C2!1 2 105)) (("1" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "Z!1=c") (("1" (replace -1) (("1" (delete -1) (("1" (lemma bestHop_primaryKey) (("1" (instantiate -1 (c e W!1 a C2!1 2 105)) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (case "Z!1=e") (("1" (replace -1) (("1" (delete -1) (("1" (lemma link_e) (("1" (instantiate -1 22) (("1" (ground) (("1" (inst 1 C1!1 b) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (instantiate -7 Z!1) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use hop_be_110_3) nil nil)) nil)) nil) unchecked ((bestHop_refresh formula-decl nil DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (Cost type-eq-decl nil DV_linkFail nil) (c 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) (hop_be_110_3 formula-decl nil converge_linkFail nil) (hop inductive-decl "bool" DV_linkFail nil) (bestHop_primaryKey formula-decl nil converge_linkFail nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a const-decl "Node" DV_linkFail nil) (= const-decl "[T, T -> boolean]" equalities nil) (bestHop_105 formula-decl nil converge_linkFail nil) (bestHop_ae_110_2 formula-decl nil converge_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (link_e formula-decl nil converge_linkFail nil) (posnat nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bestHopCost inductive-decl "bool" DV_linkFail nil)) 32316 510 t shostak)) (hop_ae_110 0 (hop_ae_110-1 nil 3427652731 3427653388 ("" (skolem!) (("" (prop) (("1" (replace -1) (("1" (delete -1) (("1" (skosimp*) (("1" (expand hop) (("1" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (use bestHop_105) (("2" (prop) (("2" (delete -2) (("2" (lemma bestHop_primaryKey) (("2" (instantiate -1 (b e a W!1 2 C2!1 105)) (("2" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (delete -1) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (use bestHop_105) (("2" (prop) (("2" (delete -1) (("2" (lemma bestHop_primaryKey) (("2" (instantiate -1 (c e a W!1 2 C2!1 105)) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (replace -1) (("3" (delete -1) (("3" (skosimp*) (("3" (expand hop) (("3" (prop) (("1" (lemma link_e) (("1" (instantiate -1 22) (("1" (ground) (("1" (inst 1 c!1 a) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma link_e) (("2" (instantiate -1 22) (("2" (ground) (("2" (inst 1 C1!1 a) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((hop inductive-decl "bool" DV_linkFail nil) (bestHop_primaryKey formula-decl nil converge_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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (bestHop_105 formula-decl nil converge_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (node_disjoint formula-decl nil converge_linkFail nil) (c const-decl "Node" DV_linkFail nil) (link_e formula-decl nil converge_linkFail nil) (posnat nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) 386695 860 t shostak)) (hop_ae_exist_TCC1 0 (hop_ae_exist_TCC1-1 nil 3427653850 nil ("" (subtype-tcc) nil nil) unchecked nil nil nil nil nil)) (hop_ae_exist 0 (hop_ae_exist-1 nil 3427653851 3427654268 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (skosimp*) (("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 C!1 c) (("1" (prop) (("1" (use link_abc) (("1" (prop) (("1" (inst 1 i!1) nil nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 T!1-5) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 C!1 c) (("2" (ground) (("1" (use link_abc) (("1" (prop) (("1" (inst 1 i!1) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 T!1-5) (("2" (ground) nil nil)) nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((hop inductive-decl "bool" DV_linkFail nil) (posnat nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers 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) (link_abc formula-decl nil converge_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (node_disjoint formula-decl nil converge_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) (Cost type-eq-decl nil DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (c const-decl "Node" DV_linkFail nil)) 173446 750 t shostak)) (bestHop_ae_t 0 (bestHop_ae_t-1 nil 3427661079 3427662949 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (skosimp*) (("" (use bestHop_refresh) (("" (grind) (("1" (use hop_ae_exist2) (("1" (grind) nil nil)) nil) ("2" (delete 2) (("2" (expand bestHopCost) (("2" (prop) (("1" (inst 1 c) (("1" (use hop_ae_exist2) (("1" (grind) nil nil)) nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (lemma link_e) (("1" (instantiate -1 i!1) (("1" (grind) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (use link_close) (("2" (prop) (("1" (replace -1) (("1" (replace -2) (("1" (delete (-1 -2)) (("1" (lemma bestHop_primaryKey) (("1" (instantiate -1 (a b W!1 c C!1 C2!1 Tp2!1)) (("1" (prop) (("1" (replace -1) (("1" (ground) nil nil)) nil) ("2" (use bestHop_primaryKey) (("2" (lemma bestHop_primaryKey) (("2" (instantiate -1 (b e c W!1 C!1 C2!1 5*i!1-5)) (("2" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (ground) (("3" (lemma bestHop_primaryKey) (("3" (instantiate -1 (b e c W!1 C!1 C2!1 5*i!1-5)) (("3" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" (replace -2) (("5" (delete -2) (("5" (replace -1) (("5" (delete -1) (("5" (lemma bestHop_primaryKey) (("5" (instantiate -1 (c e b W!1 C!1 C2!1 5*i!1-5)) (("5" (prop) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (lemma node_disjoint) (("6" (ground) nil nil)) nil) ("7" (inst 1 i!1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((bestHop_refresh formula-decl nil DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Cost type-eq-decl nil DV_linkFail nil) (c const-decl "Node" 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) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop inductive-decl "bool" DV_linkFail nil) (bestHop_primaryKey formula-decl nil converge_linkFail nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (b const-decl "Node" DV_linkFail nil) (node_disjoint formula-decl nil converge_linkFail nil) (link_close formula-decl nil converge_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (link_e formula-decl nil converge_linkFail nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bestHopCost inductive-decl "bool" DV_linkFail nil) (hop_ae_exist2 formula-decl nil converge_linkFail nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posnat nonempty-type-eq-decl nil integers 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) 605338 2230 t shostak)) (hop_be_exist 0 (hop_be_exist-1 nil 3427654320 3427654931 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (skosimp*) (("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 C!1 c) (("1" (ground) (("1" (use link_abc) (("1" (prop) (("1" (inst 1 i!1) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 T!1-5) (("2" (ground) nil nil)) nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 C!1 c) (("2" (ground) (("1" (use link_abc) (("1" (prop) (("1" (inst 1 i!1) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 T!1-5) (("2" (ground) nil nil)) nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((hop inductive-decl "bool" DV_linkFail 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) (int_minus_int_is_int application-judgement "int" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (Time type-eq-decl nil DV_linkFail nil) (link_abc formula-decl nil converge_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (node_disjoint formula-decl nil converge_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) (Cost type-eq-decl nil DV_linkFail nil) (Node type-eq-decl nil DV_linkFail nil) (c const-decl "Node" DV_linkFail nil)) 81656 520 t shostak)) (bestHop_ce_exist 0 (bestHop_ce_exist-1 nil 3427663109 3427664464 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (use bestHop_refresh) (("" (prop) (("1" (delete 2) (("1" (expand bestHopCost) (("1" (prop) (("1" (inst 1 a) (("1" (use hop_ce_exist) (("1" (grind) nil nil)) nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (lemma link_e) (("1" (instantiate -1 i!1) (("1" (prop) (("1" (inst 1 C!2 c) (("1" (ground) nil nil)) nil) ("2" (lemma link_e) (("2" (instantiate -1 i!1) (("2" (prop) (("1" (inst 1 C!2 c) (("1" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (use link_close) (("2" (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" (replace -1) (("4" (delete -1) (("4" (replace -1) (("4" (delete -1) (("4" (ground) (("4" (instantiate -9 (W!1)) (("4" (instantiate -9 (C2!1)) (("4" (prop) (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (lemma node_disjoint) (("5" (ground) nil nil)) nil) ("6" (replace -1) (("6" (replace -2) (("6" (delete -2) (("6" (delete -1) (("6" (lemma bestHop_primaryKey) (("6" (instantiate -1 (a e c W!1 C!1 C2!1 T!1-5)) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (ground) (("7" (case "Z!1=a") (("1" (replace -1) (("1" (delete -1) (("1" (lemma bestHop_primaryKey) (("1" (instantiate -1 (a e W!1 c C2!1 C!1 Tp2!1)) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (inst 2 i!1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use hop_ce_exist) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((bestHopCost inductive-decl "bool" DV_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (posnat nonempty-type-eq-decl nil integers nil) (link_e formula-decl nil converge_linkFail nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (link_close formula-decl nil converge_linkFail nil) (= const-decl "[T, T -> boolean]" equalities nil) (bestHop_primaryKey formula-decl nil converge_linkFail nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (node_disjoint formula-decl nil converge_linkFail nil) (hop inductive-decl "bool" DV_linkFail nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (hop_ce_exist formula-decl nil converge_linkFail 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (Node type-eq-decl nil DV_linkFail nil) (c 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (Time type-eq-decl nil DV_linkFail nil) (bestHop_refresh formula-decl nil DV_linkFail nil)) 314634 1170 t shostak)) (hop_be_exist2 0 (hop_be_exist2-1 nil 3427659367 3427659550 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (expand hop) (("" (prop) (("1" (delete 1) (("1" (inst 1 1 C!1 a) (("1" (ground) (("1" (use link_abc) (("1" (prop) (("1" (skosimp*) (("1" (inst 1 i!1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (inst 1 T!1-5) (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (lemma node_disjoint) (("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (delete 1) (("2" (inst 1 1 C!1 a) (("2" (ground) (("1" (use link_abc) (("1" (ground) nil nil)) nil) ("2" (expand hopMsg) (("2" (inst 1 T!1-5) (("2" (grind) nil nil)) nil)) nil) ("3" (lemma node_disjoint) (("3" (grind) 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) (node_disjoint formula-decl nil converge_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_plus_int_is_int application-judgement "int" integers nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (link_abc formula-decl nil converge_linkFail nil) (Time type-eq-decl nil 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) (posnat nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (hop inductive-decl "bool" DV_linkFail nil)) 90697 690 t shostak)) (bestHop_ce_exist2 0 (bestHop_ce_exist2-1 nil 3427664912 3427665836 ("" (skolem!) (("" (skolem!) (("" (prop) (("" (skosimp*) (("" (use bestHop_refresh) (("" (ground) (("1" (delete 2) (("1" (expand bestHopCost) (("1" (prop) (("1" (inst 1 b) (("1" (use hop_be_exist2) (("1" (ground) (("1" (inst 1 i!1) nil nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (prop) (("2" (skosimp*) (("2" (expand hop) (("2" (prop) (("1" (lemma link_e) (("1" (instantiate -1 i!1) (("1" (prop) (("1" (inst 1 C!2 c) (("1" (ground) nil nil)) nil) ("2" (delete -2) (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand hopMsg) (("2" (skosimp*) (("2" (case "Z!1=a") (("1" (replace -1) (("1" (delete -1) (("1" (ground) (("1" (instantiate -9 W!1) (("1" (instantiate -9 C2!1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "Z!1=b") (("1" (replace -1) (("1" (lemma bestHop_primaryKey) (("1" (instantiate -1 (b e W!1 a C2!1 C!1 Tp2!1)) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (case "Z!1=e") (("1" (replace -1) (("1" (delete -1) (("1" (lemma link_e) (("1" (instantiate -1 i!1) (("1" (prop) (("1" (inst 1 C1!1) (("1" (inst 1 c) (("1" (ground) nil nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (use link_close) (("2" (prop) (("1" (lemma node_disjoint) (("1" (ground) nil nil)) nil) ("2" (lemma node_disjoint) (("2" (ground) nil nil)) nil) ("3" (inst 1 i!1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use hop_be_exist2) (("2" (ground) (("2" (inst 1 i!1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((bestHop_refresh formula-decl nil DV_linkFail nil) (Time type-eq-decl nil DV_linkFail nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Cost type-eq-decl nil DV_linkFail nil) (b const-decl "Node" DV_linkFail nil) (e const-decl "Node" DV_linkFail nil) (c 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) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (hop_be_exist2 formula-decl nil converge_linkFail nil) (posnat nonempty-type-eq-decl nil integers nil) (hop inductive-decl "bool" DV_linkFail nil) (bestHop_primaryKey formula-decl nil converge_linkFail nil) (node_disjoint formula-decl nil converge_linkFail nil) (link_close formula-decl nil converge_linkFail nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (a const-decl "Node" DV_linkFail nil) (= const-decl "[T, T -> boolean]" equalities nil) (hopMsg inductive-decl "bool" DV_linkFail nil) (link_e formula-decl nil converge_linkFail nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bestHopCost 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) 155951 750 t shostak)))