proposition: Lemma formula_ex2_pr (x := formula_ex2) X: transitive_set X -> [/\ formulap x, formula_len x = card_five, free_vars x = doubleton \1c \2c & forall f, inc f (formula_val X x) <-> (inc f (formula_values X x) /\ sub (Vg f \1c) (Vg f \2c))].
proof: Proof. move => tsx. rewrite /x /formula_ex2. have v0: variablep \0c by apply:NS0. have v1: variablep \1c by apply:NS1. have v2: variablep \2c by apply:NS2. set a := (J val_in (J \0c \1c)). set na := (J val_not a). set b := (J val_in (J \0c \2c)). set onab := (J val_or (J na b)). set nonab := (J val_not onab). set enonab := (J val_ex (J \0c nonab)). set phi:= (J val_not enonab). have hb: csucc (cmax \1c \0c) = \2c by rewrite (cmax_yx cle_01) succ_one. have hc: doubleton \0c \1c \cup doubleton \0c \2c = (doubleton \1c \2c) +s1 \0c. set_extens t. case/setU2_P => /set2_P; case => ->; apply /setU1_P; fprops. case/setU1_P; last by move ->; apply /setU2_P; left; fprops. case/set2_P => ->; apply/setU2_P; [left | right]; fprops. have hd: csucc \2c = \3c by []. have he: csucc \3c = \4c by []. have hf: csucc \4c = card_five by []. have hg: (doubleton \1c \2c +s1 \0c) -s1 \0c = (doubleton \1c \2c). apply:setU1_K => /set2_P; case; fprops. move:(free_vars_in v0 v1); rewrite -/a => fva. move:(free_vars_in v0 v2); rewrite -/b => fvb. case: (fkind_in_p2 v0 v1); rewrite -/a => fa fla. case: (fkind_in_p2 v0 v2); rewrite -/b => fb flb. move:(fkind_not_p2 fa); rewrite -/na fla succ_zero; move =>[fna flna]. move:(free_vars_not fa); rewrite -/na fva => fvna. move:(fkind_or_p2 fna fb); rewrite -/onab flna flb hb; move =>[fc flc]. move:(free_vars_or fna fb); rewrite -/onab fvna fvb hc => fvc. move:(fkind_not_p2 fc); rewrite -/nonab flc hd; move =>[fd fld]. move:(free_vars_not fc); rewrite -/nonab fvc => fvd. move:(fkind_ex_p2 v0 fd); rewrite -/enonab fld he; move =>[fe fle]. move: (free_vars_ex v0 fd); rewrite -/enonab fvd hg => fvg. move :(fkind_not_p2 fe); rewrite -/phi fle hf; move =>[ff flf]. move:(free_vars_not fe); rewrite -/phi fvg => fvf. split => //. set Va:= (formula_val X a). set Vb:= (formula_val X b). set Vc := formula_val X na. set Vd := formula_val X onab. set Ve := formula_val X nonab. set Vf := formula_val X enonab. move:(proj33 (formula_val_inc X v0 v1)); rewrite -/a -/Va;move => Vap. move:(proj33(formula_val_inc X v0 v2)); rewrite -/b -/Vb;move => Vbp. move: (proj33(formula_val_not X fa)); rewrite -/na -/Va -/Vc; move => Vcp. move: (proj33(formula_val_or X fna fb)); rewrite -/onab fvna fvb -/Vd -/Vc -/Vb. move => Vdp. move: (proj33(formula_val_not X fc)); rewrite -/nonab -/Vd -/Ve => Vep. move: (proj33 (formula_val_ex X v0 fd)); rewrite -/enonab -/Ve -/Vf fvg. move => Vfp. move: (proj33(formula_val_not X fe)); rewrite -/phi -/Vf => Vgp. have q1: inc \1c (doubleton \0c \1c) by fprops. have q2: inc \0c (doubleton \0c \1c) by fprops. have q3: inc \2c (doubleton \0c \2c) by fprops. have q4: inc \0c (doubleton \0c \2c) by fprops. move => f; split. move/Vgp => [sa sb]; split => //; ex_middle bad. have [t ta tb]: exists2 t, inc t (Vg f \1c) & ~inc t (Vg f \2c). ex_middle bad2; case bad => t t1; ex_middle t3; case bad2; ex_tac. clear bad; case sb; apply /Vfp; split. by move: sa; rewrite /formula_values fvf fvg. set g := f +s1 (J \0c t). move/gfunctions_P2: sa; rewrite fvf; move => [fpa fpb fpc]. have /fpc wf2: inc (Vg f \2c) (range f). apply/(range_gP fpa); exists \2c => //;rewrite fpb; fprops. have /fpc wf1: inc (Vg f \1c) (range f). apply/(range_gP fpa); exists \1c => //;rewrite fpb; fprops. have fpd: ~ inc \0c (domain f) by rewrite fpb => /set2_P;case; fprops. have fgg: fgraph g by apply: fgraph_setU1. have dg: domain g = doubleton \1c \2c +s1 \0c. by move:(domain_setU1 f \0c t); rewrite fpb. have tX:=(tsx _ wf1 _ ta). have fpf:inc g (formula_values X nonab). apply/gfunctions_P2; rewrite fvd; split => //. rewrite /g (range_setU1) => s /setU1_P; case => //; first by apply: fpc. by move => ->. have fpg: f = restr g (doubleton \1c \2c). apply:fgraph_exten; aww => s sd; rewrite LgV//; last by ue. by symmetry;apply: setU1_V_in. have g0: (Vg g \0c) = t by rewrite setU1_V_out. have g1: (Vg g \1c) = Vg f \1c by rewrite setU1_V_in // fpb; fprops. have g2: (Vg g \2c) = Vg f \2c by rewrite setU1_V_in // fpb; fprops. have vg0x: inc (Vg g \0c) X by ue. have vg1x: inc (Vg g \1c) X by ue. have vg2x: inc (Vg g \2c) X by ue. have ea: inc (Vg g \0c) (Vg g \1c) by rewrite g0 g1. exists g => //; apply /Vep; split => //; move /Vdp => [ka]; case => kb. by move/Vcp: kb => [kc];case; apply /Vap; rewrite !LgV// Lgd; split; fprops. by move /Vbp: kb; move => [_ _ _ _];rewrite !LgV// g0 g2. move => [ga fp1]; apply/Vgp; split => // fif. move/gfunctions_P2:ga => [fgf df rgf]; rewrite fvf in df. move/Vfp:fif => [_ [g /Vep [/gfunctions_P2 [ga gb gc] gv] gw]]; case gv. rewrite fvd in gb. apply /Vdp; split; first by apply /gfunctions_P2; rewrite fvc; split. have g1: Vg g \1c = Vg f \1c by rewrite gw LgV; fprops. have g2: Vg g \2c = Vg f \2c by rewrite gw LgV; fprops. have g0x: inc (Vg g \0c) X. apply: gc; apply /(range_gP ga);exists \0c =>//;ue. have g1x: inc (Vg g \1c) X. apply: gc; apply /(range_gP ga);exists \1c =>//;ue. have g2x: inc (Vg g \2c) X. apply: gc; apply /(range_gP ga);exists \2c =>//;ue. case: (inc_or_not (Vg g \0c) (Vg g \1c)); [right | left]. apply /Vbp; rewrite Lgd !LgV//; split; fprops. by move: fp1; rewrite g2 - g1; apply. have hw: fgraph (restr g (doubleton \0c \1c)) by fprops. have hx: sub (range (restr g (doubleton \0c \1c))) X. move => t /(range_gP hw); rewrite Lgd; move => [s sa ->]. by rewrite LgV //;case /set2_P: sa => ->. apply/Vcp; split. apply /gfunctions_P2; rewrite Lgd fvna; split => //. by move/Vap => [_ _ _ ]; rewrite !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)