NF weak partition development: WPPCompactSyntaxFVExplicitPart004.

Explicit-only FV equations for the WPP extension; no global simp attributes.

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdmem : CompactSourceSyntax.synCfdmem.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdprj0 : CompactSourceSyntax.synCfdprj0.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdprj1 : CompactSourceSyntax.synCfdprj1.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfddom (A B : SemanticCore.Class) : (CompactSourceSyntax.synCfddom A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfde0 (A B : SemanticCore.Class) : (CompactSourceSyntax.synCfde0 A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfde1 (A B : SemanticCore.Class) : (CompactSourceSyntax.synCfde1 A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdsep (A B : SemanticCore.Class) : (CompactSourceSyntax.synCfdsep A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdlift (R : SemanticCore.Class) : (CompactSourceSyntax.synCfdlift R).fv = R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdnonmin (R A B : SemanticCore.Class) : (CompactSourceSyntax.synCfdnonmin R A B).fv = A.fv ∪ B.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdminsep (R A B : SemanticCore.Class) : (CompactSourceSyntax.synCfdminsep R A B).fv = A.fv ∪ B.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_csep2 (A B : SemanticCore.Class) : (CompactSourceSyntax.synCsep2 A B).fv = A.fv ∪ B.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_ckqrel (A : SemanticCore.Class) : (CompactSourceSyntax.synCkqrel A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdminvalp (R A B C : SemanticCore.Class) : (CompactSourceSyntax.synCfdminvalp R A B C).fv = A.fv ∪ B.fv ∪ C.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdminq (R A B : SemanticCore.Class) : (CompactSourceSyntax.synCfdminq R A B).fv = A.fv ∪ B.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdpivmap2 (R A B : SemanticCore.Class) : (CompactSourceSyntax.synCfdpivmap2 R A B).fv = A.fv ∪ B.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdpivrange2 (R A B : SemanticCore.Class) : (CompactSourceSyntax.synCfdpivrange2 R A B).fv = A.fv ∪ B.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfpiv (R A B C : SemanticCore.Class) : (CompactSourceSyntax.synCfpiv R A B C).fv = A.fv ∪ B.fv ∪ C.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdif (R A B : SemanticCore.Class) : (CompactSourceSyntax.synCfdif R A B).fv = A.fv ∪ B.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdrow (R A B C : SemanticCore.Class) : (CompactSourceSyntax.synCfdrow R A B C).fv = A.fv ∪ B.fv ∪ C.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdcode (R A B C : SemanticCore.Class) : (CompactSourceSyntax.synCfdcode R A B C).fv = A.fv ∪ B.fv ∪ C.fv ∪ R.fv