NF weak partition development: WPPCompactSyntaxFVExplicitPart010.

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnsicodeliftfn : CompactSourceSyntax.synChnsicodeliftfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnsicodemap (A : SemanticCore.Class) : (CompactSourceSyntax.synChnsicodemap A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnsiquomap (A : SemanticCore.Class) : (CompactSourceSyntax.synChnsiquomap A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodestrictfn : CompactSourceSyntax.synChncodestrictfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodepredfn : CompactSourceSyntax.synChncodepredfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodecarrierfn : CompactSourceSyntax.synChncodecarrierfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodesquarefn : CompactSourceSyntax.synChncodesquarefn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncoderelfn : CompactSourceSyntax.synChncoderelfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodecutfn : CompactSourceSyntax.synChncodecutfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodecutpairfn : CompactSourceSyntax.synChncodecutpairfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodecutinputs (A : SemanticCore.Class) : (CompactSourceSyntax.synChncodecutinputs A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodecutrel (A : SemanticCore.Class) : (CompactSourceSyntax.synChncodecutrel A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodecmpset (A : SemanticCore.Class) : (CompactSourceSyntax.synChncodecmpset A).fv = A.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodepredinputs (A X : SemanticCore.Class) (v : SemanticCore.Var) : (CompactSourceSyntax.synChncodepredinputs A X v).fv = A.fv ∪ X.fv ∪ {v}

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodepredends (A X : SemanticCore.Class) (v : SemanticCore.Var) : (CompactSourceSyntax.synChncodepredends A X v).fv = A.fv ∪ X.fv ∪ {v}

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppstopact (F C : SemanticCore.Class) : (CompactSourceSyntax.synCwppstopact F C).fv = C.fv ∪ F.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppstopstep (F C : SemanticCore.Class) : (CompactSourceSyntax.synCwppstopstep F C).fv = C.fv ∪ F.fv

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppfrecprefixeq (F G I : SemanticCore.Class) (k : SemanticCore.Var) : (CompactSourceSyntax.synCwppfrecprefixeq F G I k).fv = F.fv ∪ G.fv ∪ I.fv ∪ {k}