finite_seqs[T: TYPE+]: THEORY

  BEGIN

  IMPORTING structures@seqs[T], structures@majority_seq[T]

  s, s1, s2: VAR ne_seqs
  fs: VAR finite_sequence[T]

  in_consensus_function: TYPE = [s: ne_seqs -> {t: T | in?(t, s)}]
  
  i: VAR nat
  choose(i)(s): T = 
    IF i < s`length THEN s`seq(i) 
    ELSE s`seq(0)
    ENDIF

  choose_in?: LEMMA in?(choose(i)(s), s)

  choose_consensus: JUDGEMENT choose(i) HAS_TYPE in_consensus_function

  choose_extend(s): sequence[T] = LAMBDA i: choose(i)(s)

  t, d: VAR T

  majority_function: TYPE = [fs: finite_sequence[T] -> {t: T | maj_exists(fs) => is_majority(t, fs)}]

  mf: VAR majority_function

  maj_exists_same: LEMMA
      maj_exists(fs)
    IMPLIES 
      mf(fs) = maj(fs)

  mf_lem: LEMMA
      is_majority(t, fs)
    IMPLIES
      mf(fs) = t

  majority_choose(s): T =
    IF maj_exists(s) THEN maj(s) ELSE choose(0)(s) ENDIF

  majority_choose_consensus: JUDGEMENT majority_choose HAS_TYPE in_consensus_function

  majority_choose2(fs): T = 
    IF fs`length = 0 THEN choose({t:T | TRUE})
    ELSE majority_choose(fs)
    ENDIF

  majority2_choose_majority: JUDGEMENT majority_choose2 HAS_TYPE majority_function

  k: VAR nat

  uniform(fs, t, k): finite_set[below(k)] = { i : below(k) | fs`length = k & fs`seq(i) = t }

  is_majority?(fs, t, k): bool = 2 * card(uniform(fs, t, k)) > k

  majority_same: LEMMA is_majority(t, fs) IFF is_majority?(fs, t, fs`length)


  END finite_seqs