Documentation

LeanPool.NFWeakPartition.Certificates.NominalWPPReplayChunk015Compact001Block003

Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk015Compact001Part011.

source
noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqordor (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.synCstrict (Compiler.CompactSourceSyntax.synClnquo R C)))

Checked nominal proof certificate identified upstream as g_lnqordor.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnkereceqb (C R X Y : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) :
    Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (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)))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem X C) (SemanticCore.Wff.classMem Y C))).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCec X (Compiler.CompactSourceSyntax.synClnker R)) (Compiler.CompactSourceSyntax.synCec Y (Compiler.CompactSourceSyntax.synClnker R))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr X R Y) (Compiler.CompactSourceSyntax.synWbr Y R X))))

    Checked nominal proof certificate identified upstream as g_lnkereceqb.

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

      Certificates from NominalWPPReplayChunk015Compact001Part012.

      source
      noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrlnqordstrict (C R X Y : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) :
      Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (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)))) (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.synCdif (Compiler.CompactSourceSyntax.synClnqord R C) Compiler.CompactSourceSyntax.synCid) (Compiler.CompactSourceSyntax.synCec Y (Compiler.CompactSourceSyntax.synClnker R))) (Compiler.CompactSourceSyntax.synWbr X (Compiler.CompactSourceSyntax.synCdif R (Compiler.CompactSourceSyntax.synCcnv R)) Y)))

      Checked nominal proof certificate identified upstream as g_brlnqordstrict.

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

        Certificates from NominalWPPReplayChunk015Compact001Part013.

        source
        noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnquounionb (u : SemanticCore.Var) (C R S : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) :
        Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (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)))) (Compiler.CompactSourceSyntax.synWss S (Compiler.CompactSourceSyntax.synClnquo R C))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) C)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCuni S)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCec (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synClnker R)) S)))

        Checked nominal proof certificate identified upstream as g_lnquounionb.

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

          Certificates from NominalWPPReplayChunk015Compact001Part014.

          source
          noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLnqordwe (C R : SemanticCore.Class) (dv_C_R : Disjoint C.fv R.fv) :
          Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (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)))) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCdif R (Compiler.CompactSourceSyntax.synCcnv R)) Compiler.CompactSourceSyntax.synCfound C)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synClnqord R C) Compiler.CompactSourceSyntax.synCwe (Compiler.CompactSourceSyntax.synClnquo R C)))

          Checked nominal proof certificate identified upstream as g_lnqordwe.

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

            Certificates from NominalWPPReplayChunk015Compact001Part015.

            source
            noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinleastadjndv (k m n : SemanticCore.Var) (X Y : SemanticCore.Class) (_dv_X_k : k ∉ X.fv) (_dv_X_m : m ∉ X.fv) (dv_X_n : n ∉ X.fv) (_dv_Y_k : k ∉ Y.fv) (_dv_Y_m : m ∉ Y.fv) (dv_Y_n : n ∉ Y.fv) (_dv_k_m : k ≠ m) (dv_k_n : k ≠ n) (dv_m_n : m ≠ n) :
            Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synCnnc)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv m) X) (SemanticCore.Wff.classMem (SemanticCore.Class.cv k) Y)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) X).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n)))) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Y).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (SemanticCore.Class.cv n))))) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) X).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Y))) (Compiler.CompactSourceSyntax.synWral n Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv n) Y).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synC1c) X)))))).imp (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (SemanticCore.Class.cv m) (SemanticCore.Class.cv k)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv m) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv k) Compiler.CompactSourceSyntax.synC1c))))

            Checked nominal proof certificate identified upstream as g_finleastadjndv.

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