NF weak partition development: WPPCompactSyntaxFVExplicitPart008.

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

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

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

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

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppimageat (D : SemanticCore.Class) : (CompactSourceSyntax.synCwppimageat D).fv = D.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpppowateq (F D : SemanticCore.Class) : (CompactSourceSyntax.synCwpppowateq F D).fv = D.fv ∪ F.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppprecomp (F : SemanticCore.Class) : (CompactSourceSyntax.synCwppprecomp F).fv = F.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpppowcommeq (F : SemanticCore.Class) : (CompactSourceSyntax.synCwpppowcommeq F).fv = F.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwecutiso (R D S E : SemanticCore.Class) : (CompactSourceSyntax.synCwecutiso R D S E).fv = D.fv ∪ E.fv ∪ R.fv ∪ S.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwecutisogen (R D S E : SemanticCore.Class) : (CompactSourceSyntax.synCwecutisogen R D S E).fv = D.fv ∪ E.fv ∪ R.fv ∪ S.fv

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

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

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppcardtfn : CompactSourceSyntax.synCwppcardtfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppcardt2fn : CompactSourceSyntax.synCwppcardt2fn.fv = ∅