(** * Theory of Sets : Ordinals Copyright INRIA (2011-2013) Marelle Team (Jose Grimm). *) (* \$Id: sset16.v,v 1.40 2016/05/18 14:54:53 grimm Exp \$ *) Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Export sset15. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module NumberSums. (** Number of decompositions *) Definition nds_sc n X g := osum_expansion (fun z => (X (Vf g z))) n. Definition nds_sums n X := fun_image (perm_int n) (nds_sc n X). Definition nds_card n X := cardinal (nds_sums n X). Definition nds_ax X n:= ord_below_n X n. Lemma nds_a n X: natp n -> nds_card n X <=c (factorial n). Proof. move=> nN. rewrite /nds_card/nds_sums. set a := (perm_int n). set b := fun_image _ _. rewrite -(card_nat nN) -(number_of_permutations (finite_set_nat nN)). apply: surjective_cle. exists (Lf (nds_sc n X) a b); hnf; aw; split => //. apply:lf_surjective. move=> t ta; apply /funI_P; ex_tac. by move=> y /funI_P. Qed. Lemma nds_b X n f: natp n -> nds_ax X n-> inc f (perm_int n) -> (nds_ax (fun z => X (Vf f z)) n /\ ordinalp (nds_sc n X f)). Proof. move=> nN ax => /Zo_P [] /functionsP [ff sf tf] bf. suff pc: nds_ax (fun z => X (Vf f z)) n. by split => //; apply: OS_osum_expansion. move => t /(NltP nN) tn; apply: ax; apply/(NltP nN); Wtac. Qed. Lemma nds_sc_exten X X' n f: natp n -> (same_below X X' n) -> inc f (perm_int n) -> nds_sc n X f = nds_sc n X' f. Proof. move =>nN h /Zo_P [] /functionsP [fg sg tg] bg;apply: (osum_expansion_exten nN). move => i /(NltP nN) ia; apply: h; apply/(NltP nN); Wtac. Qed. Lemma nds_m n X g (Y:= fun z => X (Vf g z)): natp n -> nds_ax X n -> inc g (perm_int n) -> nds_card n X = nds_card n Y. Proof. move => nN ax /Zo_P [] /functionsP [fg sg tg] bg. rewrite /nds_card /nds_sums; apply: f_equal. set E := perm_int n. set_extens t; move /funI_P => [z ze ->]; apply /funI_P. move: (inverse_bij_fb bg) => ibg. move: ze => /Zo_P [] /functionsP [fz sz tz] bz. have fa: (inverse_fun g) \coP z by red;aw;split => //; [fct_tac | ue]. have fb: function ((inverse_fun g) \co z) by fct_tac. exists ((inverse_fun g) \co z). apply: Zo_i; [ apply /functionsP;red;aw;split => // | by apply compose_fb ]. apply:(osum_expansion_exten nN) => i lin. have iz: inc i (source z) by rewrite sz; apply /(NltP nN i). have cp: inverse_fun g \coP z by split; [ fct_tac | exact | aw; ue]. have fzy: inc (Vf z i) (target g) by rewrite tg - tz; Wtac. by rewrite /Y (compf_V cp iz) (inverse_V bg fzy). move: ze => /Zo_P [] /functionsP [fz sz tz] bz. have fa: g \coP z by red;aw;split => //; ue. have fb: function (g \co z) by fct_tac. exists (g \co z). apply: Zo_i; [ apply /functionsP;red;aw;split => // | by apply compose_fb ]. apply:(osum_expansion_exten nN) => i lin. by rewrite /Y compf_V // sz; apply/(NltP nN i). Qed. Lemma nds_c n X: natp n -> (\1c <=c nds_card n X /\ natp (nds_card n X)). Proof. move=> nN; move: (nds_a X nN) => pa. move:(NS_le_nat pa (NS_factorial nN)) => pb. split => //. rewrite /nds_card/nds_sums; apply: cge1; first by fprops. apply: card_nonempty1; apply:funI_setne. exists (identity n). apply: Zo_i; [ apply /functionsP;red;aw;split;fprops | apply identity_fb]. Qed. Lemma nds_d X n: (n = \0c \/ n = \1c) -> nds_ax X n -> nds_card n X = \1c. Proof. move=> np ax. have nN: natp n by case: np => ->; fprops. apply: cleA. by move: (nds_a X nN); case: np => ->; rewrite ? factorial0 ? factorial1. exact (proj1 (nds_c X nN)). Qed. Lemma nds_e X: nds_ax X \2c -> osum_expansion X \2c = (X \1c) +o (X \0c). Proof. rewrite - succ_one => pa. rewrite (osum_expansion_succ _ NS1) (osum_expansion1) //; apply: pa. rewrite succ_one; apply: clt_02. Qed. Lemma nds_f n X (f := identity n) : natp n -> nds_ax X n -> (inc f (perm_int n) /\ (nds_sc n X f = osum_expansion X n)). Proof. move=> nN ax. have bi: bijection f by apply identity_fb. split. by rewrite /f; apply: Zo_i => //; apply /functionsP; red;aw;split;fprops. apply:(osum_expansion_exten nN) => i lin. by rewrite /f identity_V //; apply/(NltP nN). Qed. Lemma nds_g (X:=(variant \0c \1o omega0)): nds_ax X \2c /\ nds_card \2c X = \2c. Proof. move: osum2_nc => /= nc. have nX: nds_ax X \2c by move => t t2; rewrite /X /variant; Ytac h; fprops. split => //; apply: cleA. by move: (nds_a X NS2); rewrite factorial2. move: (nds_f NS2 nX) => [ha hb]. have ne: \1c <> \0c by fprops. apply /cle2P. exists (\1o +o omega0), (omega0 +o \1o); split => //;apply /funI_P; last first. exists (identity \2c) => //. by rewrite hb (nds_e nX) /X /variant; Ytac0; Ytac0. set I:= \2c. have I1: inc \1c I by fprops. have I0: inc \0c I by fprops. have iv y: inc y \2c -> y = \0c \/ y = \1c by case/set2_P => ->; fprops. have ta: lf_axiom (variant \0c \1c \0c) I I. by move => t _; rewrite /variant; Ytac h. have fp: inc (Lf (variant \0c \1c \0c) I I) (permutations I). apply/Zo_i; first by apply /functionsP; split; [apply: lf_function | aw | aw]. apply: lf_bijective => //. move=> u v us vs. rewrite /variant; case: (iv _ us); case: (iv _ vs); move => -> ->; Ytac0 => //; Ytac0 => //. move => y yv; case: (iv _ yv); move => ->. by exists \1c => //; rewrite /variant; Ytac0. by exists \0c => //; rewrite /variant; Ytac0. have ax2:= (proj1 (nds_b NS2 nX fp)). exists (Lf (variant \0c \1c \0c) I I); first exact. by rewrite /nds_sc nds_e; aw; aw; rewrite /X /variant; repeat Ytac0. Qed. Lemma nds_h (A:= omega0 ^o \2o) (B:= omega0) (C := omega0 +o \1o) (s1 := A +o (B +o C)) (s2:= A +o (C +o B)) (s3 := B +o (A +o C)) (s4 := B +o (C +o A)) (s5:= C +o (A +o B)) (s6 := C +o (B +o A)): cardinal (((doubleton s1 s2) \cup (doubleton s3 s5)) \cup (doubleton s4 s6)) = card_five. Proof. set T := union2 _ _. move: OS_omega OS1 OS2 => oB o1 o2. have oA: ordinalp A by apply: OS_pow. have oC: ordinalp C by apply: OS_sum2. move: (ord_negl_p4 olt_02); rewrite opowx0 -/A => pa. move: (ord_negl_p4 olt_12); rewrite (opowx1 oB) -/A -/B => pb. have e1: s3 = A +o C by rewrite /s3 (osumA oB oA oC) pb. have e2: s6 = C +o A by rewrite /s6 pb. have pc: C +o A = A by rewrite - (osumA oB OS1 oA) pa pb. have pd: (doubleton s4 s6) = singleton A by rewrite /s4 e2 pc pb. have e3: s2= A +o (B +o B). by rewrite /s2 - (osumA oB o1 oB) (osum_int_omega olt_1omega). have e4: s5= A +o B by rewrite /s5 (osumA oC oA oB) pc. set T1:= (union2 (doubleton s1 s2) (doubleton s3 s5)). have bz: B <> \0o by apply: omega_nz. have onz: \1o <> \0o by fprops. case: (equal_or_not C \0o) => cz; first by move: (osum2_zero oB OS1 cz) => [_]. have nAt: ~ (inc A T1). have sA: forall b, ordinalp b ->A = A +o b -> b = \0o. move => b ob h; symmetry in h; exact (osum_a_ab oA ob h). case /setU2_P; case /set2_P. - by move/(sA _ (OS_sum2 oB oC)) => /(osum2_zero oB oC) [_]. - by move/(sA _ (OS_sum2 oC oB)) => /(osum2_zero oC oB) []. - by rewrite e1; move /(sA _ oC). - by rewrite e4; move /(sA _ oB). have ->: T = T1 +s1 A by rewrite -pd //. rewrite /card_five (csucc_pr nAt); congr csucc. set T2 := (doubleton s1 s2) +s1 s3. have ->: T1 = T2 +s1 s5. set_extens t. case /setU2_P => h; first by apply /setU1_P; left; apply /setU1_P; left. case /set2_P :h => h; first by apply /setU1_P; left; apply /setU1_P; right. by apply /setU1_P; right. case /setU1_P =>h; last by apply /setU2_P; right; apply/set2_P; right. case /setU1_P:h => h; last by apply /setU2_P; right; apply/set2_P; left. by apply /setU2_P; left. have aux: forall b c, ordinalp b -> ordinalp c -> A +o b = A +o c -> b = c. move => b c ob oc ; apply: (osum2_simpl ob oc oA). have auB: forall b c, ordinalp b -> ordinalp c -> B +o b = B +o c -> b = c. move => b c ob oc ; apply: (osum2_simpl ob oc oB). case (equal_or_not B C) => nCB; first by move: (osum_a_ab oB o1 (esym nCB)). have nat2: ~ inc s5 T2. rewrite /T2 e4 /s1 e1 e3 => /setU1_P; case => h; last first. case: nCB; exact (aux _ _ oB oC h). case /set2_P:h=> h. move: (aux _ _ oB (OS_sum2 oB oC) h) => h1; symmetry in h1. case: cz; exact: (osum_a_ab oB oC h1). move: (aux _ _ oB (OS_sum2 oB oB) h) => h1; symmetry in h1. case: bz; exact: (osum_a_ab oB oB h1). move: (olt_1omega) => [h2 h3]. move: (oltS oB) => h4. have nat3: ~ inc s3 (doubleton s1 s2). rewrite /s1 e1 e3;case /set2_P=> h. move: (aux _ _ oC (OS_sum2 oB oC) h) => h1. move: (ole_ltT h2 h4) => [_ h5]. by move: (auB _ _ o1 oC h1); rewrite /C (osucc_pr oB). move: (aux _ _ oC (OS_sum2 oB oB) h) => h1. case: h3; exact: (auB _ _ o1 oB h1). rewrite /card_four (csucc_pr nat2); apply: f_equal. rewrite /card_three (csucc_pr nat3); apply: f_equal. apply: cardinal_set2. rewrite /s1 e3 => h; move: (aux _ _ (OS_sum2 oB oC) (OS_sum2 oB oB) h) => h1. by case: nCB; rewrite (auB _ _ oC oB h1). Qed. Definition nds_F n := \osup (Zo Nat (fun z => exists2 X, nds_ax X n & nds_card n X = z)). Lemma Nat_sup_pr T (s:= \osup T) k: sub T Nat -> natp k -> (forall i, inc i T -> i <=c k) -> [/\ natp s, s <=c k, (forall i, inc i T -> i <=c s) & (T = emptyset \/ inc s T)]. Proof. move=> TN kN km. have qa: forall t, natp t -> ordinalp t. move => t tb; apply: OS_cardinal; fprops. have ok:= (qa _ kN). have pa: ordinal_set T by move=> t tT; apply: qa; apply: TN. have pb: s <=o k. apply: ord_ub_sup => // i iT; move: (km _ iT); apply: ocle. have pc: natp s. move: kN => /(oltP OS_omega) => ko; apply /(oltP OS_omega). exact:(ole_ltT pb ko). have pd: s <=c k by apply: ocle3; fprops. split => //. move=> i iT. have: i <=o s by apply:ord_sup_ub => //. apply: ocle3; fprops; exact : (CS_nat (TN _ iT)). case: (emptyset_dichot T) => tne; first by left. case: (ord_sup_inVlimit pa tne); first by right. move => li; move: (limit_ge_omega li) => [_ _ li2]. case: (ordinal_irreflexive (qa _ pc) (li2 _ pc)). Qed. Lemma nds_j n (f := nds_F n): natp n -> [/\ natp f, f <=c factorial n, (exists2 X, nds_ax X n & nds_card n X = f) & (forall X, nds_ax X n -> nds_card n X <=c f)]. Proof. move => nN. set T := (Zo Nat(fun z => exists2 X, nds_ax X n & nds_card n X = z)). have ta: sub T Nat by apply: Zo_S. move: (NS_factorial nN) => tb. have tc: (forall i, inc i T -> i <=c (factorial n)). rewrite /T;move=> i /Zo_P [iN [X ea <-]]; exact: (nds_a X nN). move: (Nat_sup_pr ta tb tc) => [pa pb pc pd]. have pe: forall X, nds_ax X n -> natp (nds_card n X). move=> X ax; move: (nds_a X nN) => le1; apply: (NS_le_nat le1 tb). have pf: forall X, nds_ax X n -> nds_card n X <=c f. move=> X xv; apply: pc; apply: Zo_i;[ exact: pe xv | by exists X]. case: pd => h; last by move:h => /Zo_P [_]. set X := (fun z: Set => \0o). have aX: nds_ax X n by rewrite /X;move => i _ /=; fprops. by empty_tac1 (nds_card n X); apply: Zo_i; [by apply: pe | exists X]. Qed. Lemma nds_k: (nds_F \0c = \1c /\ nds_F \1c = \1c). Proof. move: nds_d => h. move: (nds_j NS0); set f := nds_F \0c;move => [_ _ p3 _]. move: p3 => [X ax <-]. move: (nds_j NS1); set g := nds_F \0c;move => [_ _ p2 _]. move: p2 => [Y ay <-]. have pa: \0c = \0c \/ \0c = \1c by left. have pb: \1c = \0c \/ \1c = \1c by right. by rewrite (h X _ pa ax) (h Y _ pb ay). Qed. Lemma nds_l: nds_F \2c = \2c. Proof. move: (nds_j NS2); set f := nds_F \2c. move => [p1 p2 p3 p4]. move: nds_g => [ax xv]; move: (p4 _ ax); rewrite xv; apply:cleA. by rewrite factorial2 in p2. Qed. Lemma nds_n e c1 c2 r1 r2: ordinalp e -> ordinalp c1 -> r1 \0o ordinalp r2 -> (omega0 ^o e *o c1 +o r1) +o (omega0 ^o e *o c2 +o r2) = (omega0 ^o e *o (c1 +o c2) +o r2). Proof. set p := omega0 ^o e;move => oe oc1 pa pb or2. have op := OS_pow OS_omega oe. have or1:= (proj31_1 pa). have oc2:= (proj32_1 pb). have oa := OS_prod2 op oc1. have ob := OS_prod2 op oc2. have oc := OS_sum2 ob or2. have H:=(ord_negl_prod or1 op pb (indecomp_prop1 (indecomp_prop4 oe) pa)). rewrite - (osumA oa or1 oc) (osumA or1 ob or2) H (osumA oa ob or2). by rewrite - (oprodD oc1 oc2 op). Qed. Lemma nds_o e (c r: fterm) n: natp n -> ordinalp e -> (forall i, i<=c n -> \0o osum_expansion (fun i => omega0 ^o e *o (c i) +o r i) (csucc n) = omega0 ^o e *o (osum_expansion c (csucc n)) +o (r \0c). Proof. move => nN oe; move: (OS_pow OS_omega oe) => op. move: n nN; apply: Nat_induction. move => H; rewrite succ_zero. move: (H _ (czero_least CS0)) => [[[_ oc _] _] [[or _ _] _]]. have ot:= (OS_sum2 (OS_prod2 op oc) or). by rewrite (osum_expansion1) // (osum_expansion1 oc). move => n nN Hrec ol. have sa: forall i, i <=c n -> \0o nn i lein; apply: ol (cleT lein nn). move: (ol _ (cleR (CS_succ n))) => [/proj32_1 ocn rs]. have or0:=(proj31_1 (proj2 (ol _ (czero_least (CS_succ n))))). rewrite (osum_expansion_succ _ (NS_succ nN)) (Hrec sa). have pc: \0o i lin; exact : (proj32_1 (proj1 (sa i (proj1 lin)))). move /(OS_osum_expansion nN) => ha. have [[_ oc0 _] /nesym cnz]:= proj1 (ol _ (cleS nN)). rewrite (osum_expansion_succ _ nN). by apply:(ord_ne0_pos (OS_sum2 oc0 ha)) => /(osum2_zero oc0 ha) []. by rewrite (nds_n oe ocn rs pc or0) (osum_expansion_succ _ (NS_succ nN)). Qed. Lemma nds_p1 e (c r: fterm) n f (X := (fun i => omega0 ^o e *o (c i) +o r i)): natp n -> ordinalp e -> (forall i, i<=c n -> \0o (forall i, i<=c n -> c i inc f (perm_int (csucc n)) -> nds_sc (csucc n) X f = omega0 ^o e *o (osum_expansion c (csucc n)) +o (r (Vf f \0c)). Proof. move => nN oe h1 h2 fp. have aux: forall n Z, natp n -> (forall i, i natp (Z i)) -> osum_expansion Z n = csumb n Z. move => m z mN; move: m mN; apply: Nat_induction. move => _; rewrite osum_expansion0 /csumb csum_trivial //. bw;exact:Nint_co00. move => m mN Hrec zp; rewrite (osum_expansion_succ _ mN) (succ_of_Nat mN). have ha: forall i, i natp (z i). move => i lim; apply: zp; exact: (clt_ltT lim (cltS mN)). have zmN:= (zp _ (cltS mN)); move: (nat_irreflexive mN) => mm. have sN: natp (csumb m z). apply:finite_sum_finite; split. by hnf; bw;move => i lim; bw; apply: ha; apply /(NltP mN). by bw; apply: finite_set_nat. by rewrite (csumA_setU1 z mm) (Hrec ha) csumC (osum2_2int zmN sN). move:(fp) => /Zo_P [] /functionsP [fz sz tz] bz. have sa: forall i, i <=c n -> \0o i /(NleP nN) lin; apply: h1; apply /(NleP nN); Wtac. transitivity (osum_expansion(fun i => omega0 ^o e *o (c (Vf f i)) +o r (Vf f i)) (csucc n)). by apply:(osum_expansion_exten (NS_succ nN)) => i lin. have h3: forall i,i inc (c i) Nat. by move => i /(cltSleP nN) /h2 /olt_omegaP. have h4: forall i,i natp (c (Vf f i)). move => i /(NltP (NS_succ nN)) lin; apply: h3. apply /(NltP (NS_succ nN)); Wtac. rewrite (nds_o nN oe sa) (aux _ _ (NS_succ nN) h3) (aux _ _ (NS_succ nN) h4). rewrite - {1} sz - tz (csum_Cn' c bz); reflexivity. Qed. Lemma the_CNF_omega_k k (X := omega0 +o k) (r:= fun i => CNFbvo (Vg (P (Q (the_CNF X)))) (Vg (Q (Q (the_CNF X)))) (cpred (P (the_CNF X)))): natp k -> [/\ \0o /olt_omegaP ko. have ok:= proj31_1 ko. have ox:= (OS_sum2 OS_omega ok). have xp: \0o // sz. by move: (osum2_zero OS_omega ok sz) => [p1 _]; move: omega_nz. case : (ozero_dichot ok) => kz. set e := fun i: Set => \1o. have ax: CNFb_axo e e \1c. split; first split. + apply: ole_2omega. + move => i lin; rewrite /e; fprops. + move => i lin; rewrite /e; apply:olt_1omega. + by move => i iB /clt1 h; case: (@succ_nz i). + move => i lin; rewrite /e; apply: olt_01. move: (CNFbB_prop ax NS1); set y := (CNFbB \1c e e); move => [ax2 yv]. have py2: P y = \1c by rewrite /y /CNFbB; aw. move: (CNFB_ax_simp ax2) => [_ ax4]. move: NS0 clt_01 => b0 lt01. have eq1: X = CNFBv y. rewrite py2 in ax4. rewrite /X kz (osum0r OS_omega) /CNFBv py2 /CNFbvo. rewrite (CNFq_p3 (proj1 ax4) lt01) /cantor_mon. rewrite /y /CNFbB !(pr1_pair, pr2_pair) /e; bw; Ytac0. by rewrite (opowx1 OS_omega) (oprod1r OS_omega). move:(the_CNF_p0 ox) => [sa sb]. rewrite /X - sb in eq1; rewrite py2 in ax4. rewrite /r /the_CNF_degree. rewrite (CNFB_unique sa ax2 eq1) py2 - succ_zero (cpred_pr1 CS0). split;[ by exact | by rewrite /y /CNFbB; aw; bw; Ytac0 |]. by rewrite /CNFbvo (CNFq_p2). pose e i := Yo (i = \0c) \0o \1o. pose c i := Yo (i = \0c) k \1o. move:card1_nz => H. move: clt_12 => lt12. move: clt_02 => lt02. move: olt_01 NS0 NS1 => l01 bs0 bs1. have e0: e \0c = \0o by rewrite /e; Ytac0. have e1: e \1c = \1o by rewrite /e; Ytac0. have c0: c \0c = k by rewrite /c; Ytac0. have c1: c \1c = \1o by rewrite /c; Ytac0. have ax: CNFb_axo e c \2c. split; first split. + apply: ole_2omega. + move => i lin; rewrite /e; Ytac h; fprops. + by move => i lin; rewrite /c; Ytac h => //; apply: olt_1omega. + move => i iB /clt2; rewrite /e; move: (@succ_nz i) => ss. rewrite - succ_zero; case => // si. by move: (succ_injective1 (CS_nat iB) CS0 si) => iz;Ytac0; Ytac0. + move => i lin; rewrite /c; Ytac h => //. move: (CNFbB_prop ax NS2); set y := (CNFbB \2c e c); move => [ax2 yv]. have py2: P y = \2c by rewrite /y /CNFbB; aw. move: (CNFB_ax_simp ax2) => [_ ax4]. have eq1: X = CNFBv y. rewrite py2 in ax4. move: (CNFq_p7 (proj1 ax4) lt12). rewrite /X /CNFBv /y /CNFbB !(pr1_pair, pr2_pair) -/CNFbvo => ->. rewrite /cantor_mon; bw; repeat Ytac0; rewrite e0 c0 e1 c1. by rewrite opowx0 (opowx1 OS_omega) (oprod1r OS_omega) (oprod1l ok). move:(the_CNF_p0 ox) => [sa sb]. rewrite /X - sb in eq1; rewrite py2 in ax4. rewrite /r /the_CNF_degree. rewrite (CNFB_unique sa ax2 eq1) py2 - succ_one (cpred_pr1 CS1). split;[ by exact | by rewrite /y /CNFbB; aw; bw; Ytac0 |]. rewrite /CNFbvo (CNFq_p3 (proj1 ax4) lt02). rewrite /cantor_mon /y /CNFbB; aw; bw; Ytac0; Ytac0. by rewrite c0 e0 opowx0 (oprod1l ok). Qed. Lemma nds_q1 e X n (r:= fun i => CNFbvo (Vg (P (Q (the_CNF (X i))))) (Vg (Q (Q (the_CNF (X i))))) (cpred (P (the_CNF (X i))))) (F:= fun_image (csucc n) r): natp n -> (forall i, i<=c n -> \0o (forall i, i<=c n -> the_CNF_degree (X i) = e) -> nds_card (csucc n) X = cardinal F. Proof. move => nN pa pb. have oe: ordinalp e. have ha:= (czero_least (CS_nat nN)). rewrite -(pb _ ha); exact: (OS_the_CNF_degree (proj32_1 (pa _ ha))). pose c i := Vg (Q (Q (the_CNF (X i)))) (cpred (P (the_CNF (X i)))). have pc: forall i, i<=c n -> [/\ \0o i lein; move: (pa _ lein) (pb _ lein) => sa sb. by move: (the_CNF_split sa); rewrite sb. have pd: (forall i, i<=c n -> \0o i /pc[]. have pe: (forall i, i<=c n -> c i i /pc[]. rewrite /nds_card /nds_sums. set E := (perm_int (csucc n)). set s1:= omega0 ^o e *o (osum_expansion c (csucc n)). have os1: ordinalp s1. apply: (OS_prod2 (OS_pow OS_omega oe)). apply: (OS_osum_expansion (NS_succ nN)) => i /(cltSleP nN) lin. by move:(pc _ lin) => [ /proj32_1 h _ _ _]. set F1 := (fun_image E (nds_sc (csucc n) X)). set F2 := (fun_image E (fun f => r (Vf f \0c))). have pf: forall f, inc f E -> nds_sc (csucc n) X f = s1 +o (r (Vf f \0c)). move => f fp; rewrite - (nds_p1 nN oe pd pe fp). by apply:(nds_sc_exten (NS_succ nN) _ fp) => i /(cltSleP nN) /pc []. have pg: forall z, inc z E -> inc (Vf z \0c) (csucc n). move => z /Zo_P [] /functionsP [fz sz tz] bz; Wtac. rewrite sz; apply/(NleP nN); fprops. have osF: ordinal_set F2. by move => s /funI_P [z /pg /(NleP nN) /pc [_ _ /proj31_1 h _] ->]. have ->: cardinal F1 = cardinal F2. symmetry; apply/card_eqP; exists (Lf (fun z => s1 +o z) F2 F1). split; aw; apply:lf_bijective. + by move => s /funI_P [z ze -> ]; apply /funI_P; ex_tac; rewrite (pf _ ze). + by move => u v /osF ou /osF ov /(osum2_simpl ou ov os1). + move => s /funI_P [z ze -> ]; rewrite (pf _ ze). exists (r (Vf z \0c)) => //;apply/funI_P; ex_tac. apply: f_equal; set_extens t. move => /funI_P [z /pg ze -> ]; apply /funI_P; ex_tac. move => /funI_P [i /(NltP (NS_succ nN)) iI ->]; apply /funI_P. move: (permutation_exists1 (NS_succ nN) iI) => [f fe <-]; ex_tac. Qed. Lemma nds_q2 e X n: natp n -> (forall i, i<=c n -> \0o (forall i, i<=c n -> the_CNF_degree (X i) = e) -> nds_card (csucc n) X <=c (csucc n). Proof. move => pa pb pc; rewrite (nds_q1 pa pb pc). set r := fun i:Set => _. by move: (fun_image_smaller (csucc n) r); rewrite (card_card (CS_succ _)). Qed. Lemma nds_q3 n: natp n -> exists X, [/\ nds_ax X (csucc n), forall i, i \0o the_CNF_degree (X i) = \1o) & nds_card (csucc n) X = (csucc n)]. Proof. move=> nN. pose X i := (omega0 +o i). have Ha: (forall i, i <=c n -> \0o i lein; move:(NS_le_nat lein nN) => iN. exact:(proj31 (the_CNF_omega_k iN)). have Hb:(forall i, i <=c n -> the_CNF_degree (X i) = \1o). move => i lein; move:(NS_le_nat lein nN) => iN. exact:(proj32 (the_CNF_omega_k iN)). have Hc:(forall i, i \0o i/(cltSleP nN) /Ha. have Hd:nds_ax X (csucc n) by move => i /Hc /proj32_1. exists X; split => //. rewrite (nds_q1 nN Ha Hb). set E := (csucc n). set F := fun_image _ _. have ->: F = fun_image E id. by set_extens t => /funI_P [z ze ->]; apply/funI_P; ex_tac; rewrite (proj33 (the_CNF_omega_k (NS_inc_nat (NS_succ nN) ze))). have ->: (fun_image E id) = E. set_extens t; first by move => /funI_P [z ze ->]. move => te; apply/funI_P; ex_tac. by rewrite (card_card (CS_succ n)). Qed. Definition nds_type0 X n := exists2 i, i \0o m <=o the_CNF_degree (X i)) & cardinal (Zo n (fun i => the_CNF_degree (X i) = m)) =k]). Definition nds_type X n k:= ((k = \0c) /\ (nds_type0 X n)) \/ (k <> \0c /\ (nds_type' X n k)). Definition nds_FA n k:= \osup (Zo Nat (fun z => exists X, [/\ nds_ax X n, nds_card n X = z & nds_type X n k])). Lemma nds_type_p1 X n k1 k2: natp n -> (nds_type X n k1) -> (nds_type X n k2) -> k1 = k2. Proof. rewrite /nds_type /nds_type'; move=> nN p1 p2. case: p1; move => [pa pb]; case: p2; move => [pc pd]. + by rewrite pa pc. + by move: pb pd=> [i id vz] [pd _]; move: (proj2 (pd _ id)); case. + by move: pb pd => [pb _] [i id iz]; move: (proj2 (pb _ id)); case. + move: pb pd => [qa [m [om qb qc]]] [_ [p [op qd qe]]]. suff mp: m = p by rewrite -qc -qe mp. move: qc; set T1 := Zo _ _ => qc. have : \1c <=c (cardinal T1) by apply: cge1; fprops; ue. move /cle1P => [i] /Zo_P [/(NltP nN) /qd le1 mv]. move: qe; set T2 := Zo _ _ => qe. have : \1c <=c (cardinal T2) by apply: cge1; fprops; ue. move /cle1P => [j] /Zo_P [/(NltP nN) /qb le2 pv]. by rewrite pv in le2; rewrite mv in le1; apply:oleA. Qed. Lemma nds_type_p2 X n: natp n -> n <> \0c -> nds_ax X n -> exists2 k, k <=c n & nds_type X n k. Proof. move => nN nnz ax. case: (p_or_not_p (nds_type0 X n)) => h. exists \0c; fprops;left; split => //. set E:= fun_image n (fun i => the_CNF_degree (X i)). set m := intersection E. set F := (Zo n (fun i => the_CNF_degree (X i) = m)). have s1: sub F n by apply Zo_S. move: (sub_smaller s1); rewrite (card_nat nN) => le1. have osE: ordinal_set E. rewrite /E; move=> t /funI_P [z /(NltP nN) /ax zi ->]. by apply: OS_the_CNF_degree. have neE: nonempty E. by apply:funI_setne; exists \0c; apply/(NltP nN) /(strict_pos_P1 nN). move: (ordinal_setI neE osE); rewrite -/m => mE. have om: ordinalp m by apply:osE. have neF: nonempty F. by move: mE => /funI_P [z zn zv]; exists z; apply: Zo_i. set k := cardinal F. exists k => //; right; split => //. by apply: (card_nonempty1 neF). split. move => i lin; case: (ozero_dichot (ax _ lin)) => //. by move => baa;case: h; exists i. exists m; split => // i /(NltP nN) lin. have uE: inc (the_CNF_degree (X i)) E by apply /funI_P; ex_tac. by split; [ exact | apply: osE | apply:setI_s1]. Qed. Lemma nds_FA_ex n k: natp n -> n <> \0c -> k <=c n -> nds_FA n k <> \0c. Proof. move => nN nz klen. rewrite /nds_FA. have [X pa pb]: exists2 X, nds_ax X n & nds_type X n k. case (equal_or_not k \0c) => kz. rewrite kz; exists (fun z:Set => \0o). move => i _ /=; fprops. left; split => //; exists \0c => //; apply: card_ne0_pos; fprops. pose X i := Yo (i t _; rewrite /X; Ytac h; fprops. have hb:forall i, i \0o i _; rewrite /X; Ytac h; [apply: olt_01| apply: olt_0omega]. exists X => //; right; split => //; split => //. move: the_CNF_degree_one the_CNF_degree_omega => dg1 dgo. exists \0o; split; fprops. + by move => i /ha/OS_the_CNF_degree /ozero_least. + set E := Zo _ _. move:(NS_le_nat klen nN) => kN. have ->: E = k. set_extens t. move => /Zo_P [ /(NltP nN) lth]; rewrite /X; Ytac h1. by move => _; apply/(NltP kN). by rewrite dgo => ba; case: card1_nz. move => /(NltP kN) ltl;apply: Zo_i. apply /(NltP nN); exact:(clt_leT ltl klen). by rewrite /X; Ytac0; rewrite dg1. exact:(card_nat kN). set E := Zo Nat _. have ce: cardinal_set E by move => i /Zo_S /CS_nat. move: (nds_c X nN) => [pc pd]. have zE: inc (nds_card n X) E. apply/Zo_i => //; exists X => //. by move: (card_sup_ub ce zE) => /(cleT pc) /cge1P[_ /nesym]. Qed. Lemma nds_type_p3 n k (v := nds_FA n k): natp n -> n <> \0c -> k <=c n -> [/\ natp v, v <=c (nds_F n), (forall X, nds_ax X n -> nds_type X n k -> nds_card n X <=c v) & (exists X, [/\ nds_ax X n, nds_type X n k & nds_card n X = v])]. Proof. move=> nN nz kn. rewrite /v /nds_FA; set T:= Zo Nat _. have ta: sub T Nat by apply: Zo_S. have tb: inc (nds_F n) Nat by move: (nds_j nN) => [ok _]. have tc: (forall i, inc i T -> i <=c (nds_F n)). move => i /Zo_P [_ [X [ax <- _]]]. by move: (nds_j nN) => [_ _ _ p4]; apply: p4. move: (Nat_sup_pr ta tb tc) => [pa pb pc pd]. have pe: forall X, nds_ax X n -> inc (nds_card n X) Nat. move: (NS_factorial nN) => tb1. move=> X ax; move: (nds_a X nN) => le1; apply: (NS_le_nat le1 tb1). split => //. by move=> X ax ax2; apply: pc; apply: Zo_i; [by apply: pe | exists X ]. case: pd; last by move /Zo_P=> [_ [X [p1 p2 p3]]];exists X; split. move => te. by move: (nds_FA_ex nN nz kn); rewrite /nds_FA -/T te setU_0; case. Qed. Lemma nds_type_p4 n (g := nds_FA n) (f:= nds_F n): natp n -> n <> \0c -> [/\ (forall k, k <=c n -> (g k) <=c f), (exists2 k, k <=c n & (g k) = f) & f= \osup (fun_image (Nintc n) g) ]. Proof. move=> nN nz. have pa: (forall k : Set, k <=c n -> g k <=c f). by move => k kn; move: (nds_type_p3 nN nz kn) => [_ pa _]. move: (nds_j nN); rewrite -/f; move=> [_ _ [X x1 x2] pd]. move: (nds_type_p2 nN nz x1) => [k kn kt]. move: (nds_type_p3 nN nz kn) => [_ _ pe pf]. have pb: (exists2 k, k <=c n & g k = f). move: (pe _ x1 kt); rewrite x2 => qa. move: pf=> [Y [ax x3 x4]]; exists k => //. apply cleA. rewrite /g - x4; apply: pd => //. by apply: (cleT qa); apply cleR; move: qa => [_ ok _]. split => //. have oT: ordinal_set (fun_image (Nintc n) g). move=> t /funI_P [z zc ->]. by move: zc => /(NintcP nN) => kn1; move: (pa _ kn1) => [[ok _] _]. apply: oleA. move: pb=> [s sn sv]. apply: ord_sup_ub => //; apply /funI_P; exists s => //. by apply /(NintcP nN). apply: ord_ub_sup => //. by move: (pa _ kn) => [_ [ok _] _]. move=> t /funI_P [z zc ->]; move: zc => /(NintcP nN) => zc. exact: (ocle (pa _ zc)). Qed. Lemma nds_type_p5 n X: natp n -> nds_ax X n -> nds_type0 X n -> exists Y, [/\ nds_ax Y n, nds_card n X = nds_card n Y & Y (cpred n) = \0o]. Proof. move => nN ax [i lin vz]. move /(NltP nN):(lin) => ii. move: (cle_ltT (czero_least (proj31_1 lin)) lin) => np. case: (equal_or_not i (cpred n)) => ip. exists X; split; [exact | exact |ue]. pose g j := Yo (j = i) (cpred n) (Yo (j = (cpred n)) i j). have pa: g (cpred n) = i by rewrite /g; Ytac0; Ytac0. have nz:= (nesym (proj2 np)). move: (cpred_pr nN nz) => [pb pc]. have axx: cpred n t /(NltP nN) => h; apply /(NltP nN). by rewrite /g; Ytac h1 => //; Ytac h2. set G:= Lf g n n. have qc: inc (cpred n) n by apply /(NltP nN). have bg: bijection G. apply: lf_bijective => //. move=> u v ue ve; rewrite /g; Ytac h1; Ytac h2. + by rewrite h1 h2. + Ytac h3; [ by rewrite h3 h1 | by move=> eq; case: h3 ]. + by rewrite h2; Ytac h3; [ move => <-| Ytac h4; [| move=> h; case: h3]]. + by Ytac h3; [ move=> h4; case: h2 | Ytac h4;[ move => h5; case: h1 |]]. move=> y yE; rewrite /g. case: (equal_or_not y (cpred n)) => qa. by exists i=> //; Ytac0; Ytac0. case: (equal_or_not y i) => qb. exists (cpred n) => //;Ytac0; Ytac0 => //. by exists y => //; Ytac0; Ytac0. have qx: function (Lf g n n) by apply: lf_function. have GE: inc G (permutations n). apply: Zo_i => //; apply /functionsP;split => //; rewrite /G; aw. have ax2:= proj1(nds_b nN ax GE). exists (fun z => X (Vf G z)). by rewrite - (nds_m nN ax GE) {2}/G /g; aw; Ytac0; Ytac0; split. Qed. Lemma nds_type_p6 n X: natp n -> nds_ax X (csucc n) -> X n = \0o -> nds_card (csucc n) X = nds_card n X. Proof. move => nN ax nz. have snN := NS_succ nN. have IP := (NltP nN). have IP' := (NltP snN). have H0:=(cltSleP nN). have nn:= cltS nN. have nI': inc n (csucc n) by apply /(NltP snN). have Ha: forall i, i <=c n -> i <> n -> inc i n. by move => i lein nin; apply /(NltP nN). rewrite /nds_card; apply:f_equal; set_extens z; last first. move => /funI_P [f /Zo_P [ /functionsP [ff sf tf] bf] ->]. have Hb: forall i, i <=c n -> i <> n -> Vf f i i lein nin; move: (Ha _ lein nin); rewrite - sf => isf. by move:(Vf_target ff isf); rewrite tf sf => /(NltP nN). pose g z := Yo (z = n) n (Vf f z). have ta: lf_axiom g (csucc n) (csucc n). move => i /IP' /H0 isn;apply /IP'; rewrite /g; Ytac h; fprops. by move: (clt_ltT (Hb _ isn h) nn). have bg: bijection (Lf g (csucc n) (csucc n)). apply: lf_bijective => //. move => u v /IP' /H0 lun /IP' /H0 lvn. rewrite /g; Ytac h1; Ytac h2. + by rewrite h1 h2. + by move: (nesym (proj2 (Hb _ lvn h2))). + by move: (proj2 (Hb _ lun h1)). + by apply: (proj2 (proj1 bf)); rewrite sf; apply: Ha. move => y yI; case (equal_or_not y n) => eyn. by exists y => //; rewrite eyn /g; Ytac0. move:yI => /IP' /H0 lyn. move: (Ha _ lyn eyn); rewrite - {1} tf => /(proj2 (proj2 bf)). rewrite sf; move => [x /IP xsf <-]. move: (clt_ltT xsf nn) => /IP' xi'. by move: (proj2 xsf) => lxn; ex_tac;rewrite /g; Ytac0. apply/funI_P; exists (Lf g (csucc n) (csucc n)). apply/Zo_i => //;apply/functionsP; split; [ fct_tac | aw | aw]. rewrite /nds_sc (osum_expansion_succ _ nN) {1} /g; aw; Ytac0; rewrite nz. set A := osum_expansion _ _; set B := osum_expansion _ _. have <-: A = B. apply: (osum_expansion_exten nN) => i lin; rewrite /g. have lin':= (clt_ltT lin nn). have ii: inc i (csucc n) by apply /IP'. by aw; move: (proj2 lin) => nin; Ytac0. have oA: ordinalp A. apply: (OS_osum_expansion nN) => i lin; apply: ax. exact: (clt_ltT (Hb _ (proj1 lin) (proj2 lin)) nn). by rewrite (osum0l oA). move => /funI_P [f /Zo_P [ /functionsP [ff sf tf] bf] ->]. have ntf: inc n (target f) by rewrite tf; apply /(NltP snN). set i0:= Vf (inverse_fun f) n. have fif: function (inverse_fun f) by apply: bijective_inv_f. have i0sf: inc i0 (source f) by rewrite -ifun_t /i0; Wtac; rewrite ifun_s. have fi0: Vf f i0 = n by rewrite /i0; rewrite (inverse_V bf ntf). have iff:= (proj2 (proj1 bf)). case (equal_or_not i0 n) => ei0n. set f0:= Lf (Vf f) n n. have axf: lf_axiom (Vf f) n n. move => i /IP lin; apply/IP. have lin':= clt_ltT lin nn. have isf: inc i (source f) by rewrite sf; apply/IP'. move: (Vf_target ff isf); rewrite tf => /IP' /H0 le1. case (equal_or_not (Vf f i) n) => eq1; last by split. rewrite - eq1 in fi0. have h1:= (iff _ _ i0sf isf fi0). by case (proj2 lin); rewrite - h1 ei0n. have fp: inc f0 (permutations n). apply: Zo_i. by rewrite /f0;apply/functionsP; split; aw;apply:lf_function. apply:lf_bijective => //. move => u v /IP ui /IP vi; move:(clt_ltT ui nn)(clt_ltT vi nn) => ha hb. by apply:(iff u v);rewrite sf; apply /IP'. move => y /IP yp; move:(clt_ltT yp nn)=> yp'. have ytf: inc y (target f) by rewrite tf; apply /IP'. move:(proj2 (proj2 bf) _ ytf) => [x xsf eq1]; exists x => //. move: xsf;rewrite sf => /IP' /H0 xn. by apply /IP; split => //exn; move:(proj2 yp); rewrite -eq1 - fi0 exn ei0n. apply/funI_P; exists f0; first exact. rewrite /nds_sc (osum_expansion_succ _ nN) - {1} ei0n fi0 nz. set A := osum_expansion _ _. have oA: ordinalp A. apply: (OS_osum_expansion nN) => i lin; apply: ax. have lin':=(clt_ltT lin nn). by apply/IP'; rewrite - tf; Wtac; rewrite sf;apply/IP'. rewrite (osum0l oA); apply: (osum_expansion_exten nN). move => i /IP lin /=; rewrite /f0; aw. have li0n: i0 <=c n. apply /H0; apply/IP'; rewrite - sf - ifun_t. by apply:Vf_target => //;rewrite ifun_s. move/(cleSSP (proj31 li0n) (proj32 li0n)): (li0n) => li0n1. move: (cdiff_pr li0n1)(NS_diff (csucc i0) snN). set m := (csucc n -c csucc i0) => sa mN. have iN:=(NS_le_nat li0n nN). have siN:=(NS_le_nat li0n1 snN). have sb : i0 +c m = n. apply: (succ_injective1 (CS_sum2 i0 m) (CS_nat nN)). by rewrite - (csum_Sn _ iN) sa. pose g i := Yo (i i /IP lin; rewrite /g; Ytac h; apply /IP => //. have lin':=(clt_ltT lin nn). have isf: inc i (source f) by rewrite sf; apply /IP'. move: (Vf_target ff isf); rewrite tf => /IP' /H0 ha; split; first exact. rewrite - fi0 => h1; move: (iff _ _ isf i0sf h1) => h2. by case: (proj2 h). have isf: inc (csucc i) (source f). by rewrite sf; apply /IP'; apply :cltSS. move: (Vf_target ff isf); rewrite tf => /IP' /H0 ha; split; first exact. rewrite - fi0 => h1; move: (iff _ _ isf i0sf h1) => h2. by case: h; rewrite - h2; apply:(cltS (NS_lt_nat lin nN)). have ax1: ord_below_n f0 (csucc i0 +c m). rewrite sa => i lin; rewrite /f0; apply: ax; apply/(NltP snN). by Wtac; rewrite sf; apply/(NltP snN). have ax2: (ord_below_n g0 (i0 +c m)). rewrite sb => i /IP lin; rewrite /g0; aw; apply ax. move: (axg _ lin) => /IP h1; exact: (clt_ltT h1 nn). have osa: ordinalp (osum_expansion f0 i0). apply: (OS_osum_expansion iN) => i lin; rewrite /f0; apply: ax. apply/(NltP snN); Wtac; rewrite sf;apply/(NltP snN). exact: (clt_ltT lin (cle_ltT li0n nn)). have -> : nds_sc (csucc n) X f = nds_sc n X (Lf g n n). move: (osum_expansionA siN mN ax1); rewrite sa -/(nds_sc _ _ _) => ->. rewrite (osum_expansion_succ _ iN) {2} /f0 fi0 nz (osum0l osa). rewrite /nds_sc - {3} sb (osum_expansionA iN mN ax2); apply: f_equal2. apply:(osum_expansion_exten mN) => i lim; rewrite /f0/g0 /g. have ha: inc (i +c i0) n. apply /IP; rewrite - {1} sb (csumC _ m); apply:(csum_Mlteq iN lim). have hb: ~(i +c i0 ua ub. case: (cleNgt ua ub). by aw; Ytac0; rewrite (csum_nS _ iN). apply:(osum_expansion_exten iN) => i lim; rewrite /f0/g0 /g. aw; [ by Ytac0 |apply /IP; apply: (clt_leT lim li0n) ]. apply /funI_P; exists (Lf g n n) => //; apply: Zo_i. by apply/functionsP; split; aw; apply:lf_function. apply: lf_bijective => //. move => u v /IP ui /IP vi. move:(clt_ltT ui nn)(clt_ltT vi nn) => ui' vi'. have usf: inc u (source f) by rewrite sf;apply/IP'. have vsf: inc v (source f) by rewrite sf;apply/IP'. move:(NS_lt_nat ui nN) (NS_lt_nat vi nN) => uN vN. have u'sf: inc (csucc u) (source f). by rewrite sf;apply/IP';apply:cltSS. have v'sf: inc (csucc v) (source f). by rewrite sf;apply/IP';apply:cltSS. rewrite /g; Ytac h1; Ytac h2 => eq. + by apply: (proj2 (proj1 bf) _ _ usf vsf). + move: (proj2 (proj1 bf) _ _ usf v'sf eq) => e2. move: h1; rewrite e2 => e3; case h2; exact: (cle_ltT (cleS vN) e3). + move: (proj2 (proj1 bf) _ _ u'sf vsf eq) => e2. move: h2;rewrite - e2 => e3; case h1; exact: (cle_ltT (cleS uN) e3). + move: (proj2 (proj1 bf) _ _ u'sf v'sf eq). by move => /(succ_injective1 (proj31_1 ui) (proj31_1 vi)). move => y /IP yi; move:(clt_ltT yi nn) => yi'. have ytf: inc y (target f) by rewrite tf; apply/IP'. move: (proj2 (proj2 bf) _ ytf) => [x xsf ea]; rewrite - ea. move: xsf; rewrite sf => /IP' xsn. have xN:= (NS_lt_nat xsn snN). case: (NleT_ell iN xN) => cix. + by move:(f_equal (Vf f) cix); rewrite fi0 ea; move => eb; case: (proj2 yi). + case (equal_or_not x \0c) => xnz. rewrite xnz in cix;case:(clt0 cix). move: (cpred_pr xN xnz) => [sc sd]. move: xsn; rewrite sd;move/(cltSSP (CS_nat sc) (CS_nat nN)) => /IP ci. exists (cpred x) => //; rewrite - sd /g; Ytac h; last by rewrite - sd. by move/(cleSlt0P (CS_nat sc) iN):h; rewrite - sd => /(cltNge cix). exists x; [ apply /IP; exact:(clt_leT cix li0n) | by rewrite /g; Ytac0]. Qed. Lemma nds_type_p7 n: natp n -> nds_FA (csucc n) \0c = nds_F n. Proof. move => nN. move: (nds_type_p3 (NS_succ nN) (@succ_nz n) (czero_least (CS_succ n))). move => [pa pb pc pd]. move:pd => [X0 [aX0 Xt0 Xv]]. move: Xt0; case; [move => [_ pe] | by case]. move: (nds_type_p5 (NS_succ nN) aX0 pe) => [X2 [ax2 X2v X20]]. have pg': X2 n = \0o by move:X20; rewrite (cpred_pr2 nN). move: Xv; rewrite X2v => eq0. clear pe aX0 X20 X2v. have r1:= (nds_type_p6 nN ax2 pg'). move: (nds_j nN) => [sa sb [X4 ax4 eq1] sd]. set X5 := fun z => Yo (z = n) \0o (X4 z). have ax5: nds_ax X5 (csucc n). move => i /(cltSleP nN) lin; rewrite /X5; Ytac h; fprops; apply: ax4. split => //. have X5n: X5 n = \0c by rewrite /X5; Ytac0. have ax3: nds_ax X2 n. move => i lin; apply: (ax2 i (clt_ltT lin (cltS nN))). have nd5: nds_type X5 (csucc n) \0c. by rewrite /X5;left; split => //; exists n; fprops; Ytac0. have r2:= (nds_type_p6 nN ax5 X5n). have r3: nds_card n X5 = nds_card n X4. rewrite /nds_card/nds_sums; apply: f_equal. have H: forall z i, inc z (permutations n) -> i (Vf z i <> n). move => z i /Zo_P [] /functionsP [fz sz tz] bz /(NltP nN). rewrite - {1} sz => isz; move: (Vf_target fz isz); rewrite tz. by move/(NltP nN) => [_]. by set_extens t; move /funI_P => [z zp ->]; apply/funI_P; ex_tac; apply:(osum_expansion_exten nN) => i lin; move: (H _ _ zp lin) => w; rewrite /X5; Ytac0. apply: cleA; first by move: (sd _ ax3); rewrite - eq0 r1. by move: (pc _ ax5 nd5); rewrite r2 r3 eq1. Qed. Lemma nds_type_p8 n: natp n -> nds_FA (csucc n) (csucc n) = (csucc n). Proof. move => nN. move: (nds_type_p3 (NS_succ nN) (@succ_nz n) (cleR (CS_succ n))). set v := (nds_FA (csucc n)). move => [vB vle va vb]. move: (nds_q3 nN) => [X[pa pb pc pd]]. have pe: nds_type X (csucc n) (csucc n). right; split; first by apply: succ_nz. split => //; exists \1o; split. + apply: OS1. + move => i/(cltSleP nN) /pc ->; fprops. + set E := Zo _ _. have ->: E = (csucc n). apply: extensionality;[ apply: Zo_S | move => t ti; apply: Zo_i => //]. by apply:pc; apply /(NleP nN). by rewrite (card_card (CS_succ _)). move: (va _ pa pe); rewrite pd => le1. move: vb => [Y [ay ty yv]]. case ty; [ by move :(@succ_nz n) => sp [h _] | move => [_ [ty1 ty2]]]. move:ty2 => [m [om mp1 mp2]]. have pg:forall i, i<=c n -> the_CNF_degree (Y i) = m. move: mp2; set I := (csucc n). have ci: cardinal I = csucc n by rewrite (card_nat (NS_succ nN)). have fsI: finite_set I. rewrite /finite_set ci; apply:(Nat_hi (NS_succ nN)). set E := Zo _ _ => ce. have seI: sub E I by apply: Zo_S. move: (cardinal_setC4 seI fsI);rewrite ci ce cdiff_nn. move /card_nonempty => H. move => i /(NleP nN) iI; ex_middle bad. by empty_tac1 i; apply /setC_P; split => // /Zo_hi. have pf: forall i, i<=c n -> \0o i /(cltSleP nN) /ty1. by move: (nds_q2 nN pf pg); rewrite yv => le2; apply: cleA. Qed. Lemma nds_type_p9_aux a b i j: ordinalp a -> ordinalp b -> i j exists2 k, k oo oa ob ip jp. move: (proj31_1 ip)(proj31_1 jp) => oi oj. have oA :=OS_sum2 (OS_prod2 oo oa) oi. have ooa:= OS_prod2 oo oa. have oob:= OS_prod2 oo ob. rewrite (osumA oA oob oj) - (osumA ooa oi oob). case: (ozero_dichot ob) => bp. exists (i +o j); first by apply:osum2_lt_omega. by rewrite bp oprod0r (osum0r oa) (osum0r oi) osumA. exists j => //. move: (odiff_pr (oprod_Mle1 oo bp)) => [pb pc]; rewrite pc. by rewrite (osumA oi oo pb) (osum_int_omega ip) - pc (oprodD oa ob oo). Qed. Lemma nds_type_p9 n (X:fterm) (Y:= fun i => osucc (omega0 *o (X i))): natp n -> nds_ax X n -> nds_card n X <=c nds_card n Y. Proof. move => nN aX. have pa: forall z, inc z (perm_int n) -> exists k, (odiv_pr0 (nds_sc n Y z) omega0 (nds_sc n X z) k). move => s /permutationsP [[[fs _] _] sf tf]; rewrite /Y /nds_sc. have: forall z, z ordinalp (X (Vf s z)). move => z /(NltP nN) zb; apply: aX; apply/(NltP nN); Wtac. move: (n) nN; apply: Nat_induction. have o0 := OS0. move => _; exists \0o;hnf;rewrite !osum_expansion0 oprod0r (osum0r OS0). split => //; by exact olt_0omega. move => m mN Hrec h1. have mm:= cltS mN. have /Hrec [k [oa kb kv kp]]: (forall z, z ordinalp (X (Vf s z))). move => z zm; apply:h1 => //; exact (clt_ltT zm mm). rewrite ! (osum_expansion_succ _ mN) kv. set a := osum_expansion _ _. have ob := h1 _ mm. rewrite - (osucc_pr (OS_prod2 OS_omega ob)). move:(nds_type_p9_aux ob oa olt_1omega kp) => [k2 k2p ->]. exists k2; split; [ by apply: OS_sum2 | exact:(proj31_1 k2p) | exact | exact ]. have pb: forall z, inc z (perm_int n) -> nds_sc n X z = P (oquorem (nds_sc n Y z) omega0). move => z zp; move:(pa _ zp) => [k kp]. have o1:ordinalp(nds_sc n Y z) by move: (kp) => [ra rb -> _]; fprops. exact (proj1 (oquoremP2 o1 olt_0omega kp)). rewrite /nds_card /nds_sums. set F := fun_image _ _; set E := fun_image _ _. pose f x := P (oquorem x omega0). have ax: forall x, inc x E -> inc (f x) F. by move => x /funI_P [z zp ->]; apply/funI_P; ex_tac; rewrite /f - pb. have sjf: surjection(Lf f E F). apply: lf_surjective => //. move => y /funI_P [z zp ->]; rewrite (pb _ zp). exists (nds_sc n Y z) => //; apply/funI_P; ex_tac. move: (image_smaller (proj1 sjf)). rewrite surjective_pr0; aw. Qed. Lemma nds_type_p10 n: natp n -> exists X, [/\ nds_ax X n, forall i, i \0o nN; move:(nds_j nN) => [ _ _ [X ax xv] pb]. move: (nds_type_p9 nN ax). set Y := (fun i => osucc (omega0 *o X i)) => r1. have ha: forall i, i \0o i /ax ox; apply:olt0S;apply: (OS_prod2 OS_omega ox). have hb: nds_ax Y n by move => t /ha /proj32_1. move: (pb _ hb) => hc; rewrite xv in r1. exists Y; split;[ done | done | by apply: cleA]. Qed. Lemma nds_type_p11 n (g := nds_FA n) (f:= nds_F n): natp n -> n <> \0c -> (forall k, k <=c n -> k <> \0c -> (g k) <=c f) /\ (exists k, [/\ k <=c n, k <> \0c & (g k) = f]). Proof. move => pa pb; move:(nds_type_p4 pa pb) => [pc _ _]. split; first by move => k kn _; apply: pc. move: (nds_type_p10 pa) => [X [ax1 ax2 xv]]. move: (nds_type_p2 pa pb ax1) => [k1 k1n tX]. move:(nds_type_p3 pa pb k1n) => [_ _ qa _]. move: (qa _ ax1 tX); rewrite xv => le1. case: tX; first by move => [_ [i lin xi]]; case: (proj2 (ax2 _ lin)). move => [knz _]; exists k1; split => //. exact: (cleA (pc _ k1n) le1). Qed. Definition nds_tn_S X n:= unionf (powerset n) (fun K => fun_image (perm_int (cardinal K)) (fun s => nds_sc (cardinal K) (fun z => X (nth_elt K z)) s)). Definition nds_tn_C X n := cardinal (nds_tn_S X n). Definition ndstnC n := csucc (n *c (\2c ^c (cpred n))). Definition nds_tn_ax X n := (forall i, i \0o the_CNF_degree (X i) = e. Definition nds_tn_sup n := \osup(Zo Nat (fun z => exists2 X, nds_tn_ax X n & nds_tn_C X n = z)). Lemma nds_tn1 X n: natp n -> nds_ax X n -> nds_tn_C X n <=c (\2c ^c n) *c (factorial n). Proof. move => nN ax. rewrite /nds_tn_C /nds_tn_S. set F:= (fun K : Set => _). set pIn := (powerset n). set g1:= (Lg pIn (fun a : Set => cardinal (Vg (Lg pIn F) a))). move: (csum_pr1_bis pIn F). have <-: csum g1 = csumb pIn (fun a : Set => cardinal (F a)). apply:csumb_exten => t tx; bw. set g2 := cst_graph pIn (factorial n). have sd: domain g1 = domain g2 by rewrite /g1/g2; bw. have le1:forall x, inc x (domain g1) -> Vg g1 x <=c Vg g2 x. rewrite /g1 /g2; bw => K KN; bw; move/setP_P:KN => KN. move:(sub_smaller KN); rewrite (card_nat nN) => ka. have nKN:=(NS_le_nat ka nN). move: (factorial_monotone nN ka); apply: cleT. have pa: finite_set (cardinal K) by apply/NatP; rewrite double_cardinal. move:(number_of_permutations pa). rewrite -/(perm_int _) double_cardinal => <-. apply:fun_image_smaller. move:(csum_increasing sd le1). rewrite csum_of_same cprodC - cprod2cl card_setP - cpowcr. move => ha hb; exact:(cleT hb ha). Qed. Lemma nds_tn2 n (f:= nds_tn_sup n): natp n -> [/\ natp f, \0c nds_tn_C X n <=c f)]. Proof. move => nN. rewrite /f /nds_tn_sup; set T := Zo _ _. have TN: sub T Nat by apply: Zo_S. have kN:=(NS_prod (NS_pow NS2 nN) (NS_factorial nN)). set k := \2c ^c n *c factorial n. have H: forall X, nds_tn_ax X n -> nds_tn_C X n <=c k. by move => X [ax _]; apply:(nds_tn1 nN) => i /ax /proj32_1. have H1:forall X, nds_tn_ax X n -> inc (nds_tn_C X n) Nat. move => X x1; exact:(NS_le_nat (H _ x1) kN). have ks:forall i, inc i T -> i <=c k by move => z /Zo_hi [X /H ax <-]. pose X (i:Set):= omega0. have ax: nds_tn_ax X n. split; first by move => i _; apply: olt_0omega. exists \1o; [ apply: OS1 | move => i _; apply:the_CNF_degree_omega]. have ta: inc (nds_tn_C X n) T by apply: (Zo_i (H1 _ ax)); exists X. have ha: \0c X (nth_elt K z)) (identity n)). apply/setUf_P; exists K; first by apply:setP_Ti. rewrite /K (card_nat nN);apply/funI_P;ex_tac. move /card_nonempty1; rewrite -/(nds_tn_C X n) => h0. have cst:cardinal_set T by move => t /TN /CS_nat. exact:(clt_leT (card_ne0_pos (cst _ ta) h0) (card_sup_ub cst ta)). move: (Nat_sup_pr TN kN ks) => [pa pb pc pd];split => //; last first. move => Y x1; apply: pc; apply/ Zo_P; split; [by apply: H1 | by exists Y]. by case:pd => h1; [ empty_tac1 (nds_tn_C X n) | exact: (Zo_hi h1)]. Qed. Lemma nds_tn3: nds_tn_sup \0c = \1c. Proof. move:(nds_tn2 NS0); rewrite factorial0 cpowx0 (cprod1r CS1). set f := nds_tn_sup \0c. by move =>[pa /cge1P pb px _ _]; apply:cleA. Qed. Lemma nth_set11 K a (f:= nth_elt K)(g:= nth_elt (K +s1 a)) (q:= cardinal K) : sub K Nat -> finite_set K -> natp a -> (forall i, inc i K -> i (forall i, i f i = g i) /\ g q = a. Proof. move => KN fsK aN Ha. have anK: ~ inc a K by move => /Ha []. move:(csucc_pr anK); set q1:= cardinal (K +s1 a);rewrite -/q => qv. have K1N: sub (K +s1 a) Nat by move => t /setU1_P; case; [apply: KN | move ->]. have qN: natp q by apply /NatP. have q1N: natp q1 by rewrite qv; fprops. move:(nth_set6 qN KN) (nth_set6 q1N K1N); rewrite -/q -/q1 qv => sa sb. suff aux: forall i, i<=c q -> nth_elts K i = nth_elts (K +s1 a) i. rewrite /f/g /nth_elt. split. move => i liq. move/(cleSltP (NS_lt_nat liq qN)): (liq) => /aux ->. by rewrite (aux _ (proj1 liq)). have hb: ((K +s1 a) -s K) = singleton a. apply:set1_pr; first by apply/setC_P; split; fprops. by move => z /setC_P [/setU1_P ha hb]; case: ha. by rewrite - (aux _ (cleR (CS_nat qN))) sb sa hb setU_1. move => i ilq; move:(NS_le_nat ilq qN) => iN. move: i iN ilq; apply: Nat_induction. by rewrite /nth_elts !induction_term0. move => n nN Hrec sc. rewrite (nth_elts_succ _ nN) (nth_elts_succ _ nN). have lenk:=(cleT (cleS nN) sc). rewrite - (Hrec lenk). move:(nth_set5 nN KN lenk) => [[]]. rewrite /nth_more; set S1 := (nth_elts K n) => ha hb hc. have s1: sub (K -s S1) Nat by move => t /setC_P [/KN]. have s2: sub ((K +s1 a) -s S1) Nat by move => t /setC_P [/K1N]. case:(emptyset_dichot (K -s S1)) => ne1. move:(cardinal_setC4 ha fsK); rewrite - /q hc ne1 cardinal_set0. by move: (nesym (cdiff_nz (clt_leT (cltS nN) sc))). have ne2: nonempty ((K +s1 a) -s S1). by exists a; apply/setC_P; split; [ fprops | move/ha]. move:(inf_Nat s1 ne1); set y1:= intersection _; move => [/setC_P[hu hv] pb]. move:(inf_Nat s2 ne2); set y2:= intersection _; move => [pa' pb']. apply: f_equal; apply:f_equal. have /pb' y21: inc y1 ((K +s1 a) -s S1) by apply/setC_P; split; fprops. move/setC_P:pa' => [/setU1_P hu1 hv1]; case: hu1=> hu1. by move/(setC_P): (conj hu1 hv1) => /pb le1; apply:cleA. by move:(Ha _ hu); rewrite - hu1 => /(cleNgt y21). Qed. Lemma nds_p2 n c K: natp n -> (forall i, i natp (c i)) -> inc K (powerset n) -> osum_expansion (fun z => c (nth_elt K z)) (cardinal K) = csumb K c. Proof. move => nN cIb /setP_P Kb. have KN: sub K Nat by move => t tK; move:(NS_inc_nat nN (Kb _ tK)). have fsK:=(sub_finite_set Kb (finite_set_nat nN)). set q := cardinal K; set f := nth_elt K. have qN: natp q by apply /NatP. have ha: forall i, i inc (f i) K. move => i iq; apply:(nth_set9 (NS_lt_nat iq qN) KN iq). have: forall j, inc j K -> exists2 i, i j jK; exact(nth_set_10 KN fsK jK). have : forall i j, i j f i = f j -> i = j. move => i j /(NltP qN) iq /(NltP qN) jq. move:(proj2 (proj1 (proj1 (nth_set_fct_bf KN fsK)))). have ax: lf_axiom (nth_elt K) (cardinal K) K. by move => t /(NltP qN) /ha. rewrite /nth_set_fct; aw => h; move: (h i j iq jq);aw. have: forall i, inc i K -> natp (c i) by move => i /Kb /(NltP nN) /cIb. move: q qN (f) (K) ha fsK; clear. apply: Nat_induction. move => k K _ _ _ _ sf. have h: domain (Lg K c) = emptyset. by bw; apply /set0_P => t /sf [i /clt0]. by rewrite osum_expansion0 /csumb (csum_trivial h). move => n nN Hrec f K fK fsK cN fi fs. rewrite (osum_expansion_succ _ nN). have nn:= (cltS nN). move:(fK _ nn) => fnK. move: (setC1_K fnK); set K1:= K -s1 (f n) => Kv. have h1: forall i, i inc (f i) K1. move => i lin; move:(clt_ltT lin nn) => h; move: (fK _ h). rewrite - Kv =>/setU1_P; case => // eq; move:(fi _ _ h nn eq) => ein. by case: (proj2 lin). have h2:=(sub_finite_set (@sub_setC K (singleton (f n))) fsK). have h3: forall i, inc i K1 -> inc (c i) Nat by move => i /setC1_P [/cN]. have h4: forall i j, i j f i = f j -> i = j. move => i j lin ljn;apply (fi _ _ (clt_ltT lin nn) (clt_ltT ljn nn)). have h5:forall j, inc j K1 -> exists2 i : Set, i j /setC1_P [/fs [i /(cltSleP nN) lin ->] h]. case: (equal_or_not i n) => ein; first by case: h; rewrite ein. by exists i. have fnk1:~ inc (f n) K1 by move/setC1_P=> [ _ ]. have skN: natp (csumb K1 c) . apply:finite_sum_finite; hnf; rewrite/allf;bw;split => //. by move => t tk1; bw; apply: h3. rewrite (Hrec f K1 h1 h2 h3 h4 h5) - Kv (csumA_setU1 _ fnk1). by rewrite (osum2_2int (cN _ fnK) skN) csumC. Qed. Lemma the_CNF_omega_kj j k (X := omega0 *o j +o k) (e := (the_CNF_degree X)) (r:= CNFbvo (Vg (P (Q (the_CNF X)))) (Vg (Q (Q (the_CNF X))))(cpred (P (the_CNF X)))) (c:= (Vg (Q (Q (the_CNF X))) (cpred (P (the_CNF X))))): natp j -> natp k -> \0c \0o /olt_omegaP kj /olt_omegaP ko /proj2 jp1. have ok:= proj31_1 ko. have oj:= proj31_1 kj. have jp : \0c // sz. move: (osum2_zero op ok sz) => [p1 _]. by case: (oprod2_nz OS_omega oj omega_nz (nesym jp1)). split; first by exact. case : (ozero_dichot ok) => kz. set ee := fun i: Set => \1o. set cc := fun i: Set => j. have ax: CNFb_axo ee cc \1c. split; first split. + apply: ole_2omega. + move => i lin; rewrite /ee; fprops. + by move => i lin; rewrite /cc. + by move => i iB /clt1 h; case: (@succ_nz i). + by move => i lin. move: (CNFbB_prop ax NS1); set y := (CNFbB \1c ee cc); move => [ax2 yv]. have py2: P y = \1c by rewrite /y /CNFbB; aw. move: (CNFB_ax_simp ax2) => [_ ax4]. move: NS0 clt_01 => b0 lt01. have eq1: X = CNFBv y. rewrite py2 in ax4. rewrite /X kz (osum0r op) /CNFBv py2 /CNFbvo. rewrite (CNFq_p3 (proj1 ax4) lt01) /cantor_mon. rewrite /y /CNFbB !(pr1_pair, pr2_pair) /e; bw; Ytac0. by rewrite (opowx1 OS_omega); Ytac0. move:(the_CNF_p0 ox) => [sa sb]. rewrite - sb in eq1; rewrite py2 in ax4. rewrite /e/c /r /the_CNF_degree. rewrite (CNFB_unique sa ax2 eq1) py2 - succ_zero (cpred_pr1 CS0). rewrite /y/CNFbB; aw; bw; repeat Ytac0; rewrite /CNFbvo (CNFq_p2). by split. pose ee i := Yo (i = \0c) \0o \1o. pose cc i := Yo (i = \0c) k j. move:card1_nz => H. move: clt_12 => lt12. move: clt_02 => lt02. move: olt_01 NS0 NS1 => l01 bs0 bs1. have e0: ee \0c = \0o by rewrite /ee; Ytac0. have e1: ee \1c = \1o by rewrite /ee; Ytac0. have c0: cc \0c = k by rewrite /cc; Ytac0. have c1: cc \1c = j by rewrite /cc; Ytac0. have ax: CNFb_axo ee cc \2c. split; first split. + apply: ole_2omega. + move => i lin; rewrite /ee; Ytac h; fprops. + by move => i lin; rewrite /cc; Ytac h => //; apply: olt_1omega. + move => i iB /clt2; rewrite /ee; move: (@succ_nz i) => ss. rewrite - succ_zero; case => // si. by move: (succ_injective1 (CS_nat iB) CS0 si) => iz;Ytac0; Ytac0. + move => i lin; rewrite /cc; Ytac h => //. move: (CNFbB_prop ax NS2); set y := (CNFbB \2c ee cc); move => [ax2 yv]. have py2: P y = \2c by rewrite /y /CNFbB; aw. move: (CNFB_ax_simp ax2) => [_ ax4]. have eq1: X = CNFBv y. rewrite py2 in ax4. move: (CNFq_p7 (proj1 ax4) lt12). rewrite /X /CNFBv /y /CNFbB !(pr1_pair, pr2_pair) -/CNFbvo => ->. rewrite /cantor_mon; bw; repeat Ytac0; rewrite e0 c0 e1 c1. by rewrite opowx0 (opowx1 OS_omega) (oprod1l ok). move:(the_CNF_p0 ox) => [sa sb]. rewrite - sb in eq1; rewrite py2 in ax4. rewrite /e/c/r /the_CNF_degree. rewrite (CNFB_unique sa ax2 eq1) py2 - succ_one (cpred_pr1 CS1). rewrite /CNFbvo (CNFq_p3 (proj1 ax4) lt02) /cantor_mon /y/CNFbB/CNFbvo. by aw; bw; repeat Ytac0; rewrite e0 opowx0 c0 (oprod1l ok); split. Qed. Section NdsStudy1. Variables (X: fterm) (n:Set). Hypothesis nN: natp n. Hypothesis np: \0c [e ea eb]; rewrite /ee (eb _ np). Qed. Lemma nds_tn5 i: i the_CNF_degree (X i) = ee. Proof. by move:(proj2 ax) => [e ea eb] lin; rewrite /ee (eb _ np) (eb _ lin). Qed. Let rr:= fun i => CNFbvo (Vg (P (Q (the_CNF (X i))))) (Vg (Q (Q (the_CNF (X i))))) (cpred (P (the_CNF (X i)))). Let cc:= fun i => (Vg (Q (Q (the_CNF (X i)))) (cpred (P (the_CNF (X i))))). Lemma nds_tn6 i: i [/\ \0o lin. rewrite - (nds_tn5 lin). have xp:= (proj1 ax i lin). move:(the_CNF_p0 (proj32_1 xp)) (the_CNF_p2 xp) => [/CNFB_ax_simp [ha hb] hc]. move: ha hb hc; rewrite /cc /rr /ee /the_CNF_degree. set e := Vg (P (Q (the_CNF (X i)))). set c := Vg (Q (Q (the_CNF (X i)))). set ln := (cpred (P (the_CNF (X i)))). set lm:= (P (the_CNF (X i))). move => lmB axx Xv [lnN lmv]. have lnm: ln [_ _ pc _]; exact: (pc _ lnm). + apply:(CNFq_pg lnN); rewrite - lmv;exact:(proj1 axx). + by rewrite - Xv /CNFBv -/lm lmv /CNFbvo (CNFq_p1 _ _ _ lnN). Qed. Lemma nds_tn7 K s: K = emptyset -> nds_sc (cardinal K) (fun z => X (nth_elt K z)) s = \0c. Proof. by move => ->;rewrite cardinal_set0 /nds_sc osum_expansion0. Qed. Lemma nds_tn8 K s: inc K (powerset n) -> inc s (perm_int (cardinal K)) -> nonempty K -> nds_sc (cardinal K) (fun z => X (nth_elt K z)) s = omega0 ^o ee *o osum_expansion (fun z => cc (nth_elt K z)) (cardinal K) +o rr (nth_elt K (Vf s \0c)). Proof. move => /setP_P sb sp nek. move:(sub_smaller sb); rewrite (card_nat nN) => ckn. have ckN:=(NS_le_nat ckn nN). have cknz:= (card_nonempty1 nek). move:(cpred_pr ckN cknz); set k:= cpred _; move => [kN kv]. have ikP: forall i, i<=c k -> (nth_elt K i) i /(cltSleP kN); rewrite -kv => l1. have sKN: sub K Nat by move => t /sb/(NltP nN) => h; apply(NS_lt_nat h nN). by move: (nth_set9 (NS_lt_nat l1 ckN) sKN l1) => /sb/(NltP nN). pose Y z := X (nth_elt K z). pose c z := cc (nth_elt K z). pose r z := rr (nth_elt K z). have h2:= nds_tn4. have h3:(forall i, i <=c k -> \0o i /ikP/nds_tn6 [ra _ rb _]. have h4:(forall i, i <=c k -> c i i /ikP /nds_tn6 [_ rc _ _]. have lkn: k omega0 ^o ee *o c i +o r i) s = nds_sc (cardinal K) (fun z => X (nth_elt K z)) s. apply:(osum_expansion_exten ckN) => i /(NltP ckN) lin. move/(permutationsP): sp => [[[fs _] _] ss ts]. have: (Vf s i) /ikP /nds_tn6 [_ _ _ rd]. rewrite kv in sp. by rewrite kv (nds_p1 kN h2 h3 h4 sp); rewrite /c/r - kv. Qed. Lemma nds_tn9 v: inc v (nds_tn_S X n) <-> (v = \0o \/ exists K a, [/\ inc K (powerset n), inc a K & v = omega0 ^o ee *o osum_expansion (fun z => cc (nth_elt K z)) (cardinal K) +o rr a]). Proof. split. move/setUf_P => [K ka /funI_P [s sp sv]]. case:(emptyset_dichot K) => ke. by rewrite sv ke cardinal_set0/nds_sc osum_expansion0; left. right; exists K,(nth_elt K (Vf s \0c)). move/(permutationsP): (sp) => [[[fs _] _] ss ts]. have h:inc (nth_elt K (Vf s \0c)) K. move/setP_P: ka => ka. have sKN: sub K Nat by move => t /ka/(NltP nN) => h;apply(NS_lt_nat h nN). move:(sub_smaller ka); rewrite (card_nat nN) => ckn. have ckN:=(NS_le_nat ckn nN). have cknz:= (card_nonempty1 ke). have zi: inc \0c (cardinal K). apply /(NltP ckN); split; [ apply: czero_least; fprops | fprops]. have l1: (Vf s \0c) [/setC_P []]. by split => //; rewrite sv - (nds_tn8 ka sp ke). case => vv. apply/setUf_P; exists emptyset; first by apply: setP_0i. apply/funI_P; exists (identity (cardinal emptyset)). apply:permutation_id. by rewrite cardinal_set0 /nds_sc osum_expansion0. move:vv=> [K [a [Ks1 aK ->]]]; apply/setUf_P; exists K => //. have neK: nonempty K by ex_tac. move/setP_P: (Ks1) => ka. have sKN:= (sub_trans ka (NS_inc_nat nN)). move:(sub_smaller ka); rewrite (card_nat nN) => ckn. have cknz:= (card_nonempty1 neK). have ckN:=(NS_le_nat ckn nN). move:(cpred_pr ckN cknz); set k:= cpred _; move => [kN kv]. have fsk: finite_set K by apply/NatP. move:(nth_set_10 sKN fsk aK) => [i il1 iv]. move: (permutation_exists1 ckN il1) => [f fp fiv]. rewrite -fiv in iv. by apply/funI_P;ex_tac; rewrite (nds_tn8 Ks1 fp neK) - iv. Qed. Lemma nds_p3 a K:inc K (powerset n) -> inc a K -> omega0 ^o ee *o osum_expansion (fun z => cc (nth_elt K z)) (cardinal K) +o rr a = omega0 ^o ee *o csumb (K -s1 a) cc +o X a. Proof. move => pa pb. have h1:(forall i, i natp (cc i)). by move => i /nds_tn6 [_ /(oltP OS_omega) h _ _]. rewrite (nds_p2 nN h1 pa). move: (setC1_K pb); set K1:= K -s1 a => Kv. move/setP_P:pa => Kb. have ss1:= (@sub_setC K (singleton a)). have fsK:=(sub_finite_set Kb (finite_set_nat nN)). have h2:=(sub_finite_set ss1 fsK). have skN: natp (csumb K1 cc). apply:finite_sum_finite; hnf; rewrite/allf;bw;split => //. move => t tk1; bw; apply: h1;apply /(NltP nN); apply: (Kb _ (ss1 _ tk1)). have ak1:~ inc a K1 by move/setC1_P=> [ _ ]. move /(NltP nN): (Kb _ pb) =>/nds_tn6 [_ _ /proj31_1 o4 r2]. have ccaN: natp (cc a) by apply: h1; apply /(NltP nN);apply: Kb. rewrite -{1} Kv (csumA_setU1 _ ak1) - (osum2_2int skN ccaN). have o1:=(OS_pow OS_omega nds_tn4). move: (OS_nat ccaN) (OS_nat skN) => o2 o3. by rewrite (oprodD) // - (osumA (OS_prod2 o1 o3) (OS_prod2 o1 o2) o4) r2. Qed. Lemma nds_tn10: (nds_tn_S X n) = unionf n (fun a => fun_image (powerset (n -s1 a)) (fun K => omega0 ^o ee *o (csumb K cc) +o X a)) +s1 \0c. Proof. set_extens v. case /nds_tn9;[ move ->; fprops | move => [K [a [kp ak ->]]] ]. apply/setU1_P; left; apply /setUf_P. move/setP_P:(kp) => kb;move:(kb _ ak) => aN;ex_tac; apply /funI_P. exists (K -s1 a). by apply/setP_P => t/setC1_P [ha hb]; apply/setC1_P; split=> //; apply:kb. by rewrite nds_p3. case/setU1_P => h1; apply/nds_tn9; [right | by left]. move/setUf_P: h1 => [a aN /funI_P[K /setP_P Kb ->]]. have nk1: ~ (inc a K) by move /Kb => /setC1_P[]. have eq1:= setU1_K nk1. have ha: inc (K +s1 a) (powerset n). apply /setP_P => t/setU1_P; case; [by move/Kb => /setC1_P[] | by move ->]. have hb:inc a (K +s1 a) by fprops. by exists (K +s1 a),a; split => //; rewrite (nds_p3 ha hb) eq1. Qed. Lemma nds_tn11: (nds_tn_C X n) <=c ndstnC n. Proof. rewrite /nds_tn_C nds_tn10/ndstnC. set S := unionf _ _. suff h: cardinal S <=c (n *c \2c ^c cpred n). have w:cardinalp (n *c \2c ^c cpred n) by fprops. have w1:= (cleS0 w). case: (inc_or_not \0c S) => ha. by rewrite (setU1_eq ha); apply:cleT h w1. by rewrite (csucc_pr ha); apply /(cleSSP (CS_cardinal S) w). rewrite /S; set F:= (fun a : Set => _). move:(cpred_pr nN (nesym (proj2 np))) => [pnN pnv]. move:(csum_pr1_bis n F). set g1:= (Lg n (fun a => cardinal (Vg (Lg n F) a))). have <-: csum g1 = csumb n (fun a => cardinal (F a)). apply: csumb_exten => t tx; bw. set g2 := cst_graph n (\2c ^c cpred n). have sd: domain g1 = domain g2 by rewrite /g1/g2; bw. suff le1:forall x, inc x (domain g1) -> Vg g1 x <=c Vg g2 x. move:(csum_increasing sd le1). rewrite csum_of_same cprodC - cprod2cl (card_nat nN). move => hb ha ; exact:(cleT ha hb). rewrite /g1 /g2; bw => a abn; bw. have ->: \2c ^c cpred n = cardinal (powerset (n -s1 a)). move: (csucc_pr2 abn); rewrite (card_nat nN) => eq1. rewrite card_setP - (cpowcr _ ((n -s1 a))); apply: f_equal. apply:succ_injective1; fprops; ue. apply: fun_image_smaller. Qed. Lemma nds_tn11_ex: (forall i, X i = omega0 *o (\2c ^c i) +o i) -> (nds_tn_S X n) = unionf n (fun a => fun_image (powerset (n -s1 a)) (fun K => omega0 *o (csumb K (fun i => (\2c ^c i))) +o X a)) +s1 \0c. Proof. move => h. rewrite nds_tn10. have ha: forall i, natp i -> inc (\2c ^c i) Nat. move => i; apply:(NS_pow NS2). have hb: forall i, natp i -> \0c i ib; split;[ fprops |apply: nesym;apply: cpow2_nz]. have ->: ee = \1o. move:(proj31 (proj2 (the_CNF_omega_kj (ha _ NS0) NS0 (hb _ NS0)))). by rewrite - (h \0c). apply:f_equal2; last by exact. rewrite (opowx1 OS_omega). have aux: forall y, sub y Nat -> csumb y [eta cpow \2c] = csumb y cc. move => y yb; apply: csumb_exten => t /yb yN. move: (proj32 (proj2 (the_CNF_omega_kj (ha _ yN) yN (hb _ yN)))). by rewrite - (h t). have H2: forall y a, inc y (powerset (n -s1 a)) -> sub y Nat. by move => y a /setP_P hy t /hy /setC1_P [/(NS_inc_nat nN) ]. set F1 := fun a: Set => _; set F2 := fun a: Set => _. suff r1: forall a, inc a n -> F1 a = F2 a. set_extens t => /setUf_P [y ya yb]; apply/setUf_P; exists y; [exact |by rewrite - (r1 _ ya) | exact | by rewrite (r1 _ ya)]. move => a ab; set_extens t; move => /funI_P [y ya ->]; apply/funI_P. exists y; [exact | by rewrite (aux _ (H2 _ _ ya))]. exists y; [exact | by rewrite (aux _ (H2 _ _ ya))]. Qed. End NdsStudy1. Definition sumpow2 K := csumb K (fun z => \2c ^c z). Lemma omega_monom_inj a b c d: natp a -> natp b -> natp c -> natp d -> omega0 *o a +o b = omega0 *o c +o d -> (a = c /\ b = d). Proof. move => aN bN cN dN eq1. have aux: forall u v, natp u -> natp v ->inc (omega0 *o u +o v) Nat -> u = \0c. move => u v uN vN h; ex_middle h1. have h2:= (ozero_least (OS_nat uN)). have h3: \0o l2. by move/(oltP OS_omega): h => /(oleNgt l2). case: (equal_or_not a \0c) => az. move: eq1; rewrite az oprod0r (osum0l (OS_nat bN)) => eq1. rewrite eq1 in bN. by rewrite eq1 (aux _ _ cN dN bN) oprod0r (osum0l (OS_nat dN)). case: (equal_or_not c \0c) => cz. move: eq1; rewrite cz oprod0r (osum0l (OS_nat dN)) => eq1. case: az;rewrite - eq1 in dN; exact:(aux _ _ aN bN dN). have ap: \0c [_ [_ e1 e2]]. move:(the_CNF_omega_kj cN dN cp) => [_ [_ e3 e4]]. by rewrite eq1 in e1 e2; rewrite e1 in e3; rewrite e2 in e4. Qed. Lemma sumpow2_a K: finite_set K -> sub K Nat -> natp (sumpow2 K). Proof. move => ha hb; apply:finite_sum_finite; split; aw; bw. hnf; bw => x xk; bw; apply:(NS_pow NS2 (hb _ xk)). Qed. Lemma sumpow2_b n a K: natp n -> inc K (powerset (n -s1 a)) -> natp (sumpow2 K). Proof. move => nN /setP_P h1; move:(sub_trans h1 (@sub_setC _ _)) => h2. have h3:= (sub_trans h2 (NS_inc_nat nN)). exact (sumpow2_a (sub_finite_set h2 (finite_set_nat nN)) h3). Qed. Lemma sumpow2_c a K: ~ (inc a K) -> sumpow2 (K+s1 a) = sumpow2 K +c (\2c ^c a). Proof. by move => naK; rewrite /sumpow2 (csumA_setU1 _ naK). Qed. Lemma sumpow2_d a K: inc a K -> sumpow2 K = sumpow2 (K -s1 a) +c (\2c ^c a). Proof. by move => aK; rewrite -{1} (setC1_K aK) sumpow2_c // => /setC1_P []. Qed. Lemma sumpow2_e n a K (X := fun i => omega0 *o (\2c ^c i) +o i): natp n -> inc a n -> inc K (powerset (n -s1 a)) -> omega0 *o (sumpow2 K) +o X a = omega0 *o (sumpow2 (K +s1 a)) +o a /\ (natp (sumpow2 (K +s1 a))). Proof. move => nN ak KP. have aN := (NS_inc_nat nN ak). have haa:=(NS_pow NS2 aN). have naK: ~ inc a K by move/setP_P:KP => KP1; move /KP1 => /setC1_P [_]. move: (sumpow2_b nN KP) => sN. have o1:= (OS_nat sN). rewrite (sumpow2_c naK); split; last by fprops. rewrite {2} /sumpow2 - (osum2_2int sN haa). rewrite (oprodD o1 (OS_nat haa) OS_omega). exact:(osumA (OS_prod2 OS_omega o1) (OS_prod2 OS_omega (OS_nat haa)) (OS_nat aN)). Qed. Lemma sumpow2_f n K: natp n -> (forall i, inc i K -> i sumpow2 K nN;move:n nN K ; apply: Nat_induction. move => K h; rewrite cpowx0. case:(emptyset_dichot K). move => ->; rewrite /sumpow2/ csumb csum_trivial;bw;apply:clt_01. by move => [i /h /clt0]. move => n nN Hrec K kP. set K1:= K -s1 n. have /Hrec r1:(forall i, inc i K1 -> i i /setC1_P [/kP /(cltSleP nN) h1 h2]. rewrite (cpow_succ _ nN) cprodC two_times_n. case: (inc_or_not n K) => ink. rewrite (sumpow2_d ink); apply:csum_Mlteq; fprops. rewrite -(setC1_eq ink); apply: (clt_leT r1); apply:csum_M0le; fprops. Qed. Lemma sumpow2_g n a K1 K2 (X := fun i => omega0 *o (\2c ^c i) +o i): natp n -> inc a n -> inc K1 (powerset (n -s1 a)) -> inc K2 (powerset (n -s1 a)) -> omega0 *o (sumpow2 K1) +o X a = omega0 *o (sumpow2 K2) +o X a -> K1 = K2. Proof. move => nN ab K1b K2b. move: (sumpow2_e nN ab K1b) (sumpow2_e nN ab K2b) => [e1 e2][e3 e4]. rewrite e1 e3 => eq1. have aN := (NS_inc_nat nN ab). move: (proj1 (omega_monom_inj e2 aN e4 aN eq1)). move:(sumpow2_b nN K1b)(sumpow2_b nN K2b) => e5 e6. move/setP_P:K1b => K1b1. move/setP_P:K2b => K2b1. have naK1: ~(inc a K1) by move /K1b1 => /setC1_P [_]. have naK2: ~(inc a K2) by move /K2b1 => /setC1_P [_]. rewrite (sumpow2_c naK1) (sumpow2_c naK2) => eq2. move:(csum_eq2r (NS_pow NS2 aN) e5 e6 eq2). have: forall i, inc i K1 -> i i /K1b1 /setC1_P [/(NltP nN)]. have: forall i, inc i K2 -> i i /K2b1 /setC1_P [/(NltP nN)]. move:nN; clear; move => nN; move:n nN K1 K2; apply: Nat_induction. move => K1 K2 h1 h2 sv. case:(emptyset_dichot K1) => ha. case:(emptyset_dichot K2) => hb; first by rewrite ha hb. by move:hb => [i/h1 /clt0]. by move:ha => [i/h2 /clt0]. move => n nN Hrec K1 K2 h2 h1. have kk1:(forall i, inc i (K1 -s1 n) -> i i /setC1_P [/h1 /(cltSleP nN) hu hv]. have kk2:(forall i, inc i (K2 -s1 n) -> i i /setC1_P [/h2 /(cltSleP nN) hu hv]. have l1:(sumpow2 (K1 -s1 n)) nk1. case: (inc_or_not n K2) => nk2. have hh1:= (NS_lt_nat l1 (NS_pow NS2 nN)). have hh2:= (NS_lt_nat l2 (NS_pow NS2 nN)). rewrite (sumpow2_d nk1) (sumpow2_d nk2) => eq2. move:(csum_eq2r pN hh1 hh2 eq2) => eq3. by rewrite - (setC1_K nk1) - (setC1_K nk2) (Hrec _ _ kk2 kk1 eq3). move: l2; rewrite (sumpow2_d nk1) (setC1_eq nk2) => l2 eq. move: (csum_M0le (sumpow2 (K1 -s1 n)) (CS_nat pN)). by rewrite csumC eq => /(cltNge l2). case: (inc_or_not n K2) => nk2. move: l1; rewrite (setC1_eq nk1) (sumpow2_d nk2) => l1 eq. move: (csum_M0le (sumpow2 (K2 -s1 n)) (CS_nat pN)). by rewrite csumC - eq => /(cltNge l1). by rewrite - (setC1_eq nk1) - (setC1_eq nk2); apply: Hrec. Qed. Lemma nds_tn12 n: natp n -> \0c (nds_tn_sup n) <=c ndstnC n. Proof. move => nN np. move: (nds_tn2 nN) => [_ _ _ [X hx <-] _]; exact:(nds_tn11 nN np hx). Qed. Lemma nds_tn13 n: natp n -> nds_tn_sup n = ndstnC n. Proof. move => nN. case: (equal_or_not n \0c) => nz. by rewrite nz nds_tn3 /ndstnC cprodC cprod0r succ_zero. have np: \0c natp (\2c ^c i). move => i; apply:(NS_pow NS2). have hb: forall i, natp i -> \0c i ib; split;[ fprops |apply: nesym;apply: cpow2_nz]. have ax: nds_tn_ax X n. split. move => i lin; move:(NS_lt_nat lin nN) => yN. exact:(proj1 (the_CNF_omega_kj (ha _ yN) yN (hb _ yN))). exists \1o; first by apply:OS1. move => i lin; move:(NS_lt_nat lin nN) => yN. exact:(proj31 (proj2(the_CNF_omega_kj (ha _ yN) yN (hb _ yN)))). suff eq1: nds_tn_C X n = ndstnC n. by move: (nds_tn2 nN) => [_ _ _ _ h]; move: (h _ ax); rewrite - eq1. rewrite /nds_tn_C (nds_tn11_ex nN np ax Xv). rewrite csucc_pr; last first. move/setUf_P => [a aN /funI_P [K Ka kv]]. move/(NltP nN): aN => /(proj1 ax) => xP. have o1:=(OS_prod2 OS_omega (OS_nat (sumpow2_b nN Ka))). by move:(osum2_zero o1 (proj32_1 xP) (esym kv))=>[_ h]; case: (proj2 xP). rewrite /ndstnC; congr csucc;rewrite csum_pr4_bis; last first. move => i j iN jN; case (equal_or_not i j) => eij; [by left | right]. apply:disjoint_pr => u /funI_P [K1 K1p uv1] /funI_P [K2 K2p uv2]; case eij. move: (sumpow2_e nN iN K1p) (sumpow2_e nN jN K2p) => [e1 e2] [e3 e4]. move: uv2; rewrite uv1 e1 e3 => eq1. exact:proj2(omega_monom_inj e2 (NS_inc_nat nN iN) e4 (NS_inc_nat nN jN) eq1). set F := fun a:Set => _. suff H: forall a, inc a n -> F a = \2c ^c cpred n. rewrite - {2} (card_nat nN) (cprod2cl). by rewrite cprodC - csum_of_same; apply: csumb_exten => i ib /=; apply: H. move => a aN; rewrite /F; rewrite cardinal_fun_image. rewrite card_setP - cpowcr; apply:f_equal; symmetry. move: (cpred_pr nN (nesym (proj2 np))) => [sa sb]. move: (csucc_pr2 aN); rewrite (card_nat nN) {1} sb. apply:(succ_injective1 (CS_nat sa) (CS_cardinal _)). move => K1 K2;apply:(sumpow2_g nN aN). Qed. Definition nds_type_nor X n k e:= [/\ nds_type X n k, ordinalp e, forall i, i \0o the_CNF_degree (X i) = e & forall i, k <=c i -> i e k <> \0c -> k <=c n -> nds_type X n k -> exists Y e, nds_type_nor Y n k e /\ nds_card n Y = nds_card n X. Proof. move => nN knz lekn;case; first by move => [sa sb]; case: knz. move => [_ [ha [m [om h1]]]]. set E := Zo _ _ => ce. have ax:nds_ax X n by move => i /ha/proj32_1. have sk: sub k n by case: lekn. have kN:=(NS_le_nat lekn nN). have sE: sub E n by apply: Zo_S. move:(permutation_exists2 nN sE) => [f fp]; rewrite ce. move: (nds_m nN ax fp); set Y:= fun i =>X (Vf f i) => yv. move:fp => /Zo_P [/functionsP [ff sf tf] bf] fv. have sisf: sub k (source f) by rewrite sf. move: (cardinal_image sisf (proj1 bf));rewrite- fv (card_nat kN) => ck. have pa:forall i, i \0o i /(NltP nN) ii; apply: ha; apply/(NltP nN); Wtac. have pb: forall i, i m <=o the_CNF_degree (Y i). move => i /(NltP nN) ii; apply: h1;apply/(NltP nN); Wtac. have pc: forall i, i the_CNF_degree (Y i) = m. move => i /(NltP kN) ik. have/Zo_hi //: inc (Vf f i) E by rewrite fv; apply/(Vf_image_P ff sisf); ex_tac. have pd: (Zo n (fun i => the_CNF_degree (Y i) = m)) = k. set_extens t. move => /Zo_P [ta tb]. have: inc (Vf f t) E by apply/Zo_P; split => //; Wtac. rewrite fv => /(Vf_image_P ff sisf) [u usf]. move: ta (sk _ usf); rewrite - sf => hb hc hd. by rewrite(proj2(proj1 bf) _ _ hb hc hd). move => ta; apply /Zo_P;split; first by apply: sk. by apply: pc; apply /(NltP kN). have pf:forall i, k <=c i -> i m i ki kin; split; first by apply: pb. move => sa. have: inc i k. by rewrite - pd; apply /Zo_P; split => //; apply/(NltP nN). by move/(NltP kN) => /(cleNgt ki). have pe: nds_type Y n k. right; split; [exact| split;[ exact | exists m; split => //]]. by rewrite pd (card_nat kN). exists Y, m; rewrite - yv; split => //. Qed. Lemma nds_r1 c n X: natp n -> nds_ax X n -> ordinalp c -> osum_expansion (fun z : Set => c *o X z) n = c *o osum_expansion X n. Proof. move:n; apply: Nat_induction. by rewrite !osum_expansion0 (oprod0r). move => n nN Hrec axn oc. have nn:= (cltS nN). have ax1: nds_ax X n by move =>i lin; apply:axn; apply:(clt_ltT lin nn). rewrite !(osum_expansion_succ _ nN) (Hrec ax1 oc). by rewrite (oprodD (axn _ nn) (OS_osum_expansion nN ax1) oc). Qed. Lemma nds_r2 c n X (Y:= fun i => c *o X i): natp n -> nds_ax X n -> \0o nds_card n X = nds_card n Y. Proof. move => nN ax cp. rewrite /nds_card /nds_sums. set E := perm_int n; set A := fun_image _ _;set B := fun_image _ _. apply /card_eqP; exists (Lf (fun z => c *o z) A B). have osA: ordinal_set A. by move => z /funI_P [f /(nds_b nN ax) [_ os] ->]. have aux: forall f, inc f E -> nds_sc n Y f = c *o nds_sc n X f. move => f /(nds_b nN ax) [ax1 _ ]. apply:(nds_r1 nN ax1 (proj32_1 cp)). split; aw. apply: lf_bijective. + by move => z /funI_P [f fp ->]; apply /funI_P; exists f => //; rewrite aux. + move => u v /osA ou /osA ov h; exact (oprod2_simpl ou ov cp h). + move => z /funI_P [f fp ->]; exists(nds_sc n X f). apply /funI_P; exists f => //. by apply: aux. Qed. Lemma nds_card_exten m Y1 Y2: natp m -> same_below Y1 Y2 m -> nds_card m Y1 = nds_card m Y2. Proof. move => ha hb. rewrite /nds_card; apply:f_equal; set_extens t; move => /funI_P [z zp ->];apply/funI_P; ex_tac. by apply:nds_sc_exten. by symmetry;apply:nds_sc_exten. Qed. Lemma nds_tn_C_exten Z Y n: natp n -> same_below Z Y n -> nds_tn_C Z n = nds_tn_C Y n. Proof. move => nN h. have aux: forall K s, inc K (powerset n) -> inc s (perm_int (cardinal K)) -> nds_sc (cardinal K) (fun z : Set => Z (nth_elt K z)) s = nds_sc (cardinal K) (fun z : Set => Y (nth_elt K z)) s. move => K s /setP_P Kb /permutationsP [[[fs _] _ ] ss tf]. have fsK:=(sub_finite_set Kb (finite_set_nat nN)). have ckN: natp (cardinal K) by apply /NatP. have sKN:=(sub_trans Kb (NS_inc_nat nN)). apply:(osum_expansion_exten ckN) => i lin; apply: h. have h1: Vf s i /setUf_P [K KP /funI_P [s sp ->]]; apply /setUf_P; ex_tac;apply/funI_P; ex_tac. symmetry;exact:(aux K s KP sp). Qed. Section NdsStudy. Variables (X: fterm) (n k e: Set). Hypothesis nN: natp n. Hypothesis knz: k <> \0c. Hypothesis kln: k Vf f j = Vf g j]. Let fL f := intersection (Zo Nat (fun i => i pS f i -> False. Proof. by rewrite /pL/pS => ha /(cleNgt ha). Qed. Lemma nds_tg1 f i: inc f (perm_int n) -> inc i n -> inc (Vf f i) n. Proof. move => /permutationsP [[[ff _] _] sf tf]; rewrite -{1} sf -tf => isf; Wtac. Qed. Lemma nds_tg2 f i: inc f (perm_int n) -> inc i n -> pL f i \/ pS f i. Proof. move => fp /(nds_tg1 fp) /(NltP nN) [[cf _ _] _]. exact:(cleT_el (proj31_1 kln) cf). Qed. Lemma nds_tg3 f: inc f (perm_int n) -> [/\ inc (fL f) Nat, (fL f) <=c k, (fL f) pS f j]. Proof. move => fp; rewrite /fL; set E:= Zo _ _. move/permutationsP:(fp) =>[[injf [ff fs]] sf tf]. have nee: nonempty E. move:(perm_int_surj nN fp kln) => [i lin si]. exists i;apply:Zo_i;[ by apply: (NS_lt_nat lin nN) | split => //]. rewrite /pL si; apply: (cleR (proj31_1 kln)). have seN: sub E Nat by apply:Zo_S. move: (inf_Nat seN nee); set i:= intersection E. move => [/Zo_P [iN [ha hb]] etc]. have kN:= (NS_lt_nat kln nN). have aux: forall j, j pS f j. move => // j lji. move: (clt_ltT lji ha) => ljn; move/(NltP nN): (ljn) => jb. case:(nds_tg2 fp jb) => // sa. have: inc j E by apply:Zo_i => //;apply: (NS_lt_nat ljn nN). by move/etc => /(cltNge lji). split => //. case: (NleT_el iN kN) => // lki. have aux2: forall i, i <=c k -> pS f i. by move =>j jk; apply: aux; exact (cle_ltT jk lki). rewrite /pS in aux2. have h3: sub (Nintc k) (source f). move => j/(NintcP kN) ja; rewrite sf; apply/(NltP nN);exact (cle_ltT ja kln). have su1: sub (Vfs f (Nintc k)) k. move => t /(Vf_image_P ff h3) [u /(NintcP kN) ul1 ->]. by apply/(NltP kN); apply: aux2. move: (sub_smaller su1). rewrite(cardinal_image h3 injf) (card_Nintc kN) (card_nat kN) => l1. case: (cleNgt l1 (cltS kN)). Qed. Lemma nds_tg4 f i (q:= (fL f) +c i) : inc f (perm_int n) -> natp i -> (fL f) +c i (forall j, j pL f ((fL f) +c j)) -> [\/ (i = n -c k /\ forall j, j q <=c j -> pS f j), pL f q | q <> \0c /\ exists j, [/\ natp j, csucc (q +c j) pS f (q +c z) ]]. Proof. move => fp iN inb Hi. move: (nds_tg3 fp) => [sa _ sb sc sd]. move/permutationsP: fp => [bf sf tf]. have ff: function f by fct_tac. have qN: natp q by apply: NS_sum. have kN:= (NS_lt_nat kln nN). set E1 := Zo Nat (fun z => [/\ z [/\ z u /Zo_P[_ [_ _ ha]]/Zo_P[_ [_ _ /(cleNgt ha)]]. move/csum2_pr5;rewrite - csum2cl - csum2cr => eq1. have e2v: E2 = fun_image i (fun z => (fL f) +c z). set_extens t. move/Zo_P => [tN [tn h tq]]; apply/funI_P. case: (cleT_el (proj31_1 sb)(proj31_1 tq)) => le1. move:tq; rewrite - (cdiff_pr le1) => tq. move /(NltP iN):(csum_lt2l sa (NS_diff (fL f) tN) iN tq). move => di; ex_tac. by move: h (sd _ le1);rewrite /pL /pS => ua /(cleNgt ua). move /funI_P => [z /(NltP iN) zi ->]; apply/Zo_P. move: (clt_ltT (csum_Meqlt sa zi) inb) => lt1. move: (csum_Meqlt sa zi) => sf1. split; [ exact:(NS_lt_nat lt1 nN) | by split => //; apply: Hi ]. have e3v: E1 \cup E2 = fun_image E3 (Vf (inverse_fun f)). set_extens t => h. have[ha hb]: t /Zo_P[_ [ha hb _]]. have tsf: inc t (source f) by rewrite sf; apply /(NltP nN). have se:=(inverse_V2 bf tsf). apply/funI_P; exists (Vf f t); last by exact. apply /setC_P; split; [ Wtac | by move/(NltP kN) => /(cleNgt hb)]. move/funI_P:h => [z /setC_P [ha hb] ->]. have ft: inc z (target f) by ue. have eq2:=(inverse_V bf ft). have zt:= (inverse_Vis bf ft). rewrite sf in zt; move /(NltP nN): zt => lt1. have izN:= (NS_lt_nat lt1 nN). have zN: inc z Nat by move/(NltP nN):ha => hd; apply: (NS_lt_nat hd nN). case: (NleT_el kN zN) => zz; last by case: hb; apply /(NltP kN). by case: (NleT_el qN izN) => lea; apply /setU2_P; [left | right]; apply:Zo_i => //; split => //; rewrite /pL eq2. have sjb: (bijection (Lf (csum2 (fL f)) i E2)). apply: lf_bijective. + by rewrite e2v;move=> t ta; apply /funI_P; ex_tac. + move => u v /(NltP iN) uI /(NltP iN) vI eq. exact:(csum_eq2l sa (NS_lt_nat uI iN) (NS_lt_nat vI iN) eq). + by rewrite e2v; move=> y /funI_P. have sjc: (bijection (Lf(Vf (inverse_fun f)) E3 (E1 \cup E2))). apply: lf_bijective. + by rewrite e3v;move=> t ta; apply /funI_P; ex_tac. + move => u v /setC_P [uI _] /setC_P[vI _] eq. rewrite - tf in uI vI. by rewrite - (inverse_V bf uI) - (inverse_V bf vI) eq. + by rewrite e3v; move=> y /funI_P. move: eq1. have ->: cardinal E2 = i. rewrite - (card_nat iN); symmetry;apply/card_eqP. exists (Lf (csum2 (fL f)) i E2); split => //; aw. have fn := (finite_set_nat nN). have <-:n -c k = cardinal (E1 \cup E2). rewrite - (card_nat nN) - (card_nat kN). rewrite - (cardinal_setC4 (proj33 (proj1 kln)) fn). apply/card_eqP;exists (Lf (Vf (inverse_fun f)) E3 (E1 \cup E2)). split => //; aw. move => cc. clear e2v e3v sjb sjc E2 E3. have cE1N: natp (cardinal E1). have sw: sub E1 n by move => t /Zo_P [_ [/(NltP nN)]]. by move: (sub_finite_set sw fn) => /NatP. have ci:= (CS_nat iN). case: (cleT_ell (CS_diff n k) ci) => cink. + constructor 1; split; first by symmetry. move => j ljn lqj. have jsf: inc j (source f) by rewrite sf; apply /(NltP nN). move:(Vf_target ff jsf); rewrite tf; move/(NltP nN) => ha. case: (cleT_el (proj31_1 kln) (proj31_1 ha)) => hb; last exact. rewrite cink - {1} (csum0l ci) in cc. move:(esym(csum_eq2r iN NS0 cE1N cc))=>/card_nonempty hw. have jE1: inc j E1 by apply:Zo_i; [apply: (NS_lt_nat ljn nN) | ]. empty_tac1 j. + by move: (csum_M0le (cardinal E1) ci);rewrite csumC - cc=> /(cltNge cink). + have qsf: inc q (source f) by rewrite sf;apply/(NltP nN). move:(Vf_target ff qsf); rewrite tf => /(NltP nN) lt1. case: (cleT_el (CS_nat kN) (proj31_1 lt1)) => lt2. by constructor 2. constructor 3. case: (equal_or_not i \0c) => inz. by move:sc lt2; rewrite /pL /q inz (csum0r (proj31_1 sb))=> ua /(cleNgt ua). case: (emptyset_dichot E1) => nee. by move: (proj2 cink); rewrite cc nee cardinal_set0 (csum0l ci). have seB: sub E1 Nat by apply:Zo_S. move: (inf_Nat seB nee) =>[]; set j:= intersection E1 => ja jb. move/Zo_P: ja => [jN [ljn jc lqj]]. have eq0:= (cdiff_pr lqj). case: (equal_or_not (j -c q) \0c) => eq1. by move: jc; rewrite - eq0 eq1 (csum0r (proj31 lqj)) /pL => /(cltNge lt2). move: (cpred_pr (NS_diff _ jN) eq1)=> []. set m := (cpred (j -c q)) => mN mv. have eq4:q +c csucc m = j by rewrite - mv. have eq2: csucc (q +c m) = j by rewrite - (csum_nS _ mN). move: (cpred_pr iN inz) => [ia ib]. have eq3: q = csucc (fL f +c (cpred i)) by rewrite -(csum_nS _ ia) - ib. split; first by rewrite eq3; apply: succ_nz. move: (cpred_pr1 (CS_sum2 (fL f) (cpred i))); rewrite - eq3 => eq5. move: (cltS ia); rewrite - ib => /Hi; rewrite - eq5 => eq6. exists m; rewrite eq2; split => //. move => z /(cltSleP mN) zm. move:(csum_Meqlt qN zm); rewrite eq4 => l1. move: (clt_ltT l1 ljn) => ra. move: (NS_lt_nat ra nN) => qzN. move/(NltP nN):(ra); rewrite - sf => /(Vf_target ff); rewrite tf. move /(NltP nN) => /proj31_1 fzn. case: (cleT_el (CS_nat kN) fzn) => // l2. have: (inc (q +c z) E1). apply:Zo_i => //; split => //; apply:(csum_M0le _ (CS_nat qN)). by move/jb => /(cltNge l1). Qed. Lemma nds_tg5 i l f: inc f (perm_int n) -> natp i -> natp l -> (csucc (csucc (i +c l))) pL f i -> (forall j, j <=c l -> pS f (csucc (i+c j))) -> pL f (csucc (csucc (i +c l))) -> exists g, rp f g (csucc i) /\ pL g (csucc i). Proof. move => fp iN lN ltil2n p1 p2 p3. set i1:= csucc i; set il2:= csucc (csucc (i +c l)); set il3:= csucc il2. set il:= csucc (i +c l). rewrite -/il2 in ltil2n. have il1N:= NS_succ (NS_sum iN lN). have il2N:= (NS_lt_nat ltil2n nN). have il3N: inc il3 Nat by apply:NS_succ il2N. have i1N:= NS_succ iN. have i2N:= NS_succ i1N. have leil3n: il3 <=c n by apply/cleSltP. have lti1il2: i1 [gp gssi gsi ngsi ggi]. move/permutationsP: (gp) => [[[fg _] _] sg tg]. move/permutationsP: (fp) => [[[ff _] _] sf tf]. set h:= f \co g. have fgP: f \coP g by split => //; ue. exists h; split; last by rewrite /h /pL; aw; [ rewrite gsi | rewrite sg]. have pa: forall j, j Vf f j = Vf h j. move => j jsi. have jb: inc j n by apply /(NltP nN); exact : (clt_ltT jsi lti1n). have jb': inc j (source g) by ue. have ne1:= (proj2(clt_ltT jsi (lti1il2))). by rewrite /h; aw; rewrite ngsi //; exact (proj2 jsi). have pb: forall j, inc j n -> il3 <=c j -> Vf f j = Vf h j. move => j jsi l3. have jb': inc j (source g) by ue. have lt1:= (clt_leT (cltS il2N) l3). have ne2:= (nesym (proj2 (clt_ltT lti1il2 lt1))). have ne1:= nesym(proj2 lt1). by rewrite /h; aw;rewrite ngsi. have hp:= (permutation_Sc fp gp). split; [ exact | | exact]. move: Xax => [_ _ hw hu hv]. have ax: nds_ax X n by move => z /hw /(proj32_1). move: (nds_b nN ax fp) (nds_b nN ax hp). rewrite /nds_sc. set Y:= (fun z => X (Vf f z)). set Z:= (fun z => X (Vf h z)); move => [aY _ ] [aZ _]. move: (cdiff_pr leil3n); set m := _ -c _ => mv. have mN: inc m Nat by apply: (NS_diff _ nN). rewrite - mv in aY aZ |- *. rewrite (osum_expansionA il3N mN aY) (osum_expansionA il3N mN aZ). apply: f_equal2. apply: (osum_expansion_exten mN) => z zm. have le2:il3 <=c z +c il3 by rewrite csumC; apply: csum_M0le; fprops. have le3: inc (z +c il3) n. by apply/(NltP nN); rewrite - mv (csumC il3); apply:csum_Mlteq. by rewrite /Y/Z pb. set a := X (Vf f i); set b := X(Vf f i1); set c:= X(Vf f il2). have il2sg: inc il2 (source g) by ue. have i1sg: inc i1 (source g) by ue. have ib: inc i n by apply /(NltP nN). have ig: inc i (source g) by ue. rewrite 2! (osum_expansion_succ _ il2N). rewrite {1} /Z {1}/Y /h (compf_V fgP il2sg) gssi -/b -/c. have le2: csucc (csucc i) <=c il2. apply/(cleSSP (CS_succ i) (CS_succ ((i +c l)))). apply/(cleSSP (CS_nat iN) (CS_sum2 i l)). apply: (csum_M0le _ (CS_nat iN)). move: (cdiff_pr le2); set m1 := _ -c _ => m1v. have m1N: inc m1 Nat by apply: (NS_diff _ il2N). rewrite mv in aY aZ. have aY': nds_ax Y (csucc (csucc i) +c m1). move => z; rewrite m1v => l1; apply: aY; exact:(clt_ltT l1 ltil2n). have aZ': nds_ax Z (csucc (csucc i) +c m1). move => z; rewrite m1v => l1; apply: aZ; exact:(clt_ltT l1 ltil2n). have ha:= cltS iN. have hb:= (proj2 (clt_ltT ha lti1il2)). rewrite - m1v (osum_expansionA i2N m1N aY') (osum_expansionA i2N m1N aZ'). rewrite 2! (osum_expansion_succ _ i1N) 2! (osum_expansion_succ _ iN). rewrite {2 3} /Y {2 3} /Z /h (compf_V fgP ig)(compf_V fgP i1sg). rewrite gsi (ngsi _ ib hb (proj2 ha)) -/a -/b -/c. set A:= osum_expansion _ m1. set B:= osum_expansion _ i. have <-: A = (osum_expansion (fun z : Set => Z (z +c csucc (csucc i))) m1). apply: (osum_expansion_exten m1N) => j lej. have [_ /nesym ltb]:i1 j lej; rewrite /Y/Z pa //. exact: (clt_ltT lej ha). have oA: ordinalp A. apply: (OS_osum_expansion m1N) => j jl1; apply: aY'. rewrite (csumC _ m1); exact:(csum_Mlteq i2N jl1). have oB: ordinalp B. apply: (OS_osum_expansion iN) => j jl1; apply: aY; exact (clt_ltT jl1 ltin). have fis: Vf f i db. have d1a: the_CNF_degree b ap cp bp. move: (proj32_1 ap)(proj32_1 bp)(proj32_1 cp) => oa ob oc. have hc: l +c (csucc (csucc i)) = il2. by rewrite csumC (csum_Sn _ i1N) (csum_Sn _ iN). have [eq1 eq2]: (A +o a = a /\ A +o c = c). have: m1 <=c l. apply:(csum_le2l i2N m1N lN). rewrite m1v (csumC _ l) hc; apply:cleR; fprops. rewrite /A; move:m1N; move:(m1); apply: Nat_induction. by move => _; rewrite osum_expansion0 (osum0l oa) (osum0l oc). move => q qN Hrec sql. have ql:= (cleT (cleS qN) sql). move:(Hrec ql) => [eqa eqb]. set d := (Y (q +c csucc (csucc i))). have oD: ordinalp (osum_expansion (fun z => Y (z +c csucc (csucc i))) q). apply: (OS_osum_expansion qN) => j jlt; apply:aY. have jlt1:=(clt_leT jlt ql). move:(csum_Mlteq i2N jlt1); rewrite hc => hd;apply:(clt_ltT hd ltil2n). have ql': q hd; exact(clt_ltT hd ltil2n). have lt3: Vf f (q +c csucc (csucc i)) dd. have dp: \0o exists g, [/\ inc g (perm_int n), nds_sc n X f = nds_sc n X g, fL f = fL g & forall i, i pL g ((fL g) +c i) ]. Proof. move => fp. move: (NS_diff k nN) (cleR (CS_diff n k)). move:{1 2 4} (n -c k); apply: Nat_induction. by move => _; exists f; split => // i /clt0. move => q qN Hrec le1. move:(cleS qN) => le2. move: (Hrec (cleT le2 le1)) => [g [ga gb gc gd]]. move: (nds_tg3 ga) => [aa ab ac ad ae]. have kN:= (NS_lt_nat kln nN). move: (csum_Meqlt kN (clt_leT (cltS qN) le1)). rewrite (cdiff_pr (proj1 kln))=> lt2. move: (cle_ltT (csum_Mleeq q ab) lt2) => lt3. case:(nds_tg4 ga qN lt3 gd). + by move => [ua _]; move: le1 (cltS qN); rewrite - ua => sa /(cleNgt sa). + move => h; exists g; split; [ exact | exact| exact | ]. move => j; move/(cltSleP qN) => ljq. case: (equal_or_not j q) => ejq; [ ue | by apply: gd]. set q1:= fL g +c q. move => [q1p [ j [jN ja jb jc jd]]]. move: (cpred_pr (NS_sum aa qN) q1p); rewrite -/q1; move=> [je ef]. have eg:=(csum_Sn j je). have sa: csucc (csucc (cpred q1 +c j)) pS g (csucc (cpred q1 +c j0))). by move => j1 jl1; rewrite -(csum_Sn _ je) - ef; apply: jd. move:(nds_tg5 ga je jN sa jc sb sc). move => [g1 [[r1 r2 r3] r4]]. rewrite -ef in r3 r4. have sw: fL g = fL g1. move: (nds_tg3 r1) => [aa' _ _ ad' ae']. have af: fL g <=c q1 by apply /csum_M0le; fprops. have q1N: natp q1 by move:(NS_succ je); rewrite - ef. case: (NleT_el aa' q1N) => ag; last first. by move:(ae' _ ag) r4; rewrite /pS/pL => l1 /(cltNge l1). case:(NleT_ell aa aa') => l3. + exact. + move: (ae' _ l3) ad; rewrite /pL/pS (r3 _ (clt_leT l3 ag)). move => l1 l2; case: (cltNge l1 l2). + move: (ae _ l3) ad'; rewrite /pL/pS (r3 _ (clt_leT l3 af)). move => l1 l2;case: (cltNge l1 l2). exists g1;split; [exact | ue| by rewrite gc | ]. move => i /(cltSleP qN) isa; rewrite - sw. case:(equal_or_not i q) => eqi; first by rewrite eqi. move: (csum_Meqlt aa (conj isa eqi));rewrite /pL => /r3 <-. apply: (gd _ (conj isa eqi)). Qed. Lemma nds_tg7 f: inc f (perm_int n) -> exists K s1 s2, [/\ sub K k, inc s1 (perm_int (cardinal K)), inc s2 (perm_int (n -c k)) & nds_sc n X f = nds_sc (n-c k) (fun z => X (k +c z)) s2 +o nds_sc (cardinal K) (fun z => X (nth_elt K z)) s1]. Proof. move/nds_tg6 => [g [gp -> _ p1]]. move:(nds_tg3 gp) => [qN p2 p3 p4 p5]. move/permutationsP:gp =>[[injg [fg sjg]] sg tg]. rewrite sg tg in sjg. set q := (fL g); rewrite -/q in qN p1 p2 p3 p4 p5. have nkN:=(NS_diff k nN). have le3 := (cdiff_pr3 nN p2 (proj1 kln)). have eq2:=(cdiff_pr (proj1 p3)). have eq3:=(cdiff_pr le3). have eq4:=(cdiff_pr (proj1 kln)). have nqN:= (NS_diff q nN). have qnkN:= (NS_sum qN nkN). have kN:= (NS_lt_nat kln nN). have lt1: q +c (n -c k) <=c n. move: (csum_Mleeq n p2); rewrite - {1} eq4 (csumC k) csumA (csumC _ k). by move/(csum_le2l kN qnkN nN). have sK: sub q (source g) by rewrite sg; exact (proj33 (proj1 p3)). move: (cardinal_image sK injg);set K := Vfs g q. rewrite (card_nat qN) => cK. have iKP: forall i, inc i K <-> exists2 j, inc j q & i = Vf g j. move => i; split; by move /(Vf_image_P fg sK). have h0:sub K k. by move => t /iKP [j jE ->]; apply/(NltP kN); apply: p5; apply/(NltP qN). set E1:= (q +c (n -c k)) -s q. set K1 := Vfs g E1. have sK1: sub E1 (source g). move => t /setC_P [/(NltP qnkN) ha _]; rewrite sg; apply/(NltP nN). exact: (clt_leT ha lt1). have iK1P: forall i, inc i K1 <-> exists2 j, inc j E1 & i = Vf g j. move => i; split; by move /(Vf_image_P fg sK1). have cK1: cardinal K1 = n -c k. move: (cardinal_image sK1 injg); rewrite -/K1. have ha:=(proj33 (csum_M0le (n-c k) (CS_nat qN))). rewrite (cardinal_setC4 ha (finite_set_nat qnkN)). by rewrite (card_nat qnkN) (card_nat qN) csumC (cdiff_pr1 nkN qN). have sK1': sub K1 (n -s k). move => t/iK1P [j ja ->]; apply/setC_P; split. by move: (Vf_target fg (sK1 _ ja)); rewrite tg. have jN: natp j by move:(sK1 j ja); rewrite sg => /(NS_inc_nat nN). move/setC_P:ja => [/(NltP qnkN) ja jb]; dneg h. case: (cleT_el (CS_nat qN) (proj31_1 ja)); last by move/(NltP qN). move => le1; move:(cdiff_pr le1) => eqa. rewrite - eqa in ja. move:(csum_lt2l qN (NS_diff q jN) nkN ja) => jc. move: (p1 _ jc); rewrite eqa /pL => jd. by move/(NltP kN):h => /(cleNgt jd). case: (equal_or_not K1 (n -s k))=> eq5; last first. move: (proj33 (proj1 kln)) (finite_set_nat nN) => s1 fn. move: (sub_finite_set (@sub_setC n k) fn) => ha. move:(proj2 (strict_sub_smaller (conj sK1' eq5) ha)). by rewrite (cardinal_setC4 s1 fn) (card_nat kN) (card_nat nN) cK1. have p6: forall i, i q +c (n -c k) <=c i -> pS g i. move => i li1 li2; rewrite /pS; ex_middle h. have isn: inc i (source g) by rewrite sg; apply/(NltP nN). have: inc (Vf g i) K1. rewrite eq5; apply/setC_P; split; [Wtac | by move/(NltP kN)]. move/(iK1P) => [j /setC_P [/(NltP qnkN) ja jb] eqa]. have jsg: inc j (source g). by move: (clt_ltT (clt_leT ja li2) li1) => /(NltP nN); rewrite sg. move: ((proj2 injg) i j isn jsg eqa) => eij; rewrite - eij in ja. case: (cltNge ja li2). have sKb: sub K n by move => t /iKP [ u /sK usf ->]; Wtac. have sKN:=(sub_trans sKb (NS_inc_nat nN)). have fsK:=(sub_finite_set sKb (finite_set_nat nN)). move:(nth_set_fct_bf sKN fsK). set FK:= (nth_set_fct K); move => [pa pb]. have sFK: source FK = q by rewrite /FK/nth_set_fct cK; aw. have tFK: target FK = K by rewrite /FK/nth_set_fct; aw. have ax2: lf_axiom (nth_elt K) q K. move => t /(NltP qN) lt2; move:(lt2); rewrite - cK => lt3. by move:(nth_set7 (NS_lt_nat lt2 qN) sKN lt3) => [/setC_P []]. pose s1' i := (Vf (inverse_fun FK) (Vf g i)). have ax1: lf_axiom s1' q q. move => t ta;rewrite - sFK; apply:(inverse_Vis pa); rewrite tFK. by apply /iKP; exists t. have pc: forall i, inc i q -> Vf FK (s1' i) = Vf g i. move => i iE; rewrite /s1' (inverse_V pa) // tFK; apply/iKP; ex_tac. set s1 := Lf s1' q q . have s1fb: bijection s1. apply:lf_bijective; first by exact. move => u v uE vE eq6. move: (f_equal (Vf FK) eq6); rewrite (pc _ uE) (pc _ vE) => eq7. exact: (proj2 injg _ _ (sK _ uE) (sK _ vE) eq7). rewrite - sFK;move => y ye. move: (Vf_target (proj1(proj1 pa)) ye); rewrite tFK => /iKP [u us eq1]. by rewrite - sFK in us; ex_tac; rewrite /s1'- eq1 (inverse_V2 pa ye). have s1perm: inc s1 (perm_int q). apply/permutationsP; rewrite /s1; split; aw. set Ec:= (n -c k). pose s2' z := (Vf g (q +c z) -c k). have pd1: forall z, z inc (q +c z) (source g). move => z zi. move:(csum_Meqlt qN (clt_leT zi le3)). by rewrite eq2 => /(NltP nN);rewrite - sg => ha. have ax3: lf_axiom s2' Ec Ec. move => z /(NltP nkN) zi. move: (Vf_target fg (pd1 _ zi)); rewrite tg => /(NltP nN) lt2. rewrite -/q - cK in lt2. move:(p1 _ zi);rewrite /pL /s2' - cK=> fzi. apply/(NltP nkN); exact(cdiff_pr7 fzi lt2 nN). have pd: forall z, z (s2' z) +c k = Vf g (q +c z). move => z /p1;rewrite /pL /s2' - cK=> fzi. by rewrite csumC; apply:cdiff_pr. set s2 := Lf s2' Ec Ec. have s2fb: bijection s2. apply:bijective_if_same_finite_c_inj. + rewrite /s2; aw. + by rewrite /s2/Ec; aw; apply:finite_set_nat. + apply: lf_injective => // u v /(NltP nkN) ue /(NltP nkN) ve eq. move: (f_equal (fun z => z +c k) eq). rewrite (pd _ ue) (pd _ ve) => eq7. move:(proj2 injg _ _ (pd1 _ ue)(pd1 _ ve) eq7). exact:(csum_eq2l qN (NS_lt_nat ue nkN) (NS_lt_nat ve nkN)). have s2perm: inc s2 (perm_int (n -c k)). apply/permutationsP; rewrite /s2; split; aw. exists K, s1, s2; rewrite cK;split => //. set X1:=osum_expansion (fun z => X (nth_elt K (Vf s1 z))) q. have r1: X1 = osum_expansion (fun z => X (Vf g z)) q. apply: (osum_expansion_exten qN) => i /(NltP qN) iE. have vK: inc (Vf g i) (target FK) by rewrite tFK;apply/iKP; ex_tac. rewrite /s1/s1'; aw; rewrite -{2} (inverse_V pa vK) {2} /FK/nth_set_fct cK. aw; rewrite - sFK; apply: (inverse_Vis pa vK). set X2:= osum_expansion (fun z=> X (Vf g (z +c q))) (n -c k). have r2: X2 = osum_expansion (fun z => X (k +c Vf s2 z)) (n -c k). apply:(osum_expansion_exten nkN). move => z znk /=;rewrite (csumC z) (csumC k) - (pd _ znk) /s2; aw. by apply/(NltP nkN). move: Xax => [_ oe hw hu hv]. have aX: nds_ax (fun z => X (Vf g z)) n. move => z /(NltP nN) zi. rewrite - sg in zi. by move:(Vf_target fg zi); rewrite tg => /(NltP nN) /hw /proj32_1. have aX2: ord_below_n (fun z=> X (Vf g (z +c q))) (n -c q). move=> z zle1; apply: aX; move: (csum_Mlteq qN zle1). by rewrite (csumC (_ -c _)) eq2. rewrite /nds_sc - {1} eq2;rewrite - eq2 in aX. rewrite - eq3 in aX2. rewrite (osum_expansionA qN nqN aX) -/X1 - r1 - eq3. rewrite (osum_expansionA nkN (NS_diff (n -c k) nqN) aX2) - r2;congr (_ +o X1). have knz1:= (cdiff_nz kln). move: (cpred_pr nkN knz1) => [nk1N nk1v]. rewrite /X2 nk1v (osum_expansion_succ _ nk1N). set X3:= osum_expansion _ _. set X4:= osum_expansion _ _. set a := X _. move:(cltS nk1N); rewrite -nk1v => /p1; rewrite /pL csumC => le1. have lt2: inc ((cpred (n -c k) +c q)) (source g). rewrite csumC;apply/pd1; rewrite {2} nk1v; apply:(cltS nk1N). have lt3: Vf g (cpred (n -c k) +c q) ap da. have oa:= proj32_1 ap. have oX4: ordinalp X4. apply:(OS_osum_expansion nk1N) => t ta;apply: aX2. move: (clt_leT ta (cleS nk1N)); rewrite - nk1v => sa. exact: (clt_leT sa (csum_M0le ((n -c q) -c (n -c k)) (CS_nat nkN))). set wa:=((n -c q) -c csucc (cpred (n -c k))). have wN: natp wa by rewrite /wa; fprops. have wa1: (wa +c (n -c k)) = (n -c q). by rewrite /wa -nk1v (csumC (_ -c _)) cdiff_pr. have oX3: ordinalp X3. apply:(OS_osum_expansion wN) => z zw;apply: aX2;rewrite eq3. by move: (csum_Mlteq nkN zw); rewrite -nk1v wa1. rewrite (osumA oX3 oa oX4); congr (_ +o X4). rewrite /X3 -/wa - nk1v. have eq7: ((wa +c (n -c k)) +c q) = n by rewrite wa1 csumC eq2//. have: wa +c ((n -c k) +c q) <=c n by rewrite csumA eq7; fprops. clear eq7 wa1. move: wa wN; apply: Nat_induction. by move => _ ; rewrite osum_expansion0 (osum0l oa). move=> j jN Hrec. have sN:= NS_sum jN (NS_sum nkN qN). rewrite (csum_Sn _ jN) => /(cleSltP sN) ha. have oS: ordinalp (osum_expansion (fun z => X (Vf g ((z +c (n -c k)) +c q))) j). apply:(OS_osum_expansion jN) => z zl; apply:aX2;rewrite eq3. move:(csum_Mlteq nkN zl) => hc. move:(csum_M0le (j +c (n -c k)) (CS_nat qN)); rewrite csumC => hd. rewrite csumA in ha; move: (cdiff_pr7 hd ha nN). rewrite (cdiff_pr1 (NS_sum jN nkN) qN) => he; exact: (clt_ltT hc he). rewrite (osum_expansion_succ _ jN) - csumA. set j0 := j +c ((n -c k) +c q). have j0b: inc j0 (source g) by rewrite sg; apply/(NltP nN). rewrite -/j0 in ha. have hb:q +c (n -c k) <=c j0. rewrite /j0 csumC (csumC j); apply:csum_M0le; fprops. move:(Vf_target fg j0b); rewrite tg => /(NltP nN) => hc. have ofp:= hw _ hc. have oft:= proj32_1 ofp. rewrite - (osumA oft oS oa) (Hrec (proj1 ha)). move: (hu _ (p6 _ ha hb)) => hd. rewrite - hd in da; exact: (ord_negl_p7 ofp ap da). Qed. Lemma nds_tg8 v (X2:= (fun z => X (k +c z))): inc v (nds_sums n X) -> exists v1 v2, [/\ inc v1 (nds_tn_S X k), inc v2 (nds_sums (n -c k) X2) & v = v2 +o v1]. Proof. move => /funI_P [z zp ->]. move: (nds_tg7 zp) => [K [s1 [s2 [/setP_P pa pb pc ->]]]]. set v1:=nds_sc (cardinal K) (fun z0 => X (nth_elt K z0)) s1. set v2:=nds_sc (n -c k) (fun z => X (k +c z)) s2. have v2p:inc v2 (nds_sums (n -c k) X2) by apply/funI_P; ex_tac. exists v1, v2; split => //;apply/setUf_P; ex_tac; apply/funI_P; ex_tac. Qed. Lemma nds_tg9 (X2:= (fun z => X (k +c z))): (nds_sums n X) = unionf (nds_tn_S X k) (fun v1 => fun_image (nds_sums (n -c k) X2) (fun v2 => v2 +o v1)). Proof. set_extens v. move /nds_tg8 => [v1 [v2 [va vb vc]]]. apply/setUf_P; ex_tac; apply/funI_P; ex_tac. move/setUf_P => [v1 /setUf_P [K /setP_P Kp/funI_P [s1 s1p va]]]. move => /funI_P [v2 /funI_P [s2 s2p ->]] => ->; rewrite va; apply/funI_P. set K' := k -s K. set q := cardinal K. have kN:=(NS_lt_nat kln nN). move:(sub_smaller Kp); rewrite (card_nat kN); rewrite -/q => leqk. have lqn:=(cle_ltT leqk kln). have qN:= NS_lt_nat lqn nN. have nkN:=(NS_diff k nN). have qnN:= (NS_sum qN nkN). have sKN:= (sub_trans Kp (NS_inc_nat kN)). have sK'N: sub K' Nat by exact: (sub_trans (@sub_setC k K) (NS_inc_nat kN)). have cK': cardinal K' = k -c q. by rewrite (cardinal_setC4 Kp (finite_set_nat kN)) (card_nat kN). have qqn:=(Nsum_M0le (n -c k) qN). have kqN:= (NS_diff q kN). have fK: finite_set K by apply/NatP. have fK': finite_set K' by apply/NatP; rewrite cK'. have knk:=(cdiff_pr (proj1 kln)). set qn := q +c (n -c k); rewrite -/qn in qnN qqn. have qnkq: qn +c (k-c q) = n. by rewrite -knk /qn (csumC q) - csumA (cdiff_pr leqk) csumC. have lqnn: qn <=c n by rewrite - qnkq; apply:(Nsum_M0le _ qnN). have sBkBn:=(proj33 (proj1 kln)). move/permutationsP: (s1p) => [bs1 ss1 ts1]; move: (proj1(proj1 bs1)) => fs1. move/permutationsP: (s2p) => [bs2 ss2 ts2]; move: (proj1(proj1 bs2)) => fs2. pose s i := Yo (i s i = (nth_elt K (Vf s1 i)). by move => i liq; rewrite /s; Ytac0. have pb: forall i, i inc (s i) K. move => i iq; rewrite (pa _ iq). have p1: inc (Vf s1 i) q by rewrite /q; Wtac; rewrite ss1; apply/(NltP qN). move/(NltP qN): p1 => ha. apply:(nth_set9 (NS_lt_nat ha qN) sKN ha). have pc: forall i, qn <=c i -> s i = (nth_elt K' (i -c qn)). rewrite /s => i le1;Ytac h; first by case:(cleNgt qqn (cle_ltT le1 h)). by rewrite (Y_false (cleNgt le1)). have pd: forall i, qn <=c i -> i inc (s i) K'. move => i l1 l2; rewrite (pc _ l1); move:(NS_lt_nat l2 nN) => iN. apply:(nth_set9 (NS_diff qn iN) sK'N); rewrite cK'. by apply:(cdiff_Mlt kqN iN l1); rewrite csumC qnkq. have pe: forall i, q <=c i -> i s i = (Vf s2 (i -c q) +c k). by move => i l1 l2; rewrite /s (Y_true l2) (Y_false (cleNgt l1)). have pf: forall i, q <=c i -> i [/\ s i = (Vf s2 (i -c q) +c k), inc (Vf s2 (i -c q)) ((n -c k)) & inc (s i) (n -s k)]. move => i l1 l2; rewrite (pe i l1 l2). have iN:= NS_lt_nat l2 qnN. rewrite - {1}(cdiff_pr l1) /qn in l2. have sa:= (csum_lt2l qN (NS_diff q iN) nkN l2). have sb: inc (Vf s2 (i -c q)) (n -c k). by Wtac; rewrite ss2; apply/NltP. move/(NltP nkN):(sb) => sc. move:(csum_Mlteq kN sc); rewrite (csumC (n -c k)) knk => sd. split => //; apply/setC_P; split; first by apply /(NltP nN). move/(NltP kN); move:(csum_M0le (Vf s2 (i -c q)) (CS_nat kN)). rewrite csumC => ua ub; case: (cltNge ub ua). have ax: forall i, inc i n -> inc (s i) n. move => i /(NltP nN) lin. case: (cleT_el (CS_nat qN) (proj31_1 lin)) => le1. case: (cleT_el (CS_nat qnN) (proj31_1 lin)) => le2. by move: (pd i le2 lin) => /setC_P [/sBkBn ha _]. by move:(pf _ le1 le2) =>[_ _ /setC_P []]. by move: (pb i le1) => /Kp /sBkBn. have sjs: forall j, inc j n -> exists2 i, inc i n & j = s i. move => j /(NltP nN) ljn. have jN:= (NS_lt_nat ljn nN). case:(cleT_el (CS_nat kN) (proj31_1 ljn)) => lkj. have l1: (j -c k) [i1 l2 iv]. have i1N := NS_lt_nat l2 nkN. have l3:=(csum_Meqlt qN l2). move:(proj31 (pf _ (csum_M0le i1 (CS_nat qN)) l3)). rewrite {2} csumC (cdiff_pr1 i1N qN) iv (csumC _ k) (cdiff_pr lkj) => <-. exists (q +c i1) => //; apply/(NltP nN); exact:(clt_leT l3 lqnn). case: (inc_or_not j K) => jK. move:(nth_set_10 sKN fK jK) => [i ia ->]. move:(perm_int_surj qN s1p ia) => [i1 ib <-]. rewrite - (pa _ ib); exists i1 => //; apply/(NltP nN). exact:(clt_ltT ib lqn). have jK': inc j K' by apply/setC_P; split => //; apply/(NltP kN). move:(nth_set_10 sK'N fK' jK') => [i ia ->]. rewrite cK' in ia. move: (csum_Meqlt qnN ia); rewrite qnkq => /(NltP nN) ic; ex_tac. rewrite (pc _ (csum_M0le i (CS_nat qnN))) csumC cdiff_pr1 //. apply:(NS_lt_nat ia kqN). set sigma := Lf s n n. have sp: inc sigma (perm_int n). rewrite /sigma; apply/permutationsP; hnf; aw; split => //. apply:bijective_if_same_finite_c_surj; aw; first by apply:finite_set_nat. by apply: lf_surjective. ex_tac. move: Xax => [qa qb qc qd qe]. have: ord_below_n (fun z => X (Vf sigma z)) n. rewrite /sigma;move => y /(NltP nN) ys; aw. by move:(ax _ ys) => /(NltP nN) /qc [[]]. rewrite /nds_sc - {1 3}qnkq => ax2. have ax3: ord_below_n (fun z=> X (Vf sigma z)) (q +c (n -c k)). move => z z1; apply: ax2; rewrite qnkq; exact:(clt_leT z1 lqnn). rewrite (osum_expansionA qnN kqN ax2) (osum_expansionA qN nkN ax3). set A := osum_expansion _ _. set B := osum_expansion _ _. set C' := osum_expansion _ _. set A' := osum_expansion _ _. set B' := osum_expansion _ _. have ea: A = A'. apply: (osum_expansion_exten nkN) => i l1. have iB:= NS_lt_nat l1 nkN. move: (csum_Mlteq qN l1) ; rewrite (csumC (n -c k))- /qn => l2. have ha: inc (i +c q) n by apply /(NltP nN); exact:(clt_leT l2 lqnn). move:(csum_M0le i (CS_nat qN)); rewrite csumC => hb. by rewrite /sigma; aw; rewrite (pe _ hb l2) /X2 csumC cdiff_pr1. have eb: B = B'. apply: (osum_expansion_exten qN) => i l1. have ib:inc i n by apply /(NltP nN); exact:(clt_ltT l1 lqn). by rewrite /sigma; aw; rewrite - ( pa _ l1). have oa: ordinalp A'. apply:(OS_osum_expansion nkN) => i l1; apply: ax3. by move: (csum_Mlteq qN l1);rewrite (csumC q). have ob: ordinalp B'. apply:(OS_osum_expansion qN) => i l1; apply: ax2; rewrite qnkq. exact:(clt_ltT l1 lqn). have oc: ordinalp C'. apply:(OS_osum_expansion kqN) => i l1; apply: ax2. by rewrite (csumC qn);apply:csum_Mlteq. rewrite (osumA oc oa ob) - ea; apply: (f_equal2 _ _ eb). have knz1:= (cdiff_nz kln). move: (cpred_pr nkN knz1) => [nk1N nk1v]. rewrite /A nk1v (osum_expansion_succ _ nk1N) /X2. set C:= osum_expansion _ _ . move: (cltS nk1N); rewrite - nk1v => eq1. have oc': ordinalp C. apply:(OS_osum_expansion nk1N) => i lin. have ha:inc i (source s2). rewrite ss2; apply/(NltP nkN); exact (clt_ltT lin eq1). move:(Vf_target fs2 ha); rewrite ts2 => /(NltP nkN) lt1. by move:(csum_Meqlt kN lt1); rewrite knk => /qc /proj32_1. have ha:inc (cpred (n -c k)) (source s2). by rewrite ss2; apply/(NltP nkN); rewrite {2} nk1v; apply: cltS. move:(Vf_target fs2 ha); rewrite ts2 => /(NltP nkN) lt1. move:(csum_Meqlt kN lt1); rewrite knk => hb. move:(csum_M0le (Vf s2 (cpred (n -c k))) (CS_nat kN)) => hc. move: (qc _ hb) (qe _ hc hb);set a:= X _ => ap da. rewrite (osumA oc (proj32_1 ap) oc'); congr (_ +o C). rewrite /C'. have hd: forall i, i (Vf sigma (i +c qn)) i lik. move:(csum_Meqlt qnN lik); rewrite qnkq => l1. move: (csum_M0le i(CS_nat qnN)) => l2. move/(NltP nN):(l1) => iN. by rewrite csumC /sigma; aw; move: (pd _ l2 l1) => /setC_P []/(NltP kN). have he: forall i, i let b := X (Vf sigma (i +c qn)) in [/\ ordinalp b, \0o i l1; move:(hd _ l1) => sa. move:(qd _ sa) (qc _ (clt_ltT sa kln)) => r1 r2. split; [exact (proj32_1 r2) | exact r2| exact r1]. symmetry. move:kqN (cleR (CS_nat kqN)). have oa':=(proj32_1 ap). move: {-3} (k -c q); apply: Nat_induction. by rewrite osum_expansion0 (osum0l oa'). move => i iN Hrec le1. rewrite (osum_expansion_succ _ iN). move/(cleSltP iN): (le1) => /he []. set b := (X (Vf sigma (i +c qn))) => ob' bp db. have ikq:=(cleT (cleS iN) le1). have oc'':ordinalp (osum_expansion (fun z : Set => X (Vf sigma (z +c qn))) i). apply: (OS_osum_expansion iN) => j jli. by move: (he _ (clt_leT jli ikq)) => []. rewrite - db in da. rewrite - (osumA ob' oc'' oa'). by rewrite (Hrec ikq) (ord_negl_p7 bp ap da). Qed. Lemma nds_tg10 : nds_card n X <=c (ndstnC k) *c (nds_F (n -c k)). Proof. rewrite /nds_card nds_tg9. set F:= (fun v1 : Set => _). set E := (nds_tn_S X k). move:(csum_pr1_bis E F). set g1:= (Lg E (fun a => cardinal (Vg (Lg E F) a))). have <-: csum g1 = csumb E (fun a => cardinal (F a)). apply:csumb_exten => t tx; bw. set g2 := cst_graph E (nds_F (n -c k)). have sd: domain g1 = domain g2 by rewrite /g1/g2; bw. have kN:= NS_lt_nat kln nN. have nkN:= (NS_diff k nN). move: (nds_j nkN) => [pe _ pf pg]. move: Xax => [pa pb pc pd _]. suff le1:forall x, inc x (domain g1) -> Vg g1 x <=c Vg g2 x. move:(csum_increasing sd le1). rewrite csum_of_same cprodC - cprod2cl /E -/(nds_tn_C _ _) => ha hb. have kp: \0c i ik; apply:pc (clt_ltT ik kln) | exists e]. move: (cprod_Mlele (nds_tn11 kN kp ax) (cleR (CS_nat pe))) => hc. exact:(cleT (cleT hb ha) hc). rewrite /g1 /g2; bw => a abn; bw. have /pg:nds_ax(fun z => X (k +c z)) (n -c k). move => i ink; move:(csum_Meqlt kN ink). by rewrite(cdiff_pr (proj1 kln)) => /pc /proj32_1. apply:cleT; apply:fun_image_smaller. Qed. Lemma nds_tg11 Y : (forall i, i \0o nds_tn_C X k = ndstnC k -> nds_card (n-c k) Y = nds_F (n -c k) -> nds_card n X = (ndstnC k) *c (nds_F (n -c k)). Proof. move => yp <- <-. rewrite /nds_card nds_tg9. have kN := NS_lt_nat kln nN. have nkN := NS_diff k nN. move: Xax => [Xpa Xpb Xpc Xpd Xpe]. set c:= omega0 ^o osucc e. have cp: \0o X (k +c z))). have ax0: nds_ax Y (n -c k) by move => i /yp [] /proj32_1 h _. have aux: forall i, inc i (nds_tn_S X k) -> i i /setUf_P [K /setP_P K1 /funI_P [s sp] ->]. have sKN:= (sub_trans K1 (NS_inc_nat kN)). have fsk:= (sub_finite_set K1 (finite_set_nat kN)). have cKN: natp (cardinal K) by apply /NatP. have : forall i, i X (nth_elt K (Vf s i)) j jk. have r0: (Vf s j) [[[fs _] _] ss ts]. by apply/(NltP cKN); Wtac; rewrite ss; apply/(NltP cKN). have r1:(nth_elt K (Vf s j)) //. apply: (NS_lt_nat r0 cKN). by move: (proj2(the_CNF_p4 (Xpc _ (clt_ltT r1 kln)))); rewrite Xpd. move: (cardinal K) cKN; apply: Nat_induction. by rewrite /nds_sc osum_expansion0. move => m mN Hrec aux; rewrite /nds_sc (osum_expansion_succ _ mN). have oic:= (indecomp_prop4 (OS_succ Xpb)). have alc:=(aux _ (cltS mN)). apply: (indecomp_prop2 alc _ oic); apply: Hrec => j jm; apply:aux. exact: (clt_ltT jm (cltS mN)). have aux2: forall i j u v, inc i (nds_tn_S X k) -> inc j (nds_tn_S X k) -> inc u E -> inc v E -> u +o i = v +o j -> (u = v /\ i = j). move => i j u v ia ja /funI_P [s1 s1p v1p] /funI_P [s2 s2p v2p]. move/permutationsP:s1p => [[[fs1 _] _] sf1 tf1]. move/permutationsP:s2p => [[[fs2 _] _] sf2 tf2]. have ha: forall q, q (Vf s1 q) q qa;apply /(NltP nkN); Wtac; rewrite sf1; apply/(NltP nkN). have hb: forall q, q (Vf s2 q) q qa;apply /(NltP nkN); Wtac; rewrite sf2; apply/(NltP nkN). have v1a: u = nds_sc (n -c k) (fun z => c *o Y z) s1. by rewrite v1p; apply:(osum_expansion_exten nkN) => q /ha /yp []. have v2a: v = nds_sc (n -c k) (fun z => c *o Y z) s2. by rewrite v2p; apply:(osum_expansion_exten nkN) => q /hb/yp []. have ax1:nds_ax (fun z => Y (Vf s1 z)) (n -c k). by move => z /ha/yp [/proj32_1 hc _]. have ax2:nds_ax (fun z => Y (Vf s2 z)) (n -c k). by move => z /hb/yp [/proj32_1 hc _]. rewrite v1a v2a /nds_sc (nds_r1 nkN ax1 oc) (nds_r1 nkN ax2 oc). set v1':= osum_expansion _ _; set v2':= osum_expansion _ _ => eq1. have ov1: ordinalp v1' by apply:(OS_osum_expansion nkN); apply: ax1. have ov2: ordinalp v2' by apply:(OS_osum_expansion nkN); apply: ax2. move: (aux _ ia) (aux _ ja) => ib jb. set a := c *o v1' +o i. move:(proj31_1 ib)(proj31_1 jb) => oi oj. have oa:ordinalp a by apply (OS_sum2 (OS_prod2 oc ov1) oi). by move:(odivision_unique oa oc (And4 ov1 oi (erefl a) ib) (And4 ov2 oj eq1 jb)) => [-> rb]. pose F a :=(fun_image E (osum2^~ a)). have H: forall a, inc a (nds_tn_S X k) -> cardinal (F a) = nds_card (n -c k) Y. move => a ias. rewrite cardinal_fun_image. rewrite /E -/(nds_card _ _) (nds_r2 nkN ax0 cp). by apply:(nds_card_exten nkN) => i /yp [_ ->]. move => u v ua va /= eq; exact: (proj1 (aux2 _ _ _ _ ias ias ua va eq)). rewrite csum_pr4_bis. rewrite cprodC /nds_tn_C cprod2cr - csum_of_same /csumb. by apply: f_equal; apply: Lg_exten => i ib; apply: H. move => i j ia ja; case (equal_or_not i j) => eij; [by left | right]. apply:disjoint_pr => u /funI_P [v1 va vb] /funI_P [v2 vc vd]. rewrite vb in vd; case eij; exact: (proj2 (aux2 _ _ _ _ ia ja va vc vd)). Qed. End NdsStudy. Lemma nds_s1 n k: natp n -> k k <> \0c -> nds_FA n k <=c (ndstnC k) *c (nds_F (n -c k)). Proof. move => nN kln knz. move: (cle_ltT (czero_least (proj31_1 kln)) kln) => np. move: (nds_type_p3 nN (nesym (proj2 np)) (proj1 kln)). move=> [pa _ _ [X [pb pc <-]]]. move:(nds_type9 nN knz (proj1 kln) pc)=> [Y [e [ya <-]]]. by apply: (nds_tg10 nN knz kln ya). Qed. Lemma nds_s2 n k: natp n -> k k <> \0c -> nds_FA n k = (ndstnC k) *c (nds_F (n -c k)). Proof. move => nN kln knz; apply: cleA; first by apply:nds_s1. move: (cle_ltT (czero_least (proj31_1 kln)) kln) => np. move: (nds_type_p3 nN (nesym (proj2 np)) (proj1 kln)) => [pa _ pb _]. move:(nds_type_p10 (NS_diff k nN)) => [X [ax xa1 xv]]. move:(nds_tn2 (NS_lt_nat kln nN)) => [_ _ _ [Y [ya1 [e oe yd]] yv] _]. set c := omega0 ^o (osucc e). have cp: \0o \0o i lin; rewrite /Z; Ytac h; first by apply: ya1. case: (cleT_el (proj31_1 kln) (proj31_1 lin)) => // leki. apply: (oprod2_pos cp (xa1 _ (cdiff_pr7 leki lin nN))). have az2: forall i, i ~ i e i lin h. rewrite /Z; Ytac0;apply /oltSSP. case: (cleT_el (proj31_1 kln) (proj31_1 lin)) => // leki. have xip :=(xa1 _ (cdiff_pr7 leki lin nN)). have ha:= (oprod_Mle1 oc xip). have od:=(OS_the_CNF_degree (proj32 ha)). have:= (ole_ltT ha (proj2 (the_CNF_p4 (oprod2_pos cp xip)))). by move /(opow_Meqltr ole_2omega (OS_succ oe) ( (OS_succ od))). have az3:forall i, i the_CNF_degree (Z i) = e. by move => i lik;rewrite /Z; Ytac0;rewrite (yd _ lik). have az4:forall i, i e <=o the_CNF_degree (Z i). move => i lin; case (p_or_not_p (i h. rewrite (az3 _ h); apply: (oleR oe). exact: (proj1 (az2 _ lin h)). have ha: nds_type Z n k. right; split => //; split => //; exists e; split => //. have ->: (Zo n (fun i => the_CNF_degree (Z i) = e)) = k. set_extens i. move => /Zo_P [/(NltP nN) lin di]; apply/(NltP kN). by ex_middle h; move:(proj2 (az2 i lin h)); rewrite di; case. move => /(NltP kN) => lik; apply:Zo_i. by apply /(NltP nN); move:(clt_ltT lik kln). apply: (az3 _ lik). by rewrite (card_nat kN). have hb: nds_type_nor Z n k e. split => // i ki lin; apply: (az2 i lin); exact (cleNgt ki). have hc: forall i, i \0o i ib; split; first by apply: xa1. rewrite /Z (Y_false (cleNgt (csum_M0le i (proj31_1 kln)))). by rewrite csumC (cdiff_pr1 (NS_lt_nat ib nkN) kN). have hd:nds_tn_C Z k = ndstnC k. have sb: same_below Z Y k by move => i klik; rewrite /Z; Ytac0. have ->: nds_tn_C Z k = nds_tn_C Y k by apply:nds_tn_C_exten. by rewrite yv (nds_tn13 kN). have he: nds_ax Z n by move => i lin; exact (proj32_1 (az1 _ lin)). by rewrite - (nds_tg11 nN kln hb hc hd xv); apply: pb. Qed. Lemma ndstnC1: ndstnC \1c = \2c. Proof. rewrite /ndstnC. move:(cpred_pr1 CS0); rewrite succ_zero => ->. by rewrite cpowx0 (cprod1r CS1) succ_one. Qed. Lemma nds_s3 n: natp n -> n <> \0c -> \2c *c (nds_F n) <=c (nds_F (csucc n)). Proof. move => nN nz. have np: \0c ->. Qed. Lemma nds_s4 n: natp n -> \2c ^c n <=c (nds_F (csucc n)). Proof. move: n; apply: Nat_induction. rewrite cpowx0 succ_zero (proj2 nds_k); fprops. move => n nN hrec. move:(nds_s3 (NS_succ nN) (@succ_nz n)) => sb. move: (cleT (cprod_Mlele (cleR CS2) hrec) sb). by rewrite (cpow_succ _ nN) cprodC. Qed. Lemma nds_s5 n: natp n -> \2c n nN ngt2. have nnz:= nesym (proj2(clt_ltT clt_02 ngt2)). move:(cpred_pr nN nnz) => [n1N sa]. have npz: cpred n <> \0c. move => h; move: sa (proj1 ngt2). by rewrite h succ_zero => -> /(cltNge clt_12). move:(cpred_pr n1N npz) => [n2N sb]. have pN:= NS_pow NS2 n2N. have ha : \2c <=c \2c ^c cpred (cpred n). apply:(cpow_Mle1 CS2) => mz. by case:(proj2 ngt2); rewrite sa sb mz succ_zero succ_one. have hb: csucc (cpred n) \2c <=c n -> (forall k, k k <> \0c -> (ndstnC k) *c (nds_F (n -c k)) <=c (nds_F n)) /\ (exists k, [/\ k \0c & (ndstnC k) *c (nds_F (n -c k)) = (nds_F n)]). Proof. move => nN n2. have np:= (nesym (proj2(clt_leT clt_02 n2))). move:(nds_type_p11 nN np) => [pa [k0 [k0n k0nz kv]]]; split. by move => k kn knz; rewrite -(nds_s2 nN kn knz);apply: (pa _ (proj1 kn)). case (equal_or_not k0 n) => ekn. case (equal_or_not \2c n) => en2. rewrite - en2 nds_l; exists \1c; split. + apply: clt_12. + fprops. + move:(cpred_pr1 CS1); rewrite succ_one => cp1. by rewrite ndstnC1 - (cpred_pr4 CS2) cp1 (proj2 nds_k) (cprod1r CS2). move: (cpred_pr nN np) => [sa sb]. move: (proj2 (nds_s5 nN (conj n2 en2))). by rewrite - kv ekn sb (nds_type_p8 sa). have lkn:= (conj k0n ekn). by exists k0; split => //; rewrite -(nds_s2 nN lkn k0nz). Qed. Require Import BinNat. (* much too complicated *) Lemma nat_of_exp_bin_bis a b: (a ^ b)%num = a ^b :> nat. Proof. rewrite - {1} (nat_of_binK b). elim: (nat_of_bin b) => // n Hr; rewrite expnS. have: nat_of_bin (bin_of_nat n.+1) = nat_of_bin ((bin_of_nat n) + 1). rewrite - addn1 nat_of_add_bin // ! bin_of_natK //. move /(f_equal bin_of_nat); rewrite ! bin_of_natK nat_of_binK => ->. move: (f_equal bin_of_nat Hr). rewrite nat_of_binK. rewrite N.pow_add_r N.pow_1_r ;move => ->. by rewrite nat_of_mul_bin bin_of_natK mulnC. Qed. Lemma Nmul_lt_mono a b c: (0 < c -> a < b -> c * a < c* b)%N. Proof. by move => ha; move/(N.mul_lt_mono_pos_l c a b ha). Qed. Section NdsNat. Definition ndstnCN n := (((bin_of_nat n) * (2 ^ (bin_of_nat(n.-1)))) + 1)%N. Definition ndstnC_nat n := (n * (2 ^ (n.-1))) .+1. Notation C := ndstnCN. Notation Nle := N.le (only parsing). Lemma sameC n: ndstnC_nat n = C n. Proof. by rewrite /C /ndstnC_nat - addn1 nat_of_add_bin nat_of_mul_bin - {1} (bin_of_natK (n.-1)) nat_of_exp_bin_bis ! bin_of_natK. Qed. Lemma Ngtge a b c: (a <= b -> c < a -> b = c -> False)%N. Proof. by move => ha hb hc; case/(N.lt_nge c a): hb; rewrite - hc. Qed. Let NmulC := N.mul_comm. Ltac nextI k:= rewrite /orb ltnS => _; rewrite (leq_eqVlt k). Ltac lastI := rewrite /orb ltnS => _ /anti_leq <-. Variable F: nat -> N. Definition FP n k := (F n = (C k) * (F (n - k)))%N. Hypothesis F0: F 0 = 1%N. Hypothesis F1: F 1 = 1%N. Hypothesis HF1: forall n k, 2 <= n -> 0 < k < n -> ((C k) * (F (n - k)) <= F n)%N. Hypothesis HF2: forall n , 2 <= n -> exists2 k, 0 < k < n & FP n k. Lemma ndsC1 : C 1 = 2%N. Proof. by []. Qed. Lemma ndsC2 : C 2 = 5%N. Proof. by []. Qed. Lemma ndsC3 : C 3 = 13%N. Proof. by []. Qed. Lemma ndsC4 : C 4 = 33%N. Proof. by []. Qed. Lemma ndsC5 : C 5 = 81%N. Proof. by []. Qed. Lemma ndsC6 : C 6 = 193%N. Proof. by []. Qed. Lemma ndsC7 : C 7 = 449%N. Proof. by []. Qed. Lemma nds0 a: (a * F 1 = a) %N. Proof. by rewrite F1 N.mul_1_r. Qed. Lemma nds1 n: FP (n.+1) n = (F n.+1 = C n). Proof. by rewrite /FP subSnn nds0. Qed. Lemma ndsF2a: FP 2 1. Proof. rewrite /FP; move: (HF2 (leqnn 2)) => [k kab ->]. by move: kab; rewrite ltnS => /anti_leq <-. Qed. Lemma ndsF2: F 2 = C 1. Proof. by move: ndsF2a; rewrite nds1. Qed. Lemma ndsF3a: FP 3 2. Proof. have h0: 2 <= 3 by []. have h2: 0 < 2 < 3 by []. have ha: (C 1 * C 1 < C 2)%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite nds0 => le1. move:(HF2 h0) => [k]; rewrite ltnS; rewrite (leq_eqVlt k). case: eqP; first by move => -> _; rewrite nds1. lastI; rewrite /FP ndsF2; case/(Ngtge le1 ha). Qed. Lemma ndsF3: F 3 = C 2. Proof. by rewrite ndsF3a nds0. Qed. Lemma ndsF4a: FP 4 3. Proof. have h0: 2 <= 4 by []. have h2: 0 < 3 < 4 by []. have ha:(C 2 * C 1 < C 3)%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite nds0 => le1. move:(HF2 h0) => [k]; rewrite ltnS; rewrite (leq_eqVlt k). case: eqP; first by move => -> _ ;rewrite nds1. nextI k; case: eqP. by move => -> _; rewrite /FP ndsF2; case /(Ngtge le1 ha). lastI; rewrite /FP ndsF3 NmulC; case /(Ngtge le1 ha). Qed. Lemma ndsF4: F 4 = C 3. Proof. by rewrite ndsF4a nds0. Qed. Lemma ndsF5a: FP 5 4. Proof. have h0: 2 <= 5 by []. have h2: 0 < 4 < 5 by []. have ha: (C 3 * C 1 < C 4)%N by []. have hb: (C 2 * C 2 < C 4)%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite nds0 => le1. move:(HF2 h0) => [k]; rewrite ltnS; rewrite (leq_eqVlt k). case: eqP; [ by move => -> _ ;rewrite nds1 | rewrite /FP]. nextI k; case: eqP; first by move => -> _; rewrite ndsF2; case /(Ngtge le1 ha). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hb). lastI; rewrite ndsF4 NmulC; case /(Ngtge le1 ha). Qed. Lemma ndsF5: F 5 = C 4. Proof. by rewrite ndsF5a nds0. Qed. Lemma ndsF6a: FP 6 5. Proof. have h0: 2 <= 6 by []. have h2: 0 < 5 < 6 by []. have ha: (C 4 * C 1 < C 5)%N by []. have hb: (C 3 * C 2 < C 5)%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite nds0 => le1. move:(HF2 h0) => [k]; rewrite ltnS; rewrite (leq_eqVlt k). case: eqP; [ by move => -> _ ;rewrite nds1 | rewrite /FP]. nextI k; case: eqP; first by move => -> _; rewrite ndsF2; case /(Ngtge le1 ha). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hb). lastI; rewrite ndsF5 NmulC; case /(Ngtge le1 ha). Qed. Lemma ndsF6: F 6 = C 5. Proof. by rewrite ndsF6a nds0. Qed. Lemma ndsF7a: FP 7 6. Proof. have h0: 2 <= 7 by []. have h2: 0 < 6 < 7 by []. have ha: (C 5 * C 1 < C 6)%N by []. have hb: (C 4 * C 2 < C 6)%N by []. have hc: (C 3 * C 3 < C 6)%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite nds0 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k). case: eqP; [by move => -> _ ;rewrite nds1 | rewrite /FP ]. nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 ha). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 hb). lastI; rewrite ndsF6 NmulC; case /(Ngtge le1 ha). Qed. Lemma ndsF7: F 7 = C 6. Proof. by rewrite ndsF7a nds0. Qed. Lemma ndsF8a: FP 8 7. Proof. have h0: 2 <= 8 by []. have h2: 0 < 7 < 8 by []. have ha: (C 6 * C 1 < C 7)%N by []. have hb: (C 5 * C 2 < C 7)%N by []. have hc: (C 4 * C 3 < C 7)%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite nds0 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k). case: eqP; [by move => -> _ ;rewrite nds1 | rewrite /FP ]. nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 ha). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hb). lastI; rewrite ndsF7 NmulC; case /(Ngtge le1 ha). Qed. Lemma ndsF8: F 8 = C 7. Proof. by rewrite ndsF8a nds0. Qed. Lemma ndsF9a: FP 9 4. Proof. have h0: 2 <= 9 by []. have h2: 0 < 4 < 8 by []. have ha: (C 8 * F 1 < C 4 * C 4)%N by rewrite F1. have hb: (C 7 * C 1 < C 4 * C 4 )%N by []. have hc: (C 6 * C 2 < C 4 * C 4)%N by []. have hd: (C 5 * C 3 < C 4 * C 4)%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite ndsF5 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5. nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hc). lastI; rewrite ndsF8; case/(Ngtge le1 hb). Qed. Lemma ndsF9: (F 9 = C 4 * C 4)%N. Proof. by move: ndsF9a; rewrite /FP ndsF5. Qed. Lemma ndsF9b: F 9 = 1089%N. Proof. by rewrite ndsF9. Qed. Lemma ndsF10a: FP 10 4. Proof. have h0: 2 <= 10 by []. have h2: 0 < 4 < 10 by []. have ha: (C 9 * F 1 < C 4 * C 5 )%N by rewrite F1. have hb: (C 8 * C 1 < C 4 * C 5 )%N by []. have hc: (C 7 * C 2 < C 4 * C 5 )%N by []. have hd: (C 6 * C 3 < C 4 * C 5 )%N by []. have he: (C 1 * (C 4 * C 4) < (C 4 * C 5) )%N by []. rewrite /FP;move:(HF1 h0 h2); rewrite ndsF6 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5. nextI k; case: eqP; first by move => -> _; rewrite ndsF6. nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hc). lastI; rewrite ndsF9; case/(Ngtge le1 he). Qed. Lemma ndsF10: (F 10 = C 4 * C 5)%N. Proof. by move: ndsF10a; rewrite /FP ndsF6. Qed. Lemma ndsF10b: (F 10 = 2673)%N. Proof. by rewrite ndsF10. Qed. Lemma ndsF10c: FP 10 5. Proof. by rewrite/FP ndsF10 ndsF5. Qed. Lemma ndsF11a: FP 11 5. Proof. have h0: 2 <= 11 by []. have h2: 0 < 5 <11 by []. have ha: (C 10 * F 1 < C 5 * C 5)%N by rewrite F1. have hb: (C 9 * C 1 < C 5 * C 5)%N by []. have hc: (C 8 * C 2 < C 5 * C 5)%N by []. have hd: (C 7 * C 3 < C 5 * C 5)%N by []. have he: (C 6 * C 4 < C 5 * C 5)%N by []. have hf: (C 2 * (C 4 * C 4) < C 5 * C 5)%N by []. have hg: (C 1 * (C 4 * C 5) < C 5 * C 5)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF6 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6. nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF9; case /(Ngtge le1 hf). lastI; rewrite ndsF10; case/(Ngtge le1 hg). Qed. Lemma ndsF11: (F 11 = C 5 * C 5) %N. Proof. by move: ndsF11a; rewrite /FP ndsF6. Qed. Lemma ndsF11b: F 11 = 6561 %N. Proof. by rewrite ndsF11. Qed. Lemma ndsF12a: FP 12 5. Proof. have h0: 2 <= 12 by []. have h2: 0 < 5 <12 by []. have ha: (C 11 * F 1 < C 5 * C 6)%N by rewrite F1. have hb: (C 10 * C 1 < C 5 * C 6)%N by []. have hc: (C 9 * C 2 < C 5 * C 6)%N by []. have hd: (C 8 * C 3 < C 5 * C 6)%N by []. have he: (C 7 * C 4 < C 5 * C 6)%N by []. have hf: (C 3 * (C 4 * C 4) < C 5 * C 6)%N by []. have hg: (C 2 * (C 4 * C 5) < C 5 * C 6)%N by []. have hi: (C 1 * (C 5 * C 5) < C 5 * C 6)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF7 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6. nextI k; case: eqP; first by move => -> _; rewrite ndsF7. nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF9; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF10; case /(Ngtge le1 hg). lastI; rewrite ndsF11; case/(Ngtge le1 hi). Qed. Lemma ndsF12: (F 12 = C 5 * C 6) %N. Proof. by move: ndsF12a; rewrite /FP ndsF7. Qed. Lemma ndsF12b: (F 12 = 15633) %N. Proof. by rewrite ndsF12. Qed. Lemma ndsF12c: FP 12 6. Proof. by rewrite /FP ndsF6 ndsF12b NmulC. Qed. Lemma ndsF13a: FP 13 6. Proof. have h0: 2 <= 13 by []. have h2: 0 < 6 < 13 by []. have ha: (C 12 * F 1 < C 6 * C 6)%N by rewrite F1. have hb: (C 11 * C 1 < C 6 * C 6)%N by []. have hc: (C 10 * C 2 < C 6 * C 6)%N by []. have hd: (C 9 * C 3 < C 6 * C 6)%N by []. have hd': (C 8 * C 4 < C 6 * C 6)%N by []. have he: (C 7 * C 5 < C 6 * C 6)%N by []. have hf: (C 4 * (C 4 * C 4) < C 6 * C 6)%N by []. have hg: (C 3 * (C 4 * C 5) < C 6 * C 6)%N by []. have hi: (C 2 * (C 5 * C 5) < C 6 * C 6)%N by []. have hj: (C 1 * (C 5 * C 6) < C 6 * C 6)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF7 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 hd'). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF7. nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF9; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF10; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF11; case /(Ngtge le1 hi). lastI; rewrite ndsF12; case/(Ngtge le1 hj). Qed. Lemma ndsF13: (F 13 = C 6 * C 6) %N. Proof. by move: ndsF13a; rewrite /FP ndsF7. Qed. Lemma ndsF13b: (F 13 = 37249) %N. Proof. by rewrite ndsF13. Qed. Lemma ndsF14a: FP 14 4. Proof. have h0: 2 <= 14 by []. have h2: 0 < 4 < 14 by []. set f := 88209%N. have ha: (C 13 * F 1 < f)%N by rewrite F1. have hb: (C 12 * C 1 < f)%N by []. have hc: (C 11 * C 2 < f)%N by []. have hd: (C 10 * C 3 < f)%N by []. have he: (C 9 * C 4 < f)%N by []. have hf: (C 8 * C 5 < f)%N by []. have hg: (C 7 * C 6 < f)%N by []. have hh: (C 3 * (C 5 * C 5) < f)%N by []. have hi: (C 2 * (C 5 * C 6) < f)%N by []. have hj: (C 1 * (C 6 * C 6) < f)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF10 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF9. nextI k; case: eqP; first by move => -> _; rewrite ndsF10. nextI k; case: eqP; first by move => -> _; rewrite ndsF11; case /(Ngtge le1 hh). nextI k; case: eqP; first by move => -> _; rewrite ndsF12; case /(Ngtge le1 hi). lastI; rewrite ndsF13; case/(Ngtge le1 hj). Qed. Lemma ndsF14: (F 14 = C 4 * C 4 * C 5) %N. Proof. by move: ndsF14a; rewrite /FP ndsF10. Qed. Lemma ndsF14b: (F 14 = 88209) %N. Proof. by move: ndsF14a; rewrite /FP ndsF10. Qed. Lemma ndsF14c: FP 14 5. Proof. by rewrite /FP ndsF14 ndsF9. Qed. Lemma ndsF15a: FP 15 4. Proof. have h0: 2 <= 15 by []. have h2: 0 < 4 < 15 by []. set f := 216513%N. have ha: (C 14 * F 1 < f)%N by rewrite F1. have hb: (C 13 * C 1 < f)%N by []. have hc: (C 12 * C 2 < f)%N by []. have hd: (C 11 * C 3 < f)%N by []. have he: (C 10 * C 4 < f)%N by []. have hf: (C 9 * C 5 < f)%N by []. have hg: (C 8 * C 6 < f)%N by []. have hh: (C 7 * C 7 < f)%N by []. have hi: (C 6 * (C 4 * C 4) < f)%N by []. have hj: (C 3 * (C 5 * C 6) < f)%N by []. have hk: (C 2 * (C 6 * C 6) < f)%N by []. have hl: (C 1 * (C 4 * C 4 * C 5) < f)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF11 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hh). nextI k; case: eqP; first by move => -> _; rewrite ndsF9;case /(Ngtge le1 hi). nextI k; case: eqP; first by move => -> _; rewrite ndsF10. nextI k; case: eqP; first by move => -> _; rewrite ndsF11. nextI k; case: eqP; first by move => -> _; rewrite ndsF12; case /(Ngtge le1 hj). nextI k; case: eqP; first by move => -> _; rewrite ndsF13; case /(Ngtge le1 hk). lastI; rewrite ndsF14; case/(Ngtge le1 hl). Qed. Lemma ndsF15: (F 15 = C 4 * C 5 * C 5) %N. Proof. by move: ndsF15a; rewrite /FP ndsF11. Qed. Lemma ndsF15b: (F 15 = 216513) %N. Proof. by rewrite ndsF15. Qed. Lemma ndsF15c: FP 15 5. Proof. by rewrite /FP ndsF15 ndsF10. Qed. Lemma ndsF16a: FP 16 5. Proof. have h0: 2 <= 16 by []. have h2: 0 < 5 < 16 by []. set f := 531441%N. have ha: (C 15 * F 1 < f)%N by rewrite F1. have hb: (C 14 * C 1 < f)%N by []. have hc: (C 13 * C 2 < f)%N by []. have hd: (C 12 * C 3 < f)%N by []. have he: (C 11 * C 4 < f)%N by []. have hf: (C 10 * C 5 < f)%N by []. have hg: (C 9 * C 6 < f)%N by []. have hh: (C 8 * C 7 < f)%N by []. have hi: (C 7 * (C 4 * C 4) < f)%N by []. have hj: (C 6 * (C 4 * C 5) < f)%N by []. have hk: (C 3 * (C 6 * C 6) < f)%N by []. have hl: (C 2 * (C 4 * C 4 * C 5) < f)%N by []. have hm: (C 1 * (C 4 * C 5 * C 5) < f)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF11 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hh). nextI k; case: eqP; first by move => -> _; rewrite ndsF9;case /(Ngtge le1 hi). nextI k; case: eqP; first by move => -> _; rewrite ndsF10;case /(Ngtge le1 hj). nextI k; case: eqP; first by move => -> _; rewrite ndsF11. nextI k; case: eqP; first by move => -> _; rewrite ndsF12; case /(Ngtge le1 hj). nextI k; case: eqP; first by move => -> _; rewrite ndsF13; case /(Ngtge le1 hk). nextI k; case: eqP; first by move => -> _; rewrite ndsF14; case /(Ngtge le1 hl). lastI; rewrite ndsF15; case/(Ngtge le1 hm). Qed. Lemma ndsF16: (F 16 = C 5 * C 5 * C 5) %N. Proof. by move: ndsF16a; rewrite /FP ndsF11. Qed. Lemma ndsF16b: (F 16 = 531441) %N. Proof. by rewrite ndsF16. Qed. Lemma ndsF17a: FP 17 5. Proof. have h0: 2 <= 17 by []. have h2: 0 < 5 < 17 by []. set f := 1266273%N. have ha: (C 16 * F 1 < f)%N by rewrite F1. have hb: (C 15 * C 1 < f)%N by []. have hc: (C 14 * C 2 < f)%N by []. have hd: (C 13 * C 3 < f)%N by []. have he: (C 12 * C 4 < f)%N by []. have hf: (C 11 * C 5 < f)%N by []. have hg: (C 10 * C 6 < f)%N by []. have hh: (C 9 * C 7 < f)%N by []. have hi: (C 8 * (C 4 * C 4) < f)%N by []. have hj: (C 7 * (C 4 * C 5) < f)%N by []. have hk: (C 4 * (C 6 * C 6) < f)%N by []. have hl: (C 3 * (C 4 * C 4 * C 5) < f)%N by []. have hm: (C 2 * (C 4 * C 5 * C 5) < f)%N by []. have hn: (C 1 * (C 5 * C 5 * C 5) < f)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF12 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hh). nextI k; case: eqP; first by move => -> _; rewrite ndsF9;case /(Ngtge le1 hi). nextI k; case: eqP; first by move => -> _; rewrite ndsF10;case /(Ngtge le1 hj). nextI k; case: eqP; first by move => -> _; rewrite ndsF11. nextI k; case: eqP; first by move => -> _; rewrite ndsF12. nextI k; case: eqP; first by move => -> _; rewrite ndsF13; case /(Ngtge le1 hk). nextI k; case: eqP; first by move => -> _; rewrite ndsF14; case /(Ngtge le1 hl). nextI k; case: eqP; first by move => -> _; rewrite ndsF15; case /(Ngtge le1 hm). lastI; rewrite ndsF16; case/(Ngtge le1 hn). Qed. Lemma ndsF17: (F 17 = C 5 * C 5 * C 6) %N. Proof. by move: ndsF17a; rewrite /FP ndsF12. Qed. Lemma ndsF17b: (F 17 = 1266273) %N. Proof. by rewrite ndsF17. Qed. Lemma ndsF17c: FP 17 6. Proof. by rewrite /FP ndsF11 ndsF17. Qed. Lemma ndsF18a: FP 18 5. Proof. have h0: 2 <= 18 by []. have h2: 0 < 5 < 18 by []. set f := 3017169%N. have ha: (C 17 * F 1 < f)%N by rewrite F1. have hb: (C 16 * C 1 < f)%N by []. have hc: (C 15 * C 2 < f)%N by []. have hd: (C 14 * C 3 < f)%N by []. have he: (C 13 * C 4 < f)%N by []. have hf: (C 12 * C 5 < f)%N by []. have hg: (C 11 * C 6 < f)%N by []. have hh: (C 10 * C 7 < f)%N by []. have hi: (C 9 * (C 4 * C 4) < f)%N by []. have hj: (C 8 * (C 4 * C 5) < f)%N by []. have hk: (C 7 * (C 5 * C 5) < f)%N by []. have hl: (C 4 * (C 4 * C 4 * C 5) < f)%N by []. have hm: (C 3 * (C 4 * C 5 * C 5) < f)%N by []. have hn: (C 2 * (C 5 * C 5 * C 5) < f)%N by []. have ho: (C 1 * (C 5 * C 5 * C 6) < f)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF13 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hh). nextI k; case: eqP; first by move => -> _; rewrite ndsF9;case /(Ngtge le1 hi). nextI k; case: eqP; first by move => -> _; rewrite ndsF10;case /(Ngtge le1 hj). nextI k; case: eqP; first by move => -> _; rewrite ndsF11;case /(Ngtge le1 hk). nextI k; case: eqP; first by move => -> _; rewrite ndsF12. nextI k; case: eqP; first by move => -> _; rewrite ndsF13. nextI k; case: eqP; first by move => -> _; rewrite ndsF14; case /(Ngtge le1 hl). nextI k; case: eqP; first by move => -> _; rewrite ndsF15; case /(Ngtge le1 hm). nextI k; case: eqP; first by move => -> _; rewrite ndsF16; case /(Ngtge le1 hn). lastI; rewrite ndsF17; case/(Ngtge le1 ho). Qed. Lemma ndsF18: (F 18 = C 5 * C 6 * C 6) %N. Proof. by move: ndsF18a; rewrite /FP ndsF13. Qed. Lemma ndsF18b: (F 18 = 3017169) %N. Proof. by rewrite ndsF18. Qed. Lemma ndsF18c: FP 18 6. Proof. by rewrite /FP ndsF12 ndsF18. Qed. Lemma ndsF19a: FP 19 6. Proof. have h0: 2 <= 19 by []. have h2: 0 < 6 < 19 by []. set f := 7189057%N. have ha: (C 18 * F 1 < f)%N by rewrite F1. have hb: (C 17 * C 1 < f)%N by []. have hc: (C 16 * C 2 < f)%N by []. have hd: (C 15 * C 3 < f)%N by []. have he: (C 14 * C 4 < f)%N by []. have hf: (C 13 * C 5 < f)%N by []. have hg: (C 12 * C 6 < f)%N by []. have hh: (C 11 * C 7 < f)%N by []. have hi: (C 10 * (C 4 * C 4) < f)%N by []. have hj: (C 9 * (C 4 * C 5) < f)%N by []. have hk: (C 8 * (C 5 * C 5) < f)%N by []. have hl: (C 7 * (C 5 * C 6) < f)%N by []. have hm: (C 5 * (C 4 * C 4 * C 5) < f)%N by []. have hn: (C 4 * (C 4 * C 5 * C 5) < f)%N by []. have ho: (C 3 * (C 5 * C 5 * C 5) < f)%N by []. have hp: (C 2 * (C 5 * C 5 * C 6) < f)%N by []. have hq: (C 1 * (C 5 * C 6 * C 6) < f)%N by []. rewrite /FP;move:(HF1 h0 h2);rewrite ndsF13 => le1. move:(HF2 h0) => [k]; rewrite ltnS (leq_eqVlt k) /FP. case: eqP; first by move => -> _; case /(Ngtge le1 ha). nextI k; case: eqP;first by move => -> _; rewrite ndsF2; case /(Ngtge le1 hb). nextI k; case: eqP; first by move => -> _; rewrite ndsF3; case /(Ngtge le1 hc). nextI k; case: eqP; first by move => -> _; rewrite ndsF4; case /(Ngtge le1 hd). nextI k; case: eqP; first by move => -> _; rewrite ndsF5; case /(Ngtge le1 he). nextI k; case: eqP; first by move => -> _; rewrite ndsF6; case /(Ngtge le1 hf). nextI k; case: eqP; first by move => -> _; rewrite ndsF7; case /(Ngtge le1 hg). nextI k; case: eqP; first by move => -> _; rewrite ndsF8; case /(Ngtge le1 hh). nextI k; case: eqP; first by move => -> _; rewrite ndsF9;case /(Ngtge le1 hi). nextI k; case: eqP; first by move => -> _; rewrite ndsF10;case /(Ngtge le1 hj). nextI k; case: eqP; first by move => -> _; rewrite ndsF11;case /(Ngtge le1 hk). nextI k; case: eqP; first by move => -> _; rewrite ndsF12;case /(Ngtge le1 hl). nextI k; case: eqP; first by move => -> _; rewrite ndsF13. nextI k; case: eqP; first by move => -> _; rewrite ndsF14; case /(Ngtge le1 hm). nextI k; case: eqP; first by move => -> _; rewrite ndsF15; case /(Ngtge le1 hn). nextI k; case: eqP; first by move => -> _; rewrite ndsF16; case /(Ngtge le1 ho). nextI k; case: eqP; first by move => -> _; rewrite ndsF17; case /(Ngtge le1 hp). lastI; rewrite ndsF18; case/(Ngtge le1 hq). Qed. Lemma ndsF19: (F 19 = C 6 * C 6 * C 6) %N. Proof. by move: ndsF19a; rewrite /FP ndsF13. Qed. Lemma ndsF19b: (F 19 = 7189057) %N. Proof. by rewrite ndsF19. Qed. Definition Gp p := ((C 5) ^ (bin_of_nat p))%N. Variable G: nat -> N. Hypothesis G0: G 0 = 1%N. Hypothesis G1: G 1 = 1%N. Hypothesis G2: G 2 = 2%N. Hypothesis G3: G 3 = 5%N. Hypothesis G4: G 4 = 13%N. Hypothesis G8: G 8 = 449%N. Hypothesis G9: G 9 = 1089%N. Hypothesis G14: G 14 = 88209%N. Hypothesis Gr0: forall p, G (5 * p + 5) = (Gp p * C 4 )%N. Hypothesis Gr1: forall p, G (5 * p + 1) = (Gp p)%N. Hypothesis Gr2: forall p, G (5 * p + 7) = (Gp p * C 6)%N. Hypothesis Gr3: forall p, G (5 * p + 13) = (Gp p * C 6 * C 6)%N. Hypothesis Gr4: forall p, G (5 * p + 19) = (Gp p * C 6 * C 6 * C 6)%N. Lemma Gp_rec p : (Gp p.+1 = C 5 * (Gp p) )%N. Proof. rewrite /Gp - (add1n p). have ha:= (nat_of_add_bin 1%N (bin_of_nat p)). move: (f_equal bin_of_nat ha); rewrite bin_of_natK nat_of_binK; move => <-. by rewrite N.pow_add_r N.pow_1_r. Qed. Lemma div_by5 n: exists p, (n = 5 * p \/ n = 5 * p +1 \/ n = 5 * p +2 \/ n = 5 * p + 3 \/ n = 5 * p + 4). Proof. elim:n; first by exists 0; left; rewrite muln0. move => n [p]; case; first by move => ->; exists p; right; left; rewrite addn1. case. by move => ->; exists p; right; right; left; rewrite - addn1 - addnA. case. by move => ->; exists p; right; right; right; left; rewrite - addn1 - addnA. case. by move => ->; exists p; right;right;right;right; rewrite - addn1 - addnA. move => ->; exists p.+1; left. rewrite mulnS (addnC 5) - addn1 - addnA //. Qed. Lemma Grec n: (G (n+15+5) = C 5 * G (n+15))%N. Proof. move: (div_by5 n) => [p pv]; case pv. move => ->; rewrite - {1} (mulnDr 5 p 3) (addnA (5*p) 10 5). by rewrite - {1} (mulnDr 5 p 2) Gr0 Gr0 N.mul_assoc - Gp_rec addnS. case. have pa: 5 * p + 1 + 15 + 5 = 5 *(p + 4) + 1 by rewrite mulnDr - !addnA. have pb: 5 * p + 1 + 15 = 5 *(p + 3) + 1 by rewrite mulnDr - !addnA. by move => ->; rewrite pa pb Gr1 Gr1 - Gp_rec addnS. case. have pa: 5 * p + 2 + 15 + 5 = 5 * (p + 3) + 7 by rewrite mulnDr - !addnA. have pb: 5 * p + 2 + 15 = 5 * (p + 2) + 7 by rewrite mulnDr - !addnA. by move => ->; rewrite pa pb Gr2 Gr2 N.mul_assoc - Gp_rec addnS. case. have pa: (5 * p + 3 + 15 + 5) = 5* (p +2) + 13 by rewrite mulnDr - !addnA. have pb: 5 * p + 3 + 15 = 5* (p +1) + 13 by rewrite mulnDr - !addnA. by move => ->; rewrite pa pb Gr3 Gr3 ! N.mul_assoc - Gp_rec addnS. have pa: (5 * p + 4 + 15 + 5) = (5 * (p + 1) + 19) by rewrite mulnDr - !addnA. move => ->. by rewrite pa - addnA Gr4 Gr4 ! N.mul_assoc - Gp_rec addnS addn0. Qed. Lemma FGreq1 n: n <= 19 -> F n = G n. Proof. rewrite (leq_eqVlt n); case: eqP. by move => -> _; rewrite (Gr4 0) ndsF19. nextI n; case: eqP; first by move => -> _; rewrite ndsF18 (Gr3 1). nextI n; case: eqP; first by move => -> _; rewrite ndsF17 (Gr2 2). nextI n; case: eqP; first by move => -> _; rewrite ndsF16 (Gr1 3). nextI n; case: eqP; first by move => -> _; rewrite ndsF15 (Gr0 2). nextI n; case: eqP; first by move => -> _; rewrite ndsF14 G14. nextI n; case: eqP; first by move => -> _; rewrite ndsF13 (Gr3 0). nextI n; case: eqP; first by move => -> _; rewrite ndsF12 (Gr2 1). nextI n; case: eqP; first by move => -> _; rewrite ndsF11 (Gr1 2). nextI n; case: eqP; first by move => -> _; rewrite ndsF10 (Gr0 1). nextI n; case: eqP; first by move => -> _; rewrite ndsF9 G9. nextI n; case: eqP; first by move => -> _; rewrite ndsF8 G8. nextI n; case: eqP; first by move => -> _; rewrite ndsF7 (Gr2 0). nextI n; case: eqP; first by move => -> _; rewrite ndsF6 (Gr1 1). nextI n; case: eqP; first by move => -> _; rewrite ndsF5 (Gr0 0). nextI n; case: eqP; first by move => -> _; rewrite ndsF4 G4. nextI n; case: eqP; first by move => -> _; rewrite ndsF3 G3. nextI n; case: eqP; first by move => -> _; rewrite ndsF2 G2. nextI n; case: eqP; first by move => -> _; rewrite F1 G1. by case n => //; rewrite F0 G0. Qed. End NdsNat. End NumberSums.