Documentation

LeanPool.NFWeakPartition.WPPCompactSyntaxFVExplicitPart009

NF weak partition development: WPPCompactSyntaxFVExplicitPart009.

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

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chnbaseresfn (F : SemanticCore.Class) :

(CompactSourceSyntax.synChnbaseresfn F).fv = F.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_chncodetrnfn (F : SemanticCore.Class) :

(CompactSourceSyntax.synChncodetrnfn F).fv = F.fv

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppcardt4fn :

CompactSourceSyntax.synCwppcardt4fn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpppowsetfn :

CompactSourceSyntax.synCwpppowsetfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpphwcnsetfn :

CompactSourceSyntax.synCwpphwcnsetfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpphwgendomfn :

CompactSourceSyntax.synCwpphwgendomfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpphwgencnvfn :

CompactSourceSyntax.synCwpphwgencnvfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpphwnisosetfn :

CompactSourceSyntax.synCwpphwnisosetfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpphnpairfn :

CompactSourceSyntax.synCwpphnpairfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpphninputfn :

CompactSourceSyntax.synCwpphninputfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppqkrelkernel :

CompactSourceSyntax.synCwppqkrelkernel.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpplitphnordpointfn :

CompactSourceSyntax.synCwpplitphnordpointfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwpppowset2fn :

CompactSourceSyntax.synCwpppowset2fn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppfamilyrep2fn :

CompactSourceSyntax.synCwppfamilyrep2fn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppdirecte2famfn :

CompactSourceSyntax.synCwppdirecte2famfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppdirecth1famfn :

CompactSourceSyntax.synCwppdirecth1famfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppdirecth2famfn :

CompactSourceSyntax.synCwppdirecth2famfn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppconcrete6codefn :

CompactSourceSyntax.synCwppconcrete6codefn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppcardt6fn :

CompactSourceSyntax.synCwppcardt6fn.fv = ∅

theorem NFChoice.Compiler.WPPCompactSyntaxFVExplicit.fv_syn_cwppconcrete6fn :

CompactSourceSyntax.synCwppconcrete6fn.fv = ∅