proposition: Lemma LS_main X P f (Y:=LS_res X P) : sub P X -> pformula_in Y f -> pclosed f -> (pformula_valid_on X f <-> pformula_valid_on Y f).
proof: Proof. rename f into F; rename P into Pa;move => h0 pa pb. move: (LS_nextP_pr3 h0) => []; rewrite -/Y => h1 h2. set phi := P F; set f := Q F. suff: inc f (formula_val X phi) <-> inc f (formula_val Y phi). move => h; split. move /(pfree_vars_closed_pr X pb) => /h. apply(pfree_vars_closed_pr Y pb). move /(pfree_vars_closed_pr Y pb) => /h. apply(pfree_vars_closed_pr X pb). have df: domain f = free_vars phi. move:pa pb => [[vc vd ve vf] vg]. by rewrite /pclosed /pfree_vars => /empty_setC vh; apply: extensionality. move: pa => [[]]; rewrite -/f -/phi => _ fphi fgf _ rf. move: f df fgf rf. move: (formula_len_pr fphi) => [ua ub _];move: ua ub;clear pb. move: {1 2} (formula_len phi) => n na nb; move:n na phi nb fphi. apply: Nat_induction. move => p pl0 fp f df fgf rg; move: pl0; rewrite formulas_rec0. move/atomic_formulaP => [ha hb hc hd he]; case: he => he. move: (formula_val_inc X hc hd) (formula_val_inc Y hc hd). move => [_ _ r1][_ _ r2]; move: r1 r2; rewrite hb - he ha => r1 r2. split;last by move/r2 => [q1 q2 q3 q4 q5]; apply/r1; split => //; apply h2. move/r1 => [q1 q2 q3 q4 q5]; apply/r2; split => //; apply: rg. apply/(range_gP q1); exists (P (Q p)) => //; rewrite q2; fprops. apply/(range_gP q1); exists (Q (Q p)) => //; rewrite q2; fprops. move: (formula_val_eq X hc hd) (formula_val_eq Y hc hd). move => [_ _ r1][_ _ r2]; move: r1 r2; rewrite hb - he ha => r1 r2. split; last by move/r2 => [q1 q2 q3 q4]; apply/r1; split => //; apply h2. move/r1 => [q1 q2 q3 q4]; apply/r2; split => //; apply: rg. apply/(range_gP q1); exists (P (Q p)) => //; rewrite q2; fprops. move => n nN Hrec p pr fp f df fgf rf. have ha: inc f (formula_values X p). by apply/gfunctions_P2;split => //; apply: (sub_trans rf h2). have hb: inc f (formula_values Y p) by apply/gfunctions_P2. move: pr;rewrite(formulas_rec_succ nN); case /next_formulasP. + by move => r1;apply: Hrec. + move => [pc pd pe]. have ka:= (formula_hi nN pe). move: (formula_val_not X ka) (formula_val_not Y ka). move => [_ _ r1][_ _ r2]; move: r1 r2; rewrite -pd pc=> r1 r2. have df1:domain f = free_vars (Q p). by rewrite - (free_vars_not ka) - pd pc. have hr:= (Hrec (Q p) pe ka f df1 fgf rf). split. by move/r1 => [sa sb]; apply/r2; split => // sc; case sb; apply/hr. by move/r2 => [sa sb]; apply/r1; split => // sc; case sb; apply/hr. + move => [pc pd pe pf pg]. have ka:= (formula_hi nN pf). have kb:= (formula_hi nN pg). move: (formula_val_or X ka kb) (formula_val_or Y ka kb). move => [_ _ r1][_ _ r2]; move: r1 r2; rewrite -pd pe pc => r1 r2. move: (free_vars_or ka kb);rewrite -pd pe pc => fv. set f1:= (restr f (free_vars (P (Q p)))). set f2:= (restr f (free_vars (Q (Q p)))). have f1d: (domain f1 = free_vars (P (Q p))) by rewrite /f1 restr_d. have f2d: (domain f2 = free_vars (Q (Q p))) by rewrite /f2 restr_d. have fg1: fgraph f1 by rewrite /f1; fprops. have fg2: fgraph f2 by rewrite /f2; fprops. have sd1: sub (free_vars (P (Q p))) (domain f). by rewrite df fv => t ta; apply /setU2_P; left. have sd2: sub (free_vars (Q (Q p))) (domain f). by rewrite df fv => t ta; apply /setU2_P; right. have rg1: sub (range f1) Y by exact (sub_trans (restr_range1 fgf sd1) rf). have rg2: sub (range f2) Y by exact (sub_trans (restr_range1 fgf sd2) rf). move: (Hrec _ pf ka f1 f1d fg1 rg1) => hr1. move: (Hrec _ pg kb f2 f2d fg2 rg2) => hr2. split. by move /r1 => [ra]; case; [move/hr1 => rb | move/hr2 => rb]; apply /r2; split => //; [ left | right]. by move /r2 => [ra]; case; [move/hr1 => rb | move/hr2 => rb]; apply /r1; split => //; [ left | right]. + move => [pa pb pc pd pe]. have ka:= (formula_hi nN pe). move: (formula_val_ex X pd ka) (formula_val_ex Y pd ka)(free_vars_ex pd ka). rewrite - pb pc pa; move => [_ _ r1] [_ _ r2] fv; case: (inc_or_not (P (Q p)) (free_vars (Q (Q p)))) => hsimp; last first. move: (formula_ex_simp X pd ka hsimp) (formula_ex_simp Y pd ka hsimp). rewrite - pb pc pa => -> ->; apply: Hrec => //. by rewrite df fv; apply: setC1_eq. split; last first. move/r2 => [ua [g gv r3]]; apply/r1; split => //; exists g => //. move: (formula_val_i ka gv) => /gfunctions_P2 [sa sb sc]. by apply/ (Hrec (Q (Q p)) pe ka _ sb sa sc). move => h3;move/r1: (h3) => [_ [g gv r3]]; apply/r2; split => //. have[m mN ra]: exists2 m, inc m Nat & sub (range f) (Vf (LS_rec X Pa) m). have fa:= (proj2 (free_vars_variables fp)). have frf: finite_set (range f) by apply: finite_range => //;rewrite df. exact:(LS_nextP_pr5 h0 frf rf). set psi1 := J (Q (Q p)) f. have qa: pformula psi1. by rewrite /psi1;hnf; aw;split; fprops; rewrite df fv => t /setC1_P []. have qh:pformula_in X psi1. rewrite /psi1;split; [exact qa | aw;apply:(sub_trans rf h2)]. have qb:inc psi1 (pformulas_in (Vf (LS_rec X Pa) m)). by apply/pformulas_inP; rewrite /psi1;hnf; aw. have qc:pfree_vars psi1 = singleton (P (Q p)). rewrite /psi1/pfree_vars; aw; rewrite df fv; set_extens t. move => /setC_P [ta /setC1_P tb]; apply /set1_P; ex_middle bad. by case: tb. by move => /set1_P ->;apply /setC_P; split => // /setC1_P []. have qd: singletonp (pfree_vars psi1) by rewrite qc; exists (P (Q p)). set Pb := (Vf (LS_rec X Pa) m). case: (pformula_inst_p1 qa qd); set gg := pformula_inst _. move => [ga gb gc gd ge gf gh]. have qe: pformula_valid_on X gg. apply/(pfree_vars_closed_pr X ge); rewrite /gg /pformula_inst /psi1; aw. rewrite qc setU_1 pc - pb pa //. have qf:inc psi1 (LS_nextP_aux X Pb) by apply:Zo_i. set a := (rep (LS_setU X psi1)). have qg: inc a (LS_nextP X Pb) by apply/funI_P; ex_tac. have aa: inc a (LS_setU X psi1) by apply: rep_i; apply: gh. have aY: inc a Y. move:(induction_defined_pr (LS_nextP X) Pa). rewrite -/(LS_rec _ _); move => [_ _ _ h4']. move: qg; rewrite - (h4' _ mN) => aqg. by apply /LS_res_p0; exists (csucc m) => //; apply:NS_succ. move/(LS_setU_P a qh qd):aa; rewrite /psi1;aw; set g1 := _ +s1 _. have g1v: g1 = f +s1 J (P (Q p)) a by rewrite /g1 qc setU_1. have qi: ~ inc (P (Q p)) (domain f) by rewrite df fv => /setC1_P []. have Rf: f = restr g1 (free_vars p) by rewrite -(restr_setU1 a fgf qi) df g1v. move => [aX rc rd re]; exists g1 => //. move/(pfree_vars_closed_pr X rd): re; aw => g1X. move: rc => [[_ _]]; aw; move => ta tb tc. have dg1: domain g1 = free_vars (Q (Q p)). rewrite g1v domain_setU1 df fv; set_extens t. move => /setU1_P; case; [by move/setC1_P => [] | by move => ->]. move => h; apply/setU1_P;case: (equal_or_not t (P (Q p))); fprops. by move => t1; left; apply /setC1_P. have rg1: sub (range g1) Y. rewrite range_setU1;move => t /setU1_P; case;[ apply: rf | by move => ->]. by apply /(Hrec _ pe ka _ dg1 ta rg1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)