NF weak partition development: WPPCompactSyntaxFVExplicitPart005.

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

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

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

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cfdpointrel (A : SemanticCore.Class) : (CompactSourceSyntax.synCfdpointrel A).fv = A.fv

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

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwcodes (A : SemanticCore.Class) : (CompactSourceSyntax.synChwcodes A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwiso (A : SemanticCore.Class) : (CompactSourceSyntax.synChwiso A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwrels : CompactSourceSyntax.synChwrels.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwbij : CompactSourceSyntax.synChwbij.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwtrn : CompactSourceSyntax.synChwtrn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwgen : CompactSourceSyntax.synChwgen.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwcn (A : SemanticCore.Class) : (CompactSourceSyntax.synChwcn A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwniso (A : SemanticCore.Class) : (CompactSourceSyntax.synChwniso A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnord (A : SemanticCore.Class) : (CompactSourceSyntax.synChnord A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncard (A : SemanticCore.Class) : (CompactSourceSyntax.synChncard A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwbases (A : SemanticCore.Class) : (CompactSourceSyntax.synChwbases A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chwcards (A : SemanticCore.Class) : (CompactSourceSyntax.synChwcards A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnwcutcode (R D C : SemanticCore.Class) : (CompactSourceSyntax.synChnwcutcode R D C).fv = C.fv ∪ D.fv ∪ R.fv