%
%
% Purpose : choice functions with ordered values (exact or
%           inexact); definition of a middle value voter; definition
%           of min and max (as compute functions).
%
%

k_ordered
[
    N   : [nat -> posnat],  % Number of source nodes at each stage
    T   : TYPE+,
    <=  : (total_order?[T]),              
    error: [nat -> T]
]: THEORY

  BEGIN

  IMPORTING
    reduce_choice,
    node_functions[N, T],
    select_minmax

  j: VAR nat
  node_set: VAR [j : nat -> non_empty_finite_set[below(N(j))]] 
  sent:  VAR sent_vec 
  local: VAR sent_vec 

  v_min(sent, node_set)(j) : T = v_min[N(j), T, <=](sent(j), node_set(j))
  v_max(sent, node_set)(j) : T = v_max[N(j), T, <=](sent(j), node_set(j))


  k_consensus_function: TYPE = [j:nat -> consensus_function[T,<=]]
  cf: VAR k_consensus_function
  tau: VAR [j:nat -> tau_type]

  reduce_choice(tau, cf): choice_function = 
    LAMBDA j: reduce_choice[N(j), N(j+1), T, <=, error(j)](tau(j), cf(j))


END k_ordered