Documentation

LeanPool.NFWeakPartition.CompactSyntaxFVExplicit

NF weak partition development: CompactSyntaxFVExplicit.

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wtru :

CompactSourceSyntax.synWtru.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wb (ph ps : SemanticCore.Wff) :

(CompactSourceSyntax.synWb ph ps).fv = ph.fv ∪ ps.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wo (ph ps : SemanticCore.Wff) :

(CompactSourceSyntax.synWo ph ps).fv = ph.fv ∪ ps.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wa (ph ps : SemanticCore.Wff) :

(CompactSourceSyntax.synWa ph ps).fv = ph.fv ∪ ps.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_w3o (ph ps ch : SemanticCore.Wff) :

(CompactSourceSyntax.synW3o ph ps ch).fv = ch.fv ∪ ph.fv ∪ ps.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_w3a (ph ps ch : SemanticCore.Wff) :

(CompactSourceSyntax.synW3a ph ps ch).fv = ch.fv ∪ ph.fv ∪ ps.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wnan (ph ps : SemanticCore.Wff) :

(CompactSourceSyntax.synWnan ph ps).fv = ph.fv ∪ ps.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wex (x : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWex x ph).fv = ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wnf (x : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWnf x ph).fv = ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wsb (y x : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWsb y x ph).fv = ph.fv ∪ ph.fv.erase x ∪ {y}.erase x ∪ {x} ∪ {y}

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_weu (x : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWeu x ph).fv = ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wmo (x : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWmo x ph).fv = ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wnfc (x : SemanticCore.Var) (A : SemanticCore.Class) :

(CompactSourceSyntax.synWnfc x A).fv = A.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wne (A B : SemanticCore.Class) :

(CompactSourceSyntax.synWne A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wral (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWral x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wrex (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWrex x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wreu (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWreu x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wrmo (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWrmo x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_crab (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synCrab x A ph).fv = A.fv.erase x ∪ ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cvv :

CompactSourceSyntax.synCvv.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wsbc (A : SemanticCore.Class) (x : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synWsbc A x ph).fv = A.fv ∪ ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csb (A : SemanticCore.Class) (x : SemanticCore.Var) (B : SemanticCore.Class) :

(CompactSourceSyntax.synCsb A x B).fv = A.fv ∪ B.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cnin (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCnin A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ccompl (A : SemanticCore.Class) :

(CompactSourceSyntax.synCcompl A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cin (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCin A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cun (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCun A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cdif (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCdif A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csymdif (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCsymdif A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wss (A B : SemanticCore.Class) :

(CompactSourceSyntax.synWss A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wpss (A B : SemanticCore.Class) :

(CompactSourceSyntax.synWpss A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_c0 :

CompactSourceSyntax.synC0.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cif (ph : SemanticCore.Wff) (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCif ph A B).fv = A.fv ∪ B.fv ∪ ph.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cpw (A : SemanticCore.Class) :

(CompactSourceSyntax.synCpw A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csn (A : SemanticCore.Class) :

(CompactSourceSyntax.synCsn A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cpr (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCpr A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ctp (A B C : SemanticCore.Class) :

(CompactSourceSyntax.synCtp A B C).fv = A.fv ∪ B.fv ∪ C.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cuni (A : SemanticCore.Class) :

(CompactSourceSyntax.synCuni A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cint (A : SemanticCore.Class) :

(CompactSourceSyntax.synCint A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ciun (x : SemanticCore.Var) (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCiun x A B).fv = A.fv.erase x ∪ B.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_copk (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCopk A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_c1c :

CompactSourceSyntax.synC1c.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cpw1 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCpw1 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cuni1 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCuni1 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cxpk (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCxpk A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ccnvk (A : SemanticCore.Class) :

(CompactSourceSyntax.synCcnvk A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cins2k (A : SemanticCore.Class) :

(CompactSourceSyntax.synCins2k A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cins3k (A : SemanticCore.Class) :

(CompactSourceSyntax.synCins3k A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cimak (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCimak A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ccomk (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCcomk A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cp6 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCp6 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csik (A : SemanticCore.Class) :

(CompactSourceSyntax.synCsik A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cssetk :

CompactSourceSyntax.synCssetk.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cimagek (A : SemanticCore.Class) :

(CompactSourceSyntax.synCimagek A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cidk :

CompactSourceSyntax.synCidk.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cio (x : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synCio x ph).fv = ph.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_c0c :

CompactSourceSyntax.synC0c.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cplc (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCplc A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cnnc :

CompactSourceSyntax.synCnnc.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cfin :

CompactSourceSyntax.synCfin.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_clefin :

CompactSourceSyntax.synClefin.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cltfin :

CompactSourceSyntax.synCltfin.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cncfin (A : SemanticCore.Class) :

(CompactSourceSyntax.synCncfin A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ctfin (M : SemanticCore.Class) :

(CompactSourceSyntax.synCtfin M).fv = M.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cevenfin :

CompactSourceSyntax.synCevenfin.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_coddfin :

CompactSourceSyntax.synCoddfin.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wsfin (M N : SemanticCore.Class) :

(CompactSourceSyntax.synWsfin M N).fv = M.fv ∪ N.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cspfin :

CompactSourceSyntax.synCspfin.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cphi (A : SemanticCore.Class) :

(CompactSourceSyntax.synCphi A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cop (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCop A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cproj1 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCproj1 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cproj2 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCproj2 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_copab (x y : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synCopab x y ph).fv = (ph.fv.erase y).erase x ∪ ({x}.erase y).erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wbr (A R B : SemanticCore.Class) :

(CompactSourceSyntax.synWbr A R B).fv = A.fv ∪ B.fv ∪ R.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_c1st :

CompactSourceSyntax.synC1st.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cswap :

CompactSourceSyntax.synCswap.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csset :

CompactSourceSyntax.synCsset.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ccom (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCcom A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cima (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCima A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csi (A : SemanticCore.Class) :

(CompactSourceSyntax.synCsi A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cid :

CompactSourceSyntax.synCid.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cxp (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCxp A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ccnv (A : SemanticCore.Class) :

(CompactSourceSyntax.synCcnv A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_crn (A : SemanticCore.Class) :

(CompactSourceSyntax.synCrn A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cdm (A : SemanticCore.Class) :

(CompactSourceSyntax.synCdm A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cres (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCres A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wfun (A : SemanticCore.Class) :

(CompactSourceSyntax.synWfun A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wfn (A B : SemanticCore.Class) :

(CompactSourceSyntax.synWfn A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wf (F A B : SemanticCore.Class) :

(CompactSourceSyntax.synWf F A B).fv = A.fv ∪ B.fv ∪ F.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wf1 (F A B : SemanticCore.Class) :

(CompactSourceSyntax.synWf1 F A B).fv = A.fv ∪ B.fv ∪ F.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wfo (F A B : SemanticCore.Class) :

(CompactSourceSyntax.synWfo F A B).fv = A.fv ∪ B.fv ∪ F.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_wf1o (F A B : SemanticCore.Class) :

(CompactSourceSyntax.synWf1o F A B).fv = A.fv ∪ B.fv ∪ F.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cfv (F A : SemanticCore.Class) :

(CompactSourceSyntax.synCfv F A).fv = A.fv ∪ F.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_c2nd :

CompactSourceSyntax.synC2nd.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_co (A F B : SemanticCore.Class) :

(CompactSourceSyntax.synCo A F B).fv = A.fv ∪ B.fv ∪ F.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_coprab (x y z : SemanticCore.Var) (ph : SemanticCore.Wff) :

(CompactSourceSyntax.synCoprab x y z ph).fv = ((ph.fv.erase z).erase y).erase x ∪ (({x}.erase z).erase y).erase x ∪ (({y}.erase z).erase y).erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cmpt (x : SemanticCore.Var) (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCmpt x A B).fv = A.fv.erase x ∪ B.fv.erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cmpt2 (x : SemanticCore.Var) (A : SemanticCore.Class) (y : SemanticCore.Var) (B C : SemanticCore.Class) :

(CompactSourceSyntax.synCmpt2 x A y B C).fv = (A.fv.erase y).erase x ∪ (B.fv.erase y).erase x ∪ (C.fv.erase y).erase x ∪ ({x}.erase y).erase x

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ctxp (A B : SemanticCore.Class) :

(CompactSourceSyntax.synCtxp A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cfix (A : SemanticCore.Class) :

(CompactSourceSyntax.synCfix A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ccup :

CompactSourceSyntax.synCcup.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cdisj :

CompactSourceSyntax.synCdisj.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_caddcfn :

CompactSourceSyntax.synCaddcfn.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ccompose :

CompactSourceSyntax.synCcompose.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cins2 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCins2 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cins3 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCins3 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cimage (A : SemanticCore.Class) :

(CompactSourceSyntax.synCimage A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cins4 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCins4 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csi3 (A : SemanticCore.Class) :

(CompactSourceSyntax.synCsi3 A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cfuns :

CompactSourceSyntax.synCfuns.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cfns :

CompactSourceSyntax.synCfns.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cpw1fn :

CompactSourceSyntax.synCpw1fn.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cfullfun (F : SemanticCore.Class) :

(CompactSourceSyntax.synCfullfun F).fv = F.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cclos1 (S R : SemanticCore.Class) :

(CompactSourceSyntax.synCclos1 S R).fv = R.fv ∪ S.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ctrans :

CompactSourceSyntax.synCtrans.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cref :

CompactSourceSyntax.synCref.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cantisym :

CompactSourceSyntax.synCantisym.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cpartial :

CompactSourceSyntax.synCpartial.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cconnex :

CompactSourceSyntax.synCconnex.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cstrict :

CompactSourceSyntax.synCstrict.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cfound :

CompactSourceSyntax.synCfound.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cwe :

CompactSourceSyntax.synCwe.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_csym :

CompactSourceSyntax.synCsym.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cer :

CompactSourceSyntax.synCer.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cec (A R : SemanticCore.Class) :

(CompactSourceSyntax.synCec A R).fv = A.fv ∪ R.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cqs (A R : SemanticCore.Class) :

(CompactSourceSyntax.synCqs A R).fv = A.fv ∪ R.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cmap :

CompactSourceSyntax.synCmap.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cen :

CompactSourceSyntax.synCen.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cncs :

CompactSourceSyntax.synCncs.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_clec :

CompactSourceSyntax.synClec.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cltc :

CompactSourceSyntax.synCltc.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cnc (A : SemanticCore.Class) :

(CompactSourceSyntax.synCnc A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ctc (A : SemanticCore.Class) :

(CompactSourceSyntax.synCtc A).fv = A.fv

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_c2c :

CompactSourceSyntax.synC2c.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_c3c :

CompactSourceSyntax.synC3c.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cce :

CompactSourceSyntax.synCce.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_ctcfn :

CompactSourceSyntax.synCtcfn.fv = ∅

theorem NFChoice.Compiler.CompactSyntaxFVExplicit.fv_syn_cspac :

CompactSourceSyntax.synCspac.fv = ∅