Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C077C001Block017

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C077C001Part049.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0035 (x : SemanticCore.Var) (F I : SemanticCore.Class) :
Nominal.TAlphaWff [(nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy055 F I)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy055 F I)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt (nb077AlphaDummy000 F I) Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy000 F I)) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy056 x F)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy056 x F)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC1st) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) Compiler.CompactSourceSyntax.synC1st)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synC2nd) (Compiler.CompactSourceSyntax.synCcom F Compiler.CompactSourceSyntax.synC2nd)))).neg)

Checked nominal proof certificate identified upstream as nb077_split_alpha_0035.

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

    Certificates from NAR4C077C001Part050.

    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFrec (x : SemanticCore.Var) (F I : SemanticCore.Class) (__dv_F_x : x ∉ F.fv) (__dv_I_x : x ∉ I.fv) :
    Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfrec F I) (Compiler.CompactSourceSyntax.synCclos1 (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)) (Compiler.CompactSourceSyntax.synCpprod (Compiler.CompactSourceSyntax.synCmpt x Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)) F)))

    Checked nominal proof certificate identified upstream as nominal_df_frec.

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