Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk010Compact001Block003

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk010Compact001Part007.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnadjoin (x : SemanticCore.Var) (L N X : SemanticCore.Class) (b : SemanticCore.Var) (dv_L_b : b ∉ L.fv) (dv_L_x : x ∉ L.fv) (dv_X_b : b ∉ X.fv) (dv_X_x : x ∉ X.fv) (dv_b_x : b ≠ x) :
Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem L N) (SemanticCore.Wff.classMem X (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCuni L)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWrex b L (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsn X))))) N))

Checked nominal proof certificate identified upstream as g_nnadjoin.

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

    Certificates from NominalWPPReplayChunk010Compact001Part008.

    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnadjoinpw (A M N X : SemanticCore.Class) :
    Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A M) (SemanticCore.Wff.classMem X (Compiler.CompactSourceSyntax.synCcompl A))) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw A) N)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn X))) (Compiler.CompactSourceSyntax.synCplc N N)))

    Checked nominal proof certificate identified upstream as g_nnadjoinpw.

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