Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ml_syntax.ML Sprache: Lisp

Original von: PVS^©

(majority
(consensus_validity 0
  (consensus_validity-1 nil 3398508741
   ("" (induct "k")
    (("1" (skosimp*) (("1" (assert) nil nil)) nil)
     ("2" (skosimp*)
      (("2" (assert)
        (("2" (inst?)
          (("2" (inst?)
            (("2" (inst?)
              (("2" (inst?)
                (("2" (assert)
                  (("2" (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 (1 -2))
                      (("2" (expand "majority_correct?")
                        (("2" (skosimp*)
                          (("2" (inst?) (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("3" (hide-all-but (1 -3))
                      (("3" (expand "enabled_within?")
                        (("3" (skosimp*)
                          (("3" (inst?) (("3" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("4" (hide 2)
                      (("4" (expand "majority_correct?")
                        (("4" (expand "enabled_within?")
                          (("4" (expand "protocol")
                            (("4" (inst?)
                              (("4"
                                (inst - "j!2")
                                (("4"
                                  (inst?)
                                  (("4"
                                    (assert)
                                    (("4"
                                      (expand "majority_vote")
                                      (("4"
                                        (replace -1 :hide? t)
                                        (("4"
                                          (use
                                           "consensus_validity[N(j!2), N(1 + j!2), T]")
                                          (("4" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((consensus_validity formula-decl nil majority_stage 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (uniform? const-decl "bool" node nil)
    (nodeid_set type-eq-decl nil node nil)
    (vec type-eq-decl nil node nil)
    (enabled_within? const-decl "bool" exact_comm nil)
    (majority_correct? const-decl "bool" exact_comm nil)
    (majority_vote const-decl "choice_function" majority 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)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (majority_function type-eq-decl nil finite_seqs nil)
    (is_majority const-decl "bool" majority_seq "structures/")
    (maj_exists const-decl "bool" majority_seq "structures/")
    (below type-eq-decl nil nat_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_sequence type-eq-decl nil finite_sequences 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)
    (T formal-nonempty-type-decl nil majority 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)
    (N formal-const-decl "[nat -> posnat]" majority 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)
    (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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
(agreement_generation 0
  (agreement_generation-2 nil 3495190774
   ("" (expand "exists_all_symmetric?")
    (("" (expand "exists_all_symmetric?")
      (("" (skosimp*)
        ((""
          (case "EXISTS v: uniform?[N(1 + i!1), T](sent!1(1 + i!1), v)(common_check!1(1 + i!1))")
          (("1" (skosimp*)
            (("1" (inst?)
              (("1" (lemma "consensus_validity")
                (("1" (inst - _ _ "i!1+1" "j!1+k!1-(i!1+1)" _ _ _ _)
                  (("1" (assert)
                    (("1" (inst?)
                      (("1" (inst?)
                        (("1" (inst?)
                          (("1" (inst?)
                            (("1" (assert)
                              (("1"
                                (rewrite "majority_correct_rw")
                                (("1"
                                  (prop)
                                  (("1"
                                    (hide-all-but (1 -2))
                                    (("1"
                                      (expand "protocol")
                                      (("1"
                                        (skosimp*)
                                        (("1"
                                          (inst?)
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide-all-but (1 -7))
                                    (("2"
                                      (expand "enabled_within?")
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2 -5)
            (("2" (expand "protocol")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (replace -1)
                    (("2" (expand "majority_vote" +)
                      (("2"
                        (use "agreement_generation[N(i!1), N(i!1 + 1), T]")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists_all_symmetric? const-decl "bool" exact_comm 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)
    (sent_vec type-eq-decl nil node_functions nil)
    (sent_vec_stage type-eq-decl nil node_functions_stage nil)
    (uniform? const-decl "bool" node nil)
    (nodeid_set type-eq-decl nil node nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil) (vec type-eq-decl nil node 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)
    (N formal-const-decl "[nat -> posnat]" majority 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)
    (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)
    (T formal-nonempty-type-decl nil majority nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (i!1 skolem-const-decl "nat" majority nil)
    (j!1 skolem-const-decl "nat" majority nil)
    (k!1 skolem-const-decl "nat" majority nil)
    (check_function type-eq-decl nil node_functions nil)
    (check_stage type-eq-decl nil node_functions_stage nil)
    (protocol const-decl "bool" protocol nil)
    (enabled_within? const-decl "bool" exact_comm nil)
    (majority_correct_rw formula-decl nil exact_comm nil)
    (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil)
    (rcvd_matrix type-eq-decl nil node_functions nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (below type-eq-decl nil nat_types nil)
    (maj_exists const-decl "bool" majority_seq "structures/")
    (is_majority const-decl "bool" majority_seq "structures/")
    (majority_function type-eq-decl nil finite_seqs 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)
    (consensus_validity formula-decl nil majority nil)
    (majority_vote const-decl "choice_function" majority nil)
    (agreement_generation formula-decl nil majority_stage nil)
    (exists_all_symmetric? const-decl "bool" exact_comm nil))
   nil)
  (agreement_generation-1 nil 3398508767
   ("" (expand "exists_all_symmetric?")
    (("" (expand "exists_all_symmetric?")
      (("" (skosimp*)
        ((""
          (case "EXISTS v: uniform?[N(1 + i!1), T](sent!1(1 + i!1), v)(common_check!1(1 + i!1))")
          (("1" (skosimp*)
            (("1" (inst?)
              (("1" (lemma "consensus_validity")
                (("1" (inst - _ _ "i!1+1" "j!1+k!1-(i!1+1)" _ _ _)
                  (("1" (assert)
                    (("1" (inst?)
                      (("1" (inst?)
                        (("1" (inst?)
                          (("1" (assert)
                            (("1" (rewrite "majority_correct_rw")
                              (("1"
                                (prop)
                                (("1"
                                  (hide-all-but (1 -2))
                                  (("1"
                                    (expand "protocol")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst?)
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but (1 -7))
                                  (("2"
                                    (expand "enabled_within?")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst?)
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2 -5)
            (("2" (expand "protocol")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (replace -1)
                    (("2"
                      (use "agreement_generation[N(i!1), N(i!1 + 1), T, error(i!1)]")
                      (("2" (assert)
                        (("2" (expand "majority_voter" +)
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sent_vec type-eq-decl nil node_functions nil)
    (sent_vec_stage type-eq-decl nil node_functions_stage nil)
    (uniform? const-decl "bool" node nil)
    (vec type-eq-decl nil node nil)
    (rcvd_matrix type-eq-decl nil node_functions nil)
    (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil)
    (majority_correct_rw formula-decl nil exact_comm nil)
    (enabled_within? const-decl "bool" exact_comm nil)
    (check_stage type-eq-decl nil node_functions_stage nil)
    (check_function type-eq-decl nil node_functions nil)
    (agreement_generation formula-decl nil majority_stage nil))
   nil))
(faulty_source 0
  (faulty_source-1 nil 3398508812
   ("" (skosimp*)
    (("" (expand "protocol")
      (("" (inst?)
        (("" (assert)
          (("" (replace -1 :hide? t)
            (("" (expand "majority_vote")
              (("" (use "faulty_source[N(j!1), N(1 + j!1), T]")
                (("" (assert)
                  (("" (expand "enabled_within?")
                    (("" (inst?) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((protocol const-decl "bool" protocol nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (majority_vote const-decl "choice_function" majority nil)
    (enabled_within? const-decl "bool" fault_assumptions_stage nil)
    (enabled_within? const-decl "bool" exact_comm nil)
    (majority_function type-eq-decl nil finite_seqs nil)
    (is_majority const-decl "bool" majority_seq "structures/")
    (maj_exists const-decl "bool" majority_seq "structures/")
    (below type-eq-decl nil nat_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_sequence type-eq-decl nil finite_sequences 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)
    (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)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (faulty_source formula-decl nil majority_stage 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]" majority nil)
    (T formal-nonempty-type-decl nil majority 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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(faulty_stage 0
  (faulty_stage-1 nil 3398508856
   ("" (skosimp*)
    (("" (use "consensus_validity")
      (("" (assert)
        (("" (expand "uniform?")
          (("" (inst?) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((consensus_validity formula-decl nil majority 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)
    (majority_function type-eq-decl nil finite_seqs nil)
    (is_majority const-decl "bool" majority_seq "structures/")
    (maj_exists const-decl "bool" majority_seq "structures/")
    (below type-eq-decl nil nat_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_sequence type-eq-decl nil finite_sequences 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 majority 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)
    (N formal-const-decl "[nat -> posnat]" majority 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) (>= 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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (uniform? const-decl "bool" node nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil))
   nil))
(asymmetric_source 0
  (asymmetric_source-2 nil 3495190844
   ("" (skosimp*)
    (("" (expand "majority_correct?")
      (("" (expand "enabled_within?")
        (("" (inst?)
          (("" (inst?)
            (("" (assert)
              ((""
                (lemma "sources_disagree[N(j!1 + 1), N(j!1 + 2), T]")
                (("" (inst?)
                  (("" (inst?)
                    (("" (inst?)
                      (("" (assert)
                        (("" (expand "protocol")
                          (("" (inst?)
                            (("" (assert)
                              ((""
                                (replace -1 :hide? t)
                                ((""
                                  (expand "majority_vote")
                                  ((""
                                    (use
                                     "asymmetric_source[N(j!1), N(j!1 + 1), T]")
                                    ((""
                                      (assert)
                                      (("" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_correct? const-decl "bool" exact_comm nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (< const-decl "bool" reals 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)
    (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)
    (protocol const-decl "bool" protocol nil)
    (majority_vote const-decl "choice_function" majority nil)
    (majority_function type-eq-decl nil finite_seqs nil)
    (is_majority const-decl "bool" majority_seq "structures/")
    (maj_exists const-decl "bool" majority_seq "structures/")
    (below type-eq-decl nil nat_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (asymmetric_source formula-decl nil majority_stage 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)
    (sources_disagree formula-decl nil majority_stage 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]" majority nil)
    (T formal-nonempty-type-decl nil majority nil)
    (enabled_within? const-decl "bool" exact_comm nil))
   nil)
  (asymmetric_source-1 nil 3398508887
   ("" (skosimp*)
    (("" (expand "majority_correct?")
      (("" (expand "enabled_within?")
        (("" (inst?)
          (("" (inst?)
            (("" (assert)
              ((""
                (lemma
                 "sources_disagree[N(j!1 + 1), N(j!1 + 2), T, error(j!1+1)]")
                (("" (inst?)
                  (("" (inst?)
                    (("" (inst?)
                      (("" (assert)
                        (("" (expand "protocol")
                          (("" (inst?)
                            (("" (assert)
                              ((""
                                (replace -1 :hide? t)
                                ((""
                                  (expand "majority_voter")
                                  ((""
                                    (use
                                     "asymmetric_source[N(j!1), N(j!1 + 1), T, error(j!1)]")
                                    ((""
                                      (assert)
                                      (("" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_correct? const-decl "bool" exact_comm 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)
    (asymmetric_source formula-decl nil majority_stage nil)
    (sources_disagree formula-decl nil majority_stage nil)
    (enabled_within? const-decl "bool" exact_comm nil))
   nil)))

¤ Dauer der Verarbeitung: 0.48 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.