(** * Theory of Sets : Ordinals Copyright INRIA (2009-2013) Apics, Marelle Team (Jose Grimm). *) (* $Id: sset13.v,v 1.214 2016/04/07 16:44:23 grimm Exp$ *) Require Import ssreflect ssrfun ssrbool eqtype ssrnat. Require Export sset12. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Module Ordinals3. (** ** Cantor normal form *) (** Any ordinal is uniquely a sum of decreasing powers of omega *) Definition CNF_graph f := fgraph f /\ natp (domain f). Lemma CNF_domain0 X: CNF_graph X -> cardinal (domain X) = domain X. Proof. by move => [_ mN]; rewrite (card_nat mN). Qed. Lemma CNF_domain X: CNF_graph X -> domain X = Nint (cardinal (domain X)). Proof. by move => h; rewrite (CNF_domain0 h) (NintE (proj2 h)). Qed. Lemma CNF_domainP X: CNF_graph X -> forall i, (inc i (domain X) <-> i h i; apply: iff_sym;exact: (NltP (proj2 h)). Qed. Definition CNFrv0 (f:fterm) n := osum_expansion (fun i => (omega0 ^o (f i))) n. Definition CNFrv f := CNFrv0 (Vg f) (domain f). Definition CNFr_ax0 f n:= ord_below_n f n /\ (forall i, inc i Nat -> (csucc i) (f i) <=o (f (csucc i))). Definition CNFr_ax f:= [/\ CNF_graph f, (allf f ordinalp) & (forall i, inc i (domain f) -> inc (csucc i) (domain f) -> (Vg f i) <=o (Vg f (csucc i)))]. Lemma CNFr_ax_p1 f n: natp n -> CNFr_ax0 f n -> CNFr_ax (Lg n f). Proof. move => nN [ax1 ax2]. split; first by split; [fprops | bw]. by hnf; bw => x xd; bw; apply: ax1; apply /(NltP nN). bw; move => i i1 i2; bw. apply: ax2; [ exact:(NS_inc_nat nN i1) | by apply /(NltP nN)]. Qed. Lemma CNFr_ax_p2 f: CNFr_ax f -> CNFr_ax0 (Vg f) (domain f). Proof. move => [ax1 ax2 ax3]. split; first by move => i /(CNF_domainP ax1) idf; apply: ax2. move => i ib si. move: (cle_ltT (cleS ib) si) => /(CNF_domainP ax1) id1. by apply: ax3 => //; apply /(CNF_domainP ax1). Qed. Lemma CNFr_ax_p3 f n: natp n -> CNFr_ax0 f (csucc n) -> CNFr_ax0 f n. Proof. move => nN [ax1 ax2]; move: (cltS nN) => pa;split=> //. by move=> i lin; apply: ax1; apply:clt_ltT lin pa. move => i iN si; apply: ax2 => //;apply:clt_ltT si pa. Qed. Lemma CNFr_p1 f n: natp n -> CNFrv (Lg n f) = CNFrv0 f n. Proof. move => nN; rewrite /CNFrv Lg_domain. by apply: (osum_expansion_exten nN) => i lin; bw; apply/(NltP nN). Qed. Lemma OS_CNFr0 f n: natp n -> CNFr_ax0 f n -> ordinalp (CNFrv0 f n). Proof. move => nN [ax1 ax2];apply: (OS_osum_expansion nN) => i lin. exact: (OS_pow OS_omega (ax1 _ lin)). Qed. Lemma CNFr_p2 f n: natp n -> CNFr_ax0 f (csucc n) -> (omega0 ^o (f n)) <=o CNFrv0 f (csucc n). Proof. move => nN ax; move:(CNFr_ax_p3 nN ax) => axr. rewrite /CNFrv0 (osum_expansion_succ _ nN). have lt1:= (cltS nN). apply: osum_Mle0; last by apply: (OS_CNFr0 nN axr). exact: (OS_pow OS_omega (proj1 ax _ (cltS nN))). Qed. Lemma CNFr_p3 f n i: natp n -> CNFr_ax0 f n -> i omega0 ^o (f i) <=o CNFrv0 f n. Proof. move => nN ax lin. case (equal_or_not n \0c) => nz. by move: lin; rewrite nz=> /clt0. move: (cpred_pr nN nz) => [pN pv]; rewrite pv in ax. move: (CNFr_p2 pN ax); rewrite - pv => e1. have rec: forall j, \0c <=c j -> j omega0 ^o f (csucc j) <=o CNFrv0 f n -> omega0 ^o f j <=o CNFrv0 f n. move => j oj jln le1. have pa := (NS_lt_nat jln pN). have pb: csucc j CNFr_ax0 f (csucc n) -> f n CNFrv0 f (csucc n) nN ax lt1. suff: CNFrv0 f (csucc n) <=o (omega0 ^o (f n) *o (csucc n)). have sno: csucc n h; apply: (ole_ltT h). have [[cv _ _ ] _] := lt1. have op:= (omega_pow_pos cv). have: omega0 ^o f n *o csucc n h1; apply: (olt_leT h1). by apply: opow_Momega_le; apply /oleSltP. set p := f n. have: f n <=o p by exact:(oleR (proj31_1 lt1)). move: p; clear lt1 m. move: n nN f ax; apply: Nat_induction. move => f ax p hp. move:(OS_pow OS_omega (proj32 hp)) (OS_pow OS_omega (proj31 hp)) => ha hb. rewrite succ_zero (oprod1r ha) /CNFrv0 osum_expansion1 //. by apply:opow_Momega_le. move => n nN Hrec f ax m le1. have snN:=(NS_succ nN). have le2:=(opow_Momega_le le1). have h := (oleT (proj2 ax n nN (cltS snN)) le1). have le3:=(Hrec f (CNFr_ax_p3 snN ax) m h). move:(osum_Mlele le2 le3). rewrite {1}/CNFrv0 -(osum_expansion_succ (fun i => omega0 ^o f i) snN). have osn: ordinalp (csucc n) by apply: OS_cardinal; fprops. rewrite (osum_x_xy (OS_pow OS_omega (proj32 le1)) osn). by rewrite (osum2_2int NS1 snN) csumC - (Nsucc_rw snN). Qed. Lemma CNFr_p5 f: CNFrv0 f \0c = \0o. Proof. by rewrite /CNFrv0 osum_expansion0. Qed. Lemma CNFr_p6 f n: natp n -> CNFr_ax0 f n -> n <> \0c -> CNFrv0 f n <> \0o. Proof. move => nN ax nz rz. move: (cpred_pr nN nz) => [sa sb]. rewrite sb in ax rz. move:(CNFr_p2 sa ax); rewrite rz => /oleNgt; apply. exact: (omega_pow_pos (proj1 ax _ (cltS sa))). Qed. Lemma CNFr_unique1 f g n m: CNFr_ax0 f n -> CNFr_ax0 g m -> natp n -> natp m -> CNFrv0 f n = CNFrv0 g m -> (n = m /\ forall i, i f i = g i). Proof. move => p1 p2 p3 p4; move: n p3 m p1 p2 p4; apply: Nat_induction. move => m af ag mN sv; split; last by move => i /clt0 h; case h. symmetry;ex_middle bad. by move: (CNFr_p6 mN ag bad); rewrite - sv CNFr_p5; case. move => n nN Hrec m af ag mN sv. case: (equal_or_not m \0c) => mz. by move: (CNFr_p6 (NS_succ nN) af (@succ_nz n)); rewrite sv mz CNFr_p5; case. move: (cpred_pr mN mz); set m':= (cpred m); move => [m'N mv]. rewrite mv in ag sv. move: (CNFr_ax_p3 nN af) (CNFr_ax_p3 m'N ag) => ax1 ax2. move: sv (CNFr_p4 nN af (m:= g m')) (CNFr_p4 m'N ag (m:= f n)). move:(CNFr_p2 nN af) (CNFr_p2 m'N ag). rewrite /CNFrv0 (osum_expansion_succ _ nN)(osum_expansion_succ _ m'N). rewrite -/(CNFrv0 _ _) -/(CNFrv0 _ _). move => le1 le2 eq1 lt1 lt2. move: (cltS nN) (cltS m'N) => ns1 ns2. case (oleT_ell (proj1 af _ ns1) (proj1 ag _ ns2)). + move => eq2. rewrite eq2 in eq1. move: (osum2_simpl (OS_CNFr0 nN ax1) (OS_CNFr0 m'N ax2) (proj31 le2) eq1). move / (Hrec m' ax1 ax2 m'N)=> [ra rb]. rewrite mv -ra; split; [ reflexivity | move => i /(cltSleP nN) li]. case (equal_or_not i n); first by move => ->; rewrite eq2 ra. by move => ni; apply:rb; split. + move /lt1; rewrite eq1 => /(oleNgt le2); case. + by move /lt2; rewrite - eq1 => /(oleNgt le1); case. Qed. Lemma CNFr_unique f g: CNFr_ax f -> CNFr_ax g -> CNFrv f = CNFrv g -> f = g. Proof. move => af ag sv; rewrite /CNFrv. move:(af)(ag) => [[fgf nN] _ _ ][[fgg mN] _ _]. move: (CNFr_ax_p2 af) (CNFr_ax_p2 ag) => ax1 ax2. move:(CNFr_unique1 ax1 ax2 nN mN sv) => [sa sb]. by apply: (fgraph_exten fgf fgg sa) => i /(NltP nN) id; apply: sb. Qed. Lemma CNFr_exists x: ordinalp x -> exists2 f, CNFr_ax f & x = CNFrv f. Proof. move => ox. suff: exists f n, [/\ natp n, CNFr_ax0 f n & x = CNFrv0 f n]. move => [f [n [pa pb pc]]]. move: (CNFr_ax_p1 pa pb) (CNFr_p1 f pa); rewrite - pc => pd pe. by exists (Lg n f); [ exact | symmetry]. pose p x := exists f n, [/\ natp n, CNFr_ax0 f n & x = CNFrv0 f n]. apply: (least_ordinal2 (p:=p)) ox => y oy p2. case: (ozero_dichot oy) => yp. exists (@id Set), \0c; split; [ exact: NS0 | | by rewrite CNFr_p5 yp]. split => i; [ move /clt0; case | move => _ /clt0; case]. move: (ord_ext_div_exists ole_2omega yp) =>[e1 [c1 [rm [oe1 oc1 or [eq1 lt1 lt2 lt3]]]]]. move: (ord_rev_pred lt3); set c2 := (c1 -o \1o); move => [oc2 eql]. have eql2: c1 = c2 +o \1o. move: (osum_M0le OS1 oc2);rewrite - eql => h; move: (ole_ltT h lt2) => aa. have c2N: natp c2. apply:(olt_i aa). by move: eql; rewrite (osum2_2int NS1 c2N) csumC - (osum2_2int c2N NS1). set q := (omega0 ^o e1); set rm1 := ((q *o c2) +o rm). have oq:= proj32_1 lt1. have op2: ordinalp (q *o c2) by fprops. have orm1: ordinalp rm1 by rewrite /rm1; fprops. move: OS_omega OS1 => oo o1. have yv1: y = q +o rm1 by rewrite eq1 eql oprodD // oprod1r // /rm1 osumA. have pv2: q *o c1 = (q *o c2) +o q by rewrite eql2 oprodD // oprod1r //. have yv2: y = (q *o c2) +o (q +o rm) by rewrite eq1 pv2 osumA //. have rmy: rm1 //. rewrite /rm1 yv2 => eq3. move: (osum_Mle0 oq or);rewrite - (osum2_simpl or (OS_sum2 oq or) op2 eq3). by move => /(oleNgt) []. move:(p2 _ rmy) => [f [n [nN p4 p5]]]. have snb:= (NS_succ nN). pose g z:= (Yo (z = n) e1 (f z)). have yv3: y = CNFrv0 g (csucc n). rewrite /CNFrv0 (osum_expansion_succ _ nN) /g yv1; Ytac0; congr (osum2). by rewrite p5;apply: (osum_expansion_exten nN) => i [_ lin]; Ytac0. have ax2:CNFr_ax0 g (csucc n). split. move => i; rewrite /g; Ytac ein => //. by move/(cltSleP nN) => lin; apply:(proj1 p4). move => i iN h; rewrite /g. move/(cltSleP nN): h => sin. Ytac ein; first by move: (cltS nN); rewrite - {2} ein => /(cleNgt sin). Ytac sein; last by apply:(proj2 p4). move: (cltS iN); rewrite sein => lin. case:(oleT_el (proj1 p4 _ lin) oe1)=> // /oleSltP/opow_Momega_le sb. have aux: omega0 ^o (f i) <=o rm1 by rewrite p5;apply:(CNFr_p3 nN p4 lin). move: (osum_Meqlt lt1 op2); rewrite - pv2 => lt6. move:(oprod_Meqle (proj1 lt2) oq) => le5. move: (olt_leT lt6 le5); rewrite /q - (opow_succ oo oe1) -/rm1 => sc. case: (oleNgt sb (ole_ltT aux sc)). by exists g,(csucc n). Qed. Definition ord_negl a b := a +o b = b. Notation "x < ordinalp b -> a < ((a = \0o /\ b = \0o) \/ (a oa ob abz. case: (equal_or_not b \0o) => bz. by move: abz; rewrite bz (osum0r oa); left. right; split; first by rewrite -abz; apply: osum_Mle0. dneg ab; rewrite ab in abz; apply: (osum_a_ab ob ob abz). Qed. Lemma ord_negl_sum a b c: ordinalp a -> ordinalp b -> ordinalp c -> a < a < oa ob oc h; rewrite osumA // h. Qed. Lemma ord_negl_prod a b c: ordinalp a -> ordinalp b -> \0o a < a < oa ob cnz lab. move: (ord_rev_pred cnz) => [oy ->]. rewrite (oprodD OS1 oy ob) (oprod1r ob). by apply: ord_negl_sum => //; fprops. Qed. Lemma ord_negl_sum1 a b c: ordinalp a -> ordinalp b -> ordinalp c -> a < b < (a +o b) < oa ob oc p1 p2; by rewrite - osumA // p2 p1. Qed. Lemma ord_negl_sum2 a b c: ordinalp a -> ordinalp b -> ordinalp c -> (a +o b) < (a < oa ob oc. rewrite - (osumA oa ob oc) => h. suff: b +o c = c by move => h1; rewrite -{2} h h1. apply:oleA (osum_M0le ob oc). by move: (osum_M0le oa (OS_sum2 ob oc)); rewrite h. Qed. Lemma ord_negl_sum3 a b c: ordinalp c -> a <=o b -> b < a < oc h1; move: (h1) => [oa _ _]. by move: (odiff_pr h1) => [od -> /(ord_negl_sum2 oa od oc) []]. Qed. Lemma ord_neg_sum4 a b: ordinalp a -> ordinalp b -> a < a < oa ob; apply: osum2_simpl; fprops. Qed. Lemma ord_negl_p1 b: b b < oo bo. exact: (indecomp_prop1 indecomp_omega bo). Qed. Lemma ofinite_plus_infinite x y: finite_o x -> ordinalp y -> infinite_o y -> x +o y = y. Proof. move: OS_omega=> oo ha hb hc. move /omega_P2: (ha) => /(oltP oo) /ord_negl_p1 hd. have: omega0 <=o y by split => //; apply/(omega_P1 hb). move /odiff_pr => [he ->]; exact: (ord_negl_sum (proj1 ha) oo he hd). Qed. Lemma ord_negl_p2 b e: b \0o b < oo o1 bo ne0. move: (ord_rev_pred ne0) => [oy ->]. have ob:= proj31_1 bo. have ooy: ordinalp (omega0 ^o (e -o \1o)) by fprops. rewrite (opow_sum oo o1 oy) (opowx1 oo). by apply: ord_negl_prod => //;[ apply: omega_pow_pos | by apply: ord_negl_p1]. Qed. Lemma ord_negl_p3 b e d: b \0o \0o b < bo ne0 nd0. have ob:=(proj31_1 bo). have oe:=(proj32_1 ne0). have aux:=(ord_negl_p2 bo ne0). apply: ord_negl_prod => //; fprops. Qed. Lemma ord_negl_p4 a b: a (omega0 ^o a) < ox ltab. have leac:=proj1 ltab. have [odi pa]:= (odiff_pr leac). have dp:= (odiff_pos ltab). have ora:= proj31 leac. have oa1: ordinalp (omega0 ^o a) by fprops. have oa2: ordinalp (omega0 ^o (b -o a)) by fprops. rewrite pa (opow_sum ox ora odi) /ord_negl osum_x_xy //. congr (_ *o _); apply: ord_negl_p2 => //; apply: olt_1omega. Qed. Lemma ord_negl_p5 e c e' c': c e \0o ((omega0 ^o e) *o c) < ox ltco ltee' cnz /=. have leee':= proj1 ltee'. have [odi pa]:= (odiff_pr leee'). have orc:= proj31_1 ltco. have ore:= proj31_1 ltee'. have oc':= proj32_1 cnz. set x:= omega0. have oa1:= OS_pow ox ore. have oa2:= OS_pow ox odi. have oa3:= OS_prod2 oa2 oc'. have ->: ((x ^o e') *o c') = (x ^o e) *o ( (x ^o (e' -o e)) *o c'). rewrite oprodA // - (opow_sum ox ore odi) - pa //. rewrite /ord_negl - oprodD //. by congr (_ *o _); apply: ord_negl_p3 => //; apply: odiff_pos. Qed. Lemma ord_negl_p6 e f n: natp n -> CNFr_ax0 f (csucc n) -> e (omega0 ^o e) < oo nN h ef. have [[oe op _] _] :=ef. have o1:= OS_pow oo oe. have o2:= OS_pow oo op. have lt1:= (ord_negl_p4 ef). rewrite /CNFrv0 (osum_expansion_succ _ nN); apply: ord_negl_sum => //. exact:(OS_CNFr0 nN (CNFr_ax_p3 nN h)). Qed. Lemma ord_negl_pg (f:fterm) n (g:fterm) m: natp n -> CNFr_ax0 f (csucc n) -> natp m -> CNFr_ax0 g (csucc m) -> (g m CNFrv0 g (csucc m) < nN cf mN cg; split. move: m mN cg;apply: Nat_induction. rewrite succ_zero {1} /CNFrv0=> ax1 lt1. have h:= (OS_pow OS_omega(proj31_1 lt1)). rewrite (osum_expansion1)//; exact:(ord_negl_p6 nN cf lt1). move => m mN Hrec cdg ltspd. move: OS_omega (NS_succ mN) => oo smN. rewrite {1} /CNFrv0 (osum_expansion_succ _ smN). have ax2:= (CNFr_ax_p3 smN cdg). have o1:= (OS_pow oo (proj1 cdg _ (cltS smN))). apply:(ord_negl_sum1 o1 (OS_CNFr0 smN ax2) (OS_CNFr0 (NS_succ nN) cf)). apply: (ord_negl_p6 nN cf ltspd). apply: Hrec => //. exact : (ole_ltT (proj2 cdg m mN (cltS smN)) ltspd). rewrite {1}/CNFrv0 (osum_expansion_succ _ mN) => t2. have ax2:= (CNFr_ax_p3 mN cg). have o0:= (proj1 cg _ (cltS mN)). have o2:= (proj1 cf _ (cltS nN)). have o1:= (OS_pow OS_omega o0). have sa:= (CNFr_p2 nN cf). move: (proj1 (ord_negl_sum2 o1 (OS_CNFr0 mN ax2) (proj32 sa) t2)) => le1 {t2}. case:(ord_negl_lt o1 (proj32 sa) le1);[ move => [] | move => lt0]. by move:(omega_pow_nz o0). case:(oleT_ell o0 o2) => // le2; last first. case:(oltNge lt0 (proj1 (CNFr_p4 nN cf le2))). rewrite le2 in le1 lt0. apply:False_ind. move: nN cf le1 lt0; clear; move => nb; move: n nb. apply: Nat_induction. rewrite succ_zero => h1 _. have ha:= (OS_pow OS_omega (proj1 h1 \0o clt_01)). by rewrite /CNFrv0 osum_expansion1 //; move => []. move => n nN Hrec ax1. have snN:= (NS_succ nN). rewrite /CNFrv0 (osum_expansion_succ _ snN) -/(CNFrv0 _ _) => ha hb. have ax2:= (CNFr_ax_p3 snN ax1). have o0:= (proj1 ax1 _ (cltS snN)). have o1:= (OS_pow OS_omega o0). have o3 := (OS_CNFr0 snN ax2). have hc :=(ord_neg_sum4 o1 o3 ha). have le0:= (proj2 ax1 _ nN (cltS snN)). have le1:= (opow_Momega_le le0). move: (ord_negl_sum3 o3 le1 hc) => pra. case: (ord_negl_lt (proj31 le1) o3 pra); last by move /(Hrec ax2 pra). by move:(omega_pow_nz (proj1 ax2 _ (cltS nN))) => h1 []. Qed. Lemma cantor_of_limit x: limit_ordinal x -> exists a n, [/\ ordinalp a, ordinalp n, n <> \0o, x = a +o (omega0 ^o n) & (a = \0o \/ [/\ limit_ordinal a, (omega0 ^o n) <=o a & cardinal x = cardinal a])]. Proof. move/limit_ordinal_P => [xnz lx]. move: (CNFr_exists (proj32_1 xnz)) => [X ax xv]. move: (CNFr_ax_p2 ax) (proj2 (proj31 ax)); set n := domain X;move => ax1 nN. case: (equal_or_not n \0c) => nz. by case: xnz; rewrite xv /CNFrv /CNFrv0 -/n nz osum_expansion0. have cn1: \1c <=c n by apply: cge1; fprops. move : (cdiff_pr cn1) (NS_diff \1c nN); set m := _ -c _ => nv mN. set f1 := (fun i => omega0 ^o Vg X i). have ha: ord_below_n f1 (\1c +c m). move => i; rewrite nv => lin; apply:(OS_pow OS_omega (proj1 ax1 _ lin)). have hb: ordinalp (Vg X \0c) by apply:(proj1 ax1); apply/strict_pos_P1. have hc:= (OS_pow OS_omega hb). move: xv; rewrite /CNFrv /CNFrv0 -/n -nv. rewrite (osum_expansionA NS1 mN ha) (osum_expansion1 (f := f1) hc) {2} /f1. rewrite -/(CNFrv0 _ _); set f2:= (fun i : Set => Vg X (i +c \1c)). have ax3: CNFr_ax0 f2 m. split. move => i im; apply: (proj1 ax1); rewrite - nv (csumC \1c). apply:csum_Mlteq; fprops. move => i iN sim. have eq: (csucc i +c \1c) = csucc (i +c \1c) by rewrite (csum_Sn _ iN). rewrite /f2 eq; apply:(proj2 ax1); first by apply:(NS_sum iN NS1). rewrite - nv (csumC \1c) - eq; apply:csum_Mlteq; fprops. move:(OS_CNFr0 mN ax3); set a := CNFrv0 f2 m => oa. case (equal_or_not (Vg X \0o) \0o)=> ez. rewrite ez opowx0 (osucc_pr oa) => xsa. by move:(oltS oa); rewrite -xsa; move/lx => []; rewrite - xsa. exists a,(Vg X \0c);split => //. case: (equal_or_not m \0c) => mz. by left; rewrite /a mz /CNFrv0 osum_expansion0. have cm1: \1c <=c m by apply: cge1; fprops. move : (cdiff_pr cm1) (NS_diff \1c mN); set m' := _ -c _ => mv m'N. set f1' := (fun i => omega0 ^o (f2 i)). have oo1:ordinalp (f1' \0c). by apply: (OS_pow OS_omega);apply:(proj1 ax3); apply/strict_pos_P1. have ha': ord_below_n f1' (\1c +c m'). move => i il; apply: (OS_pow OS_omega); apply: (proj1 ax3); ue. have sn0:csucc \0c [_ /ozero_least h2 _]. move => b; case ez;rewrite - b in ez0; exact: (ole0 ez0). move:(osum_expansionA NS1 m'N ha'); rewrite mv -/(CNFrv0 _ _) -/a. rewrite (osum_expansion1 oo1); rewrite /f1' /f2 (csum0l CS1) => eq2. have ax4: CNFr_ax0 (fun z : Set => Vg X ((z +c \1c) +c \1c)) m'. split. move => i im; apply: (proj1 ax3); rewrite - mv (csumC \1c). apply:csum_Mlteq; fprops. move => i iN sim. have eq: (csucc i +c \1c) = csucc (i +c \1c) by rewrite (csum_Sn _ iN). rewrite /f2 eq; apply:(proj2 ax3); first by apply:(NS_sum iN NS1). rewrite - mv (csumC \1c) - eq; apply:csum_Mlteq; fprops. have sa:= (OS_CNFr0 m'N ax4). have sb:= (opow_Momega_le ez0). have la: limit_ordinal a. rewrite eq2;exact:(osum_limit sa (indecomp_limit2 ez')). have le3: omega0 ^o Vg X \0c <=o a. rewrite eq2; apply: (oleT sb); apply: (osum_M0le sa (proj32 sb)). right; split => //. rewrite xv (osum_cardinal oa hc). move: (ocle1 le3) => pc. have pb: omega0 <=o omega0 ^o (Vg X \0c). rewrite - {1} (opowx1 OS_omega); apply: opow_Momega_le; fprops. move: (ocle1 (oleT pb le3)). rewrite (card_card CS_omega) => pd. by apply: csum_inf => //; apply: (ge_infinite_infinite CIS_omega). Qed. (** ** General Cantor Normal Form *) Definition cantor_mon b (e c: fterm) i := (b ^o (e i)) *o (c i). Definition CNFbv b (e c:fterm) n := osum_expansion (cantor_mon b e c) n. Definition CNFq_ax b (e c: fterm) n := [/\ \2o <=o b, ord_below_n e n, (forall i, i c i (csucc i) (e i) \0o same_below c1 c2 n -> CNFq_ax b e1 c1 n -> CNFq_ax b e2 c2 n. Proof. move => h1 h2 [a1 a2 a3 a4]; split => //. + by move => i lin; rewrite - (h1 _ lin);apply: a2. + by move => i lin; rewrite - (h2 _ lin);apply: a3. + move => i iN lin; rewrite - (h1 _ lin). by rewrite -(h1 _ (cle_ltT (cleS iN) lin)); apply:a4. Qed. Lemma CNFb_ax_exten b e1 c1 e2 c2 n: same_below e1 e2 n -> same_below c1 c2 n -> CNFb_ax b e1 c1 n -> CNFb_ax b e2 c2 n. Proof. move => h1 h2 [ax1 ax2]; split; first by apply:(CNFq_ax_exten h1 h2 ax1). by move => i lin; rewrite - (h2 _ lin);apply: ax2. Qed. Lemma CNFq_exten b e1 c1 e2 c2 n: same_below e1 e2 n -> same_below c1 c2 n -> CNFq_ax b e1 c1 n -> natp n -> (CNFq_ax b e2 c2 n /\ CNFbv b e1 c1 n = CNFbv b e2 c2 n). Proof. move => h1 h2 ax nN; split; first by apply: (CNFq_ax_exten h1 h2 ax). apply: (osum_expansion_exten nN) => i lin. by rewrite /cantor_mon (h1 _ lin) (h2 _ lin). Qed. Lemma CNFb_exten b e1 c1 e2 c2 n: same_below e1 e2 n -> same_below c1 c2 n -> CNFb_ax b e1 c1 n -> natp n -> (CNFb_ax b e2 c2 n /\ CNFbv b e1 c1 n = CNFbv b e2 c2 n). Proof. move => h1 h2 [ax1 ax2] nN. move: (CNFq_exten h1 h2 ax1 nN) => [ax3 ->]; split => //; split => //. by move => i lin; rewrite - (h2 _ lin);apply: ax2. Qed. Lemma CNFq_p0 b e c n i: CNFq_ax b e c n -> i ordinalp (cantor_mon b e c i). Proof. move => [pa pb pc pd] lin. apply:OS_prod2; first by apply:(OS_pow (proj32 pa) (pb _ lin)). exact:(proj31_1 (pc _ lin)). Qed. Lemma OS_CNFq b e c n : natp n -> CNFq_ax b e c n -> ordinalp (CNFbv b e c n). Proof. by move => nb h; apply:(OS_osum_expansion nb) => i /(CNFq_p0 h). Qed. Lemma OS_CNFb b e c n : natp n -> CNFb_ax b e c n -> ordinalp (CNFbv b e c n). Proof. by move => nN [/(OS_CNFq nN) h _]. Qed. Lemma CNFq_p1 b e c n: natp n -> CNFbv b e c (csucc n) = cantor_mon b e c n +o (CNFbv b e c n). Proof. by move => nN; rewrite /CNFbv (osum_expansion_succ _ nN). Qed. Lemma CNFq_p2 b e c: CNFbv b e c \0c = \0o. Proof. apply: osum_expansion0. Qed. Lemma CNFq_p3 b e c n : CNFq_ax b e c n -> \0o CNFbv b e c \1c = cantor_mon b e c \0c. Proof. move => h np;apply: osum_expansion1; apply: (CNFq_p0 h np). Qed. Lemma CNFq_p4 b e c n i: CNFb_ax b e c n -> i \0o [[pa pb pc pd] pe] lin. apply: oprod2_pos; last by exact(pe _ lin). exact:(opow_pos (olt_leT (olt_02) pa) (pb _ lin)). Qed. Lemma CNFq_r_ax b e c n m: CNFq_ax b e c n -> m <=c n -> CNFq_ax b e c m. Proof. move => [p1 p2 p3 p4] mn; split. + done. + move => i im; apply: p2;exact: (clt_leT im mn). + move => i im; apply: p3;exact: (clt_leT im mn). + move => i iN im; apply: p4 => //; exact(clt_leT im mn). Qed. Lemma CNFb_r_ax b e c n m: CNFb_ax b e c n -> m <=c n -> CNFb_ax b e c m. Proof. move => [p1 p2] mn; split; first by exact: (CNFq_r_ax p1 mn). move => i im; apply: p2; exact:(clt_leT im mn). Qed. Lemma CNFq_p5 b e c n: natp n -> CNFq_ax b e c (csucc n) -> CNFq_ax b e c n. Proof. by move => nN ax; apply:(CNFq_r_ax ax (cleS nN)). Qed. Lemma CNFb_p5 b e c n: natp n -> CNFb_ax b e c (csucc n) -> CNFb_ax b e c n. Proof. by move => nN ax; apply:(CNFb_r_ax ax (cleS nN)). Qed. Lemma CNF_exponents_M b e c n: natp n -> CNFq_ax b e c n -> forall i j, i <=c j -> j e i <=o e j. Proof. move => nN [_ pb _ pc] i j lij ljn. have lin:=(cle_ltT lij ljn). have iN := (NS_lt_nat lin nN). pose r j := e i <=o e j. have ri:=(oleR (pb _ lin)). case: (equal_or_not n \0c) => nz. by move: lin; rewrite nz; move /clt0. move: (cpred_pr nN nz) => [mN mv]. have jcn: j <=c cpred n by apply /(cltSleP mN); rewrite -mv. move: (Nat_induction3 (r := r) iN mN ri)=> h. apply: (h _ j lij jcn) => k ik kn; rewrite /r => le1. have kN:= (NS_lt_nat kn mN). have skn : csucc k [ /(oleT le1) ]. Qed. Lemma CNF_exponents_sM b e c n: natp n -> CNFq_ax b e c n -> forall i j, i j e i nN ax i j lij ljn. have iN := (NS_lt_nat (clt_ltT lij ljn) nN). move /(cleSltP iN) :lij => leij. have sa:=(CNF_exponents_M nN ax leij ljn). move: ax => [_ _ _ ax]; exact: (olt_leT (ax i iN (cle_ltT leij ljn)) sa). Qed. Lemma CNF_exponents_I b e c n: natp n -> CNFq_ax b e c n -> forall i j, i j e i = e j -> i = j. Proof. move => nN /(CNF_exponents_sM nN) => m i j lin ljn eq. case: (cleT_ell (proj31_1 lin) (proj31_1 ljn)) => cp. + exact. + by move: (proj2 (m i j cp ljn)); rewrite eq. + by move: (proj2 (m j i cp lin)); rewrite eq. Qed. Lemma CNFq_p6 b e c n: natp n -> CNFq_ax b e c (csucc n) -> forall i, i e i nN ax i lin. exact:(CNF_exponents_sM (NS_succ nN) ax lin (cltS nN)). Qed. Lemma CNFq_p7 b e c n : CNFq_ax b e c n -> \1c CNFbv b e c \2c = cantor_mon b e c \1c +o cantor_mon b e c \0c. Proof. move=> ax n1; move:(cle_ltT cle_01 n1) => ha. by rewrite - succ_one (CNFq_p1 _ _ _ NS1) (CNFq_p3 (n:=n) ax). Qed. Lemma CNFb_p8 b e c n : CNFb_ax b e c (csucc n) -> natp n -> ordinalp (e n). Proof. move => [[_ h _ _] _] nN; exact: (h _ (cltS nN)). Qed. Definition cnf_s (f: fterm) k := (fun z => f (z +c k)). Definition cnf_m (f1 f2:fterm) k := (fun z => Yo (z Yo (z=n) x (f z)). Lemma CNFq_s_ax b e c n k m: CNFq_ax b e c m -> (n +c k) <=c m -> natp k -> natp n -> CNFq_ax b (cnf_s e k) (cnf_s c k) n. Proof. move => [p1 p2 p3 p4] mn kN nN. have aux: forall i, i i +c k i lin; move:(clt_leT(csum_Mlteq kN lin) mn). split. + done. + by move => i /aux /p2. + by move => i /aux /p3. + move => i iN /aux; rewrite /cnf_s (csum_Sn _ iN); apply: p4; fprops. Qed. Lemma CNFb_s_ax b e c n k m: CNFb_ax b e c m -> (n +c k) <=c m -> natp k -> natp n -> CNFb_ax b (cnf_s e k) (cnf_s c k) n. Proof. move => [p1 p2] mn kN nN; split; first by apply: (CNFq_s_ax p1 mn kN nN). by move => i lin; apply: p2; move:(clt_leT (csum_Mlteq kN lin) mn). Qed. Lemma CNFq_m_ax b e1 c1 e2 c2 k m: natp k -> natp m -> CNFq_ax b e1 c1 k -> CNFq_ax b e2 c2 m -> (m = \0c \/ e1 (cpred k) (CNFq_ax b (cnf_m e1 e2 k) (cnf_m c1 c2 k) (k +c m)). Proof. move => kN mN [p1 p2 p3 p4] [q1 q2 q3 q4] hs. have aux: forall i, i i i lik. move:(NS_lt_nat lik (NS_sum kN mN))=> iN. case: (cleT_el (CS_nat kN) (CS_nat iN)); last by left. move => ki; move: (cdiff_pr ki) => s1. right; split; first by move=> /(cleNgt ki). apply: (csum_lt2l kN (NS_diff k iN) mN); ue. rewrite/cnf_m; split. + done. + move => i /aux []; first by move => ik;by Ytac0; apply: p2. by move => [nik likm]; Ytac0; apply: q2. + move => i /aux []; first by move => ik;by Ytac0; apply: p3. by move => [nik likm]; Ytac0; apply: q3. + move => i iN lis; case:(aux _ lis). move => lt1; move: (cle_ltT (cleS iN) lt1) => li1. by Ytac0; Ytac0; apply:p4. move => [pa pb]; Ytac0. case: hs => hs; first by move: pb; rewrite hs => /clt0. have ci:= (CS_nat iN). have ck:= (CS_nat kN). case: (cleT_ell ck (CS_succ i)) => //. move:(cltS iN) => lt1 sa; rewrite sa cdiff_nn; Ytac0. have -> //: i = cpred k by rewrite sa cpred_pr1. move => /(cltSleP iN) ki. case: (aux _ (cle_ltT (cleS iN) lis)); first by move => /(cleNgt ki). move => [pc pd]; Ytac0. have sa: csucc i -c k = csucc (i-c k). move: (cdiff_pr4 kN iN NS0 NS1 ki cle_01). rewrite (csucc_pr4 ci) (csum0r ck) (cdiff_n0 NS1) csucc_pr4 //. exact: (proj31_1 pd). rewrite sa; apply: (q4 _ (NS_diff k iN)); ue. Qed. Lemma CNFb_m_ax b e1 c1 e2 c2 k m: natp k -> natp m -> CNFb_ax b e1 c1 k -> CNFb_ax b e2 c2 m -> (m = \0c \/ e1 (cpred k) (CNFb_ax b (cnf_m e1 e2 k) (cnf_m c1 c2 k) (k +c m)). Proof. move => kN mN [p1 p2] [p3 p4] h1. split; first by apply:CNFq_m_ax. have aux: forall i, i i i lik. move:(NS_lt_nat lik (NS_sum kN mN))=> iN. case: (NleT_el kN iN); last by left. move => ki; move: (cdiff_pr ki) => s1. right; split; first by move=> /(cleNgt ki). apply: (csum_lt2l kN (NS_diff k iN) mN); ue. move => i /aux []; first by move => ik;by rewrite /cnf_m; Ytac0; apply: p2. by move => [nik likm]; rewrite /cnf_m; Ytac0; apply: p4. Qed. Lemma CNF_change_n_ax b e c n c0 k: \0o c0 CNFb_ax b e c n -> CNFb_ax b e (cnf_change_n c k c0) n. Proof. move => c1 c2 [[p1 p2 p3 p4] p5]; rewrite/cnf_change_n. split; [split => // |]; move => i lin; Ytac cc => //; fprops. Qed. Definition CNFb_axo := CNFb_ax omega0. Definition CNFbvo := CNFbv omega0. Lemma CNFb_change_nv e c n m (c':= (cnf_change_n c n (m +o (c n)))): natp n -> CNFb_axo e c (csucc n) -> m (CNFb_axo e c' (csucc n) /\ CNFbvo e c' (csucc n) = omega0 ^o (e n) *o m +o CNFbvo e c (csucc n)). Proof. move => nN ax mo. have nn:= cltS nN. have om:=proj31_1 mo. move: (ax) => [ [_ a0 a1 _] a2]. move: (a2 _ nn) => [[_ ocn _] nnz]. have pa:= (osum2_lt_omega mo (a1 _ nn)). have pb: \0o h; move:(osum2_zero om ocn h) => [_ ]; apply: nesym. move: (CNF_change_n_ax n pb pa ax); rewrite -/c' => ax2; split; first by exact. have pc:= (OS_pow OS_omega (a0 _ nn)). have pd:= CNFq_p0 (proj1 ax) nn. have pe:=(OS_CNFq nN (CNFq_p5 nN (proj1 ax))). rewrite /CNFbvo. rewrite ! (CNFq_p1 _ _ _ nN) (osumA (OS_prod2 pc om) pd pe); apply: f_equal2. rewrite /cantor_mon /c' /cnf_change_n; Ytac0. by rewrite (oprodD om ocn pc). apply: (osum_expansion_exten nN) => i [_ lin]. by rewrite /cantor_mon /c' /cnf_change_n; Ytac0. Qed. Lemma CNFq_A b e c n m: natp n -> natp m -> CNFq_ax b e c (n +c m) -> [/\ CNFq_ax b e c n, CNFq_ax b (cnf_s e n) (cnf_s c n) m & CNFbv b e c (n +c m) = CNFbv b (cnf_s e n) (cnf_s c n) m +o CNFbv b e c n]. Proof. move => nN mN ax. have pa: ord_below_n (cantor_mon b e c) (n +c m). by move => i; apply:CNFq_p0. rewrite /CNFbv (osum_expansionA nN mN pa). have lt1: n <=c n +c m by apply:csum_M0le; fprops. have hb: CNFq_ax b e c n by apply:(CNFq_r_ax ax lt1). have hc //: CNFq_ax b (cnf_s e n) (cnf_s c n) m. have hh:m +c n <=c n +c m by rewrite csumC; exact: (cleR (proj32 lt1)). exact:(CNFq_s_ax ax hh nN mN). Qed. Lemma CNFb_A e c n m: natp n -> natp m -> CNFb_axo e c (n +c m) -> [/\ CNFb_axo e c n, CNFb_axo (cnf_s e n) (cnf_s c n) m & CNFbvo e c (n +c m) = CNFbvo (cnf_s e n) (cnf_s c n) m +o CNFbvo e c n]. Proof. move => nN mN ax. rewrite /CNFb_axo /CNFbvo. have pa: ord_below_n (cantor_mon omega0 e c) (n +c m). by move:ax => [ax _] i; apply:CNFq_p0. rewrite /CNFbv (osum_expansionA nN mN pa). have lt1: n <=c n +c m by apply:csum_M0le; fprops. have hb: CNFb_ax omega0 e c n by apply:(CNFb_r_ax ax lt1). rewrite csumC in pa. have hc //: CNFb_ax omega0 (cnf_s e n) (cnf_s c n) m. have hh:m +c n <=c n +c m. rewrite csumC;apply: (cleR (proj32 lt1)). exact:(CNFb_s_ax ax hh nN mN). Qed. Lemma CNFq_Al b e c n (e1 := fun z => e (csucc z)) (c1 := fun z => c (csucc z)): natp n -> CNFq_ax b e c (csucc n) -> [/\ ordinalp(cantor_mon b e c \0c), CNFq_ax b e1 c1 n & CNFbv b e c (csucc n) = CNFbv b e1 c1 n +o (cantor_mon b e c \0c)]. Proof. move => nN ax. have h1: forall i, i (cnf_s e \1c) i = e1 i. move => i lin; rewrite /cnf_s /e1 csucc_pr4 //; exact (proj31_1 lin). have h2: forall i, i (cnf_s c \1c) i = c1 i. move => i lin; rewrite /cnf_s /c1 csucc_pr4 //; exact (proj31_1 lin). have eq1: csucc n = \1c +c n by rewrite csumC; exact:(Nsucc_rw nN). rewrite eq1 in ax; move: (CNFq_A NS1 nN ax) => [sa sb sc]. have lt1: \0c [ax1 ->]; split => //. by apply:(CNFq_p0 ax lt1). Qed. Lemma CNFb_Al e c n (e1 := fun z => e (csucc z)) (c1 := fun z => c (csucc z)): natp n -> CNFb_axo e c (csucc n) -> [/\ ordinalp(cantor_mon omega0 e c \0o), CNFb_axo e1 c1 n & CNFbvo e c (csucc n) = CNFbvo e1 c1 n +o (cantor_mon omega0 e c \0o)]. Proof. move => nN [ax1 ax2]; move:(CNFq_Al nN ax1) => [sa sb sc]; split => //. split => // i lin; apply: ax2; apply:(cltSS lin). Qed. Lemma CNFq_pg0 b e c n: CNFq_ax b e c n -> \0o [pb _ _ _]; exact:(olt_leT olt_02 pb). Qed. Lemma CNFq_pg1 b e c n: natp n -> CNFq_ax b e c (csucc n) -> CNFbv b e c (csucc n) h; rewrite succ_zero (CNFq_p3 h (succ_positive \0c)). move: (h) => [bo ax1 ax2 _ ]. have szp:=(succ_positive \0c). move: (CNFq_pg0 h) (ax1 _ szp) (ax2 _ szp) => bp eo cb. rewrite /cantor_mon (opow_succ (proj32_1 bp) eo). exact:(oprod_Meqlt cb (opow_pos bp eo)). move=> n nN Hrec ax1. have sa:= (Hrec (CNFq_p5 (NS_succ nN) ax1)). move: (ax1) => [b2 _ ax3 ax2]. have snn:= (cltS (NS_succ nN)). move: (ax2 n nN snn) (CNFq_p0 ax1 snn) => /oleSltP lt1 o1. move:(olt_leT sa (opow_Meqle (CNFq_pg0 ax1) lt1)) => lt2. have ha:=proj32_1 lt2. have cm1:=(ax3 _ snn). have [[hb bb _] _]:= cm1. have oee := proj32 lt1. have lt3: b ^o e (csucc n) *o osucc (c (csucc n)) <=o b ^o osucc (e (csucc n)). by rewrite opow_succ //; apply: oprod_Meqle => //;move /oleSltP: cm1. move: (osum_Meqlt lt2 o1). rewrite (CNFq_p1 _ _ _ (NS_succ nN)) {2}/cantor_mon - (oprod2_succ ha hb) => h1. exact: (olt_leT h1 lt3). Qed. Lemma CNFq_pg2 b e c n a: natp n -> CNFq_ax b e c (csucc n) -> (e n) CNFbv b e c (csucc n) pa pb pc; move: (CNFq_pg1 pa pb) => h. move/oleSltP: pc => pc. exact: (olt_leT h (opow_Meqle (CNFq_pg0 pb) pc)). Qed. Lemma CNFq_pg3 b e c n a: natp n -> CNFq_ax b e c n -> ordinalp a -> (forall i, i e i CNFbv b e c n nN ax oa h; move: (CNFq_pg0 ax) => bp. case: (equal_or_not n \0c) => nz. rewrite nz CNFq_p2 //; apply: opow_pos; fprops. move: (cpred_pr nN nz) => [qa qb]. rewrite qb in h ax. have sa: (e (cpred n)) CNFq_ax b e c (csucc n) -> CNFbv b e c n nN ax. move: (ax) => [_ ax2 _ _]. exact:(CNFq_pg3 nN (CNFq_p5 nN ax) (ax2 _ (cltS nN)) (CNFq_p6 nN ax)). Qed. Lemma CNFq_pg4 b e c n: natp n -> CNFb_ax b e c (csucc n) -> (b ^o (e n)) <=o CNFbv b e c (csucc n). Proof. move => nN [ax ax2]; move: (ax) => [b2 ax3 _ _]. have nn:= (cltS nN). have pa:= (oprod_Mle1 (OS_pow (proj32 b2) (ax3 _ nn)) (ax2 _ nn)). rewrite (CNFq_p1 _ _ _ nN). exact: (oleT pa (osum_Mle0 (proj32 pa) (OS_CNFq nN (CNFq_p5 nN ax)))). Qed. Lemma CNFq_pg5 b e c n: natp n -> CNFb_ax b e c (csucc n) -> \0o nN ax. move: (opow_pos (CNFq_pg0 (proj1 ax)) (CNFb_p8 ax nN)) => cp. exact:(olt_leT cp (CNFq_pg4 nN ax)). Qed. Lemma CNFb_unique b (e1 c1:fterm) n1 (e2 c2:fterm) n2: natp n1 -> natp n2 -> CNFb_ax b e1 c1 n1 -> CNFb_ax b e2 c2 n2 -> CNFbv b e1 c1 n1 = CNFbv b e2 c2 n2 -> (n1 = n2 /\ forall i, i e1 i = e2 i /\ c1 i = c2 i). Proof. move => n1N n2N; move: n1 n1N n2 n2N; apply: Nat_induction. move=> n2 n2N ax1 ax2. case: (equal_or_not n2 \0c) => n2z. by rewrite n2z => _; split => // i /clt0. move: (cpred_pr n2N n2z) => [mb mv] eq. rewrite mv in ax2 eq. by move: (proj2 (CNFq_pg5 mb ax2)); rewrite - eq CNFq_p2;case. move =>n1 n1N Hrec n2' n2'N ax1s ax2s sv. case: (equal_or_not n2' \0c) => n2z. by move: (proj2 (CNFq_pg5 n1N ax1s)); rewrite sv n2z CNFq_p2; case. move: (cpred_pr n2'N n2z) => []; set n2 := (cpred n2'); move => n2N n2v. rewrite n2v in ax2s sv. move: (cltS n1N) (cltS n2N) => lt1 lt2. move: (ax1s) (ax2s) => [[u1 u2 u3 u4] u5] [[v1 v2 v3 v4] v5]. move: (u2 n1 lt1) (v2 n2 lt2) (u3 n1 lt1) (v3 n2 lt2) => oa1 oa2 of1 of2. move: (u5 n1 lt1) (v5 n2 lt2) => ob1 ob2. move: (proj32_1 ob1) (proj32_1 ob2) => oc1 oc2. move: (CNFb_p5 n1N ax1s)(CNFb_p5 n2N ax2s) => ax1 ax2. move: (OS_CNFq n1N (proj1 ax1)) (OS_CNFq n2N (proj1 ax2)) => oe1 oe2. set a1 := CNFbv b e1 c1 (csucc n1). set a2 := CNFbv b e2 c2 (csucc n2). move: (erefl a1); rewrite {2} /a1 (CNFq_p1 _ _ _ n1N) => ha1. move: (erefl a2); rewrite {2} /a2 (CNFq_p1 _ _ _ n2N) => ha2. move: (CNFq_pg n1N (proj1 ax1s)) (CNFq_pg n2N (proj1 ax2s)) => hb1 hb2. have og1:=(OS_CNFq (NS_succ n1N) (proj1 ax1s)). have ox1: (ord_ext_div_pr b a1 (e1 n1) (c1 n1) (CNFbv b e1 c1 n1)). split;[ exact | exact| exact | split; [exact: ha1 | exact | exact | exact]]. have ox2: (ord_ext_div_pr b a1 (e2 n2) (c2 n2) (CNFbv b e2 c2 n2)). rewrite /a1 sv -/a2. split;[ exact | exact| exact | split; [exact: ha2 | exact | exact | exact]]. move: (ord_ext_div_unique u1 og1 ox1 ox2) => [se1 sc1 sr1]. move: (Hrec _ n2N ax1 ax2 sr1) => [n12 etc]; split. by rewrite n2v - n12. move => i /(cltSleP n1N); case: (equal_or_not i n1) => in1. by rewrite in1 {4 6} n12 => _; split. by move => nin1; move: (etc _ (conj nin1 in1)). Qed. Lemma CNF_singleton b c0 e0 (c:= fun _: Set => c0)(e:= fun _: Set => e0): ordinalp e0 -> c0 \2c <=o b -> [/\ CNFq_ax b e c \1c, CNFbv b e c \1c = b ^o e0 *o c0 & (\0o CNFb_ax b e c \1c)]. Proof. move=> oe co b2. have aux: CNFq_ax b e c \1c. rewrite /e/c;split => // i ib. by rewrite - succ_zero;move/(cltSleP NS0)=> /(cltNge (@succ_positive i)). by rewrite (CNFq_p3 aux clt_01). Qed. Lemma CNF_exp_bnd b e c n e0: \2c <=o b -> ordinalp e0 -> natp n -> CNFb_ax b e c n -> CNFbv b e c n (forall i, i e i le1 oe nN ax lt1 i id. case: (equal_or_not n \0c) => nz. by move: id; rewrite nz => /clt0. move: (cpred_pr nN nz) => [mN mv]. rewrite mv in ax id. move/(cltSleP mN): id => ipn. move:(CNF_exponents_M (NS_succ mN) (proj1 ax) ipn (cltS mN)) => ha. case (oleT_el oe (proj31 ha)) => // hb. move:(CNFq_pg4 mN ax); rewrite - mv => h1; move:(ole_ltT h1 lt1) => hc. by move: (opow_Meqle (olt_leT olt_02 le1) (oleT hb ha)) => /(oltNge hc). Qed. Lemma CNFb_exists a b: ordinalp a -> \2c <=o b -> exists e c n, [/\ CNFb_ax b e c n, natp n & a = CNFbv b e c n]. Proof. move=> oa oeb. pose p a := exists e c n, [/\ CNFb_ax b e c n, natp n & a = CNFbv b e c n]. apply: (least_ordinal2 (p := p)) oa => y oy p2. case: (equal_or_not y \0o) => ynz. exists (@id Set), (@id Set), \0c; split; first split. + split => // i; try move /clt0 => //. by move => _ /clt0. + by move => i /clt0. + fprops. + by rewrite CNFq_p2. move: OS2 => o2. have cpy1:=(ord_ne0_pos oy ynz). move: (ord_ext_div_exists oeb cpy1) => [e1 [c1 [rm [oe1 oc1 or [eq1 lt1 lt2 lt3]]]]]. have rmy: rm p4. exact : (olt_leT lt1 (oleT p3 p4)). move: (p2 _ rmy) => [e [c [n [ax nN rv]]]]. have snN:= (NS_succ nN). pose e' i := Yo (i = n) e1 (e i). pose c' i := Yo (i = n) c1 (c i). exists e', c', (csucc n). have ha: CNFbv b e' c' n = CNFbv b e c n. rewrite /CNFbv; apply: osum_expansion_exten => // i [ _ lin]. by rewrite /e' /c' /cantor_mon; Ytac0; Ytac0. have hb: cantor_mon b e' c' n = b ^o e1 *o c1. by rewrite /cantor_mon /e' /c'; Ytac0; Ytac0. rewrite (CNFq_p1 _ _ _ nN) ha - rv hb - eq1. suff: CNFb_ax b e' c' (csucc n) by move => hc; split. move: (CNF_exp_bnd oeb oe1 nN ax); rewrite - rv => hx. move: ax => [[a1 a2 a3 a4] a5]; split; last first. rewrite /c';move => i /(cltSleP nN); case (equal_or_not i n). by move => -> _; Ytac0. move => i1 i2; Ytac0; exact: (a5 _ (conj i2 i1)). split; first done. + rewrite /e';move => i /(cltSleP nN); case (equal_or_not i n). by move => -> _; Ytac0. move => i1 i2; Ytac0; exact: (a2 _ (conj i2 i1)). + rewrite /c';move => i /(cltSleP nN); case (equal_or_not i n). by move => -> _; Ytac0. move => i1 i2; Ytac0; exact: (a3 _ (conj i2 i1)). + rewrite /e';move => i iN /(cltSleP nN) sin. have isi:= (clt_leT (cltS iN) sin). move: (proj2 isi) => nin; Ytac0. case (equal_or_not (csucc i) n) => ne1; Ytac0; first by exact: (hx lt1 _ isi). exact:(a4 i iN (conj sin ne1)). Qed. Definition CNFbB n e c := J n (J (Lg Nat (fun z => Yo (z Yo (z (P X) <=c i -> Vg (P (Q X)) i = \0o), (forall i, natp i -> (P X) <=c i -> Vg (Q (Q X)) i = \0o) & CNFb_ax b (Vg (P (Q X))) (Vg (Q (Q X))) (P X)]]]. Definition cnfbv X := CNFbv b (Vg (P (Q X))) (Vg (Q (Q X))) (P X). Definition cnfb_bound x:= Nat \times ((gfunctions Nat (osucc x)) \times (gfunctions Nat b)). Definition the_cnf x := select (fun X => cnfb_ax X /\ cnfbv X = x) (cnfb_bound x). Definition the_cnf_degree x := (Vg (P (Q (the_cnf x))) (cpred (P (the_cnf x)))). Lemma props_of_b: [/\ ordinalp b, b <> \0o & \0o [_ ob _]. have bp:= (olt_leT (olt_02) bg2). move: (bp) => [_ /nesym bne] //. Qed. Lemma cnfb_unique X1 X2: cnfb_ax X1 -> cnfb_ax X2 -> cnfbv X1 = cnfbv X2 -> X1 = X2. Proof. move => [p1 p2 p3 [p4 p5 p6 p7 [p8 p9 p10]]]. move => [q1 q2 q3 [q4 q5 q6 q7 [q8 q9 q10]]] sv. move:(CNFb_unique p2 q2 p10 q10 sv) =>[sa sb]. have ha: P (Q X1) = P (Q X2). apply: fgraph_exten; [exact | exact | by rewrite p6 q6 | move => i id /=]. rewrite p6 in id. case (cleT_el (CS_nat p2) (CS_nat id)) => h. by rewrite (p8 _ id h) (q8 _ id) - ?sa. exact (proj1 (sb _ h)). have hb: Q (Q X1) = Q (Q X2). apply: fgraph_exten; [exact | exact | by rewrite p7 q7 | move => i id /=]. rewrite p7 in id. case (cleT_el (CS_nat p2) (CS_nat id)) => h. by rewrite (p9 _ id h) (q9 _ id) - ?sa. exact (proj2 (sb _ h)). have hc: Q X1 = Q X2 by apply:pair_exten. by apply:pair_exten. Qed. Lemma cnfb_bound_p X: cnfb_ax X -> inc X (cnfb_bound (cnfbv X)). Proof. move => [p1 p2 p3 [p4 p5 p6 p7 [p8 p9 p10]]]. move: (p10) => [[p11 p12 p13 p14] p15]. move: (props_of_b) => [ob bnz bp]. apply/setX_P; split => //; apply/setX_P; split =>//. move: (OS_CNFq p2 (proj1 p10)) => osx. apply/gfunctions_P2; split => // v /(range_gP p4) [i]; rewrite p6 => iN ->. apply/(oleP osx). case: (NleT_el p2 iN) => h. by rewrite (p8 i iN h); apply: (ozero_least osx). have ot:= (p12 _ h). move:(oleT (oprod_M1le bp ot)(opow_Mspec2 ot bg2)). move => ha; apply: (oleT ha). case: (equal_or_not (P X) \0c) => nz. by move: h; rewrite nz => /clt0. move: (cpred_pr p2 nz) => [mN mv]. rewrite mv in p10 h. move:(CNFq_pg4 mN p10); rewrite - mv => eq1. have aa: i <=c (cpred (P X)) by apply /(cltSleP mN). have bb: (cpred (P X)) /(opow_Meqle bp). by move => hc; apply: (oleT hc eq1). apply/gfunctions_P2; split => // v /(range_gP p5) [i]; rewrite p7 => iN ->. case: (cleT_el (CS_nat p2) (CS_nat iN)) => h. rewrite (p9 i iN h);exact:(olt_i (ord_ne0_pos ob bnz)). by move: (p13 i h) => /(oltP ob). Qed. Lemma CNFbB_prop n e c: CNFb_ax b e c n -> natp n -> cnfb_ax (CNFbB n e c) /\ cnfbv (CNFbB n e c) = CNFbv b e c n. Proof. move => ax nN. move:(ax) => [[a1 a2 a3 a4] a5]; rewrite /CNFbB. rewrite /cnfb_ax /cnfbv !(pr1_pair, pr2_pair). set e1 := Lg _ _. set c1 := Lg _ _. have h1: same_below e (Vg e1) n. by move => i lin; rewrite /e1 (LVg_E _ (NS_lt_nat lin nN)); Ytac0. have h2: same_below c (Vg c1) n. by move => i lin; rewrite /c1 (LVg_E _ (NS_lt_nat lin nN)); Ytac0. move: (CNFb_exten h1 h2 ax nN) => [sa <-]. split => //; split; [fprops | exact | fprops |]. rewrite {1 2 3} /e1 {1 2 3} /c1; bw; split; fprops; split => //. move => i iN ni; bw; Ytac h; [ case:(cleNgt ni h) | done]. move => i iN ni; bw; Ytac h; [ case:(cleNgt ni h) | done]. Qed. Lemma cnfb_exists x: ordinalp x -> exists2 X, cnfb_ax X & cnfbv X = x. Proof. move => ox. move: (CNFb_exists ox bg2) => [e [c [n [ax nN ->]]]]. by move: (CNFbB_prop ax nN) => [sa sb];exists (CNFbB n e c). Qed. Lemma the_cnf_p0 x (X:= the_cnf x): ordinalp x -> cnfb_ax X /\ cnfbv X = x. Proof. move => ox. suff: (cnfb_ax X /\ cnfbv X = x) /\ inc X (cnfb_bound x) by move => []. apply: select_pr. move: (cnfb_exists ox) => [z za zb]; exists z => //. by rewrite - zb ; apply:cnfb_bound_p. move => a b' _ [p1 p2] _ [p3 p4]. rewrite - p4 in p2;exact:(cnfb_unique p1 p3 p2). Qed. Lemma cnfb_ax_simp X: cnfb_ax X -> natp (P X) /\ CNFb_ax b (Vg (P (Q X))) (Vg (Q (Q X))) (P X). Proof. by move => [ _ p2 _ [_ _ _ _ [_ _ p10]]]. Qed. Lemma the_cnf_p1: P(the_cnf \0o) = \0c. Proof. move:(the_cnf_p0 OS0) => [/cnfb_ax_simp [p2 p10] sb]. ex_middle nz. move: (cpred_pr p2 nz) => [mN mv]. rewrite mv in p10. by move:(proj2 (CNFq_pg5 mN p10)); rewrite -mv -/(cnfbv _) sb. Qed. Lemma the_cnf_p2 x (m := (cpred (P (the_cnf x)))): \0o natp m /\ P (the_cnf x) = csucc m. Proof. move => [[ _ ox _] xnz]. move:(the_cnf_p0 ox) => [/cnfb_ax_simp [nN ax] sb]. case (equal_or_not (P (the_cnf x)) \0c) => nz. by move:xnz; rewrite - sb /cnfbv nz /CNFbvo CNFq_p2. exact: (cpred_pr nN nz). Qed. Lemma the_cnf_p3 e c n: CNFb_ax b e c n -> natp n -> the_cnf (CNFbv b e c n) = (CNFbB n e c). Proof. move => ax nN. have ox:=(OS_CNFq nN (proj1 ax)). move:(CNFbB_prop ax nN) (the_cnf_p0 ox) => [sa sb] [sc sd]. rewrite - sd in sb. symmetry; exact: (cnfb_unique sa sc sb). Qed. Lemma OS_the_cnf_degree x: ordinalp x -> ordinalp (the_cnf_degree x). Proof. move => /the_cnf_p0 [sa sb]. move: sa => [p1 p2 p3 [p4 p5 p6 p7 [p8 p9 p10]]]. rewrite /the_cnf_degree. case (equal_or_not (P (the_cnf x)) \0c) => nz. rewrite nz /cpred setU_0 -/card_zero p8; fprops; rewrite nz; fprops. move: (p10) => [[_ p12 _ _] _]; apply: p12. move:(cpred_pr p2 nz) => [mN eq]; rewrite {2} eq; apply: (cltS mN). Qed. End CNF_baseb. Definition CNFB_ax X := [/\ pairp X, natp (P X), pairp (Q X) & [/\ fgraph (P (Q X)), fgraph (Q (Q X)), domain (P (Q X)) = Nat, domain (Q (Q X)) = Nat & [/\ (forall i, natp i -> (P X) <=c i -> Vg (P (Q X)) i = \0o), (forall i, natp i -> (P X) <=c i -> Vg (Q (Q X)) i = \0o) & CNFb_axo (Vg (P (Q X))) (Vg (Q (Q X))) (P X)]]]. Definition CNFBv X := CNFbvo (Vg (P (Q X))) (Vg (Q (Q X))) (P X). Definition CNFB_bound x:= Nat \times ((gfunctions Nat (osucc x)) \times (gfunctions Nat Nat)). Definition the_CNF x := select (fun X => CNFB_ax X /\ CNFBv X = x) (CNFB_bound x). Definition the_CNF_degree x := (Vg (P (Q (the_CNF x))) (cpred (P (the_CNF x)))). Lemma CNFB_unique X1 X2: CNFB_ax X1 -> CNFB_ax X2 -> CNFBv X1 = CNFBv X2 -> X1 = X2. Proof. by apply:cnfb_unique. Qed. Lemma CNFB_bound_p X: CNFB_ax X -> inc X (CNFB_bound (CNFBv X)). Proof. apply:(cnfb_bound_p ole_2omega). Qed. Lemma CNFB_exists x: ordinalp x -> exists2 X, CNFB_ax X & CNFBv X = x. Proof. apply: (cnfb_exists ole_2omega). Qed. Lemma the_CNF_p0 x (X:= the_CNF x): ordinalp x -> CNFB_ax X /\ CNFBv X = x. Proof. exact: (the_cnf_p0 ole_2omega). Qed. Lemma CNFB_ax_simp X: CNFB_ax X -> inc (P X) Nat /\ CNFb_axo (Vg (P (Q X))) (Vg (Q (Q X))) (P X). Proof. by move => [ _ p2 _ [_ _ _ _ [_ _ p10]]]. Qed. Lemma the_CNF_p1: P(the_CNF \0o) = \0c. Proof. exact: (the_cnf_p1 ole_2omega). Qed. Lemma the_CNF_p2 x (m := (cpred (P (the_CNF x)))): \0o natp m /\ P (the_CNF x) = csucc m. Proof. exact: (the_cnf_p2 ole_2omega). Qed. Lemma the_CNF_p3 e c n: CNFb_axo e c n -> natp n -> the_CNF (CNFbvo e c n) = (CNFbB n e c). Proof. exact: (the_cnf_p3 ole_2omega). Qed. Lemma OS_the_CNF_degree x: ordinalp x -> ordinalp (the_CNF_degree x). Proof. exact: (OS_the_cnf_degree ole_2omega). Qed. Lemma the_CNF_p4 x (n := the_CNF_degree x): \0o omega0 ^o n <=o x /\ x xp; move: (the_CNF_p2 xp) => []. set m := cpred _; move => mN mv. move: xp => [[ _ ox _] xnz]. move:(the_CNF_p0 ox) => [/CNFB_ax_simp [nN ax] sb]. rewrite mv in ax; split. move:(CNFq_pg4 mN ax);rewrite -mv -/CNFbvo -/(CNFBv _) sb //. move:(CNFq_pg1 mN (proj1 ax));rewrite -mv -/CNFbvo -/(CNFBv _) sb //. Qed. Lemma the_CNF_p5 e c n (x:= CNFbvo e c (csucc n)): natp n -> CNFb_axo e c (csucc n) -> \0o nN ax. move:(CNFq_pg5 nN ax) => xp. split; first by exact. move:(the_CNF_p2 xp). rewrite /x /the_CNF_degree; rewrite(the_CNF_p3 ax (NS_succ nN)). set m := (cpred (P (CNFbB (csucc n) e c))); move => [mN]. have sm:= cltS mN. rewrite /CNFbB; aw; move => /(succ_injective1 (CS_nat nN) (CS_nat mN)) ->. by bw; Ytac0. Qed. Lemma the_CNF_degree_one: the_CNF_degree \1o = \0o. Proof. move:(proj1 (the_CNF_p4 olt_01))(OS_the_CNF_degree OS1). set n := the_CNF_degree \1o. rewrite -(@opowx0 omega0) => sa sb. by case: (ozero_dichot sb) => // /opow_Momega_lt /(oleNgt sa). Qed. Lemma the_CNF_degree_omega: the_CNF_degree omega0 = \1o. Proof. move:(the_CNF_p4 olt_0omega)(OS_the_CNF_degree OS_omega). set n := the_CNF_degree omega0. rewrite -{2 3} (opowx1 OS_omega); move => [sa sb] sc. case: (oleT_el sc OS1); last by move /opow_Momega_lt => /(oleNgt sa). move => pa; case (equal_or_not n \1o) => n1//. by case: (proj2 sb); rewrite (olt1 (conj pa n1)) osucc_zero. Qed. Lemma the_CNF_split x (e:= the_CNF_degree x) (X:= (the_CNF x)) (c:= Vg (Q (Q X)) (cpred (P X))) (r := CNFbvo (Vg (P (Q X))) (Vg (Q (Q X))) (cpred (P X))): \0o [/\ \0o xp. move:(the_CNF_p2 xp). rewrite /e/c/r/X. set m := cpred _; move => [mN Pv]. move: (the_CNF_p0 (proj32_1 xp)) => [/CNFB_ax_simp [sa]]. rewrite /CNFBv Pv. set E := (Vg (P (Q (the_CNF x)))); set C := (Vg (Q (Q (the_CNF x)))). move => sb sc. move: (sb) => [[a1 a2 a3 a4] a5]. split. + exact:(a5 _ (cltS mN)). + exact:(a3 _ (cltS mN)). + exact:(CNFq_pg mN (proj1 sb)). + by rewrite -{1} sc /CNFbvo (CNFq_p1 _ _ _ mN). Qed. Lemma the_CNF_p6 a e: ordinalp e -> \0o a (the_CNF_degree a) oe ap lta. have lt2:= (ole_ltT (proj1 (the_CNF_p4 ap)) lta). have od:= (OS_the_CNF_degree (proj32_1 ap)). by rewrite (opow_Meqltr ole_2omega od oe). Qed. Lemma ord_negl_p8 ep cp p en cn n: CNFb_axo ep cp (csucc p) -> CNFb_axo en cn (csucc n) -> natp p -> natp n -> ep p (CNFbvo ep cp (csucc p)) < axp axn pN nN ln. have snN:= NS_succ nN. set x := CNFbvo en cn (csucc n). have aux: forall e c, c e ((omega0 ^o e) *o c) < e c cb ef; rewrite /x. move: (proj31_1 ef) (proj31_1 cb) => oe oc. have om:=(CNFq_p0 (proj1 axn) (cltS nN)). rewrite /CNFbvo (CNFq_p1 _ _ _ nN). apply: (ord_negl_sum (OS_prod2 (OS_pow OS_omega oe) oc) om). exact: (OS_CNFq nN (CNFq_p5 nN (proj1 axn))). apply: (ord_negl_p5 cb ef) (proj2 axn _ (cltS nN)). move:p pN axp ln; apply: Nat_induction. move => ax1 lt1; move:(ax1) => [[_ _ hc _] _]. rewrite /CNFbvo succ_zero (CNFq_p3 (proj1 ax1) (succ_positive \0c)). exact: (aux _ _ (hc _ (succ_positive \0c)) lt1). move => p pN Hrec ax1 l1. have spN:= (NS_succ pN). have axr:=(CNFb_p5 spN ax1). have spp:= (cltS spN). move:(proj1 ax1) => [_ _ hc ha]. have h0:= (olt_leT (ha p pN spp) (proj1 l1)). have h1 :=(CNFq_p0 (proj1 ax1) spp). have h6: cp (csucc p) \0o the_CNF_degree x x < xp yp. move:(the_CNF_p2 xp)(the_CNF_p2 yp). move: (the_CNF_p0 (proj32_1 xp))(the_CNF_p0 (proj32_1 yp)). rewrite /the_CNF_degree. set p:= (cpred _); set q := (cpred _). move => [/CNFB_ax_simp ax1 v1][/CNFB_ax_simp ax2 v2] [pN sp][nN sn] h. rewrite sp in ax1; rewrite sn in ax2. move: (ord_negl_p8 (proj2 ax1) (proj2 ax2) pN nN h). by rewrite - sp - sn -/(CNFBv _) v1 -/(CNFBv _) v2. Qed. Lemma CNF_sum_pr1 eX cX eY cY n m p (eZ := cnf_m eY (cnf_s eX n) (csucc p)) (cZ := cnf_m cY (cnf_s cX n) (csucc p)): natp n -> natp m -> natp p -> CNFb_axo eX cX (n +c m) -> CNFb_axo eY cY (csucc p) -> eY p (n = \0c \/ eX (cpred n) ( CNFb_axo eZ cZ (csucc p +c m) /\ CNFbvo eX cX (n +c m) +o CNFbvo eY cY (csucc p) = CNFbvo eZ cZ (csucc p +c m)). Proof. move=> nN mN pN ax ay lt1 plt2. have spN:= (NS_succ pN). move:(CNFb_A nN mN ax) => [ax4 ax5 ->]. have axz: CNFb_axo eZ cZ (csucc p +c m). apply:(CNFb_m_ax spN mN ay ax5);right. by rewrite /cnf_s (csum0l (CS_nat nN)) (cpred_pr1 (CS_nat pN)). split; first by exact. have oY:=(OS_CNFb spN ay). rewrite - (osumA (OS_CNFb mN ax5) (OS_CNFb nN ax4) oY). move:(CNFb_A spN mN axz) => [au av ->]. apply f_equal2. apply:(osum_expansion_exten mN) => i lim. have ww: ~ (i +c csucc p h; move:(cltNge h (csum_M0le i (CS_succ p))). rewrite /cantor_mon /eZ/cZ /cnf_m /cnf_s; Ytac0; Ytac0. by rewrite (cdiff_pr1 (NS_lt_nat lim mN) spN). have <-: CNFbvo eY cY (csucc p) = CNFbvo eZ cZ (csucc p). apply:(osum_expansion_exten spN) => i lim. by rewrite /eZ/cZ/cantor_mon /cnf_s /cnf_m; Ytac0; Ytac0. case (equal_or_not n \0c) => nz; first by rewrite nz CNFq_p2 osum0l //. move: ax4; move: (cpred_pr nN nz)=> [n'N ->] ax4. by apply: (ord_negl_p8 ax4 ay n'N pN); case:plt2. Qed. Lemma CNF_sum_pr2 eX cX eY cY n m p (eZ := cnf_m eY (cnf_s eX (csucc n)) (csucc p)) (cZ := cnf_m (cnf_change_n cY p ((cX n) +o (cY p))) (cnf_s cX (csucc n)) (csucc p)) (Z:= CNFbB (csucc p +c m) eZ cZ): natp n -> natp m -> natp p -> CNFb_axo eX cX (csucc n +c m) -> CNFb_axo eY cY (csucc p) -> eY p = eX n -> ( CNFb_axo eZ cZ (csucc p +c m) /\ CNFbvo eX cX ((csucc n) +c m) +o CNFbvo eY cY (csucc p) = CNFbvo eZ cZ (csucc p +c m)). Proof. move=> nN mN pN ax ay eq1. have nmN:= NS_sum nN mN. have spN := NS_succ pN. have snN:= (NS_succ nN). have cdx1: csucc n +c m = n +c csucc m. by rewrite csum_nS // csum_Sn. have nls: n [[_ _ ha _ ] _]; apply: ha. move:(CNFb_change_nv pN ay pa)=> []; rewrite -/cY -/eY => ax4 v4. move:(CNFb_A snN mN ax) => [ax5 ax6 ->]. move: (ax) => [[_ _ _ h2] _]. have axz: CNFb_axo eZ cZ (csucc p +c m). apply:(CNFb_m_ax spN mN ax4 ax6). rewrite (cpred_pr1 (CS_nat pN)) /cnf_s (csum0l (CS_nat snN)). rewrite -/eY eq1; case (equal_or_not m \0c)=> mz; first by left. right; apply: (h2 _ nN); by apply:csum_M0lt. split; first by exact. have oY:= (OS_CNFb spN ay). move: (CNFb_A spN mN axz) => [ax7 ax8 ->]. rewrite- (osumA (OS_CNFb mN ax6) (OS_CNFb snN ax5) oY); apply: f_equal2. apply: (osum_expansion_exten mN) => i im. have ww: ~ (i +c csucc p h; move:(cltNge h (csum_M0le i (CS_succ p))). rewrite /cantor_mon /eZ/cZ /cnf_m /cnf_s; Ytac0; Ytac0. by rewrite (cdiff_pr1 (NS_lt_nat im mN) spN). have ->: CNFbvo eZ cZ (csucc p) = omega0 ^o eY p *o cX n +o CNFbvo eY cY (csucc p). rewrite - v4; apply: (osum_expansion_exten spN) => i im. by rewrite /cantor_mon /eZ /cZ /cnf_s /cnf_m; Ytac0; Ytac0. have h1 :=(CNFq_p0 (proj1 ax5) (cltS nN)). have ax9:= (CNFb_p5 nN ax5). rewrite (CNFq_p1 _ _ _ nN) eq1 - (osumA h1 (OS_CNFb nN ax9) oY). congr (osum2). case (equal_or_not n \0c) => nz. rewrite nz CNFq_p2 (osum0l oY); reflexivity. move: ax9; move: (cpred_pr nN nz)=> [n'N eq]; rewrite eq => ax9. apply: (ord_negl_p8 ax9 ay n'N pN). by rewrite -/eY eq1; rewrite {2} eq; apply: h2 => //; rewrite - eq //. Qed. Lemma CNF_sum_pr3 eX cX eY cY n p (eZ := cnf_m eY (cnf_s eX (csucc n)) (csucc p)) (cZ := (cnf_change_n cY p ((cX n) +o (cY p)))): natp n -> natp p -> CNFb_axo eX cX (csucc n) -> CNFb_axo eY cY (csucc p) -> eY p = eX n -> ( CNFb_axo eZ cZ (csucc p) /\ CNFbvo eX cX (csucc n) +o CNFbvo eY cY (csucc p) = CNFbvo eZ cZ (csucc p)). Proof. move => nN pN ax ay h1. move:(Nsum0r (NS_succ nN)) (Nsum0r (NS_succ pN)) => aux2 aux1. rewrite - aux2 in ax. move:(CNF_sum_pr2 nN NS0 pN ax ay h1); rewrite aux1 aux2 -/eZ. set c2 := cnf_m _ _ _. have pa: same_below eZ eZ (csucc p) by []. have pb: same_below c2 cZ (csucc p). by move => i idn;rewrite /c2 /cZ /cnf_m/cnf_change_n; Ytac0. move =>[sa ->]; exact: (CNFb_exten pa pb sa (NS_succ pN)). Qed. Lemma CNF_prod_pr1 eX cX p k (cZ := (cnf_change_n cX p ((cX p) *o k))): \0o k natp p -> CNFb_axo eX cX (csucc p) -> (CNFb_axo eX cZ (csucc p) /\ CNFbvo eX cX (csucc p) *o k= CNFbvo eX cZ (csucc p)). Proof. move => kz ko pN ax. pose ck k := cnf_change_n cX p (cX p *o k). rewrite /cZ -/(ck k). have psp:= cltS pN. have pa: \0o [_]; apply. have H: forall k, \0o k CNFb_axo eX (ck k) (csucc p). move => n na nb; apply:CNF_change_n_ax => //; first by apply: oprod2_pos. apply: oprod2_lt_omega => //. move: (ax) => [[_ _ a2 _] _]; exact:(a2 _ psp). move: (H _ kz ko) => az; split; first by exact. pose r k := CNFbvo eX cX (csucc p) *o k = CNFbvo eX (ck k) (csucc p). have spN:= (NS_succ pN). have oX:=(OS_CNFb spN ax). have r1: r \1c. rewrite /r (oprod1r oX) ; apply: (osum_expansion_exten spN). move => i isp; rewrite /ck /cnf_change_n /cantor_mon; Ytac h=> //. rewrite h oprod1r //; exact: proj32_1 pa. have kN: inc k Nat by apply /olt_omegaP. have k1: \1c <=c k by move: (nesym (proj2 kz)); apply: cge1; fprops. apply: (Nat_induction2 (r :=r) NS1 r1 _ kN k1). move => n nN n1 rn. have on:= OS_nat nN. rewrite (succ_of_Nat nN) /r /ck (oprod2_succ oX on) rn. have n0: \0o // nz. case:(cleNgt n1); rewrite nz; exact: clt_01. have no: n [ax3 ->]. apply: (osum_expansion_exten spN) => i isb. have->: ck n p +o cX p = cX p *o osucc n. rewrite /ck /cnf_change_n; Ytac0; rewrite (oprod2_succ _ on) //. exact: proj32_1 pa. by rewrite /cantor_mon /cnf_m; Ytac0. Qed. Lemma CNF_limit e c n: natp n -> CNFb_axo e c (csucc n) -> \0o exists2 z, ordinalp z & CNFbvo e c (csucc n) = omega0 *o z. Proof. move => nN ax h0. have h1: forall k, inc k Nat -> CNFb_axo e c (csucc k) -> exists2 z, ordinalp z & cantor_mon omega0 e c k = omega0 *o z. move => k kN axk; rewrite /cantor_mon. have kp: \0c <=c k by fprops. move: (CNF_exponents_M (NS_succ kN) (proj1 axk) kp (cltS kN)) => ek. move: (ord_rev_pred (olt_leT h0 ek)) => [op ->]. have oo:= OS_omega. have ob:= OS_pow oo op. move: (proj2 axk _ (cltS kN)) => [[_ oc _] _]. rewrite (opow_sum oo OS1 op) (opowx1 oo) - (oprodA oo ob oc). exists (omega0 ^o (e k -o \1o) *o c k); [ exact: (OS_prod2 ob oc) | done]. move: n nN ax; apply: Nat_induction. move => ha; move: (h1 _ NS0 ha) =>[z z1 z2]; exists z => //. move: (proj1 ha); rewrite succ_zero /CNFbvo => hb. by rewrite (CNFq_p3 hb clt_01). move => n nN Hrec ax. rewrite /CNFbvo (CNFq_p1 _ _ _ (NS_succ nN)) -/CNFbvo. move: (Hrec (CNFb_p5 (NS_succ nN) ax)) => [z1 oz1 ->]. move:(h1 _ (NS_succ nN) ax) => [z2 oz2 ->]. rewrite - (oprodD oz2 oz1 OS_omega); exists (z2 +o z1); fprops. Qed. Lemma CNF_limit0 e c n: natp n -> CNFb_axo e c (csucc n) -> (exists2 y, ordinalp y & CNFbvo e c (csucc n) = y +o omega0 ^o (e \0c)). Proof. move => nN ax. move: (CNFb_Al nN ax) => [sa sb ->]. have osn:= (succ_positive n). move: (proj2 ax _ (succ_positive n)) => cp. move: (ax) => [[_ h1 h2 _] _]. have o1:= (OS_pow OS_omega (h1 _ osn)). have o2:= (OS_diff OS1 (proj32_1 cp)). have o3 := (OS_prod2 o1 o2). move: (oprec_nat (proj2 ax _ (succ_positive n)) (h2 _ osn)) => eq1. rewrite /cantor_mon eq1 (oprod2_succ o1 o2) (osumA (OS_CNFb nN sb) o3 o1). set y := (CNFbv _ _ _ _ +o _); exists y => //. apply: (OS_sum2 (OS_CNFb nN sb) o3). Qed. Lemma CNF_limit1 e c n: natp n -> CNFb_axo e c (csucc n) -> (e \0c) = \0o -> ~ (limit_ordinal (CNFbvo e c (csucc n))). Proof. move => nN ax; move: (CNF_limit0 nN ax) => [z zv ->] ->. rewrite opowx0 (osucc_pr zv) => lz. have h :=(limit_nonsucc lz). by apply:(proj2 (osuccVidpred (OS_succ zv))); split => //; exists z. Qed. Lemma CNF_limit2 e c n: natp n -> CNFb_axo e c (csucc n) -> \0o (limit_ordinal (CNFbvo e c (csucc n))). Proof. move => nN ax h1. move: (CNF_limit0 nN ax) => [z oz ->]. apply: osum_limit => //;apply: indecomp_limit2 => //. Qed. Lemma CNF_limit3 x: limit_ordinal x -> exists2 z, ordinalp z & x = omega0 *o z. Proof. move =>lx. move: (the_CNF_p0 (proj31 lx)) => [ax xv]. move: (CNFB_ax_simp ax) => [sa sb]. move:(the_CNF_p2 (limit_pos lx)); set m := cpred _. move => [mN pv]; rewrite pv in sb. move:(sb)=> [[_ ha _ _] _]. move: (ha _ (succ_positive m)) (CNF_limit1 mN sb). rewrite - pv -/(CNFBv _) xv => hb hc. have sc: \0o // nz; case: (hc nz). by move: (CNF_limit mN sb sc);rewrite - pv -/(CNFBv _) xv. Qed. Lemma CNF_se_p e c e0 n (eY:= fun i => e0 +o e i): natp n -> CNFb_axo e c n -> ordinalp e0 -> (CNFb_axo eY c n /\ CNFbvo eY c n = omega0 ^o e0 *o CNFbvo e c n). Proof. move => nN ax oe. have aux: forall k, CNFb_axo e c k -> CNFb_axo eY c k. move => k [[pa pb pc pd] pe]; split; [split |] => //. + move => i /pb oei; rewrite /eY; fprops. + move => i iN /(pd _ iN) sa; rewrite /eY; apply: (osum_Meqlt sa oe). split; first by apply: aux. rewrite /CNFbvo. move:n nN ax;apply: Nat_induction. by move => _; rewrite !CNFq_p2 oprod0r. move => n nN Hr ax. have ax1:= (CNFb_p5 nN ax). have oa:=(CNFq_p0 (proj1 ax) (cltS nN)). have ob:= (OS_CNFb nN ax1). have oc:= OS_pow OS_omega oe. have od:= (CNFb_p8 ax nN). move: ax => [[_ _ hb _] _]. move: (hb _ (cltS nN)) => [[og _ _] _]. rewrite (CNFq_p1 _ _ _ nN) (CNFq_p1 _ _ _ nN) (Hr ax1) (oprodD oa ob oc). rewrite /eY /cantor_mon (opow_sum OS_omega oe od). by rewrite (oprodA oc (OS_pow OS_omega od) og). Qed. Lemma CNF_prod_pr2 e c n: natp n -> CNFb_axo e c (csucc n) -> CNFbvo e c (csucc n) *o omega0 = omega0 ^o (e n) *o omega0. Proof. move=> nN ax; rewrite /CNFbvo. have nn:= cltS nN. move: (ax) => [[_ h1 h2 _] h3]. have h4:= (OS_pow OS_omega (h1 _ nn)). have h5:= OS_prod2 h4 OS_omega. have h3n:= (h3 _ nn). apply: oleA; last first. have ox:= (OS_CNFb nN (CNFb_p5 nN ax)). apply: (oprod_Mleeq _ OS_omega); apply: (oleT (oprod_Mle1 h4 h3n)). rewrite (CNFq_p1 _ _ _ nN); apply: (osum_Mle0 (CNFq_p0 (proj1 ax) nn) ox). set x := CNFbvo e c (csucc n). have pc' : \0o [pg pk]. rewrite (pk _ (omega_limit)); clear pk. apply: ord_ub_sup => //. move=> i /funI_P [z zo ->]. move: zo => /(oltP OS_omega) zo. have oz:= proj31_1 zo. case: (ozero_dichot oz) => zno. by rewrite zno (oprod0r); apply: ozero_least. move: (oprod2_lt_omega (h2 _ nn) zo) => /oleSltP so. move: (CNF_prod_pr1 zno zo nN ax) => [ax1 ->]. rewrite /CNFbvo (CNFq_p1 _ _ _ nN). have lt1: CNFbvo e (cnf_change_n c n (c n *o z)) n k kn; exact:(CNF_exponents_sM (NS_succ nN) (proj1 ax) kn nn). rewrite {1} /cnf_change_n /cantor_mon; Ytac0. have oy1:= (OS_prod2 (proj32_1 h3n) oz). move: (osum_Meqlt lt1 (OS_prod2 h4 oy1)); rewrite - (oprod2_succ h4 oy1). move => [le1 _]; apply: (oleT le1 (oprod_Meqle so h4)). Qed. Lemma CNF_prod_pr2bis x: \0o x *o omega0 = omega0 ^o (the_CNF_degree x) *o omega0. Proof. move => xp. move: (the_CNF_p0 (proj32_1 xp)) => [ax0 xv]. move: (CNFB_ax_simp ax0) (the_CNF_p2 xp) => [pb ax] [nN pc]. by rewrite pc in ax; rewrite - (CNF_prod_pr2 nN ax) - {1} xv - pc. Qed. Lemma oprod_crit_aux n x (y := omega0 ^o (omega0 ^o n)): ordinalp n -> \1o <=o x -> x x *o y = y. Proof. move => on x1 xy. move: OS_omega OS1 olt_1omega => oo o1 lt1o. have oy1:= OS_pow OS_omega on. have oy:= OS_pow OS_omega oy1. have xp: \0o //; apply: omega_pow_nz. case: (ozero_dichot on) => nz. move: xy;rewrite /y nz opowx0 (opowx1 OS_omega) => aux2. rewrite oprod_int_omega //. have aux1: omega0 *o (omega0 ^o (omega0 ^o n)) = omega0 ^o (omega0 ^o n). rewrite - {1} (opowx1 OS_omega) - opow_sum //;congr (_ ^o _). apply: ord_negl_p2 => //. have ox:= proj32 x1. have od:=(OS_the_CNF_degree ox). rewrite /y - aux1 (oprodA ox oo oy) (CNF_prod_pr2bis xp). rewrite - (oprodA (OS_pow oo od) oo oy) aux1. move: xy; rewrite - (opow_sum oo od oy1) => h2. by rewrite (indecomp_prop1 (indecomp_prop4 on) (the_CNF_p6 oy1 xp h2)). Qed. Lemma CNF_prod_pr3 x y: \0o limit_ordinal y -> x *o y = omega0 ^o (the_CNF_degree x) *o y. Proof. move=> xnz ly; move:(proj32_1 xnz) => ox. move: (CNF_limit3 ly) => [z oz yv]. have ot := (OS_pow OS_omega (OS_the_CNF_degree ox)). by rewrite yv (oprodA ox OS_omega oz) (CNF_prod_pr2bis xnz) (oprodA ot OS_omega oz). Qed. Lemma CNF_prod_pr4 eX cX n eY cY p (x:= CNFbvo eX cX (csucc n)) (y:= CNFbvo eY cY (csucc p)): natp n -> natp p -> CNFb_axo eX cX (csucc n) -> CNFb_axo eY cY (csucc p) -> \0o x *o y = omega0 ^o (eX n) *o y. Proof. move=> nN pN ax ay pnz. move: (CNF_limit2 pN ay pnz) => ly. move: (the_CNF_p5 nN ax) => [xp dx]. by move:(CNF_prod_pr3 xp ly); rewrite -/y dx. Qed. Lemma CNF_prod_pr5 eX cX n eY cY p (eZ:= fun i => (eX n) +o eY i) (x:= CNFbvo eX cX (csucc n)) (y:= CNFbvo eY cY (csucc p)): natp n -> natp p -> CNFb_axo eX cX (csucc n) -> CNFb_axo eY cY (csucc p) -> \0o (CNFb_axo eZ cY (csucc p) /\ x *o y = CNFbvo eZ cY (csucc p)). Proof. move=> nN pN ax ay pnz. move: (CNF_se_p (NS_succ pN) ay (CNFb_p8 ax nN)) => [sa ->]; split => //. by rewrite CNF_prod_pr4. Qed. Lemma CNF_prod_pr6 eX cX n eY cY p (x:= CNFbvo eX cX (csucc n)) (y:= CNFbvo eY cY (csucc p)) (cZ := cnf_m (cnf_change_n cX n (cX n *o cY \0o)) (fun z => cY (csucc z)) (csucc n)) (eZ := cnf_m eX (fun z => (eX n) +o (eY (csucc z))) (csucc n)): natp n -> natp p -> CNFb_axo eX cX (csucc n) -> CNFb_axo eY cY (csucc p) -> eY \0c = \0o -> (CNFb_axo eZ cZ (csucc (n +c p)) /\ x *o y = CNFbvo eZ cZ (csucc (n +c p))). Proof. move => nN pN ax ay tcy. rewrite /y. have spp:= (succ_positive p). have c0p:= (proj2 ay _ spp). have snN:= (NS_succ nN). have oc0:= (proj32_1 c0p). have c0o: cY \0c [[_ _ h _] _]; apply: (h _ spp). have [om1 ay1 ->] := (CNFb_Al pN ay). move: (OS_CNFb pN ay1) (OS_CNFb snN ax) => oy1 ox. rewrite (oprodD oy1 om1 ox) /cantor_mon tcy opowx0 (oprod1l oc0). move: (CNF_prod_pr1 c0p c0o nN ax) => [ax1 ->]. move: ax1; rewrite /cZ; set c1:= (cnf_change_n cX n (cX n *o cY \0c)) => ax1. case (equal_or_not p \0o) => pnz. rewrite pnz (csum0r (CS_nat nN)) CNFq_p2 oprod0r (osum0l (OS_CNFb snN ax1)). apply:(CNFb_exten _ _ ax1 snN). by move => i lin; rewrite /eZ/cnf_m; Ytac0. by move => i lin; rewrite /cnf_m; Ytac0. move: (cpred_pr pN pnz); set m := (cpred p); move => [mN mv]. rewrite mv in ay1; rewrite mv. have cp1: (\0o [ax2 ->]. have sa: \0c +c csucc m = csucc m by rewrite csum0l; fprops. have sb: eX n [ax3 ->]. rewrite sa - (csum_Sn (csucc m) nN). have hh: forall k, (k -c (csucc n)) +c \0c = (k -c (csucc n)). move=> k; exact:(csum0r (CS_cardinal (k -s csucc n))). apply: (CNFb_exten _ _ ax3 (NS_sum (NS_succ nN) (NS_succ mN))). by move => i isn; rewrite/eZ /cnf_m /cnf_s hh. by move => i isn; rewrite /cnf_m /cnf_s hh. Qed. Lemma CNF_succ_pow1 n c (x := (osucc ((omega0 ^o n) *o c))) (X:= the_CNF x) (eX := (Vg (P (Q (the_CNF x))))) (cX := (Vg (Q (Q (the_CNF x))))): \0o \0o c [/\ CNFb_axo eX cX (P X), CNFbvo eX cX (P X) = x & [/\ P X = \2c, eX \0c = \0o, eX \1c = n, cX \0c = \1o & cX \1c = c]]. Proof. move: OS0 => oz np cp lco. move: ole_2omega NS2 NS1 => le2 bs2 bs1. have oc:= proj32_1 cp. have on:= proj32_1 np. have o1:= OS_pow OS_omega on. have o2:= OS_prod2 o1 oc. move: NS0 clt_02 clt_12 clt_01 => bs0 lt02 lt12 [_ n01]. set ex := fun z => Yo (z = \0c) \0o n. set cx := fun z => Yo (z = \0c) \1o c. have e0: ex \0c = \0o by rewrite /ex; Ytac0. have e1: ex \1c = n by rewrite /ex; Ytac0. have c0: cx \0c = \1o by rewrite /cx; Ytac0. have c1: cx \1c = c by rewrite /cx; Ytac0. have ax: CNFb_axo ex cx \2c. split; first split. + exact. + by move => i lin; rewrite /ex; Ytac h. + by move => i lin; rewrite /cx; Ytac h => //; apply: olt_1omega. + move => i iN /clt2; rewrite /ex; move: (@succ_nz i) => ss. rewrite - succ_zero; case => // si. by move: (succ_injective1 (CS_nat iN) CS0 si) => iz; Ytac0; Ytac0. + by move => i lin; rewrite /cx; Ytac h => //; apply: olt_01. move: (CNFbB_prop ax NS2); set y := (CNFbB \2c ex cx); move => [ax2 yv]. have py2: P y = \2c by rewrite /y /CNFbB; aw. move: (the_CNF_p0 (OS_succ o2)); rewrite -/x; move => [ax3 xv]. move: (CNFB_ax_simp ax2) => [_ ax4]. have eq1:CNFBv (the_CNF x) = CNFBv y. rewrite py2 in ax4. move: (CNFq_p7 (proj1 ax4) lt12). rewrite xv /CNFBv /y /CNFbB !(pr1_pair, pr2_pair) -/CNFbvo => ->. rewrite /cantor_mon; bw; repeat Ytac0; rewrite e0 c0 e1 c1. by rewrite opowx0 (oprod1r OS1) (osucc_pr o2). move:(CNFB_unique ax3 ax2 eq1). rewrite -/(CNFBv (the_CNF x)) xv /eX /cX -/X => ->; split. + exact. + exact. + by rewrite /y /CNFbB !(pr1_pair, pr2_pair); bw; repeat Ytac0; split. Qed. Lemma CNF_succ_pow n (x := (osucc (omega0 ^o n))) (X:= the_CNF x) (eX := (Vg (P (Q (the_CNF x))))) (cX := (Vg (Q (Q (the_CNF x))))): \0o [/\ CNFb_axo eX cX (P X), CNFbvo eX cX (P X) = x & [/\ P X = \2c, eX \0c = \0o, eX \1c = n, cX \0c = \1o & cX \1c = \1o]]. Proof. move: olt_01 olt_1omega => hb hc ha. move:(CNF_succ_pow1 ha hb hc). by rewrite(oprod1r (OS_pow OS_omega (proj32_1 ha))). Qed. Lemma succ_pow_omega_irred p a b: ordinalp p -> ordinalp a -> ordinalp b -> osucc (omega0 ^o p) = a *o b -> (a = \1o \/ b = \1o). Proof. move=>on oa ob sab. case: (ozero_dichot on) => pz. by apply: oprod2_two => //; rewrite - sab pz opowx0 // osucc_one. move: (CNF_succ_pow pz). set ep := Vg _ ; set cp := Vg _; set np:= (P (the_CNF _)). move => [axp pv etc]. have snz: a *o b <> \0o by rewrite - sab;apply: osucc_nz. have anz: a <> \0o by move =>h; case: snz; rewrite h oprod0l. have bnz: b <> \0o by move =>h; case: snz; rewrite h oprod0r. move:(ord_ne0_pos oa anz) (ord_ne0_pos ob bnz) => ap bp. move: (the_CNF_p0 oa) (the_CNF_p0 ob) => [sa sb][sc sd]. move: (CNFB_ax_simp sa) (CNFB_ax_simp sc) (the_CNF_p2 ap) (the_CNF_p2 bp). move: sb sd; rewrite /CNFBv. set ea := Vg _ ; set ca := Vg _; set na:= (P (the_CNF a)); set ma:=(cpred na). set eb := Vg _ ; set cb := Vg _; set nb:= (P (the_CNF b)); set mb:=(cpred nb). move => va vb [naN axa] [nbN axb] [maN mav] [mbN mbv]. rewrite mav in axa; rewrite mbv in axb. move: (succ_positive ma)(succ_positive mb) => spa spb. move: (axb)(axa) => [[_ h1b h2b _] _] [[_ h1a h2a _] _]. have oeb0:= (h1b _ spb). have ocb0:= (proj31_1 (h2b _ spb)). have oca0:= (proj31_1 (h2a _ spa)). move: etc => [x0 x1 x2 x3 x4]. have npN: natp np by rewrite x0; fprops. case (ozero_dichot oeb0) => ez. move: (CNF_prod_pr6 maN mbN axa axb ez). rewrite -mav -mbv va vb; move => [su sv]. move: pv; rewrite sab sv => eq. have dN:= (NS_succ (NS_sum maN mbN)). move: (CNFb_unique npN dN axp su eq); rewrite x0; move => [ha hb]. have nap: \0c maz. rewrite mav maz succ_zero; Ytac0; move => [ua ub]. symmetry in ub; move: (oprod2_one oca0 ocb0 ub) => [ca0 _] _. left; rewrite - va mav maz succ_zero. rewrite /CNFbvo (CNFq_p3 (proj1 axa) spa). by rewrite /cantor_mon -ua ca0 opowx0 (oprod1r OS1). case (equal_or_not mb \0c) => mbz _ [ _] . move: clt_12 => l12. move:mab1; rewrite mbz (csum0r (CS_nat maN)) => ma1. rewrite mav - ma1 succ_one; Ytac0; Ytac0 => eq1. have hh: \1c /proj31_1. symmetry in eq1; move: (oprod2_one oca1 ocb0 eq1) => [_ cb0]. right; rewrite - vb mbv mbz succ_zero. rewrite /CNFbvo (CNFq_p3 (proj1 axb) spb). by rewrite /cantor_mon ez cb0 opowx0 (oprod1r OS1). move: (cge1 (CS_nat maN) maz) (cge1 (CS_nat mbN) mbz). move => l1 l2; move: (csum_Mlele l1 l2); rewrite - mab1 card_two_pr. move => /(cltNge clt_12) []. move: (CNF_prod_pr5 maN mbN axa axb ez). rewrite -mav -mbv va vb; move => [su sv]. move: pv; rewrite sab sv => eq. move: (CNFb_unique npN nbN axp su eq); rewrite x0; move => [ha hb]. move:(esym (proj1 (hb _ clt_02))); rewrite x1 => e1. move:(osum2_zero (h1a _ (cltS maN)) oeb0 e1) => [_ h]. by move: (proj2 ez); rewrite h; case. Qed. Lemma opow_int_omega n: \2o <=o n -> n n ^o omega0 = omega0. Proof. move=> n2 no. have oo:= OS_omega. have on:= proj32 n2. have nz:=(olt_leT olt_02 n2). apply:oleA. rewrite (proj2 (opow_normal n2) _ omega_limit). apply: ord_ub_sup => //. by move => x /funI_P [z /(oltP oo) /(opow_2int1 no) [zo _] ->]. by move: (opow_Mspec2 oo n2); rewrite oprod_int_omega. Qed. Lemma CNF_pow_pr1 (e c:fterm) n k (x:= CNFbvo e c (csucc n)): CNFb_axo e c (csucc n) -> \0o natp k -> natp n -> x ^o (osucc k) = (omega0 ^o ((e n) *o k)) *o x. Proof. move=> ax ep kN nN. have ox:=(OS_CNFb (NS_succ nN) ax). have olcx:= CNFb_p8 ax nN. move: k kN; apply: Nat_induction. by rewrite (oprod0r) opowx0 (oprod1l ox) osucc_zero opowx1. move=> k kN hrec. move/NatP: (kN) => p2. have ok:= proj1 p2. have osk:= OS_succ ok. have odf:=(OS_prod2 olcx ok). move: (OS_pow OS_omega odf)(OS_pow OS_omega olcx) => of1 ood. rewrite (succ_of_finite p2) (opow_succ ox osk) hrec - (oprodA of1 ox ox). rewrite (CNF_prod_pr4 nN nN ax ax ep) (oprodA of1 ood ox)(oprod2_succ olcx ok). by rewrite - (opow_sum OS_omega odf olcx). Qed. Lemma CNF_pow_pr2 ex cx ey cy n m k: CNFb_axo ex cx (csucc n) -> CNFb_axo ey cy m -> natp n -> natp m -> natp k -> k <> \0c -> \0o (CNFbvo ex cx (csucc n)) ^o k = (CNFbvo ey cy m) -> [/\ m <> \0c, ey (cpred m) = (ex n) *o k & cy (cpred m) = cx n]. Proof. move => ax ay nN mN kN kp cnp. have [pa pb]:=(cpred_pr kN kp). have snN:= (NS_succ nN). set q := cpred k in pa pb; rewrite pb. clear kN kp pb; move: q pa m ey cy mN ay; clear k. have ox:= OS_CNFb snN ax. have lts:=(cltS nN). have oo: ordinalp (ex \0o). move: (ax) =>[[_ h1 _ _] _]; exact: (h1 _ (succ_positive n)). have op:= CNFb_p8 ax nN. apply: Nat_induction. move=> m ey cy mN ay. rewrite succ_zero (opowx1 ox) (oprod1r op) => eq1. move: (CNFb_unique snN mN ax ay eq1) => [<- hb]. rewrite (cpred_pr2 nN); move:(hb _ lts) => [-> ->]. split; [apply: succ_nz | exact | exact]. move => k kN Hrec m ey cy mN ay. have skN:= (NS_succ kN). move/NatP: (skN) => p2. have ok:= proj1 p2. have osk:= OS_succ ok. rewrite (succ_of_finite p2) (opow_succ ox ok). move: (the_CNF_p0(OS_pow ox ok)) => [/CNFB_ax_simp]; rewrite /CNFBv. set w :=_ ^o _; set ew := Vg _; set cw := Vg _; set m' := P _. move => [m'N ay'] yv eq1. move: (Hrec _ _ _ m'N ay' (esym yv)) => [ha hb hc]. move: (cpred_pr m'N ha)=> [m''N mv]. rewrite mv in ay'. case (ozero_dichot oo) => h0. move: (CNF_prod_pr6 m''N nN ay' ax h0) => [ax2]. rewrite - mv yv eq1 => eq2. have nmN:= (NS_sum m''N nN). rewrite {2 5} mv in eq2. move: (CNFb_unique mN (NS_succ nmN) ay ax2 eq2) => [-> h]. rewrite (cpred_pr2 nmN); move:(h _ (cltS nmN)) => [-> ->]. case:(equal_or_not n \0c) => nez. by move: (proj2 cnp); rewrite nez h0; case. rewrite /cnf_m /cnf_change_n. move: (cpred_pr nN nez) => [hu hv]. have ->: (cpred m' +c n) = m' +c (cpred n). by rewrite {1} hv (csum_nS _ hu) - (csum_Sn _ m''N) - mv. rewrite - mv; Ytac hw; last Ytac0. case:(cltNge hw (csum_M0le (cpred n) (CS_nat m'N))). rewrite (csumC m' (cpred n)) (cdiff_pr1 hu m'N). rewrite hb (oprod2_succ op ok) - hv. split; [apply: succ_nz | exact | exact]. move: (CNF_prod_pr5 m''N nN ay' ax h0) => [ax2]. rewrite - mv yv eq1 => eq2. move: (CNFb_unique mN snN ay ax2 eq2) => [-> h]. rewrite (cpred_pr2 nN); move:(h _ (cltS nN)) => [-> ->]. rewrite hb (oprod2_succ op ok). split; [apply: succ_nz | exact | exact]. Qed. Lemma CNF_pow_pr3 (e c:fterm) n: CNFb_axo e c (csucc n) -> \0o natp n -> (CNFbvo e c (csucc n)) ^o omega0 = omega0 ^o ((e n) *o omega0). Proof. move=> ax exp nN. have oo:= OS_omega. have oen:= (proj32_1 exp). move:(CNFq_pg4 nN ax) (proj1 (CNFq_pg1 nN (proj1 ax))) => le1 le2. have pa:= (omega_pow_pos oen). move:(opow_Mleeq (nesym (proj2 pa)) le1 OS_omega). move:(opow_Mleeq (nesym (proj2 (olt_leT pa le1))) le2 OS_omega). rewrite - (opow_prod oo (OS_succ oen) oo) - (opow_prod oo oen oo). rewrite(indecomp_prod3 exp);apply: oleA. Qed. Lemma CNF_pow_pr4 ex cx n ey cy m (x:=CNFbvo ex cx (csucc n)) (y:=CNFbvo ey cy (csucc m)): CNFb_axo ex cx (csucc n) -> \0o natp n -> CNFb_axo ey cy (csucc m) -> \0o natp m -> x ^o y = omega0 ^o ((ex n) *o y). Proof. move=> ax xp nN ayn yp mN. rewrite /y;move:(CNF_limit mN ayn yp) => [z oz ->]. have ox := OS_CNFb (NS_succ nN) ax. have oo:= OS_omega. have op := (proj32_1 xp). rewrite (opow_prod ox oo oz) (CNF_pow_pr3 ax xp nN). by rewrite - (opow_prod oo (OS_prod2 op oo) oz) (oprodA op oo oz). Qed. Lemma CNF_pow_pr5 x ey cy m (y:=CNFbvo ey cy (csucc m)): \2o <=o x -> x CNFb_axo ey cy (csucc m) -> \0o natp m -> exists z, [/\ ordinalp z, y = omega0 *o z & x ^o y = omega0 ^o z]. Proof. move=> x2 xo ayn tcy mN. have ox:= proj32 x2. rewrite /y;move: (CNF_limit mN ayn tcy) => [z oz ->]. by rewrite (opow_prod ox OS_omega oz) (opow_int_omega x2 xo); exists z. Qed. (** Cantor product form *) Definition CNFp_value1 e c := osucc ((omega0 ^o e) *o c). Definition CNFp_value2 e c := (osucc (omega0 ^o e)) *o c. Lemma CNFp_pr1 e c: \0o \0o c CNFp_value1 e c = CNFp_value2 e c. Proof. move=> ep cp co. have oe:= (proj32_1 ep). have oc:= (proj32_1 cp). have os1:= (OS_pow OS_omega oe). rewrite /CNFp_value2 /CNFp_value1. move:(CNF_succ_pow ep) (CNF_succ_pow1 ep cp co). set ex := Vg _; set cx := Vg _; set n := P _. set ey := Vg _; set cy := Vg _; set m := P _. move => [ax <- [n2 ex0 ex1 cx0 cx1]] [ay <- [m2 ey0 ey1 cy0 cy1]]. move: n2; rewrite - succ_one => n2; rewrite n2; rewrite n2 in ax. move: (CNF_prod_pr1 cp co NS1 ax) => [ax2 ->]. rewrite succ_one m2. apply: (osum_expansion_exten NS2) => i i2. rewrite /cantor_mon /cnf_change_n. case: (clt2 i2) => ->. by move: card1_nz => h; rewrite ex0 cx0 ey0 cy0; Ytac0. by rewrite ex1 cx1 ey1 cy1; Ytac0; rewrite (oprod1l oc). Qed. Definition CNFp_ax e c n:= [/\ (forall i, i \0o \0o \0o \0o CNFp_value1 (e i) (c i)) n. Definition CNFpv e c n := ((omega0 ^o (e n)) *o (c n)) *o (CNFpv1 e c n). Lemma CNFp_ax_ax1 e c n: CNFp_ax e c n -> CNFp_ax1 e c n. Proof. by move => [a1 a2 _]; split => // i [lin _]; apply a2. Qed. Lemma OS_CNFp0 e c n: CNFp_ax1 e c n -> ord_below_n (fun i => (CNFp_value1 (e i) (c i))) n. Proof. move => [ax1 ax2] i lin. move: (proj32_1 (ax1 _ lin)) (proj32_1 (proj1 (ax2 _ lin))). move => o1 o2;exact : (OS_succ (OS_prod2 (OS_pow OS_omega o1) o2)). Qed. Lemma OS_CNFp1 e c n: CNFp_ax1 e c n -> natp n -> ordinalp (CNFpv1 e c n). Proof. move => ax nN; apply: (OS_oprod_expansion nN) => // i lin. apply:(OS_CNFp0 ax lin). Qed. Lemma OS_CNFp1r e c n m: CNFp_ax1 e c n -> natp n -> m <=c n -> ordinalp (CNFpv1 e c m). Proof. move => ax nN nm; apply: (OS_oprod_expansion (NS_le_nat nm nN)) => // i lin. apply:(OS_CNFp0 ax (clt_leT lin nm)). Qed. Lemma OS_CNFp e c n: CNFp_ax e c n -> natp n -> ordinalp (CNFpv e c n). Proof. move => ax nN. move: (OS_CNFp1 (CNFp_ax_ax1 ax) nN) => o1. move:ax => [_ ax2 ax3]. have oc := (proj32_1(proj1 (ax2 _ (cleR (CS_nat nN))))). exact (OS_prod2 (OS_prod2 (OS_pow OS_omega ax3) oc) o1). Qed. Lemma CNFp_0 e c: CNFpv1 e c \0c = \1o. Proof. by apply: oprod_expansion0. Qed. Lemma CNFp_1 e c n: CNFp_ax1 e c n -> \0c CNFpv1 e c \1c = CNFp_value1 (e \0c) (c \0c). Proof. move => ax1 n1; rewrite /CNFpv1 oprod_expansion1 //. apply: (OS_CNFp0 ax1 n1). Qed. Lemma CNFp_A e c n m : natp n -> natp m -> CNFp_ax1 e c (n +c m) -> CNFpv1 e c (n +c m) = (CNFpv1 e c n) *o CNFpv1 (fun z => e (z +c n)) (fun z => c (z +c n)) m. Proof. move => nN mN /OS_CNFp0; exact(oprod_expansionA nN mN). Qed. Lemma CNFp_r e c n: natp n -> CNFpv1 e c (csucc n) = CNFpv1 e c n *o (CNFp_value1 (e n) (c n)). Proof. move => nN; exact:(oprod_expansion_succ _ nN). Qed. Lemma CNFp_p2 e c n (a:= e n -o (e (cpred n))) (b := c n): CNFb_axo e c (csucc n) -> natp n -> n <> \0c -> [/\ \0o ax nN nz. move: (cpred_pr nN nz) => [pnN pn]. move: (ax) => [[_ _ pe pf] pg]. have nn:= (cltS nN). have lt1: e (cpred n) h; exact:(pf _ pnN h). move: (odiff_pos lt1);move: lt1 => [le1 _]; move: (odiff_pr le1) => [oa pi] pj. move:(pg _ nn) (pe _ nn) => pa pb. rewrite -/a in oa. split => //. move: (ord_rev_pred pj) =>[]; rewrite -/a => osa av. have ax2:= (CNFb_p5 nN ax). have pc:= (OS_CNFb nN ax2); rewrite pn in ax2. have ocn := (proj32_1 pa). have od1 := OS_pow OS_omega oa. have od2 := OS_pow OS_omega osa. have oc1 := (proj31 le1). by rewrite /CNFbvo (CNFq_p1 _ _ _ nN) /CNFp_value1 (oprod2_succ pc (OS_prod2 od1 ocn)) (oprodA pc od1 ocn) /cantor_mon pi (opow_sum OS_omega oc1 oa) av (opow_sum OS_omega OS1 osa) (opowx1 OS_omega)(oprodA (OS_pow OS_omega oc1) OS_omega od2) (oprodA pc OS_omega od2) - (CNF_prod_pr2 pnN ax2) - pn. Qed. Lemma CNFp_p3 e c n: CNFb_axo e c (csucc n) -> natp n -> exists e' c', [/\ CNFp_ax e' c' n, CNFbvo e c (csucc n) = CNFpv e' c' n, (forall i, i e' i = e (csucc i) -o (e i) /\ c' i = c (csucc i)), e' n = e \0c & c' n = c \0c]. Proof. move => ax nN; move: n nN ax; apply: Nat_induction. move => h0; exists e,c. move: (h0) (succ_positive \0c) => [[_ h1 h2 _] h4] sp. move: (h1 _ sp) (h2 _ sp) (h4 _ sp) => a1 a2 a4. have oc:= OS_prod2 (OS_pow OS_omega a1) (proj31_1 a2). rewrite /CNFpv CNFp_0 succ_zero /CNFbvo. rewrite (CNFq_p3 (proj1 h0) (cltS NS0)) (oprod1r oc). split => //; [split | by move => i /clt0]. - by move => i /clt0. - by move => i /cle0 ->. - exact. move => n nN Hrec ax. move: (CNFp_p2 ax (NS_succ nN) (@succ_nz n)) => [pa1 pa2 pa3 ->]. move: (Hrec (CNFb_p5 (NS_succ nN) ax)) => [e' [c' [ax3 -> h1 h2 h3]]]. set sa := _ -o _; set sb := c (csucc n). move: (proj32_1 pa1) (proj32_1 pa2) => osa osb. have of3:=(OS_succ (OS_prod2 (OS_pow OS_omega osa) osb)). have of1:ordinalp (omega0 ^o e' n *o c' n). rewrite h2 h3; exact:(CNFq_p0 (proj1 ax) (succ_positive (csucc n))). pose e1 i := Yo (i = (csucc n)) (e \0c) (Yo (i = n) sa (e' i)). pose c1 i := Yo (i = (csucc n)) (c \0c) (Yo (i = n) sb (c' i)). have eqA: e1 (csucc n) = e' n by rewrite /e1; Ytac0. have eqB: c1 (csucc n) = c' n by rewrite /c1; Ytac0. rewrite - h2 - h3. exists e1,c1. have nn:= (proj2 (cltS nN)). rewrite /CNFpv (CNFp_r _ _ nN) eqA eqB {3} /e1 {3} /c1;repeat Ytac0. have ->: CNFpv1 e1 c1 n = CNFpv1 e' c' n. apply:(oprod_expansion_exten nN) => i lin. move: (proj2(clt_leT lin (cleS nN))) (proj2 lin) => ha hb. by rewrite /e1 /c1; repeat Ytac0. rewrite (oprodA of1 (OS_CNFp1 (CNFp_ax_ax1 ax3) nN) of3). have aux: forall i, i (i <> csucc n /\ (i = n \/ (i <> n /\ i i h ; split; first by exact (proj2 h). move /(cltSleP nN): h => lt1. by case: (equal_or_not i n) => hc; [left | right]. split; try reflexivity; last first. move => i /aux [ha hb];rewrite /e1 /c1; Ytac0; Ytac0; case: hb. by move => ein; Ytac0; Ytac0; rewrite ein /sa (cpred_pr2 nN). by move => [ein hb]; Ytac0; Ytac0; apply: (h1 _ hb). move: ax3 => [pa pb pc]; hnf; rewrite eqA; split; last exact. move => i /aux [ha hb];rewrite /e1; Ytac0; case: hb. by move => ein; Ytac0. by move => [ein hb]; Ytac0; apply: pa. move => i isn; rewrite /c1; case (equal_or_not i (csucc n)) => eq1; Ytac0. rewrite - h3; apply:pb; fprops. case: (equal_or_not i n) => eq2; Ytac0; first done. by move /(cltSleP nN): (conj isn eq1) => /pb. Qed. Lemma CNFp_exists x: \0o exists e c n, [/\ CNFp_ax e c n, natp n & x = CNFpv e c n]. Proof. move=> xp. move: (the_CNF_p0 (proj32_1 xp)) => [ax0 xv]. move: (CNFB_ax_simp ax0) (the_CNF_p2 xp) => [pb ax] [nN pc]. rewrite pc in ax. move:(CNFp_p3 ax nN) => [e [c [sa sb _ _ _]]]. by exists e,c, (cpred (P (the_CNF x))); rewrite - sb - pc. Qed. Lemma CNFp_p4 e c n: CNFp_ax e c n -> natp n -> exists e' c', [/\ CNFb_axo e' c' (csucc n), CNFbvo e' c' (csucc n) = CNFpv e c n, forall i, i e i = e' (csucc i) -o (e' i) /\ c i = c' (csucc i), e n = e' \0c & c n = c' \0c]. Proof. move=> axy. pose e1 := induction_term (fun i z => z +o (e i)) (e n). pose c1 i := Yo (i = \0c) (c n) (c (cpred i)). move => nN. have pe: c n = c1 \0c by rewrite /c1; Ytac0. have pd: e n = e1 \0c by rewrite /e1 induction_term0. have hc: forall i, inc i Nat -> e1 (csucc i) = e1 i +o e i. by move=> i iN; rewrite /e1 induction_terms. have ose: forall i, i ordinalp (e i). move => i lin; move:(NS_lt_nat lin nN) => iN. move: axy => [a1 a2 a3]; exact(proj32_1 (a1 _ lin)). have ose1: forall i, i <=c n -> ordinalp (e1 i). move => i lin; move:(NS_le_nat lin nN) => iN. move: axy => [a1 a2 a3]. move: i iN lin; apply: Nat_induction. by rewrite - pd => _. move => i iN hr sin; rewrite (hc _ iN). have lin:= (clt_leT (cltS iN) sin). exact: (OS_sum2 (hr (proj1 lin)) (ose _ lin)). have pc: forall i,i e i = e1 (csucc i) -o e1 i /\ c i = c1 (csucc i). move => i lin; have iN:=(NS_lt_nat lin nN); split; last first. by rewrite /c1 (cpred_pr2 iN) (Y_false (@succ_nz i)). by rewrite (hc _ iN) (odiff_pr1 (ose1 _ (proj1 lin)) (ose _ lin)). have pc2: forall i, i i <> \0c -> [/\ (cpred i i lin inz. move: (cpred_pr (NS_lt_nat lin (NS_succ nN)) inz) => [pa pb]. rewrite pb in lin; move /(cltSSP (CS_nat pa) (CS_nat nN)): lin => sin. by rewrite {2} pb - (hc _ pa) /c1 (Y_false inz). have axx: CNFb_axo e1 c1 (csucc n). move: axy => [a1 a2 a3]. have [sa sb]:= (a2 _ (cleR (CS_nat nN))). split; first split. - apply: ole_2omega. - by move => i /(cltSleP nN); apply: ose1. - move => i isn; case (equal_or_not i \0c) => eiz; first by rewrite eiz - pe. move:(pc2 _ isn eiz) => [sc _ ->]; exact: (proj2 (a2 _ (proj1 sc))). - move => i iN ssin. move: (pc2 _ ssin (@succ_nz i)); rewrite (cpred_pr2 iN); move => [sc sd _]. have oe:=(ose1 _ (proj1 sc)). by move: (osum_Meqlt (a1 _ sc) oe); rewrite (osum0r oe) sd. - move => i isn; case (equal_or_not i \0c) => eiz; first by rewrite eiz - pe. move:(pc2 _ isn eiz) => [sc _ ->];exact: (proj1 (a2 _ (proj1 sc))). move: (CNFp_p3 axx nN) => [e' [c' [ ax' sv qa qb qc]]]. have sv2: CNFbvo e1 c1 (csucc n) = CNFpv e c n. rewrite sv /CNFpv qb qc pe pd; apply: f_equal. apply:(oprod_expansion_exten nN) => i lin. by move: (qa _ lin) (pc _ lin) => [-> ->] [-> ->]. by exists e1, c1. Qed. Lemma CNFp_unique e c n e' c' n' : CNFp_ax e c n -> CNFp_ax e' c' n' -> natp n -> natp n' -> CNFpv e c n = CNFpv e' c' n' -> [/\ n = n', e n = e' n, c n = c' n, same_below e e' n & same_below c c' n]. Proof. move=> ax1 ax2 nN n'N eq. move: (CNFp_p4 ax1 nN) => [e1 [c1 [pa pb pc pd pe]]]. move: (CNFp_p4 ax2 n'N) => [e1' [c1' [pa' pb' pc' pd' pe']]]. rewrite -pb -pb' in eq. move: (CNFb_unique (NS_succ nN) (NS_succ n'N) pa pa' eq) => [sa sb]. have nn:= (succ_injective1 (CS_nat nN) (CS_nat n'N) sa). have [a1 a2]: (e n = e' n /\ c n = c' n). rewrite pd pe nn pd' pe'; exact:(sb _ (succ_positive n)). rewrite - nn in pc';split. + exact. + exact. + exact. + move => i lin;rewrite (proj1 (pc _ lin)) (proj1 (pc' _ lin)). rewrite (proj1 (sb _ (clt_leT lin (cleS nN)))). by rewrite (proj1 (sb _ (cltSS lin))). + move => i lin; rewrite (proj2 (pc _ lin)) (proj2 (pc' _ lin)). exact (proj2 (sb _ (cltSS lin))). Qed. Lemma osum2_commutes a b: ordinalp a -> ordinalp b -> ((a +o b = b +o a) <-> (exists c n m, [/\ ordinalp c, natp n, natp m, a = c *o n & b = c *o m])). Proof. move=> oa ob; split; last first. move=> [c [n [m [oc nN mN av bv]]]]. have on: ordinalp n by apply: OS_cardinal; fprops. have om: ordinalp m by apply: OS_cardinal; fprops. rewrite av bv - (oprodD on om oc) - (oprodD om on oc). by rewrite (osum2_2int nN mN)(osum2_2int mN nN) csumC. move=> hc. case: (ozero_dichot oa) => az. exists b, \0c, \1c;split;fprops. by rewrite az (oprod0r). by rewrite (oprod1r ob). case: (ozero_dichot ob) => bz. exists a, \1c, \0c;split;fprops. by rewrite (oprod1r oa). by rewrite bz (oprod0r). move: (the_CNF_p0 oa) => [ax0 xv]. move: (the_CNF_p2 az)(CNFB_ax_simp ax0) => [nN pc][]. move: nN xv; rewrite /CNFBv {2 3 4} pc. set ea := Vg _; set ca := Vg _; set n := cpred _ => nN av snN axa. move: (the_CNF_p0 ob) => [ax0' xv']. move: (the_CNF_p2 bz)(CNFB_ax_simp ax0') => [nN' pc'][]. move: nN' xv'; rewrite /CNFBv {2 3 4} pc'. set eb := Vg _; set cb := Vg _; set m := cpred _ => mN bv smN axb. clear pc pc' ax0 ax0'. set ean := ea n; set can := ca n; set ebn := eb m; set cbn := cb m. move: (cltS nN) (cltS mN) => snn smm. move: (axa) (axb) => [[_ a1 a2 a3] a4] [[_ b1 b2 b3] b4]. move: (a1 _ snn) (b1 _ smm) => oean oebn. case: (oleT_ell oean oebn); last first => cpe. move: (ord_negl_p8 axb axa mN nN cpe); rewrite av bv /ord_negl - hc => bad. by case: (proj2 bz); rewrite (osum_a_ab oa ob bad). move: (ord_negl_p8 axa axb nN mN cpe); rewrite av bv /ord_negl hc => bad. by case: (proj2 az);rewrite (osum_a_ab ob oa bad). move: (CNF_sum_pr3 mN nN axb axa cpe). move: (CNF_sum_pr3 nN mN axa axb (esym cpe)). move => [ax1 v1][ax2]; rewrite av bv - hc - av -bv v1 => eq2. move: (CNFb_unique smN snN ax1 ax2 eq2) => [r1 r2]. move: (succ_injective1 (CS_nat mN) (CS_nat nN) r1) => nm. rewrite r1 in r2. move: (a2 _ snn) (a4 _ snn) (b2 _ smm) (b4 _ smm) => cao cap cbo cbp. move: (CNF_change_n_ax n olt_01 olt_1omega axa). set cx:= cnf_change_n ca n \1o => ax3. exists (CNFbvo ea cx (csucc n)), can,cbn. split. + exact: (OS_CNFb snN ax3). + by apply /olt_omegaP. + by apply /olt_omegaP. + rewrite (proj2 (CNF_prod_pr1 cap cao nN ax3)). apply:(osum_expansion_exten snN) => i isn. rewrite/cantor_mon /cx /cnf_change_n; Ytac0; Ytac h; last by Ytac0. by rewrite h (oprod1l (proj31_1 cao)). have st: forall i, i eb i = ea i /\ cb i = ca i. move => i lin; have sin:= (clt_leT lin (cleS nN)). move: lin => [_] nin; move:(r2 _ sin). by rewrite /cnf_m /cnf_change_n nm; repeat Ytac0. have <-: CNFbvo eb (cnf_change_n cb m \1o) (csucc m) = CNFbvo ea cx (csucc n). rewrite nm; apply:(osum_expansion_exten snN) => i isn. rewrite /cantor_mon/cx/cnf_change_n;Ytac h; Ytac0; first by rewrite h cpe nm. move /(cltSleP nN): isn => lin. by move: (st _ (conj lin h)) => [-> ->]. move: (CNF_change_n_ax m olt_01 olt_1omega axb) => ax4. rewrite (proj2 (CNF_prod_pr1 cbp cbo mN ax4)). apply:(osum_expansion_exten smN) => i ism. rewrite /cantor_mon /cnf_change_n; Ytac0; Ytac h; last by Ytac0. by rewrite h (oprod1l (proj31_1 cbo)). Qed. Definition oprod_comm x y := (x *o y = y *o x). Lemma oprod2_comm1 ex cx n ey cy m (x:= CNFbvo ex cx (csucc n)) (y:= CNFbvo ey cy (csucc m)): CNFb_axo ex cx (csucc n) -> CNFb_axo ey cy (csucc m) -> natp n -> natp m -> ey \0c = \0o -> \0o oprod_comm x y -> y = \1o. Proof. move => ax ay nN mN h1 h2. move: (CNF_prod_pr5 mN nN ay ax h2) => [ax1 e1]. move: (CNF_prod_pr6 nN mN ax ay h1) => [ax2 e2]. rewrite /oprod_comm {1} e2 e1 => e3. have nmN:=(NS_sum nN mN). move:(CNFb_unique (NS_succ nmN) (NS_succ nN) ax2 ax1 e3) => [e4 e5]. move: (succ_injective1 (CS_nat nmN) (CS_nat nN) e4). rewrite - {2} (Nsum0r nN) => eq3. move: (csum_eq2l nN mN NS0 eq3) => mz. rewrite /y mz succ_zero /CNFbvo (CNFq_p3 (proj1 ay) (succ_positive m)). rewrite /cantor_mon h1 opowx0. have nsm:= (cltS nN). have h:n e6. move: ((proj2 ax) _ nsm) => cnz. have ocy:= (proj32_1 ((proj2 ay) _ (succ_positive m))). by rewrite (oprod2_simpl1 ocy cnz e6) (oprod1r OS1). Qed. Lemma oprod2_comm2 e c n mu (x:= CNFbvo e c (csucc n)) (y := (omega0 ^o mu) *o x): CNFb_axo e c (csucc n) -> natp n -> \0o ordinalp mu -> (e n) +o mu = mu +o (e n) -> oprod_comm x y. Proof. move=> ax nN pxnz om c1. have oe: ordinalp (e n). move: ax => [[_ h1 _ _] _]; apply: (h1 _ (cltS nN)). have oomu:= OS_pow OS_omega om. have ooe:= OS_pow OS_omega oe. have ox:= (OS_CNFb (NS_succ nN) ax). have oo:= OS_omega. case: (ozero_dichot om) => muz; first by rewrite /y muz opowx0 (oprod1l ox). move: (ord_rev_pred muz); set t:= _ -o _; move=> [ot tv]. have oot:= OS_pow oo ot. have oot1:= OS_prod2 oo oot. rewrite /oprod_comm - (oprodA oomu ox ox) (CNF_prod_pr4 nN nN ax ax pxnz). rewrite (oprodA oomu ooe ox) - (opow_sum oo om oe) - c1 (opow_sum oo oe om). rewrite /y tv (opow_sum oo OS1 ot) (opowx1 OS_omega). rewrite (oprodA ox oot1 ox) (oprodA ox oo oot) (CNF_prod_pr2 nN ax). by rewrite - (oprodA ooe oo oot). Qed. Definition oprod2_comm_P4 x y := exists n e c gamma c1 c2, [/\ CNFb_axo e c (csucc n), \0o oprod_comm x y. Proof. move=> [n [e [c [g [c1 [c2 [axn limX nN og [c1N c2N xv lcx yv]]]]]]]]. set mu:=(g *o c2). have oc1:= OS_nat c1N. have oc2:= OS_nat c2N. have omu:=(OS_prod2 og oc2). have coms: (e n) +o mu = mu +o (e n). rewrite lcx /mu - (oprodD oc1 oc2 og) - (oprodD oc2 oc1 og). by rewrite (osum2_2int c1N c2N) (osum2_2int c2N c1N) csumC. by move: (oprod2_comm2 axn nN limX omu coms); rewrite /= -xv /mu -yv. Qed. Lemma oprod2_comm4 ex cx n ey cy m (x := CNFbvo ex cx (csucc n)) (y := CNFbvo ey cy (csucc m)): CNFb_axo ex cx (csucc n) -> CNFb_axo ey cy (csucc m) -> natp n -> natp m -> \0o \0o oprod_comm x y -> (oprod2_comm_P4 x y \/ oprod2_comm_P4 y x). Proof. move=> ax ay nN mN tcX tcY. move: (CNF_prod_pr5 mN nN ay ax tcX) => [ax2 eq2]. move: (CNF_prod_pr5 nN mN ax ay tcY) => [ax1 eq1]. rewrite /oprod_comm {1} eq1 eq2 => eq3 {eq1 eq2}. move: (CNFb_unique (NS_succ mN) (NS_succ nN) ax1 ax2 eq3) =>[e1 e2]. have mn:=(succ_injective1 (CS_nat mN) (CS_nat nN) e1). move:(OS_CNFb (NS_succ nN) ax) (OS_CNFb (NS_succ mN) ay) => ox oy. rewrite mn in e2 ay. have nn:= cltS nN. move: (ax)(ay) => [[_ h1 _ _]_][[_ h2 _ _] _]. move: (h1 _ nn) (h2 _ nn) => odx ody. move: (proj1 (e2 _ nn)); rewrite (osum2_commutes odx ody). move => [c [c1 [c2 [oc c1N c2N p1v p2v]]]]. move:(NS_diff c1 c2N) (NS_diff c2 c1N). set c3:= c2 -c c1; set c4:= c1 -c c2 => c3N c4N. move:(OS_nat c1N)(OS_nat c2N) => oc1 oc2. move:(OS_nat c3N)(OS_nat c4N) => oc3 oc4. have disj: ((c1 +c c3 = c2 /\ c4 = \0c) \/ (c2 +c c4 = c1 /\ c3 = \0c)). case: (NleT_ee c1N c2N) => le1. by left; split; [ apply: (cdiff_pr le1) | apply: (cdiff_wrong le1) ]. by right; split; [ apply: (cdiff_pr le1) | apply: (cdiff_wrong le1) ]. have [t [ot tp1 tp2]]: exists t, [/\ ordinalp t, c1 = t +o c4 & c2 = t +o c3]. move:(esym (osum0r oc1))(esym (osum0r oc2)) => sa sb. move:(esym (osum2_2int c1N c3N))(esym (osum2_2int c2N c4N)) => sc sd. by case: disj;move => [<- ->]; [exists c1 | exists c2]; split. move: (p1v); rewrite tp1 (oprodD ot oc4 oc) => p1. move: (p2v); rewrite tp2 (oprodD ot oc3 oc) => p2. have occ3: ordinalp (c *o c3) by fprops. have occ4: ordinalp (c *o c4) by fprops. have sYv: (omega0 ^o (c *o c3)) *o x = (omega0 ^o (c *o c4)) *o y. move: (proj2 (CNF_se_p (NS_succ nN) ax occ3)) => sa. move: (proj2 (CNF_se_p (NS_succ nN) ay occ4)) => sb. rewrite /y mn -{1} sa - sb; apply: (osum_expansion_exten (NS_succ nN)). move => i lin; move: (e2 _ lin) => []. move: (ax)(ay) => [ [ _ r4 _ _] _] [ [ _ s4 _ _] _]. move: (r4 _ lin) (s4 _ lin) => oa ob. move:(OS_prod2 oc ot) (OS_prod2 oc oc4) (OS_prod2 oc oc3) => o1 o2 o3. rewrite p1 p2 - (osumA o1 o2 ob) - (osumA o1 o3 oa). move/(osum2_simpl (OS_sum2 o2 ob) (OS_sum2 o3 oa) o1). by rewrite /cantor_mon => -> ->. case: disj; move=> [pr1 pr2]. left; exists n, ex, cx, c,c1, c3. rewrite sYv pr2 (oprod0r) opowx0 (oprod1l oy) -p1v. by split; last split ;try reflexivity. right; exists m, ey, cy, c, c2, c4. rewrite - sYv pr2 (oprod0r) opowx0 (oprod1l ox) -/x -/y mn. by split; last split; try reflexivity. Qed. Lemma oprod2_comm5 ex cx n ey cy m (x := CNFbvo ex cx (csucc n)) (y := CNFbvo ey cy (csucc m)): CNFb_axo ex cx (csucc n) -> CNFb_axo ey cy (csucc m) -> ex \0c = \0o -> ey \0c = \0o -> n = \0c -> natp m -> oprod_comm x y -> (x = \1o \/ (finite_o x /\ finite_o y)). Proof. move=> ax ay limX limY nz mN. have nN: natp n by rewrite nz; fprops. have [fx xv]: finite_o x /\ x = cx \0c. move: (ax)(succ_positive n) => [[_ _ h _] _] sn. move: (h _ sn) => cp. rewrite /x nz succ_zero /CNFbvo (CNFq_p3 (proj1 ax) sn). rewrite /cantor_mon limX opowx0 (oprod1l (proj31_1 cp)). split; [ by apply /omega_P2; apply /(oltP OS_omega) | exact]. case: (NleT_el (NS_succ nN) mN) => mn; last first. move/(cltSleP nN): mn; rewrite nz => /cle0 mz. right; split; first by exact. move: (ay)(succ_positive m) => [[_ _ h _] _] sm. move: (h _ sm) => cp. rewrite /y mz succ_zero /CNFbvo (CNFq_p3 (proj1 ay) sm). rewrite /cantor_mon limY opowx0 (oprod1l (proj31_1 cp)). by apply /omega_P2; apply /(oltP OS_omega). move:(CNF_prod_pr6 nN mN ax ay limY) => [ax2 eq1]. move:(CNF_prod_pr6 mN nN ay ax limX) => [ax1 eq2]. rewrite /oprod_comm {1} eq1 eq2 => eq3 {eq1 eq2}. have cm:=(CS_nat mN). have mnn: m +c n = m by rewrite nz (csum0r cm). have ha: m = (csucc (m -c csucc n)). rewrite - (csucc_diff mN nN) nz; [ by rewrite (cdiff_n0 mN) | ue ]. rewrite (csumC n m) in ax1 ax2 eq3. rewrite mnn in ax1 ax2 eq3. move: (NS_succ mN) (cltS mN) => smN lt1. move: (proj2 (CNFb_unique smN smN ax2 ax1 eq3)) => hsv. move: (proj2 (hsv _ (cltS mN))); rewrite /cnf_m /cnf_change_n - ha. move:(cleNgt mn) => mn'. repeat Ytac0; rewrite - xv;move => eq2;left. exact: (oprod2_simpl1 (proj1 fx) (proj2 ay _ lt1) (esym eq2)). Qed. Definition CNF_mpe ex ey n m := fun z => Yo (z = (csucc n +c m)) (ex (csucc n)) (Yo (z = n) (ex n) (Yo (z Yo (z = (csucc n +c m)) (cx (csucc n)) (Yo (z = n) (cx n *o cy m) (Yo (z CNFp_ax ey cy m -> natp n -> natp m -> (CNFp_ax ez cz (csucc n +c m) /\ (cx (csucc n) *o (CNFpv1 ex cx (csucc n))) *o ((cy m) *o (CNFpv1 ey cy m)) = (cx (csucc n)) *o CNFpv1 ez cz (csucc n +c m)). Proof. move=> ax ay nN mN. move:(ax) (ay) => [p1 p2 p3] [p4 p5 p6]. have snN:= NS_succ nN. have ltnsn:=(cltS nN). have lenn:= cleR (proj32_1 ltnsn). have cnn:=(CS_nat nN). have axz: CNFp_ax ez cz (csucc n +c m). have aux: forall i, i i <> n -> ~ i (i -c (csucc n) i pa. case: (cleT_ell cnn (proj31_1 pa)) => //; first by move => ->. move => /(cleSltP nN) => ha _ _. rewrite csumC in pa; have hh:= (NS_sum mN snN). exact: (cdiff_Mlt mN (NS_lt_nat pa hh) ha pa). split. + move => i isn; rewrite /ez /CNF_mpe. move: (proj2 isn) => ha; Ytac0; clear ha. Ytac h0; first by apply:(p1 _ ltnsn). Ytac h3; first by apply:(p1 _ (clt_leT h3 (proj1 ltnsn))). exact: (p4 _ (aux _ isn h0 h3)). + move => i isn; rewrite /cz /CNF_mpc. Ytac h1; [by apply: (p2 _ lenn) | Ytac h0 ]. move:(p2 _ (proj1 ltnsn))(p5 _ (cleR (CS_nat mN))) => [s1 s2][s3 s4]. by split; [ apply: oprod2_pos| apply: oprod2_lt_omega]. Ytac h3; first by apply:(p2 _ (cleT (proj1 h3) (proj1 ltnsn))). exact: (p5 _ (proj1 (aux _ (conj isn h1) h0 h3))). + rewrite /ez /CNF_mpe; Ytac0;apply: p3. split; first by exact. have ax':= (CNFp_ax_ax1 ax). have ox:=(OS_CNFp1 ax' snN). have oy:=(OS_CNFp1 (CNFp_ax_ax1 ay) mN). have ocy :=(proj32_1 (proj1 (p5 _ (cleR (CS_nat mN))))). have occ :=(proj32_1 (proj1 (p2 _ lenn))). rewrite - (oprodA occ ox (OS_prod2 ocy oy)) (oprodA ox ocy oy); apply: f_equal. rewrite (CNFp_A snN mN (CNFp_ax_ax1 axz)). apply: f_equal2; last first. apply: (oprod_expansion_exten mN) => i im. rewrite /CNFp_value1/cz/ez/CNF_mpe /CNF_mpc. have iN:= (NS_lt_nat im mN). move: (proj2 (csum_Mlteq snN im));rewrite (csumC m). move:(csum_Mlteq nN (succ_positive i)). rewrite (csum0l cnn) (cdiff_pr1 iN snN) (csum_nS _ nN). rewrite - (csum_Sn _ iN); move => [sa sb] sc. by move:(cleNgt sa) => sa'; repeat Ytac0. have nn1: n [p7 p8 p9]. move: (p2 _ (proj1 ltnsn)) (p1 _ ltnsn) => [s5 s6] s4. move: (p7 _ nn1) (p8 _ (proj1 nn1)) => s1 [s2 s3]. move: (OS_CNFp0 (CNFp_ax_ax1 ax) (cltS nN)). rewrite (CNFp_r _ _ nN)(CNFp_r _ _ nN)(CNFp_pr1 s4 s5 s6)(CNFp_pr1 s1 s2 s3). move => o2. rewrite -(oprodA (OS_CNFp1r ax' snN (proj1 ltnsn)) o2 ocy); apply: f_equal2. apply: (oprod_expansion_exten nN) => i lin. rewrite / CNFp_value1 /ez/cz/CNF_mpe/CNF_mpc. move:(proj2 (clt_leT lin (proj1 nn1))) (proj2 lin) => lt1 ne1. by repeat Ytac0. rewrite /CNFp_value2/ez/cz/CNF_mpe/CNF_mpc;repeat Ytac0. move:(proj32_1 s4) (proj32_1 s5) => oex ocx. exact (esym (oprodA (OS_succ (OS_pow OS_omega oex)) ocx ocy)). Qed. Definition CNFp_ax4 e c n x := [/\ CNFp_ax e c (csucc n), natp n, e (csucc n) = \0c & x = (c (csucc n)) *o CNFpv1 e c (csucc n)]. Lemma CNFp_ph ex cx n ey cy m x y (ez1 := CNF_mpe ex ey n (csucc m)) (cz1:=CNF_mpc cx cy n (csucc m)) (ez2 := CNF_mpe ey ex m (csucc n)) (cz2:=CNF_mpc cy cx m (csucc n)): CNFp_ax4 ex cx n x -> CNFp_ax4 ey cy m y -> oprod_comm x y -> [/\ (same_below ez1 ez2 (csucc n +c csucc m)), (same_below cz1 cz2 (csucc n +c csucc m)), ( n = m -> x = y) & ( m exists ez cz p z, [/\ CNFp_ax4 ez cz p z, x = z *o y, z *o y = y *o z & p [ ax nN exn xv] [ ay mN eym yv]. move:(NS_succ mN)(NS_succ nN) => smN snN. have sc1:= (csumC (csucc m)(csucc n)). have eq0:= (erefl(csucc n +c csucc m)). move: (CNFp_pg ax ay nN smN) (CNFp_pg ay ax mN snN). rewrite - {1} xv - {1} yv; move => [at1 eq1]. rewrite - {1} xv - {1} yv; move => [at2 eq2]. rewrite /oprod_comm eq1 eq2; clear eq1 eq2. move: (CNFp_unique at1 at2 (NS_sum snN smN) (NS_sum smN snN)); rewrite /CNFpv. set z1 := CNFpv1 _ _ _; set z2 := CNFpv1 _ _ _. rewrite /CNF_mpe /CNF_mpc sc1 4!(Y_true eq0) exn eym opowx0. have oq1: ordinalp (cx (csucc n)). by move: ax => [_ a2 _]; move: (a2 _ (cleR (CS_succ n))) => [[[]]]. have oq2: ordinalp (cy (csucc m)). by move: ay => [_ a2 _]; move: (a2 _ (cleR (CS_succ m))) => [[[]]]. rewrite (oprod1l oq1) (oprod1l oq2) -{4 7} sc1. rewrite -{1} exn - eym => eq1 eq3;move: (eq1 eq3) => [_ me1 me] {eq1}. rewrite -{1} me1 => sae sac. split; [ exact sae | exact sac | |]. move => enm; rewrite - enm in sac sae oq2. rewrite xv yv - enm. have saec: forall i, i (cy i = cx i /\ ey i = ex i). move => i lt1. have ha:= (csum_Mlteq snN lt1). have iN:= (NS_lt_nat lt1 snN). have eq2:= (cdiff_pr1 iN snN). move: (csum_M0le i (CS_nat nN)); rewrite csumC => l1. have [hb1 hb2]: n hb3. move: (sae _ ha)(sac _ ha); move:(proj2 ha)=> hb. by rewrite eq2; repeat Ytac0;split. have ->: cy (csucc n) = cx (csucc n). have nsn:= (cltS nN). move:(proj1 (saec _ nsn)) => hc. move: nsn =>[hb1 hb2]. move:(ax) =>[ _ a2 _]; move: (proj1 (a2 _ hb1)) => cxnp. have l1:= (csum_M0le (csucc n) (CS_nat nN)). move /(cltSleP ((NS_sum nN snN))):l1. rewrite - (csum_Sn _ nN) => ha. move:(proj2 ha) => hb. move:(sac _ ha); repeat Ytac0; rewrite hc => hd. exact:(oprod2_simpl oq2 oq1 cxnp hd). by apply: f_equal; apply: (oprod_expansion_exten snN) => i /saec [-> ->]. move=> ltnm. have snmnz: n -c m <> \0c by apply: (cdiff_nz ltnm). move: ltnm => [lenm nenm]. move: (cdiff_pr lenm) (NS_diff m nN) => snmp snmN. move: (cpred_pr snmN snmnz); set p := cpred (n -c m); move=> [pN pv1]. have spN: natp (csucc p) by fprops. set nm := (csucc n) +c (csucc m). have nmN:= NS_sum snN smN. have spm:csucc p +c csucc m = csucc n. by rewrite (csum_nS _ mN) csumC -pv1 snmp. have spm1: p +c csucc m = n. by rewrite (csum_nS _ mN) csumC - (csum_nS _ pN) -pv1. have nsm: (n -c csucc m) = p by apply: cdiff_pr2 => //. have pltn: p [ a1 a2 a3]. have aux: forall i, i i +c (csucc m) i isp. by move: (csum_Mlteq smN isp); rewrite spm. hnf; rewrite /z {1 2} /ez {1 3} /cz exn;Ytac0; Ytac0. split; [ split | exact | exact | reflexivity ]. + move => i lip;move:(lip) => [_ h]; Ytac0; exact:(a1 _ (aux _ lip)). + move => i lip; Ytac h; first exact: (a2 _ (cleR (CS_succ n))). exact:(a2 _ (proj1 (aux _ (conj lip h)))). + Ytac0; apply: OS0. set ea:= CNF_mpe ez ey p (csucc m) ; set ca := CNF_mpc cz cy p (csucc m). have eqa: forall i, i (ea i = ex i /\ ca i= cx i). move => i ism; rewrite /ea /ca. have ha:=(csum_Mlteq smN ism). move: (sae _ ha) (sac _ ha); rewrite sc1. rewrite /CNF_mpe/CNF_mpc /cz/ez spm. rewrite 4!(Y_false (proj2 ha)) 2!(Y_false (proj2 ism)). have iN:= (NS_lt_nat ism snN). move: (csum_M0le i (CS_nat mN)); rewrite csumC => li1. move/(cltSleP (NS_sum iN mN)):li1. rewrite - (csum_nS _ mN) => - [ha4 ha5]. have ha7 := cleNgt ha4. have h3:= (proj2 (cltS pN)). repeat Ytac0. rewrite (cdiff_pr1 iN smN). case: (cleT_ell (proj31_1 ism) (CS_nat pN)) => cip. + by have ht:= (cleNgt lenm); rewrite cip spm1; repeat Ytac0; split. + move:(csum_Mlteq smN cip); rewrite spm1 => ha1. have ha6:= (proj2 (clt_leT cip (cleS pN))). by move:(proj2 cip)(proj2 ha1) => ha2 ha3; repeat Ytac0; split. + move:(csum_Mlteq smN cip); rewrite spm1; move => [/cleNgt hb1 hb2]. have ->: (i +c csucc m) -c csucc n = i -c csucc p. move/(cleSltP pN): cip => lt2. rewrite - {1} (cdiff_pr lt2) (csumC (csucc p)) - csumA spm. apply: (cdiff_pr1 (NS_diff (csucc p) iN) snN). move: cip => [/cleNgt ha8 ha9]. by repeat Ytac0; split. set eb:=(CNF_mpe ey ez m (csucc p)); set cb:= (CNF_mpc cy cz m (csucc p)). have eqb: forall i, i (ex i = eb i /\ cx i= cb i). move => i iln; rewrite /eb /cb. have ha:=(clt_leT iln (csum_M0le (csucc m) (CS_succ n))). move: (sae _ ha) (sac _ ha). rewrite/CNF_mpe/CNF_mpc /cz/ez sc1. move: (proj2 iln) (proj2 ha) => nin nin2. rewrite (csumC (csucc m)(csucc p)) spm; repeat Ytac0. case (equal_or_not i n) => ein. move => _ _. have h3:= (proj2 (cltS pN)); have h:= (cleNgt lenm). by rewrite ein nsm spm1; repeat Ytac0; split. have lin1: i cim. + by rewrite cim; repeat Ytac0; split. + by move: (proj2 cim) => hb; repeat Ytac0; split. + have smi: csucc m <=c i by move/(cleSltP mN): cim. rewrite (csumC (i -c csucc m)) (cdiff_pr smi). case: (equal_or_not (i -c csucc m) (csucc p)) => hu. by move: (cdiff_pr smi) nin; rewrite hu csumC spm => ->; case. move: cim => [/cleNgt hb hc]. by move => _ _; repeat Ytac0; split. have czp: cz (csucc p) = cx (csucc n) by rewrite /cz; Ytac0. move: (axz)=> [az1 az2 az3]. move: (CNFp_pg az1 ay pN smN) => [_]. have ->: CNFpv1 ea ca (csucc p +c csucc m) = CNFpv1 ex cx (csucc n). by rewrite spm; apply:(oprod_expansion_exten snN) => i /eqa [-> ->]. move => sa sb. move: sa; rewrite - {1} sb czp - xv - yv => eqc. move: (CNFp_pg ay az1 mN spN) => [_]. rewrite - {1} yv. have ->: CNFpv1 eb cb (csucc m +c csucc p) = CNFpv1 ex cx (csucc n). by rewrite csumC spm; apply:(oprod_expansion_exten snN) => i /eqb [-> ->]. rewrite - sb - me - xv => sc. by exists ez, cz, p, z; rewrite eqc sc; split. Qed. Definition oprod2_comm_P1 x y := exists c n m, [/\ ordinalp c, natp n, natp m, x = c ^o n & y = c ^o m]. Lemma oprod2_comm6 ex cx n x ey cy m y: CNFp_ax4 ex cx n x -> CNFp_ax4 ey cy m y -> oprod_comm x y -> oprod2_comm_P1 x y. Proof. move => h1 h2 h3. move:(h1)(h2) => [_ nN _ _] [_ mN _ _]. move:(NS_sum nN mN);set p := n +c m => pN. have aux: n +c m <=c p by rewrite /p; fprops. move: p pN aux => p pN aux. move: p pN ex cx n x ey cy m y h1 h2 h3 aux nN mN. have ores: forall ex cx n x, CNFp_ax4 ex cx n x -> ordinalp x. move=> ex cx n x [ax1 nN _ ->]; move: (ax1) => [_ ax2 _]. move: (proj32_1 (proj1 (ax2 _ (cleR (CS_succ n))))) => o1. exact: (OS_prod2 o1 (OS_CNFp1 (CNFp_ax_ax1 ax1) (NS_succ nN))). have special: forall ex cx n x, CNFp_ax4 ex cx n x -> oprod2_comm_P1 x x. move=> ex cx n x /ores h; move: (opowx1 h) => p1. exists x; exists \1c; exists \1c; split;fprops. apply: Nat_induction. move=> ex cx n x ey cy m y pa pb h1 h2 nN mN. move: (cle0 h2). rewrite -(osum2_2int nN mN) => nmz. move: (osum2_zero (OS_nat nN) (OS_nat mN) nmz) => [nz mz]. rewrite - mz in nz;move: (CNFp_ph pa pb h1) => [_ _ ok _]. move: (ok nz) => ok0; rewrite - ok0; apply: special pa. move=> sm smN hrec ex cx n x ey cy m y pa pb h1 h2 nN mN. wlog:ex cx ey cy n m x y pa pb h1 h2 nN mN / (m <=c n). move=> aux. case: (cleT_el (CS_nat mN) (CS_nat nN)). apply: aux pa pb h1 h2 nN mN. symmetry in h1; rewrite csumC in h2. move=> [lemn _]; move: (aux _ _ _ _ _ _ _ _ pb pa h1 h2 mN nN lemn). move => [z [xe [ye [oz xeN yeN eq1 e2]]]]. exists z; exists ye; exists xe; split => //. move: (CNFp_ph pa pb h1) => [_ _ pc pd]. move=> lenm; case: (equal_or_not m n) => dnm. symmetry in dnm;rewrite -(pc dnm); apply: (special _ _ _ _ pa). have ltnm: m [Z [pZ [p [z [pe xv h3 ltpn]]]]]. have pN: natp p by move: ltpn => [lepn _];apply: (NS_le_nat lepn nN). move: (csum_Mlteq mN ltpn) => r1. move /(cltSleP smN): (clt_leT r1 h2) => le1. move: (hrec _ _ _ _ _ _ _ _ pe pb h3 le1 pN mN)=> xx. move: xx =>[t [xe [ye [oz xeN yeN eq1 e2]]]]. exists t; exists (xe +c ye); exists ye; split;fprops. have oxe: ordinalp xe by apply: OS_cardinal; fprops. have oye: ordinalp ye by apply: OS_cardinal; fprops. by rewrite xv eq1 e2 - (opow_sum oz oxe oye) (osum2_2int xeN yeN). Qed. Theorem oprod2_comm x y: ordinalp x -> ordinalp y -> ((oprod_comm x y) <-> (x = \0o \/ y = \0o \/ (oprod2_comm_P4 x y \/ oprod2_comm_P4 y x) \/ (finite_o x /\ finite_o y) \/ oprod2_comm_P1 x y)). Proof. move=> ox oy. split; last first. rewrite /oprod_comm. move => h; case: h; first by move=> ->; rewrite (oprod0r) (oprod0l). case; first by move=> ->; rewrite (oprod0r) (oprod0l). case; first by case ;[ apply: oprod2_comm3 | symmetry; apply: oprod2_comm3 ]. case. move => [/NatP xN /NatP yN]. by rewrite (oprod2_2int xN yN)(oprod2_2int yN xN) cprodC. move=> [c [n [m [oc nN mN -> ->]]]]. move:(OS_nat nN) (OS_nat mN) => on om. rewrite - (opow_sum oc on om) - (opow_sum oc om on). by rewrite (osum2_2int nN mN)(osum2_2int mN nN) csumC. move=> h. case: (ozero_dichot ox) => xnz; first by left. case: (ozero_dichot oy) => ynz; [by right;left | right; right]. case: (equal_or_not y \1c) => y1. by right;right;exists x, \1o, \0c;split;fprops; rewrite ?opowx1 // y1 opowx0. case: (equal_or_not x \1c) => x1. by right;right;exists y,\0c,\1c;split;fprops; rewrite ? opowx1 // x1 opowx0. move: (the_CNF_p0 ox) => [ax0]. move: (the_CNF_p2 xnz)(CNFB_ax_simp ax0). rewrite /CNFBv;set ex := Vg _ ; set cx := Vg _; set n' := P _; set n:= cpred _. move => [nN nn] [n'N ax] xv. move: (the_CNF_p0 oy)=> [ay0]. move: (the_CNF_p2 ynz)(CNFB_ax_simp ay0). rewrite /CNFBv;set ey := Vg _ ; set cy := Vg _; set m' := P _; set m:= cpred _. move => [mN mm] [m'N ay] yv. clear ax0 ay0. rewrite nn in ax xv; rewrite mm in ay yv. have h1:oprod_comm (CNFbvo ex cx (csucc n)) (CNFbvo ey cy (csucc m)). by rewrite xv yv. move: (ax) (ay) => [[_ ax0 _ _] _][[_ ay0 _ _] _]. move: (ax0 _ (succ_positive n)) (ay0 _ (succ_positive m)) => oex0 oey0. case: (ozero_dichot oex0) => limX; last first. case: (ozero_dichot oey0) => limY; last first. by move: (oprod2_comm4 ax ay nN mN limX limY h1); rewrite xv yv; left. move:(oprod2_comm1 ax ay nN mN limY limX h1);rewrite yv => h2; contradiction. case: (ozero_dichot oey0) => limY; last first. symmetry in h1. move: (oprod2_comm1 ay ax mN nN limX limY h1); rewrite xv => h2;contradiction. case: (equal_or_not n \0c) => n1. move: (oprod2_comm5 ax ay limX limY n1 mN h1); rewrite xv yv. case => h2; [ by case: x1 | by right;left]. case: (equal_or_not m \0c) => m1. symmetry in h1. move: (oprod2_comm5 ay ax limY limX m1 nN h1); rewrite xv yv. case => h2; [ by case: y1 |move: h2 => [q1 q2];by right;left; split]. right; right. move: (CNFp_exists xnz) => [ex' [cx' [n'' [ax2 n''N xv2]]]]. move: (CNFp_p4 ax2 n''N) => [e''x [c''x [ax3 xv3 ex1 eqx2 eqx3]]]. rewrite - xv2 - xv in xv3. move: (CNFb_unique (NS_succ n''N) (NS_succ nN) ax3 ax xv3) => [sa scx]. have mn:=(succ_injective1 (CS_nat n''N) (CS_nat nN) sa). rewrite mn in eqx2 eqx3 scx xv2 ax2; clear sa mn xv3. move: (CNFp_exists ynz) => [ey' [cy' [m'' [ay2 m''N yv2]]]]. move: (CNFp_p4 ay2 m''N) => [e''y [c''y [ay3 yv3 ey1 eqy2 eqy3]]]. rewrite - yv2 - yv in yv3. move: (CNFb_unique (NS_succ m''N) (NS_succ mN) ay3 ay yv3) => [sa scy]. have mn:=(succ_injective1 (CS_nat m''N) (CS_nat mN) sa). rewrite mn in eqy2 eqy3 scy yv2 ay2; clear sa mn yv3. move:(proj2 ax _ (succ_positive n)) (proj2 ay _ (succ_positive m)) => c1a c2a. move:(proj32_1 c1a) (proj32_1 c2a) => oc1 oc2. move: xv2 yv2; rewrite /CNFpv eqy2 eqx2 eqx3 eqy3. move: (scy _ (succ_positive m))(scx _ (succ_positive n)) => [e1 e2][e3 e4]. rewrite e1 e2 e3 e4 limX limY opowx0 (oprod1l oc1) (oprod1l oc2) => xv4 yv4. have ax5: (CNFp_ax4 ex' cx' (cpred n) x). move: (cpred_pr nN n1) => [qa qb]. by hnf; rewrite - qb eqx2 eqx3 e4 e3 limX - xv4; split. have ay5: (CNFp_ax4 ey' cy' (cpred m) y). move: (cpred_pr mN m1) => [qa qb]. by hnf; rewrite - qb eqy2 eqy3 e2 e1 limY - yv4; split. exact: (oprod2_comm6 ax5 ay5 h). Qed. (** Natural sum of ordinals *) Definition CNF_exponents e n:= fun_image n e. Notation CNF_coefficients := CNF_exponents (only parsing). Lemma CNF_exponentsP e n: natp n -> forall z, (inc z (CNF_exponents e n) <-> exists2 i, i nN z;split. by move/funI_P => [i /(NltP nN) idf ->]; exists i. move => [i /(NltP nN) idf ->]; apply/funI_P; ex_tac. Qed. Lemma CNF_exponents_exten e e' n: natp n -> same_below e e' n -> CNF_exponents e n = CNF_exponents e' n. Proof. move => nN h. by set_extens t; move /(CNF_exponentsP _ nN) => [i lin ->]; apply /(CNF_exponentsP _ nN); exists i; rewrite ? (h _ lin). Qed. Lemma CNFq_exists3 a y (X := the_CNF a) : ordinalp y -> a (forall z, inc z (CNF_exponents (Vg (P (Q X))) (P X)) -> z oe ale. move: (proj31_1 ale) => oa. move:(the_CNF_p0 oa) => [/CNFB_ax_simp [nN ax] sb]. move => z /(CNF_exponentsP _ nN) [i lin ->]. case: (ozero_dichot oa) => az. by move:the_CNF_p1 lin; rewrite - az => -> /clt0. case: (oleT_el oe (OS_the_CNF_degree oa)). move/opow_Momega_le. case/(oltNge (ole_ltT (proj1 (the_CNF_p4 az)) ale)). move: (the_CNF_p2 az) => []; set m := (cpred (P (the_CNF a))) => mN mv la. have ha: i <=c m by apply /(cltSleP mN); rewrite - mv. have hb: m natp n -> n = cardinal (CNF_exponents e n). Proof. move => h nN. rewrite - {1} (card_nat nN). set f := Lf e n (CNF_exponents e n). suff bf: bijection f by apply /card_eqP;exists f; split => //; rewrite /f; aw. apply: lf_bijective. - move => t /= td; apply /funI_P; ex_tac. - move => u v /(NltP nN) ui /(NltP nN) vi sv. exact: (CNF_exponents_I nN h ui vi sv). - by move=> y /funI_P. Qed. Lemma CNF_exponents_of b e c n (E := CNF_exponents e n): CNFq_ax b e c n -> natp n -> (finite_set E /\ ordinal_set E). Proof. move => h nN; split. by hnf; rewrite - (CNF_exponents_card h nN); apply /NatP. move => t /(CNF_exponentsP _ nN) [i lin ->]. move: h => [_ h1 _ _]; apply: (h1 _ lin). Qed. Lemma CNF_exponents_compare_expo b e c n a (E:= CNF_exponents e n) : CNFq_ax b e c n -> ordinalp a -> natp n -> [\/ inc a E, (forall t, inc t E -> t a H oa nN. have K:= (CNF_exponentsP e nN). move: (NltP nN) => K1. move: (H) => [pa pb pc pd]. case: (equal_or_not n \0c) => nz. constructor 3 => t /K [i lin ->]; move: lin. rewrite nz => h;case: (clt0 h). move: (cpred_pr nN nz); set n' := cpred n; move=> [cn' cnv]. have n'd: n' cl; last first. constructor 2 => t /K [j jdf ->]; move: (pb _ jdf) => ejb. have lt1: (j <=c n') by apply/(cltSleP cn'); rewrite - cnv. exact: (ole_ltT (CNF_exponents_M nN H lt1 n'd) cl). have on': ordinalp n' by apply: OS_cardinal; apply: CS_nat. pose p j := j [_ [jd jl] jp]. case: (equal_or_not a (e j)) => eq1. by constructor 1; rewrite eq1;apply/K; exists j. case: (equal_or_not j \0c) => jz. constructor 3 => t /K [k kd ->]. have jk : j <=c k. rewrite jz; apply: (czero_least (proj31_1 kd)). exact: (olt_leT (conj jl eq1) (CNF_exponents_M nN H jk kd)). have jN:=(NS_lt_nat jd nN). move: (cpred_pr jN jz); set k := cpred j ; move=> [kN jv]. have ok:=(OS_nat kN). move: (cltS kN); rewrite -jv => lkj. have lkn:=(clt_leT lkj (proj1 jd)). constructor 4; exists k; rewrite -jv;split => //. move: (pb _ lkn) => vo; case: (oleT_el oa vo) => // aux. case: (oleNgt(jp _ ok (conj lkn aux)) (oclt lkj)). Qed. Lemma CNFq_axm_exp ex n ey m: natp n -> natp m -> CNF_exponents (cnf_m ex ey n) (n +c m) = (CNF_exponents ex n) \cup (CNF_exponents ey m). Proof. move => nN mN. have mkN := (NS_sum nN mN). rewrite /cnf_m;set_extens t. move /(CNF_exponentsP _ mkN) => [i limn ->]; apply /setU2_P. Ytac jk; first by left; apply /(CNF_exponentsP _ nN); exists i. right; apply /(CNF_exponentsP _ mN); exists (i -c n) => //. have iN:= (NS_lt_nat limn mkN). case: (NleT_el nN iN) => // lmi. apply: (csum_lt2l nN (NS_diff n iN) mN). by rewrite (cdiff_pr lmi). move => tx; apply/(CNF_exponentsP _ mkN); case /setU2_P: tx. move /(CNF_exponentsP _ nN) => [i lin ->]; exists i. by apply: clt_leT (csum_M0le m (CS_nat nN)). by Ytac0. move /(CNF_exponentsP _ mN) => [i lin ->]; exists (i +c n). by rewrite (csumC n m); apply: (csum_Mlteq nN). move:(csum_M0le i (CS_nat nN)); rewrite csumC => /cltNge h. by rewrite (Y_false h) (cdiff_pr1 (NS_lt_nat lin mN)). Qed. Definition CNF_ext_coeffs (ex cx:fterm) nx (ey cy:fterm) ny := (forall i, i exists j, [/\ j ordinalp a -> natp n -> (forall t : Set, inc t E -> a exists e' c' n', [/\ CNFq_ax b e' c' n', CNF_exponents e' n'= E +s1 a, natp n', CNFbv b e c n = CNFbv b e' c' n' & CNF_ext_coeffs e c n e' c' n']. Proof. move => ax oa nN H. move: (CNFq_pg0 ax) => omp. move: (ax) =>[ax1 ax2 ax3 ax4]. set ey:= fun i => (Yo (i = \0c) a (e (cpred i))). set cy:= fun i => (Yo (i = \0c) \0o (c (cpred i))). have aux: forall i, i <> \0c -> i (cpred i) i ine lin; move: (NS_lt_nat lin (NS_succ nN)) => iN. move: (cpred_pr iN ine) => [sa sb]. by apply/(cltSSP (CS_nat sa) (CS_nat nN)); rewrite - sb. have aux2: forall i, i ( (csucc i i lin; move:(NS_lt_nat lin nN) => iN. by move:(cltSS lin) => inz; rewrite (cpred_pr1 (CS_nat iN)). have snN:= NS_succ nN. have ay:CNFq_ax b ey cy (csucc n). split. + exact. + move => i iz; rewrite /ey; Ytac h;[ exact | apply: (ax2 _ (aux _ h iz))]. + move => i iz; rewrite /cy; Ytac h;[ exact | apply: (ax3 _ (aux _ h iz))]. + move => i iN siz; rewrite /ey. rewrite (Y_false (@succ_nz i)) (cpred_pr1 (CS_nat iN)). move/(cltSSP (CS_nat iN) (CS_nat nN)): siz => inz. Ytac h; first by apply: H; apply /(CNF_exponentsP _ nN); exists i. move: (cpred_pr iN h) => [sa sb]; rewrite {2} sb;apply: ax4 => //; ue. have h1: CNFbv b e c n = CNFbv b (fun z=> ey (csucc z)) (fun z => cy (csucc z)) n. apply: (osum_expansion_exten nN) => i lin. rewrite /cantor_mon /cy/ey (cpred_pr1 (proj31_1 lin)). by rewrite !(Y_false (@succ_nz i)). have yv: CNFbv b e c n = CNFbv b ey cy (csucc n). rewrite (proj33 (CNFq_Al nN ay)) - h1 /cantor_mon/ey/cy; Ytac0; Ytac0. rewrite oprod0r (osum0r (OS_CNFq nN ax)); reflexivity. have ee: CNF_exponents ey (csucc n) = E +s1 a. set_extens t. move/(CNF_exponentsP _ snN) => [i lin ->]; rewrite /ey; Ytac h; fprops. apply: setU1_r; apply/(CNF_exponentsP _ nN); move: (aux _ h lin) => h2. by exists (cpred i). case/setU1_P. move /(CNF_exponentsP _ nN) => [i lin ->]; apply /(CNF_exponentsP _ snN). move: (aux2 _ lin) => [sa sb]; exists (csucc i); first by exact. by rewrite /ey (Y_false (@succ_nz i)) sb. move => ->; apply /(CNF_exponentsP _ snN). exists \0c; [apply succ_positive | by rewrite /ey; Ytac0]. have h2:CNF_ext_coeffs e c n ey cy (csucc n). move => i /aux2 [sa sb]; exists (csucc i). by rewrite /ey /cy !(Y_false (@succ_nz i)) sb; split. by exists ey, cy, (csucc n); split. Qed. Lemma CNF_exp_add_expo b (e c:fterm) n a (E:= CNF_exponents e n) : CNFq_ax b e c n -> ordinalp a -> natp n -> exists (e':fterm) (c':fterm) n', [/\ CNFq_ax b e' c' n', CNF_exponents e' n' = E +s1 a, natp n', CNFbv b e c n = CNFbv b e' c' n' & CNF_ext_coeffs e c n e' c' n']. Proof. move=> ax oa nN. move: (CNFq_pg0 ax) => omp. case: (CNF_exponents_compare_expo ax oa nN) => cp. + exists e, c, n; split => //; first by rewrite (setU1_eq cp). by move => i lin; exists i. + pose e1 i := Yo (i = n) a (e i); pose c1 i := Yo (i = n) \0o (c i). have snN:= NS_succ nN. have nsn:= (cltS nN). have aux: forall i, i i <> n -> i i /(cltSleP nN) h1 h2; split. have ay: CNFq_ax b e1 c1 (csucc n). move: (ax) =>[ax1 ax2 ax3 ax4]. split. + exact. + move => i isn; rewrite /e1; Ytac h; [ exact |apply: (ax2 _ (aux _ isn h))]. + move => i isn; rewrite /c1; Ytac h; [ exact |apply: (ax3 _ (aux _ isn h))]. + move => i iN siz; rewrite /e1. move/(cltSSP (CS_nat iN) (CS_nat nN)): siz => lin. rewrite (Y_false (proj2 lin)); Ytac h. by apply: cp;apply/(CNF_exponentsP _ nN); exists i; rewrite /e1. exact: (ax4 _ iN (conj (proj2 (cleSlt0P (CS_nat iN) nN) lin) h)). have ha :CNF_exponents e1 (csucc n) = E +s1 a. rewrite /e1;set_extens t. move/(CNF_exponentsP _ snN) => [i lin ->]; Ytac h; fprops. apply: setU1_r; apply/(CNF_exponentsP _ nN). by move: (aux _ lin h) => lin1;exists i. case/(setU1_P). move/(CNF_exponentsP _ nN) => [i [u v] ->]; apply/(CNF_exponentsP _ snN). exists i; [ exact:(cle_ltT u nsn) | by Ytac0]. move => ->; apply/(CNF_exponentsP _ snN); exists n; [exact | by Ytac0]. have hc:CNFbv b e c n = CNFbv b e1 c1 (csucc n). have ss:CNFbv b e c n = CNFbv b e1 c1 n. apply: (osum_expansion_exten nN) => i [ _ lin]. by rewrite /cantor_mon /e1 /c1; Ytac0; Ytac0. rewrite (CNFq_p1 _ _ _ nN) - ss /cantor_mon /e1 /c1;Ytac0; Ytac0. rewrite oprod0r (osum0l (OS_CNFq nN ax)); reflexivity. have hd: CNF_ext_coeffs e c n e1 c1 (csucc n). move => i [lin nin]; move: (cle_ltT lin nsn)=> l2. by exists i; rewrite /e1 /c1; Ytac0; Ytac0; split. by exists e1,c1, (csucc n); split. + by apply:CNF_exp_add_expo1. + move:cp=> [k [lkn lskn cla cga]]. move: (cdiff_pr (proj1 lskn)) (NS_diff (csucc k) nN). set m := _ -c _ => mn' mN; symmetry in mn'. move: (CNF_exponents_sM nN ax) => mono. rewrite mn' in ax. have kN:= (NS_lt_nat lkn nN). have skN := NS_succ kN. move:(CS_nat kN) (CS_nat skN)(CNFq_A skN mN ax) => ck csk []. set e1 := (cnf_s e (csucc k)); set c1:= (cnf_s c (csucc k)) => ax1 ax2 xv. have ha: forall t, inc t (CNF_exponents e1 m) -> a t /(CNF_exponentsP _ mN) [ i ik ->]. have eq1: e (csucc k) = e1 \0c by rewrite /e1 /cnf_s (csum0l csk). move: (CNF_exponents_M mN ax2 (czero_least (proj31_1 ik)) ik). by move: cga; rewrite eq1; apply:olt_leT. have [e3 [c3 [n3 [ax3 ex3 n3N x3v cx3]]]]:=(CNF_exp_add_expo1 ax2 oa mN ha). have hb:(n3 = \0c \/ e (cpred (csucc k)) n3p; [by left | right]. have: inc (e3 \0c) (CNF_exponents e3 n3). apply /(CNF_exponentsP _ n3N); exists \0c; [split; fprops | exact]. rewrite ex3; case /setU1_P; last by move => ->. move /(CNF_exponentsP _ mN) => [i lim ->]; rewrite /e1 /cnf_s. have hc: k hd. exact:(mono _ _ hc hd). move: (CNFq_m_ax skN n3N ax1 ax3 hb). set e4:= (cnf_m e e3 (csucc k)); set c4:= (cnf_m c c3 (csucc k)) => ax4. set e5 := (cnf_s e4 (csucc k)); set c5:= (cnf_s c4 (csucc k)). have sa: CNFbv b e3 c3 n3 = CNFbv b e5 c5 n3. apply:(osum_expansion_exten n3N) => i lin. have iN:= (NS_lt_nat lin n3N). move: (csum_M0le i csk); rewrite csumC => hc. rewrite /cantor_mon /e5/e4 /c5/c4 /cnf_s /cnf_m (cdiff_pr1 iN skN). by rewrite !(Y_false (cleNgt hc)). have sb: CNFbv b e c (csucc k) = CNFbv b e4 c4 (csucc k). apply:(osum_expansion_exten skN) => i lin. by rewrite /e4 /c4 /cnf_m /cantor_mon; Ytac0; Ytac0. have kn3N:= (NS_sum skN n3N). have hc:CNF_exponents e4 (csucc k +c n3) = E +s1 a. rewrite (CNFq_axm_exp e e3 skN n3N) ex3 setU2_A; congr union2. rewrite -(CNFq_axm_exp e e1 skN mN) - mn'. have H: forall i, i cnf_m e e1 (csucc k) i = e i. move => i lin; rewrite /e1 /cnf_m /cnf_s. case: (cleT_el csk(proj31_1 lin))=> h; last by Ytac0. by rewrite (Y_false (cleNgt h)) csumC (cdiff_pr h). apply:(CNF_exponents_exten nN H). have hd:CNF_ext_coeffs e c n e4 c4 (csucc k +c n3). move=> i lin; case: (cleT_el csk (proj31_1 lin)) => cik. move: (cdiff_pr cik) (NS_lt_nat lin nN) => ea iN. move: (csum_lt2l skN (NS_diff (csucc k) iN) mN). rewrite ea - mn' => hu; move: (hu lin) => /cx3 [j [ja]]. rewrite /e1/c1 /cnf_s csumC ea => -> ->. move:(NS_lt_nat ja n3N) => jN. move: (csum_M0le j csk) (csum_Mlteq skN ja); rewrite csumC => lt1 lt2. rewrite csumC; exists (j +c csucc k). rewrite /e4 /c4 /cnf_m. rewrite !(Y_false (cleNgt lt1)) (cdiff_pr1 jN skN); split; exact. have ik1:= (clt_leT cik (csum_M0le n3 csk)). by exists i; rewrite /e4/c4 /cnf_m; Ytac0; Ytac0; split. move: (CNFq_A skN n3N ax4) => [ax5 ax6]. move:xv; rewrite -mn' x3v sa sb => <- <-. exists e4, c4, (csucc k +c n3); split; try reflexivity;exact. Qed. Lemma CNF_exp_add_expos b e c n A (E:= CNF_exponents e n) : CNFq_ax b e c n -> natp n -> finite_set A -> ordinal_set A -> exists e' c' n', [/\ CNFq_ax b e' c' n', CNF_exponents e' n' = E \cup A, natp n', CNFbv b e c n = CNFbv b e' c' n' & CNF_ext_coeffs e c n e' c' n']. Proof. move => ax nN fs; move: A fs. apply: finite_set_induction. move => _; exists e,c,n;split => //; first by rewrite setU2_0. by move => i id; exists i. move => A a Hrec os1. have osa: ordinal_set A by move=> t ta; apply: os1; fprops. move: (Hrec osa)=> [e' [c' [n' [ax2 ev n'N sv ]]]]. have ob: ordinalp a by apply os1; fprops. move: (CNF_exp_add_expo ax2 ob n'N) => [e'' [c'' [n''[ax3 ew sw exv h1 h2]]]]. exists e'',c'',n''; rewrite ew - exv - sv ev. split; [ exact | by rewrite setU2_A | exact | reflexivity | ]. move => i ia; move: (h2 _ ia) => [j [jb -> ->]]. by move: (h1 _ jb) => [k [kc -> ->]]; exists k; split. Qed. Lemma CNFq_exponents_r b e c n (e0 := e n) (E := (CNF_exponents e (csucc n))): CNFq_ax b e c (csucc n) -> inc n Nat -> [/\ inc e0 E, (forall a, inc a E -> a <=o e0) & (CNF_exponents e n) = E -s1 e0]. Proof. move=> ax nN; move: (NS_succ nN) => snN. have ha:= (cltS nN). have p1: inc e0 E by apply/(CNF_exponentsP _ snN);exists n;fprops. have mono:= (CNF_exponents_M snN ax). have pb: (forall a, inc a E -> a <=o e0). move => a /(CNF_exponentsP _ (NS_succ nN)) [j /(cltSleP nN) jl ->]. by apply: (CNF_exponents_M snN ax _ ha). split => //; set_extens t. move /(CNF_exponentsP _ nN) => [i lin ->]; apply /setC1_P; split. apply/(CNF_exponentsP _ snN); exists i => //; exact:(clt_ltT lin ha). exact: (proj2 ((CNF_exponents_sM snN ax) i n lin (cltS nN))). case/setC1_P => /(CNF_exponentsP _ snN) [i lin ->] ns. apply/(CNF_exponentsP _ nN); exists i => //; split. by move/(cltSleP nN): lin. by dneg h; rewrite h. Qed. Lemma CNFq_extensionality1 b (ex cx:fterm) n (ey cy:fterm) m: natp n -> natp m -> CNFq_ax b ex cx n -> CNFq_ax b ey cy m -> CNF_exponents ex n = CNF_exponents ey m -> (n = m /\ forall i, i ex i = ey i). Proof. move => nN; move:n nN m; apply: Nat_induction. move => m mN ax1 ax2 eq1. have zm: \0c = m. by rewrite (CNF_exponents_card ax1 NS0) eq1 - (CNF_exponents_card ax2 mN). by split => // i /clt0. move => n nN Hrec m mN ax1 ax2 sv. have snN:= NS_succ nN. have sm: csucc n = m. by rewrite (CNF_exponents_card ax1 snN) (CNF_exponents_card ax2 mN) sv. split; first by exact. rewrite - sm in ax2 sv. move: (CNFq_exponents_r ax1 nN) => [sa sb sc]. move:(CNFq_exponents_r ax2 nN) => [sa' sb' sc']. rewrite - sv in sa' sb' sc'. have ha:= (oleA(sb' _ sa)(sb _ sa')). have hn: CNF_exponents ex n = CNF_exponents ey n by rewrite sc sc' ha. clear sa sb sc sa' sb' sc'. move: (proj2 (Hrec _ nN (CNFq_p5 nN ax1) (CNFq_p5 nN ax2) hn)) => sa. move => i /(cltSleP nN) lin; case: (equal_or_not i n) => ein. by rewrite ein ha. by apply: sa; split. Qed. Lemma CNFq_zero b e c n: natp n -> CNFq_ax b e c n -> CNFbv b e c n = \0o -> forall i, i c i = \0o. Proof. move: n; apply: Nat_induction; first by move => _ _ i /clt0. move => n nN Hrec ax; rewrite (CNFq_p1 _ _ _ nN) => eq. have o1:=(CNFq_p0 ax (cltS nN)). have o2 :=(OS_CNFq nN (CNFq_p5 nN ax)). move: (osum2_zero o1 o2 eq) => [eq1 eq2] i lin; case:(equal_or_not i n) => h. move: (ax) => [_ a1 a2 _]. have oc:=(proj31_1 (a2 _ (cltS nN))). rewrite h;case: (ozero_dichot oc) => // cp. move: (opow_pos (CNFq_pg0 ax) (a1 _ (cltS nN))) => h'. by move: (proj2 (oprod2_pos h' cp)); rewrite -/(cantor_mon b e c n) eq1. apply: (Hrec (CNFq_p5 nN ax) eq2); split => //. by move/(cltSleP nN): lin. Qed. Lemma CNFq_extensionality b ex cx n ey cy m : natp n -> natp m -> CNFq_ax b ex cx n -> CNFq_ax b ey cy m -> CNFbv b ex cx n = CNFbv b ey cy m -> CNF_exponents ex n = CNF_exponents ey m -> (n = m /\ forall i, i ex i = ey i /\ cx i = cy i). Proof. move => nN; move: n nN m; apply: Nat_induction. move => m mN ax ay sv se. move: (CNFq_extensionality1 NS0 mN ax ay se) => [mz _]. split; [ exact | move => i /clt0; case]. move => n nN Hrec m mN ax ay sv se. have nn:= (cltS nN). move: (CNFq_extensionality1 (NS_succ nN) mN ax ay se) => [mn eq1]. split; first by exact. rewrite -mn in sv ay. have se1: ex n = ey n by apply: (eq1 _ nn). move: (ax)(ay)=> [_ a1 a2 _][_ _ a3 _]. move: (a1 _ nn)(proj31_1 (a2 _ nn))(a3 _ nn)=> oexn ocxn [[ocyn ob _] _]. move: (OS_pow ob oexn) => o1. move: (OS_prod2 o1 ocxn)(OS_prod2 o1 ocyn) => o2 o3. move: sv. rewrite (CNFq_p1 _ _ _ nN) (CNFq_p1 _ _ _ nN) /cantor_mon - se1. move: (CNFq_pg nN ax) (CNFq_pg nN ay); rewrite - se1 => lt1 lt2 eq3. move:(proj31_1 lt2) (proj31_1 lt1)=> o4 o5. move: (osum_Meqlt lt1 o2); rewrite - (oprod2_succ o1 ocxn). move: (osum_Meqlt lt2 o3); rewrite - (oprod2_succ o1 ocyn). move: (osum_Mle0 o3 o4) (osum_Mle0 o2 o5);rewrite eq3 => lta ltb ltc ltd. move: (ole_ltT lta ltd) (ole_ltT ltb ltc) => la lb. move: (oprod_Meqltr ocyn (OS_succ ocxn) o1 la) => /oltSleP. move: (oprod_Meqltr ocxn (OS_succ ocyn) o1 lb) => /oltSleP lc ld. move: (oleA lc ld) => e1. have ha:CNF_exponents ex n = CNF_exponents ey n. rewrite (proj33 (CNFq_exponents_r ax nN))(proj33 (CNFq_exponents_r ay nN)). by rewrite - se1 se mn. rewrite - e1 in eq3. move: (osum2_simpl o5 o4 o2 eq3) => eq2. move: (Hrec n nN (CNFq_p5 nN ax) (CNFq_p5 nN ay) eq2 ha) => [_] hb. move => i lin; case: (equal_or_not i n) => ein. by rewrite ein e1 se1; split. apply: hb; split; [ by move/(cltSleP nN): lin | exact]. Qed. Definition CNFQ_bound b I ne:= Nat \times ((gfunctions I ne) \times (gfunctions I b)). Definition CNFq_extension b e c n e' := let ne := (CNF_exponents e n) \cup e' in select (fun X => [/\ CNFq_ax b (Vg (P (Q X))) (Vg (Q (Q X))) (P X), CNFbv b (Vg (P (Q X))) (Vg (Q (Q X))) (P X) = CNFbv b e c n, CNF_exponents (Vg (P (Q X))) (P X) = ne & CNF_ext_coeffs e c n (Vg (P (Q X))) (Vg (Q (Q X))) (P X)]) (CNFQ_bound b (cardinal ne) ne). Lemma CNFq_extension_pr b e c n A (B :=(CNF_exponents e n) \cup A) (Y := CNFq_extension b e c n A) (m := P Y) (e' := Vg (P (Q Y))) (c' := Vg (Q (Q Y))): CNFq_ax b e c n -> natp n -> finite_set A -> ordinal_set A -> [/\ CNFq_ax b e' c' m, CNF_exponents e' m = B, natp m & [/\ domain (P (Q Y)) = m, domain (Q (Q Y)) = m, CNFbv b e c n = CNFbv b e' c' m & CNF_ext_coeffs e c n e' c' m]]. Proof. move => ha hb hc hd. set E := (CNFQ_bound b (cardinal B) B). pose p := (fun X => [/\ CNFq_ax b (Vg (P (Q X))) (Vg (Q (Q X))) (P X), CNFbv b (Vg (P (Q X))) (Vg (Q (Q X))) (P X) = CNFbv b e c n, CNF_exponents (Vg (P (Q X))) (P X) = B & CNF_ext_coeffs e c n (Vg (P (Q X))) (Vg (Q (Q X))) (P X)]). have h: singl_val2 (inc^~ E) p. move => X X' /= /setX_P [sa sb /setX_P [sc sd se]] [sf sg sh si]. move => /setX_P [sa' sb' /setX_P [sc' sd' se']] [sf' sg' sh' si']. move:(CNF_exponents_card sf sb); rewrite sh => sj. move:(CNF_exponents_card sf' sb'); rewrite sh' => sj'. rewrite - sj in sd se; rewrite - sj' in sd' se'. rewrite - sg' in sg; rewrite - sh' in sh. move: (CNFq_extensionality sb sb' sf sf' sg sh) => [sa'' sb'']. have eq1: P (Q X) = P (Q X'). move/ gfunctions_P2: sd => [u1 u2 u3]. move/ gfunctions_P2: sd' => [u1' u2' u3']. apply:fgraph_exten; [exact | exact | by rewrite u2 u2' sa''| move => i id]. by rewrite u2 in id; move/(NltP sb): id => /sb'' []. have eq2: Q (Q X) = Q (Q X'). move/ gfunctions_P2: se => [u1 u2 u3]. move/ gfunctions_P2: se' => [u1' u2' u3']. apply:fgraph_exten; [exact | exact | by rewrite u2 u2' sa''| move => i id]. by rewrite u2 in id; move/(NltP sb): id => /sb'' []. have qq: Q X = Q X' by apply: pair_exten. by apply: pair_exten. move: (CNF_exp_add_expos ha hb hc hd) => [e'' [c'' [n'' [a1 a2 a3 a4 a5]]]]. set X := J n'' (J (Lg n'' e'') (Lg n'' c'')). have pX: p X. have s1: same_below e'' (Vg (P (Q X))) n''. by move => i lin; rewrite /X; aw; bw; move/(NltP a3):lin. have s2: same_below c'' (Vg (Q (Q X))) n''. by move => i lin; rewrite /X; aw; bw; move/(NltP a3):lin. have nn: P X = n'' by rewrite /X; aw. move: (CNFq_exten s1 s2 a1 a3)=> [sa sb]. have cc :CNF_exponents (Vg (P (Q X))) n'' = B. by rewrite /B -a2; set_extens t; move /(CNF_exponentsP _ a3) => [i lin ->]; apply /(CNF_exponentsP _ a3); exists i; try (exact lin); rewrite (s1 _ lin). have ce:CNF_ext_coeffs e c n (Vg (P (Q X))) (Vg (Q (Q X))) n''. move => i lin;move :(a5 _ lin) => [j [lj -> ->]]. by rewrite (s1 _ lj) (s2 _ lj); exists j; split. hnf; rewrite nn - sb a4; split; (try reflexivity); exact. move:(CNF_exponents_card a1 a3); rewrite a2 -/B => eq1. have XE: inc X E. have p1: fgraph (Lg n'' e'') by fprops. have p2: fgraph (Lg n'' c'') by fprops. rewrite /X;apply/setX_P; split; [fprops | aw | aw ]. apply/setX_P; split;fprops; apply/gfunctions_P2;rewrite ?pr1_pair ?pr2_pair; bw. split; [ exact | by rewrite eq1 | move => i /(range_gP p1)]. bw; move => [x xd ->]; bw; rewrite /B - a2; apply/(CNF_exponentsP _ a3). exists x; [ by apply/(NltP a3) | exact]. split; [ exact | by rewrite eq1 | move => i /(range_gP p2)]. bw; move => [x xd ->]; bw; move/(NltP a3): xd => xn. by move: (a1) => [a7 _ a6 _]; move/(oltP (proj32 a7)):(a6 _ xn). move: (select_uniq h XE pX) => xy. have XY: X = Y by rewrite xy ; reflexivity. have -> : m = n'' by rewrite /m - XY /X; aw. have s1: same_below e'' e' n''. by move => i lin; rewrite /e' - XY /X; aw; bw; move/(NltP a3):lin. have s2: same_below c'' c' n''. by move => i lin; rewrite /c' - XY /X; aw; bw; move/(NltP a3):lin. have cc: CNF_exponents e' n'' = B. rewrite /B -a2; symmetry; apply: (CNF_exponents_exten a3 s1). have cd:CNF_ext_coeffs e c n e' c' n''. move => i lin; move :(a5 _ lin) => [j [lj -> ->]]. by rewrite (s1 _ lj)(s2 _ lj); exists j; split. move: (CNFq_exten s1 s2 a1 a3) => [sa <-]. move: XE; rewrite XY => /setX_P [_ _ /setX_P [_ /gfunctions_P2 [_ -> _]]]. move => /gfunctions_P2 [_ -> _]; rewrite - eq1. by split;last split. Qed. Lemma CNFq_extension2_pr b ex cx n ey cy m (Ex := CNF_exponents ex n) (Ey := CNF_exponents ey m) (X := CNFq_extension b ex cx n Ey) (Y := CNFq_extension b ey cy m Ex) (n' := P X) (ex' := Vg (P (Q X))) (cx' := Vg (Q (Q X))) (m' := P Y) (ey' := Vg (P (Q Y))) (cy' := Vg (Q (Q Y))): natp n -> natp m -> CNFq_ax b ex cx n -> CNFq_ax b ey cy m -> [/\ CNFq_ax b ex' cx' n', CNFq_ax b ey' cy' m', CNFbv b ex cx n = CNFbv b ex' cx' n', CNFbv b ey cy m = CNFbv b ey' cy' m'& [/\ n' = m', natp n', domain (Q (Q X)) = n', domain (Q (Q Y)) = n' & [/\ same_below ex' ey' n', CNF_exponents ex' n' = Ex \cup Ey, CNF_ext_coeffs ex cx n ex' cx' n' & CNF_ext_coeffs ey cy m ey' cy' m']]]. Proof. move => nN mN pa pb. move :(CNF_exponents_of pa nN) (CNF_exponents_of pb mN) => [qa qb] [qc qd]. move: (CNFq_extension_pr pa nN qc qd); rewrite -/X -/ex' -/cx' -/n'. move: (CNFq_extension_pr pb mN qa qb); rewrite -/Y -/ey' -/cy' -/m'. move=> [ra rb m'N [d1 d2 rc rc']] [rd re n'N [d1' d2' rf rf']]. have ss: CNF_exponents ex' n' = CNF_exponents ey' m' by rewrite re setU2_C - rb. move: (CNFq_extensionality1 n'N m'N rd ra ss) => [nn sv]. rewrite - nn in d2;rewrite d2. split; last split; last split;exact. Qed. Lemma CNF_sum_ax ex cx n ey cy : CNFq_ax omega0 ex cx n -> CNFq_ax omega0 ey cy n -> natp n -> CNFq_ax omega0 ex (fun i => (cx i) +o (cy i)) n. Proof. move => [a1 a2 a3 a4] [_ b2 b3 b4]; split; try exact. by move => i lin; apply: (osum2_lt_omega (a3 _ lin) (b3 _ lin)). Qed. Lemma CNF_sum_bounded1 ex cx n ey cy : CNFq_ax omega0 ex cx n -> CNFq_ax omega0 ey cy n -> natp n -> forall i, i cx i <=o \osup (CNF_coefficients (fun i => (cx i) +o (cy i)) n). Proof. move => [_ _ ax _] [_ _ ay _] sd i idx. have oq2:= (proj31_1 (ay _ idx)). have oq1:= (proj31_1 (ax _ idx)). apply: (oleT (osum_Mle0 oq1 oq2)). apply: ord_sup_ub. move => k /(CNF_exponentsP _ sd) [j ljn ->]. move: (proj31_1 (ay _ ljn)) (proj31_1 (ax _ ljn)) => ob oa. apply: (OS_sum2 oa ob). by apply/(CNF_exponentsP _ sd); exists i. Qed. Lemma CNF_sup_coef_pr e c n (s := \osup (CNF_coefficients c n)) : natp n -> CNFq_ax omega0 e c n -> (s = \0c \/ exists2 i, i nN [_ _ h _]. have cs: ordinal_set (CNF_coefficients c n). by move => t /funI_P [z /(NltP nN) /h /proj31_1 ze ->]. move: (wordering_ole_pr cs). set r := (ole_on (CNF_coefficients c n)). move => [qa qb]; move: (worder_total qa) => tor. have fs: finite_set (substrate r). by rewrite qb;apply:finite_fun_image; apply:finite_set_nat. case: (emptyset_dichot (substrate r)) => es. by left; rewrite /s -qb es setU_0. move: (finite_set_torder_greatest tor fs es) => [x []]. rewrite qb; move => xr sm. move: (xr) => /(CNF_exponentsP _ nN) [z zi zv]. right; exists z; [exact | ]. rewrite - zv; apply: oleA. apply: ord_ub_sup => //; first by apply: cs. by move=> i id; move: (sm _ id) => /graph_on_P1 [_ _]. apply: ord_sup_ub => //. Qed. Definition natural_sum_aux x y := let X := the_CNF x in let Y := the_CNF y in let ex := Vg (P (Q X)) in let ey := Vg (P (Q Y)) in let Ex := CNF_exponents ex (P X) in let Ey := CNF_exponents ey (P Y) in let xa := CNFq_extension omega0 ex (Vg (Q (Q X))) (P X) Ey in let ya := CNFq_extension omega0 ey (Vg (Q (Q Y))) (P Y) Ex in let cxa := Q (Q xa) in let cya := Q (Q ya) in J (P xa) (J (P (Q xa)) (Lg (domain (Q (Q xa))) (fun i : Set => Vg cxa i +o Vg cya i))). Lemma natural_sum_p1 x y (s := natural_sum_aux x y) (X:= the_CNF x) (n := P s) (e := Vg (P (Q s))) (c := Vg (Q (Q s))): ordinalp x -> ordinalp y -> [/\ natp n, CNFb_axo e c n & forall i, i Vg (Q (Q X)) i <=o \osup (CNF_coefficients (Vg (Q (Q s))) (P s)) ]. Proof. move => ox oy. move:(the_CNF_p0 ox) => [/CNFB_ax_simp]. move:(the_CNF_p0 oy) => [/CNFB_ax_simp]. set ex:= (Vg (P (Q (the_CNF x)))); set ey := (Vg (P (Q (the_CNF y)))). set cx:= (Vg (Q (Q (the_CNF x)))); set cy := (Vg (Q (Q (the_CNF y)))). set ny:= (P (the_CNF y)); set nx:= (P (the_CNF x)). move => [nyN ay] yv [nxN ax] xv. move: (CNFq_extension2_pr nxN nyN (proj1 ax) (proj1 ay)). rewrite /e/c/n/s /natural_sum_aux. rewrite !(pr1_pair, pr2_pair). set nz:= P _. set X1 := CNFq_extension _ _ _ _ _. set Y1 := CNFq_extension _ _ _ _ _. set n1 := P X1; set m1:= P Y1. set e1 :=Vg (P (Q X1)); set e2:=Vg (P (Q Y1)). set c1 :=Vg (Q (Q X1)); set c2:=Vg (Q (Q Y1)). move => [ax1 ax2 eq1 eq2 [nm1 n1N d1 _ [eq3 eq4 s1 s2]]]. rewrite - nm1 in eq2 ax2. move:(CNF_sum_bounded1 ax1 ax2 n1N). set x1 := CNF_exponents _ _; set x2 := CNF_exponents _ _ => ha. have <- : x1 = x2. apply: (CNF_exponents_exten n1N) => i lin; bw; rewrite d1. by apply /(NltP n1N). split; [ exact | |by move => i inx;move: (s1 _ inx) => [j [/ha ja _ ->]] ]. split. move: (CNF_sum_ax ax1 ax2 n1N);apply:CNFq_ax_exten => i lein; first exact. by bw; rewrite d1; apply /(NltP n1N). move => i lin1; bw; last by rewrite d1; apply /(NltP n1N). have oc1: ordinalp (c1 i) by exact (proj31 (ha _ lin1)). have oc2: ordinalp (c2 i). by move:(ax2) => [_ _ h _]; exact:(proj31_1 (h _ lin1)). apply: (ord_ne0_pos (OS_sum2 oc1 oc2)) => eq5. move: (osum2_zero oc1 oc2 eq5) => [c1z c2z]. have: inc (e1 i) (CNF_exponents e1 n1). by apply/(CNF_exponentsP _ n1N); exists i. rewrite eq4; case /setU2_P. move/(CNF_exponentsP _ nxN) => [j ljn eq7]. move: (s1 j ljn) => [k [km va vb]]; rewrite - eq7 in va. move: ax => [_ h]; move: (proj2 (h _ ljn)); rewrite vb. by rewrite - (CNF_exponents_I n1N ax1 lin1 km va) c1z; case. have ->: e1 i = e2 i by apply: eq3. move/(CNF_exponentsP _ nyN) => [j ljn eq7]. move: (s2 j ljn) => [k [km va vb]]; rewrite - eq7 in va. move: ay => [_ h]; move: (proj2 (h _ ljn)); rewrite vb. rewrite - nm1 in km. by rewrite - (CNF_exponents_I n1N ax2 lin1 km va) c2z; case. Qed. Definition natural_sum x y:= let s:= natural_sum_aux x y in CNFbvo (Vg (P (Q s))) (Vg (Q (Q s))) (P s). Notation "x +#o y" := (natural_sum x y) (at level 50). Lemma OS_natural_sum x y : ordinalp x -> ordinalp y -> ordinalp (x +#o y). Proof. move => ox oy; move: (natural_sum_p1 ox oy) => [sa sb sc]. exact:(OS_CNFb sa sb). Qed. (* A bit tricky; it takes too much time without the reflexivity *) Lemma natural_sum_p2 x y (s := the_CNF (x +#o y)) (ex := Vg (P (Q (the_CNF x)))) (cx := Vg (Q (Q (the_CNF x)))) (es:= Vg (P (Q s))) (cs:= Vg (Q (Q s))) (n:= P (the_CNF x))(m:= P s): ordinalp x -> ordinalp y -> (sub (CNF_exponents ex n) (CNF_exponents es m) /\ (forall i, i cx i <=o \osup (CNF_coefficients cs m))). Proof. move => ox oy; move: (erefl m); rewrite {1} /m /cs /es /s. move: (natural_sum_p1 ox oy) => []. move:(the_CNF_p0 ox) => [/CNFB_ax_simp]. move:(the_CNF_p0 oy) => [/CNFB_ax_simp]; rewrite -/ex -/cx. set ey := (Vg (P (Q (the_CNF y)))); set cy := (Vg (Q (Q (the_CNF y)))). rewrite -/n ; move=>[nyN ay] _ [nN ax] _. rewrite /natural_sum;set u := (natural_sum_aux x y). move => H1 H2 H3 H4; set W := _ /\ _. move: (erefl u); rewrite {1}/u /natural_sum_aux. set X := (the_CNF x) ; set Y := (the_CNF y). set X':= CNFq_extension omega0 ex cx (P X) (CNF_exponents (Vg (P (Q Y))) (P Y)). set Y':= CNFq_extension omega0 ey cy (P Y) (CNF_exponents (Vg (P (Q X))) (P X)). move => uv. have ha: P u = (P X') by rewrite - uv pr1_pair; reflexivity. have hb: P (Q u) = (P (Q X')) by rewrite - uv pr2_pair pr1_pair; reflexivity. have hc: Q (Q u) = (Lg (domain (Q (Q X'))) (fun i : Set => Vg (Q (Q X')) i +o Vg (Q (Q Y')) i)). rewrite - uv; aw. move:H1 H2 H3 H4;rewrite /W ha hb hc. set Z := the_CNF _ => pa pb pc pd. clear W u uv ha hb hc. move: (the_CNF_p3 pb pa); rewrite -/Z /CNFbB. set ez:= Lg _ _; set cz := Lg _ _ => eq1. have eq0: m = P X' by rewrite -pd eq1 pr1_pair; reflexivity. move: (f_equal Q eq1);rewrite pr2_pair => eq2. move: (f_equal P eq2) (f_equal Q eq2); rewrite pr2_pair pr1_pair => -> ->. move: (CNFq_extension2_pr nN nyN (proj1 ax) (proj1 ay)). rewrite -/Y' -/X'; move => [_ _ _ _[ _ _ dy _ [_ eqa _ _]]]. split. have ssae: same_below (Vg (P (Q X'))) (Vg ez) (P X'). by move => i lin; move: (NS_lt_nat lin pa) => iN; rewrite /ez; bw;Ytac0. rewrite eq0 -(CNF_exponents_exten pa ssae) eqa;apply:subsetU2l. have ssac: same_below (Vg (Lg (domain (Q (Q X'))) (fun k => Vg (Q (Q X')) k +o Vg (Q (Q Y')) k))) (Vg cz) (P X'). move => i lin; rewrite /cz; move: (NS_lt_nat lin pa) => iN. have id: inc i (domain (Q (Q X'))) by rewrite dy; apply /(NltP pa). by bw; Ytac0. by move: pc; rewrite (CNF_exponents_exten pa ssac) eq0. Qed. Lemma natural_sum0 x : ordinalp x -> (x +#o \0o) = x. Proof. move => ox. move:(the_CNF_p0 ox) => [/CNFB_ax_simp [mN ay yv]]. move:(the_CNF_p0 OS0) => [/CNFB_ax_simp [nN ax xv]]. rewrite /natural_sum /natural_sum_aux !(pr1_pair, pr2_pair). move: (CNFq_extension2_pr mN nN (proj1 ay) (proj1 ax)). set Y:= CNFq_extension _ _ _ _ _. set X:= CNFq_extension _ _ _ _ _. move => [pa pb pc pd [pe pf pg _ _]]. rewrite - yv /CNFBv /CNFbvo pg [RHS] pc. apply: (osum_expansion_exten pf) => i lin. have idx: inc i (P Y) by apply /(NltP pf). rewrite /cantor_mon; bw. move: pa => [_ _ ha _]; move: (proj31_1 (ha _ lin)) => oc1. move: xv; rewrite /CNFBv /CNFbvo pd => xv;rewrite pe in pf lin. by rewrite(CNFq_zero pf pb xv lin) (osum0r oc1). Qed. Lemma natural_sumC x y : ordinalp x -> ordinalp y -> (x +#o y) = (y +#o x). Proof. move => ox oy. move:(the_CNF_p0 ox) => [/CNFB_ax_simp [mN ay yv]]. move:(the_CNF_p0 oy) => [/CNFB_ax_simp [nN ax xv]]. rewrite /natural_sum /natural_sum_aux !(pr1_pair, pr2_pair). move: (CNFq_extension2_pr nN mN (proj1 ax) (proj1 ay)). set X1:= CNFq_extension _ _ _ _ _. set Y1:= CNFq_extension _ _ _ _ _. move => [pa pb pc pd [pe pf pg w [ph _ _ _]]]. rewrite -pe; apply: (osum_expansion_exten pf) => i lin. have ha: inc i (domain (Q (Q X1))) by rewrite pg; apply /(NltP pf). rewrite w - pg /cantor_mon (ph _ lin) {1} (LVg_E _ ha) (LVg_E _ ha). move: pa pb => [a1 a2 a3 _] [_ b2 b3 _]; rewrite - pe in b3. move:(a3 _ lin) (b3 _ lin) => sa sb. have ub: inc (Vg (Q (Q X1)) i) Nat by apply /olt_omegaP. have vb: inc (Vg (Q (Q Y1)) i) Nat by apply /olt_omegaP. by rewrite (osum2_2int ub vb)(osum2_2int vb ub) csumC. Qed. Lemma CNF_M0le b ex cx n ey cy : natp n -> CNFq_ax b ex cx n -> CNFq_ax b ey cy n -> (forall i, i (ex i) = ey i /\ cx i <=o cy i) -> CNFbv b ex cx n <=o CNFbv b ey cy n. Proof. move: n; apply: Nat_induction. move => _ _ _; rewrite CNFq_p2 CNFq_p2; apply: (oleR OS0). move => n nN Hrec ax1 ax2 h. rewrite (CNFq_p1 _ _ _ nN) (CNFq_p1 _ _ _ nN). have h1: (forall i, i ex i = ey i /\ cx i <=o cy i). move => i lin; exact (h _ (clt_leT lin (cleS nN))). have l1:= (Hrec (CNFq_p5 nN ax1) (CNFq_p5 nN ax2) h1). rewrite /cantor_mon;move: (h _ (cltS nN)) => [-> le2]. move: (ax2) => [[_ ob _] oen _ _]. exact:(osum_Mlele (oprod_Meqle le2 (OS_pow ob (oen _ (cltS nN)))) l1). Qed. Lemma natural_small x y e : ordinalp e -> x y (x +#o y) oe qa qb. have ox:= proj31_1 qa. have oy:= proj31_1 qb. move:(natural_sum_p1 ox oy). rewrite /natural_sum /natural_sum_aux !(pr1_pair, pr2_pair). set X:= CNFq_extension _ _ _ _ _. set Y:= CNFq_extension _ _ _ _ _. move => [sa sb _]; apply: (CNFq_pg3 sa (proj1 sb) oe) => i ip. move: (CNFq_exists3 oe qa) (CNFq_exists3 oe qb) => qc qd. move:(the_CNF_p0 ox) => [/CNFB_ax_simp [nN ax] xv]. move:(the_CNF_p0 oy) => [/CNFB_ax_simp [mN ay] yv]. move: (CNFq_extension2_pr nN mN (proj1 ax) (proj1 ay)) => [_ _ _ _ [_ _ _ _ [_ e3 _ _]]]. have : inc (Vg (P (Q X)) i) (CNF_exponents (Vg (P (Q X))) (P X)). by apply /(CNF_exponentsP _ sa); exists i. rewrite e3; case /setU2_P; fprops. Qed. Lemma natural_M0le x y : ordinalp x -> ordinalp y -> x <=o (x +#o y). Proof. move => ox oy. move:(natural_sum_p1 ox oy). rewrite /natural_sum /natural_sum_aux !(pr1_pair, pr2_pair). move => [sa sb _]. move:(the_CNF_p0 ox) => [/CNFB_ax_simp [nN ax] xv]. move:(the_CNF_p0 oy) => [/CNFB_ax_simp [mN ay] yv]. move: (CNFq_extension2_pr nN mN (proj1 ax) (proj1 ay)). set X:= CNFq_extension _ _ _ _ _. set Y:= CNFq_extension _ _ _ _ _. move => [ax1 ax2 v1 _ [n1n2 n1N d1 _ [e1 e2 e3 e4]]]. rewrite -xv /CNFBv /CNFbvo [in X in X <=o _] v1. apply:(CNF_M0le n1N ax1 (proj1 sb)); rewrite -/X -/Y. move => i lin. have id: inc i (domain (Q (Q X))) by rewrite d1; apply /(NltP n1N). move: ax1 => [_ _ a1 _]; move: (proj31_1 (a1 _ lin)) => o1. split; [exact | bw]; rewrite n1n2 in lin. move: ax2 => [_ _ a2 _]; exact (osum_Mle0 o1 (proj31_1 (a2 _ lin))). Qed. Definition CNF_subset x:= let X := the_CNF x in let n:= P X in let e := Vg (P (Q X)) in let c := Vg (Q (Q X)) in let E1:=(CNF_exponents e n) in let E2:=(osucc (\osup (CNF_coefficients c n))) in let G:= fun z => singleton z \times (gfunctions (Nint z) E1 \times gfunctions (Nint z) E2) in let G1 := unionf (Nintc n) G in fun_image G1 (fun z => CNFbvo (Vg (P (Q z))) (Vg (Q (Q z))) (P z)). Lemma natural_sum_p3 x y (E :=CNF_subset (x +#o y)): ordinalp x -> ordinalp y -> (inc x E /\ finite_set E). Proof. move => ox oy. have oz:=(OS_natural_sum ox oy). split. rewrite /E /CNF_subset; apply /funI_P. move:(the_CNF_p0 ox) => [/CNFB_ax_simp [nN ax] xv]. move:(the_CNF_p0 oy) => [/CNFB_ax_simp [mN [ay _]] yv]. move: (CNFq_extension2_pr nN mN (proj1 ax) ay). set X:= CNFq_extension _ _ _ _ _. set Y:= CNFq_extension _ _ _ _ _. move => [ax1 ax2 v1 _ [n1n2 n1N d1 _ [e1 e2 e3 e4]]]. set n :=(P (the_CNF x)). set e := (Lg (Nint n) (Vg (P (Q (the_CNF x))))). set c := (Lg (Nint n) (Vg (Q (Q (the_CNF x))))). have sa: same_below (Vg (P (Q (the_CNF x)))) (Vg e) n. by move => i /(NintP nN) lin; rewrite /e; bw. have sb: same_below (Vg (Q (Q (the_CNF x)))) (Vg c) n. move => i/(NintP nN) lin; rewrite /c; bw. move: (CNFb_exten sa sb ax nN) => [sc sd]. exists (J n (J e c)); last first. symmetry; move: sd; rewrite -/e -/c !(pr1_pair, pr2_pair) /CNFbvo. move => <-; exact: xv. have ha: fgraph (Lg (Nint n) (Vg (P (Q (the_CNF x))))) by fprops. have hb: fgraph (Lg (Nint n) (Vg (Q (Q (the_CNF x))))) by fprops. move: (natural_sum_p2 ox oy) => [se sf]. have nI: inc n (Nintc (P (the_CNF (x +#o y)))). move:(the_CNF_p0 oz) => [/CNFB_ax_simp [snN [az _]] zv]. apply /(NintcP snN). rewrite /n (CNF_exponents_card (proj1 ax) nN) (CNF_exponents_card az snN). exact: (sub_smaller se). apply/setUf_P; exists n; [exact | apply /setX_P]. split; [ fprops | apply /set1_P; aw | apply /setX_P]. split; first by rewrite pr2_pair; apply: pair_is_pair. rewrite pr2_pair pr1_pair /e;apply /gfunctions_P2; split; [exact | bw |]. rewrite /e => t /(range_gP ha); bw. move => [z zi ->]; bw;apply: se; apply/(CNF_exponentsP _ nN). exists z ; [by apply /(NintP nN)| exact]. rewrite !pr2_pair /c; apply /gfunctions_P2; split; [ exact | bw | ]. move => t /(range_gP hb); bw; move => [z zi ->]; bw. move /(NintP nN): zi => zlp. move: (sf _ zlp) => h; move/(oleP (proj32 h)): h; exact. apply: finite_fun_image. set I:= (Nintc (P (the_CNF (x +#o y)))). set f := fun z: Set => _. have ->: (unionf I f) = unionb (Lg I f). rewrite /unionb;bw; set_extens t => /setUf_P [u uI uv]; apply/setUf_P; ex_tac; [ bw | move: uv; bw]. move:(the_CNF_p0 oz) => [/CNFB_ax_simp [mN ay] yv]. have: finite_set (domain (Lg I f)) by bw; apply:finite_Nintcc. apply: finite_union_finite; hnf; bw => z zI; bw. have Hb: forall A B,finite_set A -> finite_set B -> finite_set (gfunctions A B). move => A B /card_finite_setP ha /card_finite_setP hb. apply /card_finite_setP; move:(Eq_fun_set A B) => /card_eqP <-. by rewrite cpow_pr1; fprops. have fi: finite_set (Nint z) by apply:finite_Nint. move: (proj1 (CNF_exponents_of (proj1 ay) mN)) => fs1. move: (CNF_sup_coef_pr mN (proj1 ay)); set s := union _ => sp. have sb: s ->; apply: olt_0omega. by move => [i iln ->]; move: ay => [[_ _ h2 _] _]; apply:h2. have sc:finite_set (osucc s). move:(olt_i sb) => sN. rewrite - (succ_of_Nat sN). by apply/card_finite_setP; rewrite (card_card (CS_succ s)); apply:NS_succ. apply: finite_prod2; first by apply: set1_finite. by apply: finite_prod2 ; apply: Hb. Qed. Lemma natural_finite_cover x e (E:= omega0 ^o e): ordinalp e -> inc x E -> let n := cardinal (Zo (coarse E) (fun z => natural_sum (P z) (Q z)= x)) in inc n Nat /\ n <> \0c. Proof. move=> oe xE; set F := Zo _ _ => n. have oE :=(OS_pow OS_omega oe). have ox:= (ordinal_hi oE xE). move: (proj2 (natural_sum_p3 ox OS0));rewrite (natural_sum0 ox) => h. move: (finite_prod2 h h); set G:= (CNF_subset x) => h1. have h2: sub F (G \times G). move => t /Zo_P [/setX_P [pt Pt Qt] s]. move: (ordinal_hi oE Pt) (ordinal_hi oE Qt) => op oq. move:(proj1 (natural_sum_p3 op oq)) (proj1 (natural_sum_p3 oq op)). rewrite (natural_sumC oq op) s -/G => sa sb. by apply/ setX_P. split; first by move: (sub_finite_set h2 h1) => /card_finite_setP. apply: card_nonempty1. have zE: inc \0o E. apply /(oltP oE); split; first by apply: ozero_least. exact: (nesym(omega_pow_nz oe)). exists (J x \0o); apply: Zo_i;first by apply :setXp_i. by aw; apply: natural_sum0. Qed. End Ordinals3. Export Ordinals3.