Documentation

LeanPool.NFWeakPartition.NAR4H5C093M3Part003

NF weak partition development: NAR4H5C093M3Part003.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093SplitAlpha0002 (A : SemanticCore.Class) (r d : SemanticCore.Var) :
Nominal.TAlphaWff [(nb093AlphaDummy070 A, nb093AlphaDummy071 r), (nb093AlphaDummy068 A, nb093AlphaDummy069 r), (nb093AlphaDummy059 A, nb093AlphaDummy061 r), (nb093AlphaDummy058 A, nb093AlphaDummy060 r), (nb093AlphaDummy062 A, nb093AlphaDummy063 r), (nb093AlphaDummy056 A, nb093AlphaDummy057 r), (nb093AlphaDummy054 A, nb093AlphaDummy055 r), (nb093AlphaDummy052 A, nb093AlphaDummy053 r), (nb093AlphaDummy045 A, nb093AlphaDummy047 r d), (nb093AlphaDummy044 A, nb093AlphaDummy046 r d), (nb093AlphaDummy050 A, nb093AlphaDummy051 r d), (nb093AlphaDummy048 A, nb093AlphaDummy049 r d), (nb093AlphaDummy000 A, d), (nb093AlphaDummy001 A, r), (nb093AlphaDummy006 A, nb093AlphaDummy007 r d), (nb093AlphaDummy004 A, nb093AlphaDummy005 A r d), (nb093AlphaDummy002 A, nb093AlphaDummy003 A r d)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy070 A)) (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy070 A)) (SemanticCore.Class.cab (nb093AlphaDummy064 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy065 A) (SemanticCore.Class.cv (nb093AlphaDummy058 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy064 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy071 r)) (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy071 r)) (SemanticCore.Class.cab (nb093AlphaDummy066 r) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy067 r) (SemanticCore.Class.cv (nb093AlphaDummy060 r)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy066 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r))))))).neg)

Checked nominal proof certificate identified upstream as nb093_split_alpha_0002.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093SplitAlpha0003 (A : SemanticCore.Class) (r d : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb093AlphaDummy098 A, nb093AlphaDummy099 r), (nb093AlphaDummy096 A, nb093AlphaDummy097 r), (nb093AlphaDummy065 A, nb093AlphaDummy067 r), (nb093AlphaDummy064 A, nb093AlphaDummy066 r), (nb093AlphaDummy094 A, nb093AlphaDummy095 r), (nb093AlphaDummy068 A, nb093AlphaDummy069 r), (nb093AlphaDummy059 A, nb093AlphaDummy061 r), (nb093AlphaDummy058 A, nb093AlphaDummy060 r), (nb093AlphaDummy062 A, nb093AlphaDummy063 r), (nb093AlphaDummy056 A, nb093AlphaDummy057 r), (nb093AlphaDummy054 A, nb093AlphaDummy055 r), (nb093AlphaDummy052 A, nb093AlphaDummy053 r), (nb093AlphaDummy045 A, nb093AlphaDummy047 r d), (nb093AlphaDummy044 A, nb093AlphaDummy046 r d), (nb093AlphaDummy050 A, nb093AlphaDummy051 r d), (nb093AlphaDummy048 A, nb093AlphaDummy049 r d), (nb093AlphaDummy000 A, d), (nb093AlphaDummy001 A, r), (nb093AlphaDummy006 A, nb093AlphaDummy007 r d), (nb093AlphaDummy004 A, nb093AlphaDummy005 A r d), (nb093AlphaDummy002 A, nb093AlphaDummy003 A r d)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy098 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy098 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy065 A)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy099 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy099 r)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy067 r)))).neg)

    Checked nominal proof certificate identified upstream as nb093_split_alpha_0003.

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