Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk015Compact001Block002

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part007.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrlnqordkern (C R X Y : SemanticCore.Class) (_dv_C_R : Disjoint C.fv R.fv) :
Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref C) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans C)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C C))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem X C) (SemanticCore.Wff.classMem Y C)))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCec X (Compiler.CompactSourceSyntax.synClnker R)) (Compiler.CompactSourceSyntax.synClnqord R C) (Compiler.CompactSourceSyntax.synCec Y (Compiler.CompactSourceSyntax.synClnker R))) (Compiler.CompactSourceSyntax.synWbr X R Y)))

Checked nominal proof certificate identified upstream as g_brlnqordkern.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqordref (C R : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) :
    Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref C) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans C)) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex C)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C C)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synClnqord R C) Compiler.CompactSourceSyntax.synCref (Compiler.CompactSourceSyntax.synClnquo R C)))

    Checked nominal proof certificate identified upstream as g_lnqordref.

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

      Certificates from NominalWPPReplayChunk015Compact001Part008.

      source
      noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqordtrans (C R : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) :
      Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref C) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans C)) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex C)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C C)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synClnqord R C) Compiler.CompactSourceSyntax.synCtrans (Compiler.CompactSourceSyntax.synClnquo R C)))

      Checked nominal proof certificate identified upstream as g_lnqordtrans.

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

        Certificates from NominalWPPReplayChunk015Compact001Part009.

        source
        noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqordconnex (C R : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) :
        Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref C) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans C)) (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex C)) (Compiler.CompactSourceSyntax.synWss R (Compiler.CompactSourceSyntax.synCxp C C)))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synClnqord R C) Compiler.CompactSourceSyntax.synCconnex (Compiler.CompactSourceSyntax.synClnquo R C)))

        Checked nominal proof certificate identified upstream as g_lnqordconnex.

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