From Coq Require Import ZArith.
From Coq Require Import Lia.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import Count.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Tree_topology.
From Padec Require Import KDomSet_specification_tree_topology.
From Padec Require Import KDomSet_algo_tree_topology.
From Padec Require Import KDomSet_correctness_tree_topology.
From Padec Require Import KDomSet_termination_tree_topology.
From Padec Require Import KDomSet_count_tree_topology.

Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Section KDomSet_Specification_Proved.

  Context {Chans: Channels}
          {Net: Network}
          {DTN: Down_Tree_Network Net}
          {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

  Notation Tree := (DTN_topo (Net := Net)).
  Context {SPAN: is_spanning _ Tree}.

  Notation Algo := KDom_algo.
  Notation Env := (Env (Net := Net) (Algo := KDom_algo)).

  Existing Instance KDom_Stable.
  Existing Instance KDom_RO_assumption.

  Section Silent_Self_Stabilization.

    Theorem kdom_silent_self_stabilization:
      silence KDom_RO_assumption unfair_daemon /\
      self_stabilization KDom_RO_assumption unfair_daemon (only_one (kDOM kDominator_ (k := k))).

  End Silent_Self_Stabilization.

  Section Counting.

    Definition Dominators (g: Env) := { n: Node | kDominator_ g n }.

    Theorem counting:
      forall (g: Env),
        Assume g -> terminal g ->
        exists N D: nat,
          Num_Card Same Node N /\ Num_Card Same (Dominators g) D /\
          (N - 1 >= S (Z.to_nat k) * (D - 1))%nat.

  End Counting.

End KDomSet_Specification_Proved.

Close Scope Z_scope.
Close Scope signature_scope.
Unset Implicit Arguments.