# Library inw_def

Set Implicit Arguments.

Require Import Bool.
Require Import Omega.
Require Import misc.

Coercion Local Z_of_nat : nat >-> Z.

Definition inw := nat -> nat.

Fixpoint ones (w:inw) (i:nat) { struct i } :=
match i with
| 0 => 0
| S i' =>
w i + ones w i'
end.

Definition inw_of_ones (ones_w: nat -> nat): inw :=
fun i =>
match i with
| O => 0
| S i' => (ones_w i) - (ones_w i')
end.

Fixpoint sum (w:inw) d k { struct k } :=
match k with
| 0 => 0
| S k' => w (k + d) + sum w d k'
end.

Definition on (w1:inw) (w2:inw) : inw :=
(fun i => sum w2 (ones w1 (pred i)) (w1 i)).

Definition prec (w1 w2: inw) : Prop :=
forall i,
ones w1 i >= ones w2 i.

Definition ones_supremum (w1 w2: inw) : nat -> nat :=
fun i => Arith.Min.min (ones w1 i) (ones w2 i).

Definition ones_infimum (w1 w2: inw) : nat -> nat :=
fun i => Arith.Max.max (ones w1 i) (ones w2 i).

Definition supremum (w1 w2: inw) : inw :=
inw_of_ones (ones_supremum w1 w2).

Definition infimum (w1 w2: inw) : inw :=
inw_of_ones (ones_infimum w1 w2).

Definition sync (w1 w2: inw) : Prop :=
exists b1: Z,
exists b2: Z,
forall i,
(b1 <= ones w2 i - ones w1 i <= b2)%Z.

Definition adaptability (w1 w2: inw) : Prop :=
prec w1 w2 /\ sync w1 w2.

Definition size (w1 w2: inw) (s: nat) :=
forall i,
(ones w1 i) - (ones w2 i) <= s
/\
exists i, (ones w1 i) - (ones w2 i) = s.