| products/sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: TestSuite.vdmpp Sprache: LispUntersuchung PVS© |
|
||||||
|
(exact_reduce
(lower_validity 0 (lower_validity-2 nil 3398099404 ("" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (use "reflexive[T]") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (lemma "transitive[T]") (("1" (invoke (inst - _ "%1" "%2" "%3") (! -2 l) (! -2 r) (! 1 r)) (("1" (inst?) (("1" (assert) (("1" (hide 2 -1) (("1" (expand "v_min") (("1" (expand "quorum_correct?") (("1" (expand "enabled_within?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "protocol") (("1" (inst?) (("1" (expand "reduce_choice") (("1" (replace -1 :hide? t) (("1" (use "reduce_min_validity[N(j!2 + j!1), N(1 + j!1 + j!2), T, <=, error(j!1 + j!2)]") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "quorum_correct?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (transitive formula-decl nil relations_extra nil) (transitive? const-decl "bool" relations 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (reduce_min_validity formula-decl nil exact_reduce_stage nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (PRED type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (reflexive formula-decl nil relations_extra nil) (nat_induction formula-decl nil naturalnumbers nil) (v_min const-decl "T" k_ordered nil) (enabled_within? const-decl "bool" exact_comm nil) (quorum_correct? const-decl "bool" exact_comm nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (choice_function type-eq-decl nil node_functions nil) (choice_stage type-eq-decl nil node_functions_stage nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (tau_type type-eq-decl nil tau_declaration nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (k_consensus_function type-eq-decl nil k_ordered nil) (error formal-const-decl "[nat -> T]" exact_reduce nil) (N formal-const-decl "[nat -> posnat]" exact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (consensus_function type-eq-decl nil ordered_finite_sequences nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil min_seq "structures/") (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (<= formal-const-decl "(total_order?[T])" exact_reduce nil) (total_order? const-decl "bool" orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ne_seqs type-eq-decl nil seqs "structures/") (T formal-nonempty-type-decl nil exact_reduce 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)) nil) (lower_validity-1 nil 3397944768 ("" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (use "reflexive[T]") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (lemma "transitive[T]") (("1" (invoke (inst - _ "%1" "%2" "%3") (! -2 l) (! -2 r) (! 1 r)) (("1" (inst?) (("1" (assert) (("1" (hide 2 -1) (("1" (expand "v_min") (("1" (expand "generalized_majority_correct?") (("1" (expand "enabled_within?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "protocol") (("1" (inst?) (("1" (expand "reduce_select") (("1" (replace -1 :hide? t) (("1" (use "reduce_min_validity[N(j!2 + j!1), N(1 + j!1 + j!2), T, <=, error(j!1 + j!2)]") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "generalized_majority_correct?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((transitive formula-decl nil relations_extra nil) (reduce_min_validity formula-decl nil exact_reduce_stage nil) (reflexive formula-decl nil relations_extra nil) (v_min const-decl "T" k_ordered nil) (choice_function type-eq-decl nil node_functions nil) (choice_stage type-eq-decl nil node_functions_stage nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil)) nil)) (upper_validity 0 (upper_validity-2 nil 3398099426 ("" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (use "reflexive[T]") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (inst - _ _ "j!2" _ _ _ _) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (lemma "transitive[T]") (("1" (invoke (inst - _ "%1" "%2" "%3") (! 1 l) (! -2 l) (! -2 r)) (("1" (inst?) (("1" (assert) (("1" (hide 2 -1) (("1" (expand "v_max") (("1" (expand "quorum_correct?") (("1" (expand "enabled_within?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "protocol") (("1" (inst?) (("1" (expand "reduce_choice") (("1" (replace -1 :hide? t) (("1" (use "reduce_max_validity[N(j!2 + j!1), N(1 + j!1 + j!2), T, <=, error(j!1 + j!2)]") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "quorum_correct?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((reduce_max_validity formula-decl nil exact_reduce_stage nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (transitive? const-decl "bool" relations nil) (transitive formula-decl nil relations_extra nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (PRED type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (reflexive formula-decl nil relations_extra nil) (nat_induction formula-decl nil naturalnumbers nil) (v_max const-decl "T" k_ordered nil) (enabled_within? const-decl "bool" exact_comm nil) (quorum_correct? const-decl "bool" exact_comm nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (choice_function type-eq-decl nil node_functions nil) (choice_stage type-eq-decl nil node_functions_stage nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (tau_type type-eq-decl nil tau_declaration nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (k_consensus_function type-eq-decl nil k_ordered nil) (error formal-const-decl "[nat -> T]" exact_reduce nil) (N formal-const-decl "[nat -> posnat]" exact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (consensus_function type-eq-decl nil ordered_finite_sequences nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil min_seq "structures/") (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (<= formal-const-decl "(total_order?[T])" exact_reduce nil) (total_order? const-decl "bool" orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ne_seqs type-eq-decl nil seqs "structures/") (T formal-nonempty-type-decl nil exact_reduce 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)) nil) (upper_validity-1 nil 3397948096 ("" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (use "reflexive[T]") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (inst - _ _ "j!2" _ _ _ _) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (lemma "transitive[T]") (("1" (invoke (inst - _ "%1" "%2" "%3") (! 1 l) (! -2 l) (! -2 r)) (("1" (inst?) (("1" (assert) (("1" (hide 2 -1) (("1" (expand "v_max") (("1" (expand "generalized_majority_correct?") (("1" (expand "enabled_within?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "protocol") (("1" (inst?) (("1" (expand "reduce_select") (("1" (replace -1 :hide? t) (("1" (use "reduce_max_validity[N(j!2 + j!1), N(1 + j!1 + j!2), T, <=, error(j!1 + j!2)]") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "generalized_majority_correct?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((reduce_max_validity formula-decl nil exact_reduce_stage nil) (transitive formula-decl nil relations_extra nil) (reflexive formula-decl nil relations_extra nil) (v_max const-decl "T" k_ordered nil) (choice_function type-eq-decl nil node_functions nil) (choice_stage type-eq-decl nil node_functions_stage nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil)) nil)) (consensus_validity 0 (consensus_validity-2 nil 3397948690 ("" (skosimp*) (("" (forward-chain "lower_validity") (("" (forward-chain "upper_validity") (("" (hide -5 -4 -3) (("" (rewrite "v_minmax_choose_alt[N(j!1 + k!1), T, <=]") (("" (rewrite "v_minmax_choose_alt[N(j!1), T, <=]") (("" (lemma "transitive[T]") (("" (prop) (("1" (invoke (inst - "<=" "%1" "%2" "v!1") (! -2 l) (! -2 r)) (("1" (assert) (("1" (expand "v_max" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (invoke (inst - "<=" "v!1" "%1" "%2") (! -3 l) (! -3 r)) (("2" (assert) (("2" (expand "v_min" -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lower_validity formula-decl nil exact_reduce nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil exact_reduce nil) (ne_seqs type-eq-decl nil seqs "structures/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" exact_reduce nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers 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) (> const-decl "bool" 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) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (dom type-eq-decl nil min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (consensus_function type-eq-decl nil ordered_finite_sequences nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "[nat -> posnat]" exact_reduce nil) (error formal-const-decl "[nat -> T]" exact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (v_max const-decl "T" k_ordered nil) (transitive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (v_min const-decl "T" k_ordered nil) (transitive formula-decl nil relations_extra nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (v_minmax_choose_alt formula-decl nil select_minmax nil) (vec type-eq-decl nil node nil) (upper_validity formula-decl nil exact_reduce nil)) nil) (consensus_validity-1 nil 3397948520 (";;; Proof upper_validity-1 for formula exact_reduce.upper_validity" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (use "reflexive[T]") nil))))) ("2" (skosimp*) (("2" (assert) (("2" (inst - _ "j!2" _ _ _ _ _) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (lemma "transitive[T]") (("1" (invoke (inst - _ "%1" "%2" "%3") (! 1 l) (! -2 l) (! -2 r)) (("1" (inst?) (("1" (assert) (("1" (hide 2 -1) (("1" (expand "v_max") (("1" (expand "generalized_majority_correct?") (("1" (expand "enabled_within?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "protocol") (("1" (inst?) (("1" (expand "reduce_select") (("1" (replace -1 :hide? t) (("1" (use "reduce_max_validity[N(j!2 + j!1), N(1 + j!1 + j!2), T, <=, error(j!1 + j!2)]") (("1" (assert) nil))))))))))))))))))))))))))))))))) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil))))))))) ("3" (hide-all-but (1 -2)) (("3" (expand "generalized_majority_correct?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil))))))))) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil)))))))))))))))))))))))))))) ";;; developed with shostak decision procedures") nil nil)) (exact_agreement_propagation 0 (exact_agreement_propagation-1 nil 3397948722 ("" (skosimp*) (("" (forward-chain "lower_validity") (("" (forward-chain "upper_validity") (("" (replace*) (("" (hide-all-but (-1 -2 1)) (("" (lemma "transitive[T]") (("" (invoke (inst - "<=" "%1" "%2" "%3") (! -2 l) (! -2 r) (! -3 r)) (("" (assert) (("" (hide-all-but (1 -1)) (("" (expand* "v_max" "v_min") (("" (rewrite "min_le_max_alt[N(j!1 + k!1), T, <=]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lower_validity formula-decl nil exact_reduce nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-nonempty-type-decl nil exact_reduce nil) (ne_seqs type-eq-decl nil seqs "structures/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" exact_reduce nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (number nonempty-type-decl nil numbers 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) (> const-decl "bool" 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) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (dom type-eq-decl nil min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (consensus_function type-eq-decl nil ordered_finite_sequences nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "[nat -> posnat]" exact_reduce nil) (error formal-const-decl "[nat -> T]" exact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (transitive formula-decl nil relations_extra nil) (min_le_max_alt formula-decl nil select_minmax nil) (vec type-eq-decl nil node nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (v_min const-decl "T" k_ordered nil) (v_max const-decl "T" k_ordered nil) (transitive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (upper_validity formula-decl nil exact_reduce nil)) nil)) (agreement_generation 0 (agreement_generation-1 nil 3397948743 ("" (expand "exists_all_symmetric?") (("" (skosimp*) (("" (lemma "exact_agreement_propagation") (("" (inst - _ _ "i!1+1" "j!1+k!1-(i!1+1)" _ _ _ _) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "protocol") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 1)) (("2" (expand "enabled_within?") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -5 -6 2) (("3" (expand* "v_max" "v_min") (("3" (expand "protocol") (("3" (inst?) (("3" (expand "reduce_choice") (("3" (assert) (("3" (use "reduce_min_eq_max[N(i!1), N(1 + i!1), T, <=, error(i!1)]") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (k!1 skolem-const-decl "nat" exact_reduce nil) (j!1 skolem-const-decl "nat" exact_reduce nil) (i!1 skolem-const-decl "nat" exact_reduce nil) (nat nonempty-type-eq-decl nil naturalnumbers 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 "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets 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) (reduce_choice const-decl "choice_function" k_ordered nil) (reduce_min_eq_max formula-decl nil exact_reduce_stage nil) (v_max const-decl "T" k_ordered nil) (v_min const-decl "T" k_ordered nil) (enabled_within? const-decl "bool" exact_comm nil) (protocol const-decl "bool" protocol nil) (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" exact_reduce nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (dom type-eq-decl nil min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (consensus_function type-eq-decl nil ordered_finite_sequences nil) (error formal-const-decl "[nat -> T]" exact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered nil) (tau_type type-eq-decl nil tau_declaration nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil) (T formal-nonempty-type-decl nil exact_reduce nil) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "[nat -> posnat]" exact_reduce 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (exact_agreement_propagation formula-decl nil exact_reduce nil) (exists_all_symmetric? const-decl "bool" exact_comm nil)) nil))) ¤ Dauer der Verarbeitung: 0.59 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
