|
(exact_reduce_integration
(lower_validity 0
(lower_validity-1 nil 3399288882
("" (skosimp*)
(("" (replace -1 :hide? t)
(("" (expand "protocol")
(("" (use "quorum_correct_integration")
(("" (assert)
(("" (use "lower_validity")
(("" (assert)
(("" (hide-all-but 1)
(("" (expand "enabled_within?")
(("" (skosimp*)
(("" (expand "conforms")
((""
(use "scheduled_conform[N(i!1), N(1 + i!1), T]")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((quorum_correct_integration formula-decl nil comm_integration 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(N formal-const-decl "[nat -> posnat]" exact_reduce_integration
nil)
(T formal-nonempty-type-decl nil exact_reduce_integration nil)
(tau_type type-eq-decl nil tau_declaration nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(node_status type-eq-decl nil integration_fault_model nil)
(fault_class type-decl nil integration_fault_model nil)
(conforms const-decl "check_stage[N(i), N(i + 1), UT]"
comm_integration nil)
(check_stage type-eq-decl nil node_functions_stage nil)
(UT type-eq-decl nil comm_integration nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets 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)
(valid_check_function type-eq-decl nil comm_integration nil)
(valid_check_stage type-eq-decl nil comm_integration_stage nil)
(msg_checker nonempty-type-eq-decl nil comm_integration_stage nil)
(garbled adt-constructor-decl "(garbled?)" message_adt nil)
(garbled? adt-recognizer-decl "[message -> boolean]" message_adt
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(message type-decl nil message_adt 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)
(< const-decl "bool" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(source_error formal-const-decl "[nat -> message]"
exact_reduce_integration nil)
(<= const-decl "bool" ordered_message nil)
(<= formal-const-decl "(total_order?[T])" exact_reduce_integration
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(lower_validity formula-decl nil exact_reduce nil)
(sent_vec type-eq-decl nil node_functions nil)
(sent_vec_stage type-eq-decl nil node_functions_stage nil)
(rcvd const-decl "[below(N(i + 1)) -> [below(N(i)) -> UT]]"
comm_integration 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)
(k_consensus_function type-eq-decl nil k_ordered 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/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(scheduled_conform formula-decl nil comm_integration_stage nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(enabled_within? const-decl "bool" exact_comm nil)
(message_total_order name-judgement "(total_order?[message[T]])"
exact_reduce_integration nil)
(protocol const-decl "bool" protocol_integration nil))
nil))
(upper_validity 0
(upper_validity-1 nil 3399288900
("" (skosimp*)
(("" (replace -1 :hide? t)
(("" (expand "protocol")
(("" (use "quorum_correct_integration")
(("" (assert)
(("" (use "upper_validity")
(("" (assert)
(("" (hide-all-but 1)
(("" (expand "enabled_within?")
(("" (skosimp*)
(("" (expand "conforms")
((""
(use "scheduled_conform[N(i!1), N(1 + i!1), T]")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((quorum_correct_integration formula-decl nil comm_integration 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(N formal-const-decl "[nat -> posnat]" exact_reduce_integration
nil)
(T formal-nonempty-type-decl nil exact_reduce_integration nil)
(tau_type type-eq-decl nil tau_declaration nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(node_status type-eq-decl nil integration_fault_model nil)
(fault_class type-decl nil integration_fault_model nil)
(conforms const-decl "check_stage[N(i), N(i + 1), UT]"
comm_integration nil)
(check_stage type-eq-decl nil node_functions_stage nil)
(UT type-eq-decl nil comm_integration nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets 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)
(valid_check_function type-eq-decl nil comm_integration nil)
(valid_check_stage type-eq-decl nil comm_integration_stage nil)
(msg_checker nonempty-type-eq-decl nil comm_integration_stage nil)
(garbled adt-constructor-decl "(garbled?)" message_adt nil)
(garbled? adt-recognizer-decl "[message -> boolean]" message_adt
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(message type-decl nil message_adt 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)
(< const-decl "bool" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(source_error formal-const-decl "[nat -> message]"
exact_reduce_integration nil)
(<= const-decl "bool" ordered_message nil)
(<= formal-const-decl "(total_order?[T])" exact_reduce_integration
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(upper_validity formula-decl nil exact_reduce nil)
(sent_vec type-eq-decl nil node_functions nil)
(sent_vec_stage type-eq-decl nil node_functions_stage nil)
(rcvd const-decl "[below(N(i + 1)) -> [below(N(i)) -> UT]]"
comm_integration 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)
(k_consensus_function type-eq-decl nil k_ordered 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/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(scheduled_conform formula-decl nil comm_integration_stage nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(enabled_within? const-decl "bool" exact_comm nil)
(message_total_order name-judgement "(total_order?[message[T]])"
exact_reduce_integration nil)
(protocol const-decl "bool" protocol_integration nil))
nil))
(agreement_generation 0
(agreement_generation-1 nil 3399288912
("" (skosimp*)
(("" (replace -1 :hide? t)
(("" (expand "protocol")
(("" (use "all_symmetric_integration")
(("" (assert)
(("" (use "agreement_generation")
(("" (assert)
(("" (hide-all-but 1)
(("" (expand "enabled_within?")
(("" (skosimp*)
(("" (expand "conforms")
((""
(use "scheduled_conform[N(i!1), N(1 + i!1), T]")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((all_symmetric_integration formula-decl nil comm_integration 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(N formal-const-decl "[nat -> posnat]" exact_reduce_integration
nil)
(T formal-nonempty-type-decl nil exact_reduce_integration nil)
(tau_type type-eq-decl nil tau_declaration nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(node_status type-eq-decl nil integration_fault_model nil)
(fault_class type-decl nil integration_fault_model nil)
(conforms const-decl "check_stage[N(i), N(i + 1), UT]"
comm_integration nil)
(check_stage type-eq-decl nil node_functions_stage nil)
(UT type-eq-decl nil comm_integration nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets 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)
(valid_check_function type-eq-decl nil comm_integration nil)
(valid_check_stage type-eq-decl nil comm_integration_stage nil)
(msg_checker nonempty-type-eq-decl nil comm_integration_stage nil)
(garbled adt-constructor-decl "(garbled?)" message_adt nil)
(garbled? adt-recognizer-decl "[message -> boolean]" message_adt
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(message type-decl nil message_adt 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)
(< const-decl "bool" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(source_error formal-const-decl "[nat -> message]"
exact_reduce_integration nil)
(<= const-decl "bool" ordered_message nil)
(<= formal-const-decl "(total_order?[T])" exact_reduce_integration
nil)
(total_order? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(agreement_generation formula-decl nil exact_reduce nil)
(sent_vec type-eq-decl nil node_functions nil)
(sent_vec_stage type-eq-decl nil node_functions_stage nil)
(rcvd const-decl "[below(N(i + 1)) -> [below(N(i)) -> UT]]"
comm_integration 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)
(k_consensus_function type-eq-decl nil k_ordered 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/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(scheduled_conform formula-decl nil comm_integration_stage nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(enabled_within? const-decl "bool" exact_comm nil)
(protocol const-decl "bool" protocol_integration nil))
nil)))
¤ Dauer der Verarbeitung: 0.30 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
