proposition: Lemma CNFp_p4 p n: CNFp_ax p n -> natp n -> exists e c, [/\ CNFb_axo e c (csucc n), CNFbvo e c (csucc n) = CNFpv p n, forall i, i <c n -> p i = J (e (csucc i) -o (e i)) (c (csucc i)) & p n = J (e \0c)(c \0c)].
proof: Proof. move=> [ax1 ax2] nN. pose e := induction_term (fun i z => z +o (P (p i))) (P (p n)). pose c i := Yo (i = \0c) (Q (p n)) (Q (p (cpred i))). have pe1: P (p n) = (e \0c) by rewrite /e induction_term0. have pe2: Q (p n) = (c \0c) by rewrite/c ; Ytac0. have pe: p n = J (e \0c) (c \0c) by rewrite - pe1 - pe2 (proj31 ax2). have hc i: natp i -> e (csucc i) = e i +o (P (p i)). by move=> iN; rewrite /e induction_terms. have ose i: i<c n -> ordinalp (P (p i)). move => lin; move:(NS_lt_nat lin nN) => iN. exact:(proj32_1(proj32(ax1 i lin))). have ose1 i: i <=c n -> ordinalp (e i). move => lin; move:(NS_le_nat lin nN) => iN. move: i iN lin; apply: Nat_induction. by rewrite - pe1;case: ax2. 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 i: i <c n -> p i = J(e (csucc i) -o e i)(c (csucc i)). move => lin; have iN:=(NS_lt_nat lin nN); rewrite /c (Y_false (@succ_nz i)). rewrite (cpred_pr2 iN) (hc _ iN) - {1} (proj31 (ax1 _ lin)). by rewrite (odiff_pr1 (ose1 _ (proj1 lin)) (ose _ lin)). have pc2 i:i <c csucc n -> i <> \0c -> [/\ (cpred i <c n), e i = e (cpred i) +o (P (p (cpred i))) & c i = Q (p(cpred i))]. move => 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) /c (Y_false inz). have cv i: i <c csucc n -> exists2 j, j <=c n & c i = Q (p j). move => /(cltSleP nN) lin; rewrite /c; Ytac ei0. exists n; fprops. exists (cpred i)=> //; exact: (cleT (cpred_le (proj31 lin)) lin). have axx: CNFb_axo e c (csucc n). have aux i: i <=c n -> posnatp (Q (p i)). by case/cle_eqVlt; [ move ->; case: ax2 | case/ax1]. split; first split. - apply: ole_2omega. - by move => i /(cltSleP nN); apply: ose1. - by move => i /cv [j /aux/posnat_ordinalp/proj2 ok ->]. - 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 (proj32(ax1 _ sc)) oe); rewrite (osum0r oe) sd. - by move => i /cv [j /aux/posnat_ordinalp/proj1 ok ->]. move: (CNFp_p3 axx nN) => [p' [ ax' sv qa qc]]. have sv2: CNFbvo e c (csucc n) = CNFpv p n. rewrite sv /CNFpv qc pe; apply: f_equal. apply:(oprodf_exten nN) => i lin. by rewrite /cantor_pmon (qa _ lin) (pc _ lin). by exists e, c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)