Documentation

LeanPool.NFWeakPartition.NAR4C084C001Part003

NF weak partition development: NAR4C084C001Part003.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084SplitAlpha0000 (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (d : SemanticCore.Var) :
Nominal.TAlphaWff [(nb084AlphaDummy015 A B R, nb084AlphaDummy016 x y A R), (nb084AlphaDummy013 A B R, nb084AlphaDummy014 x y A R), (nb084AlphaDummy004 A B R, nb084AlphaDummy006 x y A R), (nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy015 A B R)) (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy015 A B R)) (SemanticCore.Class.cab (nb084AlphaDummy009 A B R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy010 A B R) (SemanticCore.Class.cv (nb084AlphaDummy003 A B R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy009 A B R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy010 A B R))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy016 x y A R)) (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb084AlphaDummy016 x y A R)) (SemanticCore.Class.cab (nb084AlphaDummy011 x y A R) (Compiler.CompactSourceSyntax.synWrex (nb084AlphaDummy012 x y A R) (SemanticCore.Class.cv (nb084AlphaDummy005 x y A R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb084AlphaDummy011 x y A R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb084AlphaDummy012 x y A R))))))).neg)

Checked nominal proof certificate identified upstream as nb084_split_alpha_0000.

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