NF weak partition development: CompactSourceSyntax.

Definition-transparent compact interpretation of every source syntax head in the exact nchoice closure. Free-variable support, rather than nominal .vars, is the correct semantic DV boundary because all generated dummies are bound internally.

def NFChoice.Compiler.CompactSourceSyntax.synWtru : SemanticCore.Wff

Compact nominal syntax for the upstream wtru operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWtru = NFChoice.SemanticCore.Wff.falsum.imp NFChoice.SemanticCore.Wff.falsum

def NFChoice.Compiler.CompactSourceSyntax.synWb (ph ps : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wb operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWb ph ps = ((ph.imp ps).imp (ps.imp ph).neg).neg

def NFChoice.Compiler.CompactSourceSyntax.synWo (ph ps : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wo operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWo ph ps = ph.neg.imp ps

def NFChoice.Compiler.CompactSourceSyntax.synWa (ph ps : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wa operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWa ph ps = (ph.imp ps.neg).neg

def NFChoice.Compiler.CompactSourceSyntax.synW3o (ph ps ch : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream w3o operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synW3o ph ps ch = NFChoice.Compiler.CompactSourceSyntax.synWo (NFChoice.Compiler.CompactSourceSyntax.synWo ph ps) ch

def NFChoice.Compiler.CompactSourceSyntax.synW3a (ph ps ch : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream w3a operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synW3a ph ps ch = NFChoice.Compiler.CompactSourceSyntax.synWa (NFChoice.Compiler.CompactSourceSyntax.synWa ph ps) ch

def NFChoice.Compiler.CompactSourceSyntax.synWnan (ph ps : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wnan operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWnan ph ps = (NFChoice.Compiler.CompactSourceSyntax.synWa ph ps).neg

def NFChoice.Compiler.CompactSourceSyntax.synWex (x : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wex operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWex x ph = (NFChoice.SemanticCore.Wff.all x ph.neg).neg

def NFChoice.Compiler.CompactSourceSyntax.synWnf (x : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wnf operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWnf x ph = NFChoice.SemanticCore.Wff.all x (ph.imp (NFChoice.SemanticCore.Wff.all x ph))

def NFChoice.Compiler.CompactSourceSyntax.synWsb (y x : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wsb operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWeu (x : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream weu operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWmo (x : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wmo operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWmo x ph = (NFChoice.Compiler.CompactSourceSyntax.synWex x ph).imp (NFChoice.Compiler.CompactSourceSyntax.synWeu x ph)

def NFChoice.Compiler.CompactSourceSyntax.synWnfc (x : SemanticCore.Var) (A : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wnfc operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWne (A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wne operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWne A B = (NFChoice.SemanticCore.Wff.classEq A B).neg

def NFChoice.Compiler.CompactSourceSyntax.synWral (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wral operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWral x A ph = NFChoice.SemanticCore.Wff.all x ((NFChoice.SemanticCore.Wff.classMem (NFChoice.SemanticCore.Class.cv x) A).imp ph)

def NFChoice.Compiler.CompactSourceSyntax.synWrex (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wrex operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWreu (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wreu operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWrmo (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wrmo operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCrab (x : SemanticCore.Var) (A : SemanticCore.Class) (ph : SemanticCore.Wff) : SemanticCore.Class

Compact nominal syntax for the upstream crab operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCvv : SemanticCore.Class

Compact nominal syntax for the upstream cvv operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWsbc (A : SemanticCore.Class) (x : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Wff

Compact nominal syntax for the upstream wsbc operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWsbc A x ph = NFChoice.SemanticCore.Wff.classMem A (NFChoice.SemanticCore.Class.cab x ph)

def NFChoice.Compiler.CompactSourceSyntax.synCsb (A : SemanticCore.Class) (x : SemanticCore.Var) (B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream csb operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCnin (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cnin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCcompl (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ccompl operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCcompl A = NFChoice.Compiler.CompactSourceSyntax.synCnin A A

def NFChoice.Compiler.CompactSourceSyntax.synCin (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cin operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCin A B = NFChoice.Compiler.CompactSourceSyntax.synCcompl (NFChoice.Compiler.CompactSourceSyntax.synCnin A B)

def NFChoice.Compiler.CompactSourceSyntax.synCun (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cun operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCdif (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cdif operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCdif A B = NFChoice.Compiler.CompactSourceSyntax.synCin A (NFChoice.Compiler.CompactSourceSyntax.synCcompl B)

def NFChoice.Compiler.CompactSourceSyntax.synCsymdif (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream csymdif operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWss (A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wss operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWss A B = NFChoice.SemanticCore.Wff.classEq (NFChoice.Compiler.CompactSourceSyntax.synCin A B) A

def NFChoice.Compiler.CompactSourceSyntax.synWpss (A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wpss operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synC0 : SemanticCore.Class

Compact nominal syntax for the upstream c0 operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synC0 = NFChoice.Compiler.CompactSourceSyntax.synCdif NFChoice.Compiler.CompactSourceSyntax.synCvv NFChoice.Compiler.CompactSourceSyntax.synCvv

def NFChoice.Compiler.CompactSourceSyntax.synCif (ph : SemanticCore.Wff) (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cif operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCpw (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cpw operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCsn (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream csn operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCpr (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cpr operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCpr A B = NFChoice.Compiler.CompactSourceSyntax.synCun (NFChoice.Compiler.CompactSourceSyntax.synCsn A) (NFChoice.Compiler.CompactSourceSyntax.synCsn B)

def NFChoice.Compiler.CompactSourceSyntax.synCtp (A B C : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ctp operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCuni (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cuni operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCint (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cint operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCiun (x : SemanticCore.Var) (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ciun operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCopk (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream copk operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synC1c : SemanticCore.Class

Compact nominal syntax for the upstream c1c operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCpw1 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cpw1 operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCpw1 A = NFChoice.Compiler.CompactSourceSyntax.synCin (NFChoice.Compiler.CompactSourceSyntax.synCpw A) NFChoice.Compiler.CompactSourceSyntax.synC1c

def NFChoice.Compiler.CompactSourceSyntax.synCuni1 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cuni1 operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCuni1 A = NFChoice.Compiler.CompactSourceSyntax.synCuni (NFChoice.Compiler.CompactSourceSyntax.synCin A NFChoice.Compiler.CompactSourceSyntax.synC1c)

def NFChoice.Compiler.CompactSourceSyntax.synCxpk (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cxpk operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCcnvk (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ccnvk operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCins2k (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cins2k operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCins3k (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cins3k operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCimak (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cimak operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCcomk (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ccomk operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCp6 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cp6 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCsik (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream csik operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCssetk : SemanticCore.Class

Compact nominal syntax for the upstream cssetk operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCimagek (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cimagek operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCidk : SemanticCore.Class

Compact nominal syntax for the upstream cidk operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCio (x : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Class

Compact nominal syntax for the upstream cio operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synC0c : SemanticCore.Class

Compact nominal syntax for the upstream c0c operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synC0c = NFChoice.Compiler.CompactSourceSyntax.synCsn NFChoice.Compiler.CompactSourceSyntax.synC0

def NFChoice.Compiler.CompactSourceSyntax.synCplc (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cplc operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCnnc : SemanticCore.Class

Compact nominal syntax for the upstream cnnc operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCfin : SemanticCore.Class

Compact nominal syntax for the upstream cfin operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCfin = NFChoice.Compiler.CompactSourceSyntax.synCuni NFChoice.Compiler.CompactSourceSyntax.synCnnc

def NFChoice.Compiler.CompactSourceSyntax.synClefin : SemanticCore.Class

Compact nominal syntax for the upstream clefin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCltfin : SemanticCore.Class

Compact nominal syntax for the upstream cltfin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCncfin (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cncfin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCtfin (M : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ctfin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCevenfin : SemanticCore.Class

Compact nominal syntax for the upstream cevenfin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCoddfin : SemanticCore.Class

Compact nominal syntax for the upstream coddfin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWsfin (M N : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wsfin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCspfin : SemanticCore.Class

Compact nominal syntax for the upstream cspfin operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCphi (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cphi operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCop (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cop operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCproj1 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cproj1 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCproj2 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cproj2 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCopab (x y : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Class

Compact nominal syntax for the upstream copab operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWbr (A R B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wbr operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synWbr A R B = NFChoice.SemanticCore.Wff.classMem (NFChoice.Compiler.CompactSourceSyntax.synCop A B) R

def NFChoice.Compiler.CompactSourceSyntax.synC1st : SemanticCore.Class

Compact nominal syntax for the upstream c1st operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCswap : SemanticCore.Class

Compact nominal syntax for the upstream cswap operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCsset : SemanticCore.Class

Compact nominal syntax for the upstream csset operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCcom (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ccom operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCima (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cima operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCsi (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream csi operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCid : SemanticCore.Class

Compact nominal syntax for the upstream cid operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCxp (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cxp operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCcnv (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ccnv operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCrn (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream crn operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCrn A = NFChoice.Compiler.CompactSourceSyntax.synCima A NFChoice.Compiler.CompactSourceSyntax.synCvv

def NFChoice.Compiler.CompactSourceSyntax.synCdm (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cdm operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCdm A = NFChoice.Compiler.CompactSourceSyntax.synCrn (NFChoice.Compiler.CompactSourceSyntax.synCcnv A)

def NFChoice.Compiler.CompactSourceSyntax.synCres (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cres operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCres A B = NFChoice.Compiler.CompactSourceSyntax.synCin A (NFChoice.Compiler.CompactSourceSyntax.synCxp B NFChoice.Compiler.CompactSourceSyntax.synCvv)

def NFChoice.Compiler.CompactSourceSyntax.synWfun (A : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wfun operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWfn (A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wfn operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWf (F A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wf operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWf1 (F A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wf1 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWfo (F A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wfo operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synWf1o (F A B : SemanticCore.Class) : SemanticCore.Wff

Compact nominal syntax for the upstream wf1o operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCfv (F A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cfv operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synC2nd : SemanticCore.Class

Compact nominal syntax for the upstream c2nd operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCo (A F B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream co operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCo A F B = NFChoice.Compiler.CompactSourceSyntax.synCfv F (NFChoice.Compiler.CompactSourceSyntax.synCop A B)

def NFChoice.Compiler.CompactSourceSyntax.synCoprab (x y z : SemanticCore.Var) (ph : SemanticCore.Wff) : SemanticCore.Class

Compact nominal syntax for the upstream coprab operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCmpt (x : SemanticCore.Var) (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cmpt operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCmpt2 (x : SemanticCore.Var) (A : SemanticCore.Class) (y : SemanticCore.Var) (B C : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cmpt2 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCtxp (A B : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ctxp operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCfix (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cfix operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCfix A = NFChoice.Compiler.CompactSourceSyntax.synCrn (NFChoice.Compiler.CompactSourceSyntax.synCin A NFChoice.Compiler.CompactSourceSyntax.synCid)

def NFChoice.Compiler.CompactSourceSyntax.synCcup : SemanticCore.Class

Compact nominal syntax for the upstream ccup operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCdisj : SemanticCore.Class

Compact nominal syntax for the upstream cdisj operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCaddcfn : SemanticCore.Class

Compact nominal syntax for the upstream caddcfn operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCcompose : SemanticCore.Class

Compact nominal syntax for the upstream ccompose operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCins2 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cins2 operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCins2 A = NFChoice.Compiler.CompactSourceSyntax.synCtxp NFChoice.Compiler.CompactSourceSyntax.synCvv A

def NFChoice.Compiler.CompactSourceSyntax.synCins3 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cins3 operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCins3 A = NFChoice.Compiler.CompactSourceSyntax.synCtxp A NFChoice.Compiler.CompactSourceSyntax.synCvv

def NFChoice.Compiler.CompactSourceSyntax.synCimage (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cimage operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCins4 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cins4 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCsi3 (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream csi3 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCfuns : SemanticCore.Class

Compact nominal syntax for the upstream cfuns operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCfns : SemanticCore.Class

Compact nominal syntax for the upstream cfns operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCpw1fn : SemanticCore.Class

Compact nominal syntax for the upstream cpw1fn operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCfullfun (F : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cfullfun operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCclos1 (S R : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cclos1 operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCtrans : SemanticCore.Class

Compact nominal syntax for the upstream ctrans operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCref : SemanticCore.Class

Compact nominal syntax for the upstream cref operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCantisym : SemanticCore.Class

Compact nominal syntax for the upstream cantisym operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCpartial : SemanticCore.Class

Compact nominal syntax for the upstream cpartial operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCconnex : SemanticCore.Class

Compact nominal syntax for the upstream cconnex operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCstrict : SemanticCore.Class

Compact nominal syntax for the upstream cstrict operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCfound : SemanticCore.Class

Compact nominal syntax for the upstream cfound operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCwe : SemanticCore.Class

Compact nominal syntax for the upstream cwe operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCwe = NFChoice.Compiler.CompactSourceSyntax.synCin NFChoice.Compiler.CompactSourceSyntax.synCstrict NFChoice.Compiler.CompactSourceSyntax.synCfound

def NFChoice.Compiler.CompactSourceSyntax.synCsym : SemanticCore.Class

Compact nominal syntax for the upstream csym operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCer : SemanticCore.Class

Compact nominal syntax for the upstream cer operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCer = NFChoice.Compiler.CompactSourceSyntax.synCin NFChoice.Compiler.CompactSourceSyntax.synCsym NFChoice.Compiler.CompactSourceSyntax.synCtrans

def NFChoice.Compiler.CompactSourceSyntax.synCec (A R : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cec operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCec A R = NFChoice.Compiler.CompactSourceSyntax.synCima R (NFChoice.Compiler.CompactSourceSyntax.synCsn A)

def NFChoice.Compiler.CompactSourceSyntax.synCqs (A R : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cqs operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCmap : SemanticCore.Class

Compact nominal syntax for the upstream cmap operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCen : SemanticCore.Class

Compact nominal syntax for the upstream cen operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCncs : SemanticCore.Class

Compact nominal syntax for the upstream cncs operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCncs = NFChoice.Compiler.CompactSourceSyntax.synCqs NFChoice.Compiler.CompactSourceSyntax.synCvv NFChoice.Compiler.CompactSourceSyntax.synCen

def NFChoice.Compiler.CompactSourceSyntax.synClec : SemanticCore.Class

Compact nominal syntax for the upstream clec operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCltc : SemanticCore.Class

Compact nominal syntax for the upstream cltc operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCltc = NFChoice.Compiler.CompactSourceSyntax.synCdif NFChoice.Compiler.CompactSourceSyntax.synClec NFChoice.Compiler.CompactSourceSyntax.synCid

def NFChoice.Compiler.CompactSourceSyntax.synCnc (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream cnc operator.

Equations

• NFChoice.Compiler.CompactSourceSyntax.synCnc A = NFChoice.Compiler.CompactSourceSyntax.synCec A NFChoice.Compiler.CompactSourceSyntax.synCen

def NFChoice.Compiler.CompactSourceSyntax.synCtc (A : SemanticCore.Class) : SemanticCore.Class

Compact nominal syntax for the upstream ctc operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synC2c : SemanticCore.Class

Compact nominal syntax for the upstream c2c operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synC3c : SemanticCore.Class

Compact nominal syntax for the upstream c3c operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCce : SemanticCore.Class

Compact nominal syntax for the upstream cce operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCtcfn : SemanticCore.Class

Compact nominal syntax for the upstream ctcfn operator.

Equations

• One or more equations did not get rendered due to their size.

def NFChoice.Compiler.CompactSourceSyntax.synCspac : SemanticCore.Class

Compact nominal syntax for the upstream cspac operator.

Equations

• One or more equations did not get rendered due to their size.

Small reduction checks for a no-dummy and a dummy-bearing definition.