NF weak partition development: WPPCompactSyntaxFVExplicitPart006.

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnwcutmap (R D : SemanticCore.Class) : (CompactSourceSyntax.synChnwcutmap R D).fv = D.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnqmap1 (A : SemanticCore.Class) : (CompactSourceSyntax.synChnqmap1 A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clntp : CompactSourceSyntax.synClntp.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clntpc (A : SemanticCore.Class) : (CompactSourceSyntax.synClntpc A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clnker (R : SemanticCore.Class) : (CompactSourceSyntax.synClnker R).fv = R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clnquo (R A : SemanticCore.Class) : (CompactSourceSyntax.synClnquo R A).fv = A.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpphit (F I C : SemanticCore.Class) : (CompactSourceSyntax.synCwpphit F I C).fv = C.fv ∪ F.fv ∪ I.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnwsegfn (R D : SemanticCore.Class) : (CompactSourceSyntax.synChnwsegfn R D).fv = D.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnwcodefn (R : SemanticCore.Class) : (CompactSourceSyntax.synChnwcodefn R).fv = R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnwcutfn (R D : SemanticCore.Class) : (CompactSourceSyntax.synChnwcutfn R D).fv = D.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnwcutrel (R D : SemanticCore.Class) : (CompactSourceSyntax.synChnwcutrel R D).fv = D.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clnqrel (R : SemanticCore.Class) : (CompactSourceSyntax.synClnqrel R).fv = R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clnqord (R C : SemanticCore.Class) : (CompactSourceSyntax.synClnqord R C).fv = C.fv ∪ R.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clnpwc (A : SemanticCore.Class) : (CompactSourceSyntax.synClnpwc A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfrecteq (F G I : SemanticCore.Class) : (CompactSourceSyntax.synCfrecteq F G I).fv = F.fv ∪ G.fv ∪ I.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnqinc (D A : SemanticCore.Class) : (CompactSourceSyntax.synChnqinc D A).fv = A.fv ∪ D.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clndifop : CompactSourceSyntax.synClndifop.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_clnpwasymfn : CompactSourceSyntax.synClnpwasymfn.fv = ∅

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