# Library inw_prop

Set Implicit Arguments.

Require Import Bool.
Require Import Omega.
Require Import misc.
Require Import inw_def.
Require Import inw_aux.

Remark ones_eq_equiv_w_eq:
forall (w1: inw) ,
forall (w2: inw) ,
(forall i, ones w1 i = ones w2 i) <-> (forall i, i > 0 -> w1 i = w2 i).
Proof.
intros w1 w2.
split.
intros H_ones i H_i_ge_1.
apply ones_eq_impl_w_eq; auto.
intro H_w.
apply w_eq_impl_ones_eq; auto.
Qed.

Remark inw_of_ones_correctness:
forall w: inw,
forall H_wf_w: well_formed_inw w,
forall i,

inw_of_ones (ones w) i = w i.
Proof.
apply inw_of_ones_ones_w_eq_w.
Qed.

Remark inw_of_ones_correctness2:
forall ones_w: nat -> nat,
forall H_wf_ones: well_formed_ones ones_w,
forall i,
ones (inw_of_ones ones_w) i = ones_w i.
Proof.
apply ones_inw_of_ones_ones_w_eq_ones_w.
Qed.

Property ones_on:
forall w1 w2 :inw,
forall i,
ones (on w1 w2) i = ones w2 (ones w1 i).
Proof.
apply ones_on_def.
Qed.

Corollary on_assoc:
forall w1 w2 w3: inw,

forall i,
forall H_i_ge_1: i > 0,
(on (on w1 w2) w3) i = (on w1 (on w2 w3)) i.
Proof.
apply on_assoc_aux.
Qed.

Remark prec_partial_order:
(forall w: inw, prec w w)
/\
(forall w1 w2 w3: inw, prec w1 w2 -> prec w2 w3 -> prec w1 w3)
/\
forall w1 w2: inw, well_formed_inw w1 -> well_formed_inw w2 ->
prec w1 w2 -> prec w2 w1 -> (forall i, i > 0 -> w1 i = w2 i).
Proof.
repeat split.
apply prec_refl.
apply prec_trans.
intros; apply prec_antisym; auto.
Qed.

Remark sync_equiv_relation:
(forall w: inw, sync w w)
/\
(forall w1 w2 w3: inw, sync w1 w2 -> sync w2 w3 -> sync w1 w3)
/\
(forall w1 w2: inw, sync w1 w2 -> sync w2 w1).
Proof.
intros.
repeat split.
apply sync_refl.
apply sync_trans.
apply sync_sym.
Qed.