%
% Purpose : instantiation of multiple-stage majority exchange with 
%           the integration fault model.
%
%


majority_integration
[
  N: [nat -> posnat],
  T: TYPE+
] : THEORY

  BEGIN

  i, j, k: VAR nat


  IMPORTING
    protocol_integration[N, T],
    majority[N, message[T]]

  v: VAR message[T]

  status:       VAR [i : nat -> node_status[N(i)]]
  sent:         VAR [i : nat -> [below(N(i)) -> message[T]]]
  common_check: VAR [i: nat -> non_empty_finite_set[below(N(i))]]
  msg_check:    VAR valid_check_function
  check:        VAR valid_check_function
  mf:           VAR [nat -> majority_function[message[T]]]

  consensus_validity: THEOREM
      check = conforms(msg_check, common_check) AND
      protocol(sent, check, majority_vote(mf), status, j, j + k) AND
      majority_correct?(sent, check, status, j, j + k) AND
      uniform?(sent(j), v)(common_check(j))
    IMPLIES
      uniform?(sent(j + k), v)(common_check(j + k))

  agreement_generation: THEOREM
      check = conforms(msg_check, common_check) AND
      protocol(sent, check, majority_vote(mf), status, j, j + k) AND
      exists_all_symmetric?(sent, check, status, j, j + k)
    IMPLIES
      EXISTS v:
        uniform?(sent(j + k), v)(common_check(j + k))

END majority_integration