# Library JordanCurveTheorem.Jordan2

Require Export Jordan1.

Inductive set:Set:=
Vs : set | Is : set dart set.

Fixpoint exds(s:set)(z:dart){struct s}:Prop:=
match s with
VsFalse
| Is s0 xx=z exds s0 z
end.

Lemma exds_dec: (s:set)(z:dart),
{exds s z}+{¬exds s z}.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intro.
generalize (eq_dart_dec d z).
generalize (IHs z).
tauto.
Qed.

Lemma not_exds_Vs: s:set,
( z:dart, ¬exds s z) s = Vs.
Proof.
intros.
induction s.
tauto.
generalize (H d).
simpl in |- ×.
tauto.
Qed.

Lemma not_exds_diff: (s:set)(z:dart),
¬exds s z
(t:dart), exds s t z t.
Proof.
intros.
induction s.
simpl in H0.
tauto.
simpl in H0.
simpl in H.
elim H0.
intros.
rewrite <- H1.
intro.
symmetry in H2.
tauto.
apply IHs.
tauto.
Qed.

Fixpoint Ds(s:set)(z:dart){struct s}:set:=
match s with
VsVs
| Is s0 x
if eq_dart_dec x z then (Ds s0 z)
else Is (Ds s0 z) x
end.

Lemma not_exds_Ds:(s:set)(z:dart),
¬exds (Ds s z) z.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d z).
intro.
apply (IHs z).
simpl in |- ×.
generalize (IHs z).
tauto.
Qed.

Lemma exds_Ds:(s:set)(x z:dart),
x z
(exds s z exds (Ds s x) z).
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d x).
intro.
rewrite a.
generalize (IHs x z).
tauto.
intro.
simpl in |- ×.
generalize (IHs x z).
tauto.
Qed.

Lemma exds_Ds_diff:(s:set)(x z:dart),
exds (Ds s x) z x z.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros x z.
elim (eq_dart_dec d x).
intro.
apply IHs.
simpl in |- ×.
intros.
elim H.
intro.
rewrite <- H0.
intro.
rewrite H1 in b.
tauto.
apply IHs.
Qed.

Lemma Ds_s:(s:set)(z:dart),
¬exds s z Ds s z = s.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d z).
intro.
rewrite a.
generalize (IHs z).
intros.
split.
tauto.
intro.
assert (exds (Is s z) z).
simpl in |- ×.
tauto.
rewrite <- H0 in H1.
absurd (exds (Ds s z) z).
apply not_exds_Ds.
tauto.
intro.
split.
intros.
generalize (IHs z).
intros.
assert (Ds s z = s).
tauto.
rewrite H1.
tauto.
intros.
injection H.
generalize (IHs z).
tauto.
Qed.

Lemma not_exds_Ds_bis:(s:set)(x z:dart),
¬exds s z ¬exds (Ds s x) z.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d x).
intro.
apply IHs.
tauto.
simpl in |- ×.
intro.
generalize (IHs x z).
tauto.
Qed.

Lemma exds_Ds_exds:(s:set)(x z:dart),
exds (Ds s x) z exds s z.
Proof.
intros.
generalize (exds_dec s z).
intro.
generalize (exds_dec (Ds s x) z).
intro.
generalize (not_exds_Ds_bis s x z).
tauto.
Qed.

Fixpoint card(s:set):nat:=
match s with
Vs ⇒ 0%nat
| Is s0 x
if exds_dec s0 x then card s0
else (1 + card s0)%nat
end.

Lemma card_Ds: (s:set)(z:dart),
(card (Ds s z) card s)%nat.
Proof.
induction s.
simpl in |- ×.
intro.
omega.
simpl in |- ×.
intro.
elim (eq_dart_dec d z).
intro.
elim (exds_dec s d).
intro.
apply IHs.
intro.
generalize (IHs z).
intro.
omega.
simpl in |- ×.
elim (exds_dec s d).
elim (exds_dec (Ds s z) d).
intros.
apply IHs.
intros.
generalize (exds_Ds s z d).
assert (z d).
intro.
rewrite H in b0.
tauto.
tauto.
elim (exds_dec (Ds s z) d).
intros.
generalize (IHs z).
intro.
omega.
intros.
generalize (IHs z).
intro.
omega.
Qed.

Lemma not_exds_card_Ds: (s:set)(z:dart),
¬exds s z card (Ds s z) = card s.
Proof.
intros.
generalize (Ds_s s z).
intros.
assert (Ds s z = s).
tauto.
rewrite H1.
tauto.
Qed.

Lemma exds_card_pos: (s:set)(z:dart),
exds s z (0 < card s)%nat.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s d).
intro.
apply (IHs d a); tauto.
intro.
omega.
Qed.

Lemma exds_card_Ds: (s:set)(z:dart),
exds s z card (Ds s z) = (card s - 1)%nat.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d z).
intro.
elim (exds_dec s d).
intro.
rewrite a in a0.
apply IHs.
tauto.
intro.
rewrite a in b.
rewrite not_exds_card_Ds.
omega.
tauto.
simpl in |- ×.
elim (exds_dec (Ds s z) d).
elim (exds_dec s d).
intros.
rewrite IHs.
tauto.
tauto.
intros.
generalize (exds_Ds s z d).
assert (z d).
intro.
rewrite H0 in b0.
tauto.
tauto.
elim (exds_dec s d).
intros.
generalize (exds_Ds s z d).
assert (z d).
intro.
rewrite H0 in b0.
tauto.
tauto.
intros.
rewrite IHs.
assert (0 < card s)%nat.
apply exds_card_pos with z.
tauto.
omega.
tauto.
Qed.

Lemma exds_card_Ds_inf: (s:set)(z:dart),
exds s z (card (Ds s z) < card s)%nat.
Proof.
intros.
generalize (exds_card_pos s z H).
generalize (exds_card_Ds s z H).
intros.
omega.
Qed.

Fixpoint fmap_to_set(m:fmap):set:=
match m with
VVs
| I m0 x _ _Is (fmap_to_set m0) x
| L m0 _ _ _ ⇒ (fmap_to_set m0)
end.

Lemma exd_exds:(m:fmap)(z:dart),
exd m z exds (fmap_to_set m) z.
Proof.
induction m.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
generalize (IHm z); tauto.
simpl in |- ×.
tauto.
Qed.

Fixpoint ndN (m:fmap):nat:=
match m with
V ⇒ 0%nat
| I m0 x _ _
if exd_dec m0 x then ndN m0
else (1 + ndN m0)%nat
| L m0 _ _ _ndN m0
end.

Lemma nd_card:(m:fmap),
ndN m = card (fmap_to_set m).
Proof.
induction m.
simpl in |- ×.
tauto.
simpl in |- ×.
elim (exd_dec m d).
elim (exds_dec (fmap_to_set m) d).
tauto.
intros.
generalize (exd_exds m d).
tauto.
elim (exds_dec (fmap_to_set m) d).
intros.
generalize (exd_exds m d).
tauto.
rewrite IHm.
tauto.
simpl in |- ×.
tauto.
Qed.

Fixpoint set_minus(s1 s2:set){struct s1}:set:=
match s1 with
VsVs
| Is s0 x
if exds_dec s2 x then set_minus s0 s2
else Is (set_minus s0 s2) x
end.

Lemma not_exds_minus: (s1 s2:set)(z:dart),
¬ exds s1 z
¬ exds (set_minus s1 s2) z.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s2 d).
intro.
apply IHs1.
tauto.
simpl in |- ×.
intro.
generalize (IHs1 s2 z).
tauto.
Qed.

Lemma exds_set_minus: (s1 s2:set)(z:dart),
exds s1 z ¬exds s2 z
exds (set_minus s1 s2) z.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s2 d).
intro.
elim H.
intro.
rewrite H1 in a.
tauto.
intro.
apply IHs1.
tauto.
tauto.
simpl in |- ×.
intro.
elim H.
tauto.
generalize (IHs1 s2 z).
tauto.
Qed.

Lemma not_exds_set_minus: (s1 s2:set)(z:dart),
exds s2 z ¬exds (set_minus s1 s2) z.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s2 d).
intro.
apply IHs1.
tauto.
simpl in |- ×.
intro.
generalize (IHs1 s2 z).
intro.
assert (d z).
intro.
rewrite H1 in b.
tauto.
tauto.
Qed.

Lemma exds_set_minus_eq:(s1 s2:set)(z:dart),
(exds s1 z ¬exds s2 z) exds (set_minus s1 s2) z.
Proof.
intros.
generalize (not_exds_set_minus s1 s2 z).
generalize (exds_set_minus s1 s2 z).
generalize (exds_dec s2 z).
generalize (exds_dec (set_minus s1 s2) z).
generalize (exds_dec s1 z).
generalize (not_exds_minus s1 s2 z).
tauto.
Qed.

Inductive incls(s1 s2:set):Prop:=
exds2 : ( z:dart, exds s1 z exds s2 z)
incls s1 s2.

Lemma set_minus_s_Ds :(s1 s2:set)(x:dart),
¬ exds s1 x exds s2 x
set_minus s1 (Ds s2 x) = set_minus s1 s2.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec (Ds s2 x) d).
elim (exds_dec s2 d).
intros.
apply IHs1.
tauto.
tauto.
intros.
generalize (exds_Ds s2 x d).
intros.
assert (x d).
intro.
rewrite H2 in H.
tauto.
tauto.
elim (exds_dec s2 d).
intros.
generalize (exds_Ds s2 x d).
intros.
assert (x d).
intro.
rewrite H2 in H.
tauto.
tauto.
intros.
rewrite IHs1.
tauto.
tauto.
tauto.
Qed.

Lemma card_minus_set:(s1 s2:set),
incls s2 s1
(card (set_minus s1 s2) + card s2 = card s1)%nat.
Proof.
induction s1.
simpl in |- ×.
intros.
inversion H.
simpl in H0.
generalize (not_exds_Vs s2 H0).
intro.
rewrite H1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
inversion H.
simpl in H0.
elim (exds_dec s2 d).
elim (exds_dec s1).
intros.
apply IHs1.
constructor.
intros.
elim (H0 z H1).
intro.
rewrite <- H2.
tauto.
tauto.
intros.
generalize (IHs1 (Ds s2 d)).
intros.
inversion H.
assert (incls (Ds s2 d) s1).
constructor.
intros.
assert (d z).
intro.
rewrite H4 in H3.
apply (not_exds_Ds s2 z H3).
generalize (exds_Ds s2 d z H4).
intro.
assert (exds s2 z).
tauto.
assert (exds (Is s1 d) z).
apply H2.
tauto.
simpl in H7.
tauto.
generalize (set_minus_s_Ds s1 s2 d b a).
intro.
rewrite H4 in H1.
generalize (exds_card_Ds s2 d a).
intro.
rewrite H5 in H1.
rewrite <- H1.
generalize (exds_card_pos s2 d a).
intro.
omega.
tauto.
intro.
simpl in |- ×.
elim (exds_dec (set_minus s1 s2) d).
elim (exds_dec s1 d).
intros.
apply IHs1.
constructor.
intros.
elim (H0 z H1).
intro.
rewrite H2 in b.
tauto.
tauto.
intros.
generalize (exds_set_minus_eq s1 s2 d).
tauto.
elim (exds_dec s1 d).
intros.
elim b0.
apply (exds_set_minus s1 s2 d a b).
intros.
rewrite <- IHs1 with s2.
omega.
constructor.
intros.
elim (H0 z).
intro.
rewrite H2 in b.
tauto.
tauto.
tauto.
Qed.

Definition impls(s1 s2:set):Prop:=
z:dart, exds s1 z exds s2 z.

Definition eqs(s1 s2:set):Prop:=
z:dart, exds s1 z exds s2 z.

Definition disjs(s1 s2:set):Prop:=
z:dart, exds s1 z exds s2 z False.

Definition Rs(sy sx:set):=
(card sy < card sx)%nat.

Lemma Acc_set: s:set, Acc Rs s.
Proof.
induction s.
apply Acc_intro.
unfold Rs at 1 in |- ×.
simpl in |- ×.
intros.
inversion H.
apply Acc_intro.
intro y.
unfold Rs at 1 in |- ×.
simpl in |- ×.
inversion IHs.
intro.
elim (eq_nat_dec (card y) (card s)).
intro.
apply Acc_intro.
intro y0.
unfold Rs at 1 in |- ×.
rewrite a.
intro.
apply H.
unfold Rs in |- ×.
tauto.
intro.
apply Acc_intro.
unfold Rs at 1 in |- ×.
intros.
generalize H0.
clear H0.
elim (exds_dec s d).
intros.
apply H.
unfold Rs in |- ×.
omega.
intros.
apply H.
unfold Rs in |- ×.
omega.
Qed.

Lemma Rs_wf : well_founded Rs.
Proof.
unfold well_founded in |- ×.
apply Acc_set.
Qed.

Lemma exds_Rs_Ds:
(s:set)(z:dart),
exds s z Rs (Ds s z) s.
Proof.
unfold Rs in |- ×.
simpl in |- ×.
intros.
apply exds_card_Ds_inf.
tauto.
Qed.

Fixpoint Iter(g:dartdart)(n:nat)(z:dart){struct n}:dart:=
match n with
0%natz
| S n0g (Iter g n0 z)
end.

Module Type Sigf.
Parameter f : fmap dart dart.
Parameter f_1 : fmap dart dart.
Axiom exd_f: (m:fmap)(z:dart),
inv_hmap m (exd m z exd m (f m z)).
Axiom bij_f : m:fmap,
inv_hmap m bij_dart (exd m) (f m).
Axiom exd_f_1: (m:fmap)(z:dart),
inv_hmap m (exd m z exd m (f_1 m z)).
Axiom bij_f_1 : m:fmap,
inv_hmap m bij_dart (exd m) (f_1 m).
Axiom f_1_f : (m:fmap)(z:dart),
inv_hmap m exd m z f_1 m (f m z) = z.
Axiom f_f_1 : (m:fmap )(z:dart),
inv_hmap m exd m z f m (f_1 m z) = z.
End Sigf.

Module Mf(M:Sigf)<:Sigf
with Definition f:=M.f
with Definition f_1:=M.f_1.
Definition f:=M.f.
Definition f_1:=M.f_1.
Definition exd_f:=M.exd_f.
Definition exd_f_1:=M.exd_f_1.
Definition bij_f:=M.bij_f.
Definition bij_f_1:=M.bij_f_1.
Definition f_1_f:=M.f_1_f.
Definition f_f_1:=M.f_f_1.

Lemma exd_Iter_f:(m:fmap)(n:nat)(z:dart),
inv_hmap m (exd m z exd m (Iter (f m) n z)).
Proof.
induction n.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
generalize (exd_f m (Iter (f m) n z)).
generalize (IHn z).
generalize (IHn (Iter (f m) n z)).
tauto.
Qed.

Lemma exd_Iter_f_1:(m:fmap)(n:nat)(z:dart),
inv_hmap m (exd m z exd m (Iter (f_1 m) n z)).
Proof.
induction n.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
generalize (exd_f_1 m (Iter (f_1 m) n z)).
generalize (IHn z).
generalize (IHn (Iter (f_1 m) n z)).
tauto.
Qed.

Theorem Iter_rem_F :
(m:fmap)(z:dart),
sx: set, ( sy: set, Rs sy sx set)
set.
Proof.
intros m z.
refine
(fun sx F
let n:= ((ndN m)-(card sx))%nat in
let zn := Iter (f m) n z in
match exds_dec sx zn with
left _F (Ds sx zn) _
| right _sx
end).
apply exds_Rs_Ds.
tauto.
Defined.

Definition Iter_rem_aux(m:fmap)(z:dart):
set set
:= Fix Rs_wf (fun _:setset) (Iter_rem_F m z).

Definition Iter_upb_aux(m:fmap)(z:dart)(s:set):nat:=
((ndN m) - (card (Iter_rem_aux m z s)))%nat.

Definition Iter_rem(m:fmap)(z:dart):set:=
Iter_rem_aux m z (fmap_to_set m).

Definition Iter_upb(m:fmap)(z:dart):nat:=
((ndN m) - (card (Iter_rem m z)))%nat.

Definition Iter_orb_aux(m:fmap)(z:dart)(s:set):set:=
set_minus (fmap_to_set m) (Iter_rem_aux m z s).

Definition Iter_orb(m:fmap)(z:dart):set:=
set_minus (fmap_to_set m) (Iter_rem m z).

Theorem Iter_rem_aux_equation :
(m:fmap)(z:dart)(sx:set),
Iter_rem_aux m z sx =
let n := ((ndN m) - (card sx))%nat in
let zn := Iter (f m) n z in
if exds_dec sx zn
then Iter_rem_aux m z (Ds sx zn)
else sx.
Proof.
intros m z sx.
unfold Iter_rem_aux in |- ×.
rewrite Fix_eq.
auto.
intros x0 f0 g0 Heqfg.
unfold Iter_rem_F in |- ×.
destruct (exds_dec x0 (Iter (f m)
((ndN m - card x0))%nat z)).
rewrite Heqfg.
trivial.
trivial.
Qed.

Definition P1
(m:fmap)(z:dart)(s:set):Prop:=
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
¬ exds sr (Iter (f m) n z).

Lemma not_exds_rem_upb :
(m:fmap)(z:dart)(s:set),
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
¬ exds sr (Iter (f m) n z).
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P1 m z) _).
unfold P1 in |- ×.
unfold Iter_upb_aux in |- ×.
simpl in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
simpl in |- ×.
apply exds_card_Ds_inf.
tauto.
tauto.
Qed.

Lemma not_exds_Iter_rem_upb :
(m:fmap)(z:dart),
let n:= Iter_upb m z in
¬ exds (Iter_rem m z) (Iter (f m) n z).
Proof.
unfold Iter_rem in |- ×.
unfold Iter_upb in |- ×.
intros m z.
unfold Iter_rem in |- ×.
generalize (not_exds_rem_upb m z (fmap_to_set m)).
simpl in |- ×.
unfold Iter_upb_aux in |- ×.
tauto.
Qed.

Lemma exd_Iter_upb:
(m:fmap)(z:dart), inv_hmap m
exd m z exd m (Iter (f m) (Iter_upb m z) z).
Proof.
intros.
generalize (exd_Iter_f m (Iter_upb m z) z).
tauto.
Qed.

Lemma exd_Iter_orb_upb :
(m:fmap)(z:dart),
inv_hmap m exd m z
let n:= Iter_upb m z in
exds (Iter_orb m z) (Iter (f m) n z).
Proof.
unfold Iter_orb in |- ×.
intros.
apply exds_set_minus.
generalize (exd_exds m (Iter (f m) (Iter_upb m z) z)).
intro.
generalize (exd_Iter_upb m z H H0).
tauto.
apply not_exds_Iter_rem_upb.
Qed.

Lemma exds_rem_orb:(m:fmap)(z t:dart),
inv_hmap m exd m t
(¬exds (Iter_rem m z) t exds (Iter_orb m z) t).
Proof.
intros.
unfold Iter_orb in |- ×.
generalize (exds_set_minus_eq (fmap_to_set m) (Iter_rem m z) t).
generalize (exd_exds m t).
tauto.
Qed.

Definition R3
(m:fmap)(z t:dart)(s:set):Prop:=
¬ exds s t
let sr := Iter_rem_aux m z s in
¬ exds sr t.

Lemma LR3:(m:fmap)(z t:dart)(s:set),
¬ exds s t
let sr := Iter_rem_aux m z s in
¬ exds sr t.
Proof.
intros m z t.
refine (well_founded_ind Rs_wf (R3 m z t) _).
unfold R3 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
apply not_exds_Ds_bis.
tauto.
tauto.
Qed.

Definition R2
(m:fmap)(z:dart)(s:set):Prop:=
let sr := Iter_rem_aux m z s in
¬ exds sr (Iter (f m) (ndN m - card s)%nat z).

Lemma LR2 :
(m:fmap)(z:dart)(s:set),
let sr := Iter_rem_aux m z s in
¬ exds sr (Iter (f m) (ndN m - card s)%nat z).
Proof.
intros m z.
simpl in |- ×.
refine (well_founded_ind Rs_wf (R2 m z) _).
unfold R2 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply LR3.
apply not_exds_Ds.
tauto.
Qed.

Definition R1
(m:fmap)(z:dart)(i:nat)(s:set):Prop:=
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
(ndN m - card s i n)%nat
¬ exds sr (Iter (f m) i z).
Lemma LR1 :
(m:fmap)(z:dart)(i:nat)(s:set),
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
(ndN m - card s i n)%nat
¬ exds sr (Iter (f m) i z).
Proof.
intros m z i.
refine (well_founded_ind Rs_wf (R1 m z i) _).
unfold R1 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
elim (eq_nat_dec i (ndN m - card x)%nat).
intro.
rewrite a.
apply LR2.
intro.
generalize H0.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intros.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
split.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x)%nat z) a).
intro.
rewrite H2.
elim H0.
intros.
clear H a H1 H2 H0 H4.
omega.
tauto.
intros.
clear H H0 b0.
omega.
Qed.

Lemma not_exds_Iter_f_i :
(m:fmap)(z:dart)(i:nat),
let sr := Iter_rem m z in
let n := Iter_upb m z in
(i n)%nat ¬ exds sr (Iter (f m) i z).
Proof.
simpl in |- ×.
unfold Iter_upb in |- ×.
unfold Iter_rem in |- ×.
intros.
apply LR1.
generalize (nd_card m).
intro.
rewrite H0.
simpl in |- ×.
unfold Iter_upb in |- ×.
unfold Iter_upb_aux in |- ×.
omega.
Qed.

Lemma exds_Iter_f_i :
(m:fmap)(z:dart)(i:nat),
inv_hmap m exd m z
let s := Iter_orb m z in
let n := Iter_upb m z in
(i n)%nat exds s (Iter (f m) i z).
Proof.
intros.
assert (exd m (Iter (f m) i z)).
generalize (exd_Iter_f m i z H).
intro.
tauto.
generalize (exds_rem_orb m z (Iter (f m) i z) H H2).
unfold s in |- ×.
intros.
generalize (not_exds_Iter_f_i m z i).
simpl in |- ×.
tauto.
Qed.

Definition P2
(m:fmap)(z:dart)(s:set):Prop:=
(card s < ndN m
card (Iter_rem_aux m z s) < ndN m)%nat.

Lemma card_rem_aux:(m:fmap)(z:dart)(s:set),
(card s < ndN m
card (Iter_rem_aux m z s) < ndN m)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P2 m z) _).
unfold P2 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
omega.
tauto.
Qed.

Definition P2_bis
(m:fmap)(z:dart)(s:set):Prop:=
(card s ndN m
card (Iter_rem_aux m z s) ndN m)%nat.

Lemma card_rem_aux_bis:(m:fmap)(z:dart)(s:set),
(card s ndN m
card (Iter_rem_aux m z s) ndN m)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P2_bis m z) _).
unfold P2_bis in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
omega.
tauto.
Qed.

Lemma upb_pos_aux:(m:fmap)(z:dart),
exd m z
(card (Iter_rem m z) < ndN m)%nat.
Proof.
intros.
unfold Iter_rem in |- ×.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec (fmap_to_set m) (Iter (f m) (ndN m - card (fmap_to_set m)) z)).
intro.
apply card_rem_aux.
assert
(card (Ds (fmap_to_set m)
(Iter (f m) (ndN m - card (fmap_to_set m)) z)) <
card (fmap_to_set m))%nat.
apply exds_card_Ds_inf.
tauto.
generalize (nd_card m).
intro.
omega.
intro.
generalize (nd_card m).
intro.
assert (ndN m - card (fmap_to_set m) = 0)%nat.
omega.
rewrite H1 in b.
simpl in b.
generalize (exd_exds m z).
intro.
generalize (exds_dec (fmap_to_set m) z).
tauto.
Qed.

Theorem upb_pos:(m:fmap)(z:dart),
exd m z (0 < Iter_upb m z)%nat.
Proof.
unfold Iter_upb in |- ×.
intros.
generalize (upb_pos_aux m z).
intros.
generalize (H0 H).
intro.
omega.
Qed.

Definition Q1(m:fmap)(z:dart)(s:set):Prop:=
(card (Iter_rem_aux m z s) card s)%nat.

Lemma LQ1:(m:fmap)(z:dart)(s:set),
(card (Iter_rem_aux m z s) card s)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (Q1 m z) _).
unfold Q1 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
assert (card (Ds x (Iter (f m)
(ndN m - card x) z)) < card x)%nat.
apply exds_card_Ds_inf.
tauto.
assert
(card (Iter_rem_aux m z
(Ds x (Iter (f m) (ndN m - card x) z)))
card (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
apply H.
unfold Rs in |- ×.
tauto.
omega.
intro.
omega.
Qed.

Definition Q2(m:fmap)(z:dart)(s:set):Prop:=
exds s (Iter (f m) (ndN m - card s)%nat z)
(card (Iter_rem_aux m z s) < card s)%nat.

Lemma LQ2:(m:fmap)(z:dart)(s:set),
exds s (Iter (f m) (ndN m - card s) z)
(card (Iter_rem_aux m z s) < card s)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (Q2 m z) _).
unfold Q2 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
assert
(card (Iter_rem_aux m z (Ds x (Iter (f m)
(ndN m - card x) z)))
card (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
apply LQ1.
omega.
tauto.
Qed.

Definition PL2(m:fmap)(z t:dart)(x:set):Prop:=
inv_hmap m exd m z exds x t
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t
exds x zn0
¬ exds (Iter_rem_aux m z (Ds x zn0)) t.

Lemma L2:(m:fmap)(z t:dart)(x:set),
inv_hmap m exd m z exds x t
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t
exds x zn0
¬ exds (Iter_rem_aux m z (Ds x zn0)) t.
Proof.
intros m z t.
refine (well_founded_ind Rs_wf (PL2 m z t) _).
unfold PL2 in |- ×.
intros.
generalize H3.
clear H3.
rewrite (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
tauto.
tauto.
Qed.

Definition PL3(m:fmap)(z t:dart)(x:set):Prop:=
inv_hmap m exd m z exds x t
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t
exds x zn0.

Lemma L3:(m:fmap)(z t:dart)(x:set),
inv_hmap m exd m z exds x t
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t
exds x zn0.
Proof.
intros m z t.
refine (well_founded_ind Rs_wf (PL3 m z t) _).
unfold PL3 in |- ×.
intros.
generalize H3.
clear H3.
rewrite (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
tauto.
tauto.
Qed.

Definition P4(m:fmap)(z t:dart)(s:set):Set:=
inv_hmap m exd m z exds s t
(card s ndN m)%nat
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
¬ exds sr t
{i:nat | (i < nr)%nat Iter (f m) i z = t}.

Lemma ex_i_aux :(m:fmap)(z t:dart)(s:set),
inv_hmap m exd m z exds s t
(card s ndN m)%nat
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
¬ exds sr t
{i:nat | (i < nr)%nat Iter (f m) i z = t}.
Proof.
intros m z t.
refine (well_founded_induction Rs_wf (P4 m z t) _).
unfold P4 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x)%nat z)).
intro.
elim (eq_dart_dec (Iter (f m) (ndN m - card x)%nat z) t).
intro.
split with (ndN m - card x)%nat.
split.
assert
(card (Iter_rem_aux m z (Ds x (Iter (f m)
(ndN m - card x) z)))
card (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
apply LQ1.
generalize (exds_card_Ds_inf x
(Iter (f m) (ndN m - card x)%nat z)).
intros.
generalize (H6 a).
intro.
omega.
tauto.
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
tauto.
tauto.
generalize (exds_Ds x (Iter (f m) (ndN m - card x)%nat z) t).
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
omega.
apply L2.
tauto.
tauto.
tauto.
tauto.
tauto.
intro.
absurd (exds x (Iter (f m) (ndN m - card x)%nat z)).
tauto.
eapply L3.
tauto.
tauto.
apply H2.
tauto.
Qed.

Lemma ex_i :(m:fmap)(z t:dart),
inv_hmap m exd m z exd m t
let sr:= Iter_rem m z in
let nr:= Iter_upb m z in
¬ exds sr t
{i : nat | (i < nr)%nat Iter (f m) i z = t}.
Proof.
unfold Iter_rem in |- ×.
unfold Iter_upb in |- ×.
intros.
generalize ex_i_aux.
simpl in |- ×.
unfold Iter_rem in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
apply H3.
tauto.
tauto.
generalize (exd_exds m t).
tauto.
rewrite nd_card.
omega.
tauto.
Qed.

Lemma ex_i_upb :(m:fmap)(z:dart),
inv_hmap m exd m z
let nr:= Iter_upb m z in
{i : nat | (i < nr)%nat Iter (f m) i z = Iter (f m) nr z}.
Proof.
intros.
unfold nr in |- ×.
apply ex_i.
tauto.
tauto.
generalize (exd_Iter_f m (Iter_upb m z) z).
tauto.
generalize not_exds_rem_upb.
simpl in |- ×.
intros.
unfold Iter_rem in |- *; unfold Iter_upb in |- ×.
unfold Iter_rem in |- ×.
unfold Iter_upb_aux in H1.
apply H1.
Qed.

Lemma Iter_plus:(m:fmap)(z:dart)(p i:nat),
inv_hmap m exd m z
Iter (f m) (p + i)%nat z = Iter (f m) i z
Iter (f m) p z = z.
Proof.
induction i.
simpl in |- ×.
assert (p + 0 = p)%nat.
omega.
rewrite H.
tauto.
simpl in |- ×.
assert (p + S i = S (p + i))%nat.
omega.
rewrite H.
simpl in |- ×.
clear H.
intros.
assert
(f_1 m (f m (Iter (f m) (p + i)%nat z)) =
f_1 m (f m (Iter (f m) i z))).
rewrite H1.
tauto.
rewrite f_1_f in H2.
rewrite f_1_f in H2.
apply IHi.
tauto.
tauto.
tauto.
tauto.
generalize (exd_Iter_f m i z).
tauto.
tauto.
generalize (exd_Iter_f m (p + i) z).
tauto.
Qed.

Lemma Iter_plus_inv:(m:fmap)(z:dart)(p i:nat),
inv_hmap m exd m z
Iter (f m) p z = z
Iter (f m) (p + i)%nat z = Iter (f m) i z.
Proof.
induction i.
simpl in |- ×.
assert (p + 0 = p)%nat.
omega.
rewrite H.
tauto.
simpl in |- ×.
assert (p + S i = S (p + i))%nat.
omega.
rewrite H.
simpl in |- ×.
clear H.
intros.
rewrite IHi.
tauto.
tauto.
tauto.
tauto.
Qed.

Lemma Iter_mult:(m:fmap)(z:dart)(n p:nat),
inv_hmap m exd m z
Iter (f m) p z = z Iter (f m) (n×p)%nat z = z.
Proof.
induction n.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
rewrite Iter_plus_inv.
apply (IHn p H H0 H1).
tauto.
tauto.
tauto.
Qed.

Lemma Iter_plus_mult:(m:fmap)(z:dart)(n p i:nat),
inv_hmap m exd m z
Iter (f m) p z = z
Iter (f m) (i + n×p)%nat z = Iter (f m) i z.
Proof.
intros.
induction n.
simpl in |- ×.
assert (i + 0 = i)%nat.
omega.
rewrite H2.
tauto.
simpl in |- ×.
assert (i + (p + n × p) = p + (i + n × p))%nat.
omega.
rewrite H2.
rewrite Iter_plus_inv.
tauto.
tauto.
tauto.
tauto.
Qed.

Lemma Iter_comp:(m:fmap)(i j:nat)(z:dart),
Iter (f m) (i+j)%nat z = Iter (f m) i (Iter (f m) j z).
Proof.
induction i.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
rewrite IHi.
tauto.
Qed.

Lemma f_1_Iter_f:(m:fmap)(i:nat)(z:dart),
inv_hmap m exd m z
(f_1 m) (Iter (f m) (S i) z) = Iter (f m) i z.
Proof.
induction i.
simpl in |- ×.
intros.
apply f_1_f.
trivial.
trivial.
simpl in |- ×.
intros.
rewrite f_1_f.
tauto.
tauto.
assert (f m (Iter (f m) i z) = Iter (f m) (S i) z).
simpl in |- ×.
tauto.
rewrite H1.
generalize (exd_Iter_f m (S i) z).
tauto.
Qed.

Lemma Iter_f_f_1 :(m:fmap)(i j:nat)(z:dart),
inv_hmap m exd m z (j i)%nat
Iter (f_1 m) j (Iter (f m) i z) =
Iter (f m) (i - j)%nat z.
Proof.
induction i.
intros.
assert (j = 0)%nat.
omega.
rewrite H2.
simpl in |- ×.
trivial.
induction j.
simpl in |- ×.
tauto.
intros.
simpl in |- ×.
assert (f m (Iter (f m) i z) = Iter (f m) (S i) z).
simpl in |- ×.
tauto.
rewrite H2.
rewrite IHj.
assert (S i - j = S (i - j))%nat.
omega.
rewrite H3.
apply f_1_Iter_f.
trivial.
trivial.
trivial.
trivial.
omega.
Qed.

Lemma Iter_f_f_1_i:(m:fmap)(i:nat)(z:dart),
inv_hmap m exd m z
Iter (f_1 m) i (Iter (f m) i z) = z.
Proof.
intros.
rewrite Iter_f_f_1.
assert (i - i = 0)%nat.
omega.
rewrite H1.
simpl in |- ×.
trivial.
trivial.
trivial.
omega.
Qed.

Lemma Iter_f_Si:(m:fmap)(i:nat)(z:dart),
inv_hmap m exd m z
Iter (f m) (S i) z = Iter (f m) i (f m z).
Proof.
simpl in |- ×.
intros.
induction i.
simpl in |- ×.
tauto.
simpl in |- ×.
rewrite IHi in |- ×.
tauto.
Qed.

Lemma Iter_f_1_Si:(m:fmap)(i:nat)(z:dart),
inv_hmap m exd m z
Iter (f_1 m) (S i) z = Iter (f_1 m) i (f_1 m z).
Proof.
simpl in |- ×.
intros.
induction i.
simpl in |- ×.
tauto.
simpl in |- ×.
rewrite IHi in |- ×.
tauto.
Qed.

Definition diff_int_aux
(m:fmap)(z:dart)(a b:nat)(t:dart): Prop:=
i : nat, (a i b)%nat
Iter (f m) i z t.

Lemma diff_int_aux_dec:(m:fmap)(z:dart)(a b:nat)(t:dart),
{diff_int_aux m z a b t} + {¬diff_int_aux m z a b t}.
Proof.
intros.
elim (le_gt_dec b a).
intro.
elim (eq_nat_dec a b).
intro.
rewrite <- a1.
elim (eq_dart_dec (Iter (f m) a z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a2.
apply H.
omega.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
assert (i = a).
omega.
rewrite H0.
tauto.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
omega.
induction b.
intro.
absurd (0 > a)%nat.
omega.
tauto.
intro.
elim (eq_nat_dec a b).
intro.
rewrite a0.
elim (eq_dart_dec (Iter (f m) b z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a1.
apply H.
omega.
intro.
elim (eq_dart_dec (Iter (f m) (S b) z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a1.
apply H.
omega.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
assert (i = b i = S b).
omega.
elim H0.
intro.
rewrite H1.
tauto.
intro.
rewrite H1.
tauto.
intro.
assert (b > a)%nat.
omega.
elim (IHb H).
intro.
elim (eq_dart_dec (Iter (f m) (S b) z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a1.
apply H0.
omega.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
unfold diff_int_aux in a0.
elim (eq_nat_dec i (S b)).
intro.
rewrite a1.
tauto.
intro.
assert (a i b)%nat.
omega.
apply (a0 i H1).
intro.
right.
unfold diff_int_aux in |- ×.
unfold diff_int_aux in b2.
intro.
apply b2.
intros.
apply H0.
omega.
Qed.

Definition diff_int
(m:fmap)(z:dart)(a b:nat): Prop:=
i j : nat, (a i i < j j b)%nat
Iter (f m) i z Iter (f m) j z.

Lemma diff_int_le:(m:fmap)(z:dart)(a b:nat),
(b a)%nat diff_int m z a b.
Proof.
intros.
unfold diff_int in |- ×.
intros.
omega.
Qed.

Lemma diff_int_dec:(m:fmap)(z:dart)(a b:nat),
{diff_int m z a b} + {¬diff_int m z a b}.
Proof.
intros.
induction b.
left.
unfold diff_int in |- ×.
intros.
omega.
elim IHb.
intro.
generalize (diff_int_aux_dec m z a b (Iter (f m) (S b) z)).
intros.
elim H.
intro.
clear IHb H.
left.
unfold diff_int in |- ×.
intros.
unfold diff_int in a0.
unfold diff_int_aux in a1.
elim (eq_nat_dec j (S b)).
intro.
rewrite a2.
apply a1.
omega.
intro.
apply a0.
omega.
intro.
clear IHb H.
unfold diff_int_aux in b0.
right.
unfold diff_int in |- ×.
intro.
apply b0.
intros.
apply H.
omega.
intro.
unfold diff_int in b0.
right.
unfold diff_int in |- ×.
intro.
apply b0.
intros.
apply H.
omega.
Qed.

Definition exds_int(m:fmap)(z:dart)(a b:nat)(s:set):Prop:=
i:nat, (a i b)%nat
exds s (Iter (f m) i z).

Lemma exds_int_gt:(m:fmap)(z:dart)(a b:nat)(s:set),
(b < a)%nat exds_int m z a b s.
Proof.
intros.
unfold exds_int in |- ×.
intros.
absurd (b < a)%nat.
omega.
tauto.
Qed.

Lemma exds_int_dec : (m:fmap)(z:dart)(a b:nat)(s:set),
{exds_int m z a b s} + {¬exds_int m z a b s}.
Proof.
intros.
elim (le_gt_dec a b).
intro.
induction b.
elim (exds_dec s z).
intro.
left.
unfold exds_int in |- ×.
intros.
assert (i = 0)%nat.
omega.
rewrite H0.
simpl in |- ×.
tauto.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b.
assert (exds s (Iter (f m) 0%nat z)).
apply H.
omega.
simpl in H0.
tauto.
elim (eq_nat_dec a (S b)).
intro.
rewrite <- a1.
elim (exds_dec s (Iter (f m) a z)).
intro.
left.
unfold exds_int in |- ×.
intros.
assert (i = a).
omega.
rewrite H0.
tauto.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b0.
apply H.
omega.
intro.
assert (a b)%nat.
omega.
elim (IHb H).
intro.
elim (exds_dec s (Iter (f m) (S b) z)).
intro.
left.
unfold exds_int in |- ×.
intros.
elim (eq_nat_dec i (S b)).
intro.
rewrite a3.
tauto.
intro.
unfold exds_int in a1.
apply a1.
omega.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b1.
apply H0.
omega.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b1.
unfold exds_int in |- ×.
intros.
apply H0.
omega.
intro.
left.
apply exds_int_gt.
omega.
Qed.

Lemma rem_1_step :(m:fmap)(z:dart)(s:set),
inv_hmap m
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
(card sr + 1 card s
exds s (Iter (f m) (ndN m - card s) z))%nat.
Proof.
simpl in |- ×.
intros.
generalize (Iter_rem_aux_equation m z s).
simpl in |- ×.
intro.
split.
intro.
generalize H0.
elim (exds_dec s (Iter (f m) (ndN m - card s) z)).
tauto.
intros.
rewrite H2 in H1.
absurd (card s + 1 card s)%nat.
omega.
tauto.
intro.
generalize (LQ2 m z s H1).
intro.
omega.
Qed.

Lemma rem_2_steps :(m:fmap)(z:dart)(s:set),
inv_hmap m
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
(card sr + 2 card s
exds (Ds s (Iter (f m) (ndN m - card s) z))
(Iter (f m) (ndN m + 1 - card s) z))%nat.
Proof.
intros.
generalize (rem_1_step m z
(Ds s (Iter (f m) (ndN m - card s)%nat z)) H).
simpl in |- ×.
generalize (rem_1_step m z s H).
simpl in |- ×.
intros.
assert (card (Iter_rem_aux m z s) + 1 card s)%nat.
unfold sr in H0. clear H1 H2.
omega.
assert (exds s (Iter (f m) (ndN m - card s)%nat z)).
tauto.
generalize (Iter_rem_aux_equation m z s).
simpl in |- ×.
elim (exds_dec s (Iter (f m) (ndN m - card s) z)).
intros.
assert (card (Ds s (Iter (f m) (ndN m - card s) z)) + 1
= card s)%nat.
rewrite exds_card_Ds.
clear H1 H2 H3 H4 a H5.
omega.
tauto.
assert (card (Ds s (Iter (f m) (ndN m - card s) z))
= card s - 1)%nat.
clear H1 H2 H3 H4 a H5.
omega.
unfold sr in H0.
rewrite H7 in H2.
rewrite <- H5 in H2.
assert (card (Iter_rem_aux m z s) + 1 card s - 1)%nat.
clear H1 H2 H3 H4 a H5 H6 H7.
omega.
assert (ndN m + 1 - card s = ndN m - (card s - 1))%nat.
clear H1 H2 H3 H4 a H5 H6 H7 H8.
omega.
rewrite <- H9 in H2.
tauto.
tauto.
Qed.

Definition P6(m:fmap)(z:dart)(s:set):Prop:=
inv_hmap m
(card s ndN m
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z)
exds_int m z n0 (nr - 1) s)%nat.

Lemma LP6:(m:fmap)(z:dart)(s:set),
inv_hmap m
(card s ndN m
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z)
exds_int m z n0 (nr - 1) s)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P6 m z) _).
unfold P6 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
generalize (LQ1 m z x).
intro.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
intro.
rewrite H4.
generalize H4.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intros.
clear H4.
generalize
(exds_card_Ds x (Iter (f m) (ndN m - card x)%nat z) a).
intro.
generalize (H (Ds x (Iter (f m) (ndN m - card x)%nat z))).
intros.
generalize (rem_1_step m z x H0).
simpl in |- ×.
intros.
assert (card (Iter_rem_aux m z x) + 1 card x)%nat.
tauto.
clear H7.
elim (eq_nat_dec (card (Iter_rem_aux m z x) + 1)
(card x))%nat.
intro.
rewrite <- H5.
assert (ndN m - card (Iter_rem_aux m z x) - 1
= ndN m - card x)%nat.
clear H3 H4 H8.
omega.
rewrite H7.
unfold exds_int in |- ×.
intros.
assert (i = ndN m - card x)%nat.
clear H1 H3 H4 H8 a0 H7.
omega.
rewrite H10.
tauto.
intro.
assert (card (Iter_rem_aux m z x) + 2 card x)%nat.
clear H1 H3 H4.
omega.
generalize (rem_2_steps m z x H0 H7).
intro.
rewrite H4 in H6.
assert (ndN m - (card x - 1) = ndN m + 1 - card x)%nat.
clear H3 H4 H5 H8 b.
omega.
rewrite H10 in H6.
rewrite <- H5.
rewrite <- H5 in H6.
unfold exds_int in |- ×.
intros.
elim (eq_nat_dec (ndN m - card x) i)%nat.
intro.
rewrite <- a0.
tauto.
intro.
assert
(exds_int m z (ndN m + 1 - card x)
(ndN m - card (Iter_rem_aux m z x) - 1)
(Ds x (Iter (f m) (ndN m - card x) z)))%nat.
apply H6.
unfold Rs in |- ×.
clear H1 H3 H5 H8 b H10 H11 b0.
omega.
tauto.
clear H3 H5 H4 H8 H7 H10 H11 b0.
omega.
tauto.
unfold exds_int in H12.
assert (exds (Ds x (Iter (f m)
(ndN m - card x) z)) (Iter (f m) i z))%nat.
apply H12.
clear H10.
clear H1 H3 H5 H4 H8 H7 H8 b.
omega.
eapply exds_Ds_exds.
apply H13.
tauto.
Qed.

Definition P7(m:fmap)(z:dart)(s:set):Prop:=
inv_hmap m
(card s ndN m
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z)
j:nat, n0 < j nr - 1
Iter (f m) n0 z Iter (f m) j z)%nat.

Lemma LP7:(m:fmap)(z:dart)(s:set),
inv_hmap m
(card s ndN m
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z)
j:nat, n0 < j nr - 1
Iter (f m) n0 z Iter (f m) j z)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P7 m z) _).
unfold P7 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
generalize (LQ1 m z x).
generalize (rem_1_step m z x H0).
simpl in |- ×.
intro.
assert (card (Iter_rem_aux m z x) + 1 card x)%nat.
tauto.
clear H4.
intro.
clear H4.

elim (eq_nat_dec (card (Iter_rem_aux m z x) + 1)
(card x))%nat.
intro.
clear H5.
omega.
intro.
assert (card (Iter_rem_aux m z x) + 2 card x)%nat.
omega.
generalize (rem_2_steps m z x H0 H4).
intro.
clear b H5.
elim
(eq_dart_dec (Iter (f m) (ndN m - card x) z)
(Iter (f m)
(ndN m - card (Iter_rem_aux m z x) - 1) z))%nat.
intros.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
= card x - 1)%nat.
rewrite exds_card_Ds.
tauto.
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
ndN m)%nat.
omega.
generalize (LP6 m z
(Ds x (Iter (f m) (ndN m - card x) z)) H0 H7)%nat.
simpl in |- ×.
intros.
rewrite H5 in H8.
unfold Iter_upb_aux in H8.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intros.
clear a0.
rewrite <- H9 in H8.
assert (ndN m - (card x - 1) =
ndN m + 1 - card x)%nat.
clear H3 a H5 H7 H9.
omega.
rewrite H10 in H8.
generalize (H8 H6).
intro.
clear H8.
unfold exds_int in H11.
assert
(exds (Ds x (Iter (f m) (ndN m - card x) z))
(Iter (f m)
(ndN m - card (Iter_rem_aux m z x) - 1) z))%nat.
apply H11.
split.
clear H3 a H H7 H9 H10.
omega.
apply le_refl.
rewrite <- a in H8.
absurd
(exds (Ds x (Iter (f m) (ndN m - card x) z))
(Iter (f m) (ndN m - card x) z))%nat.
apply not_exds_Ds.
tauto.
tauto.
intros.
elim (eq_nat_dec
(ndN m - card (Iter_rem_aux m z x) - 1) j)%nat.
intro.
rewrite <- a.
tauto.
intro.
generalize (H (Ds x (Iter (f m)
(ndN m - card x) z)))%nat.
intro.
assert
( j : nat,
ndN m - card (Ds x (Iter (f m) (ndN m - card x) z))
< j ndN m - card (Iter_rem_aux m z
(Ds x (Iter (f m) (ndN m - card x) z))) - 1
Iter (f m)
(ndN m - card (Ds x (Iter (f m) (ndN m - card x) z))) z
Iter (f m) j z)%nat.
apply H5.
unfold Rs in |- ×.
rewrite exds_card_Ds.
clear H1 H3 b b0.
omega.
tauto.
tauto.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x) z) H2)%nat.
intro.
rewrite H7.
clear H3 H4 b b0 H7.
omega.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x) z) H2)%nat.
intro.
rewrite H7.
assert (ndN m - (card x - 1) =
ndN m + 1 - card x)%nat.
clear H3 b b0 H7.
omega.
rewrite H8.
tauto.
clear H5.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x) z) H2)%nat.
intro.
rewrite H5 in H7.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z))%nat.
intros.
clear a.
rewrite <- H8 in H7.
assert (ndN m - (card x - 1) = ndN m + 1 - card x)%nat.
clear H3 b b0 H5 H8.
omega.
rewrite H9 in H7.
intro.
assert (Iter (f m) (S (ndN m - card x)) z
= Iter (f m) (S j) z)%nat.
simpl in |- ×.
rewrite H10.
tauto.
generalize H11.
assert (S (ndN m - card x) = ndN m + 1 - card x)%nat.
clear H9.
clear H5.
clear H3 b b0 H8 H10 H11.
omega.
rewrite H12.
apply H7.
split.
rewrite <- H12.
apply lt_n_S.
tauto.
clear H12.
clear H9.
clear H5.
clear H4.
clear H1 b H8 H10 H11.
elim H3.
intros.
clear H1.
clear H3.
omega.
tauto.
Qed.

Definition P8(m:fmap)(z:dart)(s:set):Prop:=
inv_hmap m
(card s ndN m
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z)
diff_int m z n0 (nr - 1))%nat.

Lemma LP8:(m:fmap)(z:dart)(s:set),
inv_hmap m
(card s ndN m
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z)
diff_int m z n0 (nr - 1))%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P8 m z) _).
unfold P8 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
generalize (rem_1_step m z x H0).
simpl in |- ×.
intro.
assert (card (Iter_rem_aux m z x) + 1 card x)%nat.
tauto.
clear H3.
elim (eq_nat_dec (card (Iter_rem_aux m z x) + 1)
(card x))%nat.
intro.
clear H4.
assert (ndN m - card (Iter_rem_aux m z x) - 1
= ndN m - card x)%nat.
omega.
rewrite H3.
apply diff_int_le.
apply le_refl.
intro.
assert (card (Iter_rem_aux m z x) + 2 card x)%nat.
omega.
clear b H4.
generalize (rem_2_steps m z x H0 H3).
intro.
generalize (LP7 m z x H0 H1 H2).
intro.
unfold diff_int in |- ×.
intros.
elim (eq_nat_dec (ndN m - card x) i)%nat.
intro.
rewrite <- a.
unfold Iter_upb_aux in H5.
apply H5.
split.
rewrite a.
tauto.
tauto.
intro.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
= card x - 1)%nat.
rewrite exds_card_Ds.
tauto.
tauto.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z))%nat.
intros.
clear a.
clear H5.
generalize (H (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
intros.
assert
(diff_int m z
(ndN m - card (Ds x (Iter (f m) (ndN m - card x) z)))
(ndN m -
card (Iter_rem_aux m z
(Ds x (Iter (f m) (ndN m - card x) z))) -
1))%nat.
apply H5.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
tauto.
rewrite H7.
omega.
rewrite H7.
assert (ndN m - (card x - 1) = ndN m + 1 - card x)%nat.
clear H5.
clear H.
clear H8.
omega.
rewrite H9.
tauto.
clear H5 H.
rewrite <- H8 in H9.
unfold diff_int in H9.
rewrite H7 in H9.
apply H9.
split.
clear H8 H9.
clear H1 H3 H4.
clear H0.
omega.
tauto.
tauto.
Qed.

Definition diff_orb(m:fmap)(z:dart):Prop:=
let nr:= Iter_upb_aux m z (fmap_to_set m) in
(diff_int m z 0 (nr - 1))%nat.

Theorem exd_diff_orb:(m:fmap)(z:dart),
inv_hmap m exd m z
diff_orb m z.
intros.
unfold diff_orb in |- ×.
generalize (nd_card m).
intro.
assert (ndN m - card (fmap_to_set m) = 0)%nat.
rewrite H1.
omega.
cut
(diff_int m z (ndN m - card (fmap_to_set m))
(Iter_upb_aux m z (fmap_to_set m) - 1))%nat.
rewrite H2.
tauto.
apply LP8.
tauto.
rewrite H1.
apply le_refl.
rewrite H2.
simpl in |- ×.
generalize (exd_exds m z).
tauto.
Qed.

Theorem Iter_upb_period:(m:fmap)(z:dart),
inv_hmap m exd m z
let nr:= Iter_upb m z in
Iter (f m) nr z = z.
Proof.
simpl in |- ×.
intros.
generalize (ex_i_upb m z H H0).
simpl in |- ×.
intros.
elim H1.
intros i Hi.
clear H1.
elim (eq_nat_dec i 0%nat).
intro.
rewrite a in Hi.
simpl in Hi.
symmetry in |- ×.
tauto.
intro.
decompose [and] Hi.
clear Hi.
assert (f_1 m (Iter (f m) i z) =
f_1 m (Iter (f m) (Iter_upb m z) z)).
rewrite H2.
tauto.
set (i1 := (i - 1)%nat) in |- ×.
set (nr1 := (Iter_upb m z - 1)%nat) in |- ×.
assert (i = S i1).
unfold i1 in |- ×.
omega.
assert (Iter_upb m z = S nr1).
unfold nr1 in |- ×.
omega.
rewrite H5 in H3.
rewrite H4 in H3.
simpl in H3.
rewrite f_1_f in H3.
rewrite f_1_f in H3.
unfold i1 in H3.
unfold nr1 in H3.
absurd (Iter (f m) (i - 1)%nat z =
Iter (f m) (Iter_upb m z - 1)%nat z).
generalize (LP8 m z (fmap_to_set m) H).
simpl in |- ×.
intros.
unfold diff_int in H6.
assert
( i j : nat,
ndN m - card (fmap_to_set m) i
i < j Iter_upb_aux m z (fmap_to_set m) - 1
Iter (f m) i z Iter (f m) j z)%nat.
apply H6.
rewrite nd_card.
apply le_refl.
assert (ndN m - card (fmap_to_set m) = 0)%nat.
rewrite nd_card.
simpl in |- ×.
omega.
rewrite H7.
simpl in |- ×.
generalize (exd_exds m z).
tauto.
apply H7.
split.
clear H6.
clear H7.
clear H2.
rewrite nd_card.
omega.
clear H7 H6.
clear H2.
split.
omega.
unfold Iter_upb in |- ×.
unfold Iter_upb_aux in |- ×.
unfold Iter_rem in |- ×.
apply le_refl.
tauto.
tauto.
generalize (exd_Iter_f m nr1 z).
tauto.
tauto.
generalize (exd_Iter_f m i1 z).
tauto.
Qed.

Lemma Iter_period:(m:fmap)(z:dart)(i n:nat),
inv_hmap m exd m z
let p:= Iter_upb m z in
Iter (f m) (i + n×p)%nat z = Iter (f m) i z.
Proof.
intros.
intros.
assert (Iter (f m) p z = z).
unfold p in |- ×.
apply Iter_upb_period.
tauto.
tauto.
rewrite Iter_plus_mult.
trivial.
assumption.
assumption.
assumption.
Qed.

Require Import Euclid.

Lemma mod_p:(m:fmap)(z:dart)(i:nat),
inv_hmap m exd m z
let p := Iter_upb m z in
{j :nat | Iter (f m) i z = Iter (f m) j z (j < p)%nat}.
Proof.
intros.
assert (p > 0)%nat.
unfold p in |- ×.
generalize (upb_pos m z H0).
intro.
omega.
generalize (modulo p H1 i).
intro.
elim H2.
intros r Hr.
split with r.
elim Hr.
intros q Hq.
elim Hq.
clear Hq.
intros.
split.
rewrite H3.
rewrite plus_comm.
unfold p in |- ×.
rewrite Iter_period.
trivial.
tauto.
tauto.
omega.
Qed.

Require Export Compare.

Lemma period_uniform : (m:fmap)(z:dart)(i:nat),
inv_hmap m exd m z
Iter_upb m z = Iter_upb m (Iter (f m) i z).
Proof.
intros.
set (zi := Iter (f m) i z) in |- ×.
set (p := Iter_upb m z) in |- ×.
set (q := Iter_upb m zi) in |- ×.
generalize (Iter_upb_period m z H H0).
simpl in |- ×.
fold p in |- ×.
intro.
assert (exd m zi).
unfold zi in |- ×.
generalize (exd_Iter_f m i z H).
tauto.
generalize (Iter_upb_period m zi H H2).
simpl in |- ×.
fold q in |- ×.
intro.
assert (Iter (f m) (i + q)%nat z = Iter (f m) q zi).
unfold zi in |- ×.
rewrite plus_comm.
apply Iter_comp.
assert (Iter (f m) q z = z).
apply (Iter_plus m z q i H H0).
fold zi in |- ×.
rewrite plus_comm.
rewrite <- H3.
tauto.
assert (Iter (f m) p zi = zi).
unfold zi in |- ×.
rewrite <- Iter_comp.
rewrite plus_comm.
assert (i + p = i + 1 × p)%nat.
omega.
rewrite H6.
unfold p in |- ×.
rewrite Iter_period.
trivial.
trivial.
trivial.
clear H4.
elim (lt_eq_lt_dec p q).
intro.
elim a.
clear a.
intro.
generalize (exd_diff_orb m zi H H2).
unfold diff_orb in |- ×.
unfold Iter_upb in q.
unfold Iter_rem in q.
unfold Iter_upb_aux in |- ×.
fold q in |- ×.
unfold diff_int in |- ×.
intros.
absurd (Iter (f m) p zi = zi).
intro.
symmetry in H7.
replace zi with (Iter (f m) 0%nat zi) in H7.
generalize H7.
clear H7.
apply H4.
split.
omega.
split.
unfold p in |- ×.
apply upb_pos.
tauto.
omega.
simpl in |- ×.
trivial.
tauto.
tauto.
intro.
generalize (exd_diff_orb m z H H0).
unfold diff_orb in |- ×.
unfold Iter_upb in p.
unfold Iter_rem in p.
unfold Iter_upb_aux in |- ×.
fold p in |- ×.
unfold diff_int in |- ×.
intros.
symmetry in H5.
absurd (z = Iter (f m) q z).
replace z with (Iter (f m) 0%nat z).
apply H4.
split.
omega.
split.
unfold q in |- ×.
apply upb_pos.
tauto.
omega.
simpl in |- ×.
trivial.
tauto.
Qed.

Lemma unicity_mod_p:(m:fmap)(z:dart)(j k:nat),
inv_hmap m exd m z
let p := Iter_upb m z in
(j < p)%nat (k < p)%nat
Iter (f m) j z = Iter (f m) k z j = k.
Proof.
intros.
generalize (exd_diff_orb m z H H0).
unfold diff_orb in |- ×.
unfold Iter_upb in p.
unfold Iter_upb_aux in |- ×.
unfold Iter_rem in p.
fold p in |- ×.
unfold diff_int in |- ×.
intros.
elim (le_gt_dec j k).
elim (eq_nat_dec j k).
intros.
tauto.
intros.
absurd (Iter (f m) j z = Iter (f m) k z).
apply (H4 j k).
omega.
tauto.
intro.
symmetry in H3.
absurd (Iter (f m) k z = Iter (f m) j z).
apply (H4 k j).
omega.
tauto.
Qed.

Definition expo(m:fmap)(z t:dart):Prop:=
exd m z i:nat, Iter (f m) i z = t.

Definition expo1
(m:fmap)(z t:dart):Prop:=
exd m z
let p:= Iter_upb m z in
j:nat, (j < p)%nat Iter (f m) j z = t.

Lemma expo_expo1:
(m:fmap)(z t:dart), inv_hmap m
(expo m z t expo1 m z t).
Proof.
unfold expo in |- ×.
unfold expo1 in |- ×.
intros.
unfold expo in |- ×.
unfold expo1 in |- ×.
intros.
split.
intros.
elim H0.
clear H0.
intros.
split.
tauto.
elim H1.
intros i Hi.
clear H1.
generalize (mod_p m z i H H0).
simpl in |- ×.
intros.
elim H1.
intros j Hj.
split with j.
split.
tauto.
rewrite Hi in Hj.
symmetry in |- ×.
tauto.
intros.
elim H0.
clear H0.
intros.
split.
tauto.
elim H1.
intros.
split with x.
tauto.
Qed.

Definition modulo(m:fmap)(z:dart)(i:dart)
(hi:inv_hmap m)(he:exd m z):nat.
Proof.
intros.
assert
(let p := Iter_upb m z in
{j : nat | Iter (f m) i z = Iter (f m) j z (j < p)%nat}).
apply mod_p.
tauto.
tauto.
simpl in H.
elim H.
intros.
apply x.
Defined.

Lemma expo_exd:
(m:fmap)(z t:dart),
inv_hmap m expo m z t exd m t.
Proof.
unfold expo in |- ×.
intros.
decompose [and] H0.
elim H2.
intros i Hi.
rewrite <- Hi.
generalize (exd_Iter_f m i z).
tauto.
Qed.

Lemma expo_refl:
(m:fmap)(z:dart), exd m z expo m z z.
Proof.
intros.
unfold expo in |- ×.
split.
tauto.
split with 0%nat.
simpl in |- ×.
tauto.
Qed.

Lemma expo_trans:
(m:fmap)(z t u:dart),
expo m z t expo m t u expo m z u.
Proof.
unfold expo in |- ×.
intros.
intuition.
elim H2.
intros j Hj.
elim H3.
intros i Hi.
split with (i + j)%nat.
rewrite Iter_comp.
rewrite Hj.
tauto.
Qed.

Lemma expo_symm:(m:fmap)(z t:dart),
inv_hmap m
expo m z t expo m t z.
Proof.
intros m z t Hm He.
assert (exd m t).
apply expo_exd with z.
tauto.
tauto.
unfold expo in |- ×.
unfold expo in He.
intuition.
elim H1.
intros i Hi.
rewrite <- Hi.
clear H1.
generalize (mod_p m z i Hm H0).
intro.
simpl in H1.
elim H1.
intros r Hr.
elim Hr.
clear Hr H1.
intros.
split with (Iter_upb m z - r)%nat.
rewrite H1.
rewrite <- Iter_comp.
assert (Iter_upb m z - r + r = Iter_upb m z)%nat.
omega.
rewrite H3.
apply Iter_upb_period.
tauto.
tauto.
Qed.

Fixpoint ex_j
(m:fmap)(z t:dart)(n:nat){struct n}:Prop:=
match n with
0%natz = t
| S n0Iter (f m) n z = t ex_j m z t n0
end.

Lemma ex_j_dec:
(m:fmap)(z t:dart)(n:nat),
{ex_j m z t n} + {¬ex_j m z t n}.
Proof.
induction n.
simpl in |- ×.
apply eq_dart_dec.
simpl in |- ×.
generalize (eq_dart_dec (f m (Iter (f m) n z)) t).
tauto.
Qed.

Lemma ex_j_exist_j:(m:fmap)(z t:dart)(n:nat),
ex_j m z t n
j :nat, (j n)%nat Iter (f m) j z = t.
Proof.
induction n.
simpl in |- ×.
split.
intro.
split with 0%nat.
split.
omega.
simpl in |- ×.
tauto.
intro.
elim H.
intros j Hj.
intuition.
inversion H0.
rewrite H2 in H1.
simpl in |- ×.
simpl in H1.
tauto.
simpl in |- ×.
split.
intro.
elim H.
intro.
split with (S n).
split. clear IHn H H0.
omega.
simpl in |- ×.
tauto.
intro.
assert ( j : nat, (j n)%nat
Iter (f m) j z = t).
tauto.
elim H1.
intros j Hj.
split with j.
split. decompose [and] Hj. clear H H0 H1 Hj H3 IHn.
omega.
tauto.
intros.
elim H.
intros j Hj.
elim (eq_nat_dec j (S n)).
intro.
rewrite a in Hj.
simpl in Hj.
tauto.
intro.
assert ( j : nat, (j n)%nat
Iter (f m) j z = t).
split with j.
split. clear IHn.
omega.
tauto.
tauto.
Qed.

Lemma expo1_ex_j:
(m:fmap)(z t:dart), inv_hmap m exd m z
let p:= Iter_upb m z in
(ex_j m z t (p - 1)%nat expo1 m z t).
Proof.
intros.
generalize (Iter_upb_period m z H H0).
generalize (upb_pos m z H0).
rename H into hm.
rename H0 into hz.
fold p in |- ×.
intros Hp1 Hp2.
generalize (ex_j_exist_j m z t (p - 1)%nat).
unfold expo1 in |- ×.
fold p in |- ×.
intros.
split.
intro.
assert ( j : nat, (j p - 1)%nat
Iter (f m) j z = t).
tauto.
elim H1.
intros j Hj.
split.
tauto.
split with j.
split. clear H H0.
omega.
tauto.
intro.
elim H0.
intros.
elim H2.
clear H0 H2.
intros i Hj.
assert ( j : nat, (j p - 1)%nat
Iter (f m) j z = t).
split with i.
split. clear H.
omega.
tauto.
tauto.
Qed.

Lemma expo1_dec :
(m:fmap)(z t:dart),
inv_hmap m exd m z
{expo1 m z t} + {¬expo1 m z t}.
Proof.
intros.
set (p := Iter_upb m z) in |- ×.
generalize (ex_j_dec m z t (p - 1)).
intro.
elim H1.
intro.
left.
generalize (expo1_ex_j m z t H H0).
simpl in |- ×.
fold p in |- ×.
tauto.
intro.
right.
intro.
generalize (expo1_ex_j m z t H H0).
simpl in |- ×.
fold p in |- ×.
tauto.
Qed.

Lemma expo_dec: (m:fmap)(z t:dart),
inv_hmap m
{expo m z t} + {¬expo m z t}.
Proof.
intros m z t hm.
generalize (expo_expo1 m z t hm).
generalize (expo1_dec m z t hm).
intros.
elim (exd_dec m z).
tauto.
unfold expo in |- ×.
tauto.
Qed.

Theorem period_expo : (m:fmap)(z t:dart),
inv_hmap m expo m z t
Iter_upb m z = Iter_upb m t.
Proof.
unfold expo in |- ×.
intros.
elim H0.
clear H0.
intros.
elim H1.
intros i Hi.
rewrite <- Hi.
apply period_uniform.
tauto.
tauto.
Qed.

Open Scope nat_scope.

Theorem period_lub : (m:fmap)(z:dart),
inv_hmap m exd m z
let nr:= Iter_upb m z in
0 < nr Iter (f m) nr z = z
i:nat, 0 < i < nr Iter (f m) i z z.
Proof.
intros.
split.
unfold nr in |- ×.
apply upb_pos.
tauto.
split.
unfold nr in |- ×.
apply Iter_upb_period.
tauto.
tauto.
intros.
generalize (exd_diff_orb m z).
unfold diff_orb in |- ×.
unfold Iter_upb in nr.
unfold Iter_rem in nr.
unfold Iter_upb_aux in |- ×.
fold nr in |- ×.
unfold diff_int in |- ×.
intros.
assert
( i j : nat,
0 i i < j nr - 1
Iter (f m) i z Iter (f m) j z).
tauto.
clear H2.
generalize (H3 0 i).
intros.
simpl in H2.
intro.
symmetry in H4.
apply H2.
split.
omega.
omega.
assumption.
Qed.

Require Import Recdef.

Open Scope nat_scope.

Lemma ndN_pos:(m:fmap)(z:dart),
exd m z 0 < ndN m.
Proof.
induction m.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exd_dec m d).
intro.
apply IHm with d.
tauto.
intro.
omega.
simpl in |- ×.
tauto.
Qed.

Function degree_aux(m:fmap)(z:dart)(n:nat)
{measure (fun i:natndN m - i) n}:nat:=
if le_lt_dec n (ndN m)
then if eq_dart_dec z (Iter (f m) n z) then n
else if eq_nat_dec n (ndN m) then (ndN m) + 1
else degree_aux m z (n+1)
else (ndN m) + 1.
Proof.
intros.
omega.
Defined.

Definition degree(m:fmap)(z:dart):=
degree_aux m z 1.

Definition P_degree_pos(m:fmap)(z:dart)(n1 n2:nat):
Prop:= exd m z 0 < n1 0 < n2.

Lemma degree_pos_aux:(m:fmap)(z:dart),
P_degree_pos m z 1 (degree m z).
Proof.
unfold degree in |- ×.
intros.
apply degree_aux_ind.
intros.
unfold P_degree_pos in |- ×.
tauto.
intros.
unfold P_degree_pos in |- ×.
intros.
omega.
intros.
unfold P_degree_pos in |- ×.
unfold P_degree_pos in H.
assert (0 < n + 1).
omega.
tauto.
intros.
unfold P_degree_pos in |- ×.
intros.
omega.
Qed.

Theorem degree_pos:(m:fmap)(z:dart),
exd m z 0 < degree m z.
Proof.
unfold degree in |- ×.
intros.
generalize (degree_pos_aux m z).
unfold P_degree_pos in |- ×.
unfold degree in |- ×.
intros.
assert (0 < 1).
omega.
tauto.
Qed.

Definition P_degree_diff(m:fmap)(z:dart)(n1 n2:nat):
Prop:= inv_hmap m exd m z 0 < n1
i:nat, n1 i < n2 Iter (f m) i z z.

Lemma degree_diff_aux:(m:fmap)(z:dart),
P_degree_diff m z 1 (degree m z).
Proof.
unfold degree in |- ×.
intros.
apply degree_aux_ind.
intros.
unfold P_degree_diff in |- ×.
intros.
omega.
intros.
unfold P_degree_diff in |- ×.
intros.
rewrite _x1 in H2.
assert (i = n).
rewrite _x1 in |- ×.
omega.
rewrite H3 in |- ×.
intro.
symmetry in H4.
assert (z Iter (f m) n z).
apply _x0.
tauto.
intros.
unfold P_degree_diff in |- ×.
unfold P_degree_diff in H.
intros.
elim (eq_nat_dec n i).
intro.
rewrite <- a in |- ×.
intro.
assert (z Iter (f m) n z).
apply _x0.
symmetry in H4.
tauto.
intro.
apply H.
tauto.
tauto.
omega.
split.
omega.
tauto.
intros.
unfold P_degree_diff in |- ×.
intros.
omega.
Qed.

Theorem degree_diff: (m:fmap)(z:dart),
inv_hmap m exd m z
i:nat, 0 < i < (degree m z)
Iter (f m) i z z.
Proof.
intros.
generalize (degree_diff_aux m z).
unfold P_degree_diff in |- ×.
intros.
assert ( i : nat, 1 i < degree m z Iter (f m) i z z).
apply H2.
tauto.
tauto.
omega.
apply H3.
omega.
Qed.

Lemma degree_bound: (m:fmap)(z:dart),
inv_hmap m exd m z degree m z ndN m.
Proof.
intros.
elim (le_lt_dec (degree m z) (ndN m)).
tauto.
intro.
generalize (degree_diff m z H H0).
intro.
set (nr := Iter_upb m z) in |- ×.
assert (Iter (f m) nr z = z).
unfold nr in |- ×.
apply Iter_upb_period.
tauto.
tauto.
assert (nr ndN m).
unfold nr in |- ×.
unfold Iter_upb in |- ×.
omega.
absurd (Iter (f m) nr z = z).
apply H1.
split.
unfold nr in |- ×.
apply upb_pos.
tauto.
omega.
tauto.
Qed.

Definition P_degree_per(m:fmap)(z:dart)(n1 n2:nat):
Prop:= inv_hmap m exd m z 0 < n1 n2 ndN m
Iter (f m) n2 z = z.

Lemma degree_per_aux: (m:fmap)(z:dart),
P_degree_per m z 1 (degree m z).
Proof.
unfold degree in |- ×.
intros.
apply degree_aux_ind.
intros.
unfold P_degree_per in |- ×.
symmetry in |- ×.
tauto.
intros.
unfold P_degree_per in |- ×.
intros.
absurd (ndN m + 1 ndN m).
omega.
tauto.
intros.
unfold P_degree_per in |- ×.
unfold P_degree_per in H.
intros.
apply H.
tauto.
tauto.
omega.
tauto.
intros.
unfold P_degree_per in |- ×.
intros.
absurd (ndN m + 1 ndN m).
omega.
tauto.
Qed.

Theorem degree_per: (m:fmap)(z:dart),
inv_hmap m exd m z
Iter (f m) (degree m z) z = z.
Proof.
intros.
apply degree_per_aux.
tauto.
tauto.
omega.
apply degree_bound.
tauto.
tauto.
Qed.

Theorem degree_lub: (m:fmap)(z:dart),
inv_hmap m exd m z
let p:= degree m z in
0 < p Iter (f m) p z = z
i:nat, 0 < i < p Iter (f m) i z z.
Proof.
intros.
unfold p in |- ×.
split.
apply degree_pos.
tauto.
split.
apply degree_per.
tauto.
tauto.
apply degree_diff.
tauto.
tauto.
Qed.

Require Import Arith.

Theorem upb_eq_degree:(m:fmap)(z:dart),
inv_hmap m exd m z
Iter_upb m z = degree m z.
Proof.
intros.
set (p := degree m z) in |- ×.
set (nr := Iter_upb m z) in |- ×.
generalize (period_lub m z H H0).
generalize (degree_lub m z H H0).
simpl in |- ×.
fold p in |- ×.
fold nr in |- ×.
intros.
decompose [and] H1.
clear H1.
decompose [and] H2.
clear H2.
elim (lt_eq_lt_dec nr p).
intro.
elim a.
intro.
absurd (Iter (f m) nr z = z).
apply H6.
omega.
tauto.
tauto.
intro.
absurd (Iter (f m) p z = z).
apply H8.
omega.
tauto.
Qed.

Theorem expo_degree : (m:fmap)(z t:dart),
inv_hmap m expo m z t
degree m z = degree m t.
Proof.
intros.
generalize (period_expo m z t H H0).
rewrite upb_eq_degree in |- ×.
rewrite upb_eq_degree in |- ×.
tauto.
tauto.
apply (expo_exd m z t H H0).
tauto.
unfold expo in H0.
tauto.
Qed.

Theorem degree_uniform : (m:fmap)(z:dart)(i:nat),
inv_hmap m exd m z
degree m z = degree m (Iter (f m) i z).
Proof.
intros.
generalize (period_uniform m z i H H0).
rewrite upb_eq_degree in |- ×.
rewrite upb_eq_degree in |- ×.
tauto.
tauto.
generalize (exd_Iter_f m i z).
tauto.
tauto.
tauto.
Qed.

Theorem degree_unicity:(m:fmap)(z:dart)(j k:nat),
inv_hmap m exd m z
let p := degree m z in
j < p k < p
Iter (f m) j z = Iter (f m) k z j = k.
Proof.
intros.
generalize (unicity_mod_p m z j k H H0).
simpl in |- ×.
rewrite upb_eq_degree in |- ×.
fold p in |- ×.
tauto.
tauto.
tauto.
Qed.

Open Scope R_scope.

Lemma incls_orbit:(m:fmap)(x:dart),
inv_hmap m exd m x
incls (Iter_orb m x) (fmap_to_set m).
Proof.
intros.
apply exds2.
intro.
unfold Iter_orb in |- ×.
generalize (exds_set_minus_eq (fmap_to_set m)
(Iter_rem m x) z).
tauto.
Qed.

Lemma exds_orb_exd:(m:fmap)(x z:dart),
inv_hmap m exd m x
exds (Iter_orb m x) z exd m z.
Proof.
intros.
generalize (incls_orbit m x H H0).
intro.
inversion H2.
generalize (H3 z H1).
intro.
generalize (exd_exds m z).
tauto.
Qed.

Lemma incls_rem:(m:fmap)(x:dart),
inv_hmap m exd m x
incls (Iter_rem m x) (fmap_to_set m).
Proof.
unfold Iter_rem in |- ×.
intros.
apply exds2.
intro.
intro.
generalize (LR3 m x z (fmap_to_set m)).
simpl in |- ×.
generalize (exds_dec (fmap_to_set m) z).
generalize (exds_dec (Iter_rem_aux m x (fmap_to_set m)) z).
tauto.
Qed.

Lemma card_orbit:(m:fmap)(x:dart),
inv_hmap m exd m x
card (Iter_orb m x) = Iter_upb m x.
Proof.
unfold Iter_orb in |- ×.
unfold Iter_upb in |- ×.
intros.
generalize (incls_rem m x H H0).
intros.
rewrite nd_card in |- ×.
generalize (card_minus_set (fmap_to_set m) (Iter_rem m x) H1).
intro.
omega.
Qed.

Lemma exds_orb_ex :(m:fmap)(z t:dart),
inv_hmap m exd m z
let s:= Iter_orb m z in
let p:= Iter_upb m z in
exds s t
{i : nat | (i < p)%nat Iter (f m) i z = t}.
Proof.
intros.
intros.
assert (exd m t).
generalize (incls_orbit m z H H0).
intro.
inversion H2.
generalize (H3 t H1).
intro.
generalize (exd_exds m t).
tauto.
assert (¬ exds (Iter_rem m z) t).
generalize (exds_rem_orb m z t H H2).
tauto.
apply (ex_i m z t H H0 H2 H3).
Qed.

Theorem exds_orb_eq_ex :(m:fmap)(z t:dart),
inv_hmap m exd m z
let s:= Iter_orb m z in
let p:= Iter_upb m z in
(exds s t
i:nat,(i < p)%nat Iter (f m) i z = t).
Proof.
split.
intro.
generalize (exds_orb_exd m z t H H0 H1).
intro.
generalize (exds_orb_ex m z t H H0 H1).
intro.
elim H3.
intros.
split with x.
tauto.
intros.
elim H1.
intros i Hi.
clear H1.
decompose [and] Hi.
clear Hi.
rewrite <- H2 in |- ×.
apply exds_Iter_f_i.
tauto.
tauto.
omega.
Qed.

Open Scope nat_scope.

Theorem exds_orb_eq_ex_large :(m:fmap)(z t:dart),
inv_hmap m exd m z
let s:= Iter_orb m z in
let p:= Iter_upb m z in
(exds s t i:nat, Iter (f m) i z = t).
Proof.
split.
intro.
generalize (exds_orb_exd m z t H H0 H1).
intro.
generalize (exds_orb_eq_ex m z t H H0).
simpl in |- ×.
intro.
assert ( i : nat,
i < Iter_upb m z Iter (f m) i z = t).
tauto.
clear H3.
elim H4.
intros.
split with x.
tauto.
intro.
assert (expo m z t).
unfold expo in |- ×.
split.
tauto.
tauto.
generalize (expo_expo1 m z t H).
unfold expo1 in |- ×.
intro.
assert ( j : nat,
j < Iter_upb m z Iter (f m) j z = t).
tauto.
generalize (exds_orb_eq_ex m z t H H0).
simpl in |- ×.
tauto.
Qed.

Theorem expo_eq_exds_orb :(m:fmap)(z t:dart),
inv_hmap m exd m z
(expo m z t exds (Iter_orb m z) t).
Proof.
intros.
generalize (exds_orb_eq_ex_large m z t H H0).
simpl in |- ×.
intro.
unfold expo in |- ×.
tauto.
Qed.

Theorem expo1_eq_exds_orb :(m:fmap)(z t:dart),
inv_hmap m exd m z
(expo1 m z t exds (Iter_orb m z) t).
Proof.
intros.
generalize (exds_orb_eq_ex m z t H H0).
simpl in |- ×.
intro.
unfold expo1 in |- ×.
tauto.
Qed.

Lemma impls_orb:(m:fmap)(x y:dart),
inv_hmap m exd m x
expo m x y
impls (Iter_orb m x) (Iter_orb m y).
Proof.
unfold impls in |- ×.
intros.
assert (exd m y).
generalize (expo_exd m x y).
tauto.
generalize (exds_orb_eq_ex_large m x z H H0).
intros.
generalize (exds_orb_eq_ex_large m y z H H3).
intro.
assert (exd m z).
generalize (exd_exds m z).
intro.
generalize (incls_orbit m x H H0).
intro.
inversion H7.
generalize (H8 z H2).
tauto.
simpl in H4.
assert ( i : nat, Iter (f m) i x = z).
tauto.
elim H7.
clear H7.
intros i Hi.
assert (expo m x z).
unfold expo in |- ×.
split.
tauto.
split with i.
tauto.
assert (expo m y z).
apply expo_trans with x.
apply expo_symm.
tauto.
tauto.
tauto.
assert ( i : nat, Iter (f m) i y = z).
unfold expo in H8.
tauto.
simpl in H5.
tauto.
Qed.

Lemma eqs_orb:(m:fmap)(x y:dart),
inv_hmap m
expo m x y
eqs (Iter_orb m x) (Iter_orb m y).
Proof.
unfold eqs in |- ×.
intros.
assert (exd m x).
unfold expo in H0.
tauto.
assert (exd m y).
apply expo_exd with x.
tauto.
tauto.
split.
generalize (impls_orb m x y H H1 H0).
unfold impls in |- ×.
intro.
apply H3.
assert (expo m y x).
apply expo_symm.
tauto.
tauto.
generalize (impls_orb m y x H H2 H3).
unfold impls in |- ×.
intro.
apply H4.
Qed.

Lemma orb_impls_expo:(m:fmap)(x y:dart),
inv_hmap m exd m x exd m y
impls (Iter_orb m x) (Iter_orb m y) expo m x y.
Proof.
intros.
unfold impls in H2.
generalize (H2 x).
intro.
assert (exds (Iter_orb m x) x).
generalize (expo_eq_exds_orb m x x H H0).
intro.
assert (expo m x x).
apply expo_refl.
tauto.
tauto.
apply expo_symm.
tauto.
generalize (expo_eq_exds_orb m y x H H1).
tauto.
Qed.

Theorem expo_eq_eqs_orb:(m:fmap)(x y:dart),
inv_hmap m exd m x exd m y
(expo m x y eqs (Iter_orb m x) (Iter_orb m y)).
Proof.
split.
apply (eqs_orb m x y H).
unfold eqs in |- ×.
intro.
generalize (orb_impls_expo m x y H H0 H1).
unfold impls in |- ×.
intro.
assert ( z : dart,
exds (Iter_orb m x) z exds (Iter_orb m y) z).
intro.
intro.
generalize (H2 z).
tauto.
tauto.
Qed.

Lemma disjs_orb:(m:fmap)(x y:dart),
inv_hmap m exd m x exd m y
¬expo m x y
disjs (Iter_orb m x) (Iter_orb m y).
Proof.
unfold disjs.
intros.
assert (exd m z).
generalize (incls_orbit m x H H0).
intro.
inversion H5.
clear H5.
generalize (H6 z).
intro.
assert (exds (fmap_to_set m) z).
tauto.
clear H6 H5.
generalize (exd_exds m z).
tauto.
generalize (exds_orb_eq_ex m x z H H0).
generalize (exds_orb_eq_ex m y z H H1).
simpl in |- ×.
set (px := Iter_upb m x) in |- ×.
set (py := Iter_upb m y) in |- ×.
intros.
assert ( i : nat, i < py Iter (f m) i y = z).
tauto.
clear H6.
assert ( i : nat, i < px Iter (f m) i x = z).
tauto.
clear H7.
elim H8.
intros i Hi.
clear H8.
elim H6.
intros j Hj.
clear H6.
decompose [and] Hi.
clear Hi.
intros.
decompose [and] Hj.
clear Hj.
intros.
assert (expo m y z).
unfold expo in |- ×.
split.
tauto.
split with i.
tauto.
assert (expo m x z).
unfold expo in |- ×.
split.
tauto.
split with j.
tauto.
elim H2.
apply expo_trans with z.
tauto.
apply expo_symm.
tauto.
tauto.
Qed.

Lemma disjs_orb_not_expo:(m:fmap)(x y:dart),
inv_hmap m exd m x exd m y
disjs (Iter_orb m x) (Iter_orb m y) ¬expo m x y.
Proof.
unfold disjs in |- ×.
intros.
generalize (H2 x).
intros.
assert (exds (Iter_orb m x) x).
generalize (expo_eq_exds_orb m x x H H0).
intro.
assert (expo m x x).
apply expo_refl.
tauto.
tauto.
intro.
assert (expo m y x).
apply expo_symm.
tauto.
tauto.
generalize (expo_eq_exds_orb m y x H H1).
tauto.
Qed.

Theorem not_expo_disjs_orb:(m:fmap)(x y:dart),
inv_hmap m exd m x exd m y
(¬expo m x y
disjs (Iter_orb m x) (Iter_orb m y)).
Proof.
split.
apply (disjs_orb m x y H H0 H1).
apply (disjs_orb_not_expo m x y H H0 H1).
Qed.

Lemma incls_minus: (m:fmap)(x y:dart),
inv_hmap m exd m x exd m y
¬expo m x y
let s:= fmap_to_set m in
let sx:= Iter_orb m x in
let sy:= Iter_orb m y in
incls sy (set_minus s sx).
Proof.
intros.
apply exds2.
intros.
apply exds_set_minus.
generalize (incls_orbit m y H H1).
intro.
inversion H4.
fold s in H5.
apply H5.
fold sy in |- ×.
tauto.
intro.
generalize (disjs_orb m x y H H0 H1 H2).
unfold disjs in |- ×.
intro.
apply (H5 z H4 H3).
Qed.

Open Scope nat_scope.

Theorem upb_sum_bound: (m:fmap)(x y:dart),
inv_hmap m exd m x exd m y ¬expo m x y
Iter_upb m x + Iter_upb m y ndN m.
Proof.
intros.
rewrite <- card_orbit in |- ×.
rewrite <- card_orbit in |- ×.
set (s := fmap_to_set m) in |- ×.
set (sx := Iter_orb m x) in |- ×.
set (sy := Iter_orb m y) in |- ×.
generalize (incls_minus m x y H H0 H1 H2).
simpl in |- ×.
fold s in |- ×.
fold sx in |- ×.
fold sy in |- ×.
intro.
generalize (incls_orbit m x H H0).
fold s in |- ×.
fold sx in |- ×.
intro.
generalize (card_minus_set s sx H4).
intro.
generalize (card_minus_set (set_minus s sx) sy H3).
intro.
generalize (nd_card m).
intro.
fold s in H7.
rewrite H7 in |- ×.
clear H7.
omega.
tauto.
tauto.
tauto.
tauto.
Qed.

Theorem degree_sum_bound: (m:fmap)(x y:dart),
inv_hmap m exd m x exd m y ¬expo m x y