Documentation

LeanPool.NFWeakPartition.NAR4C070C001Part004

NF weak partition development: NAR4C070C001Part004.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070WppRefl0010 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) :
Nominal.TReflOn [(nb070AlphaDummy009 A, nb070AlphaDummy011 x), (nb070AlphaDummy008 A, nb070AlphaDummy010 x), (nb070AlphaDummy001 A, x), (nb070AlphaDummy000 A, b), (nb070AlphaDummy002 A, nb070AlphaDummy003 x A b), (nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] Compiler.CompactSourceSyntax.synCen.fv

Checked nominal proof certificate identified upstream as nb070_wpp_refl_0010.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb070SplitAlpha0006 (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_b_x : b ≠ x) :
    Nominal.TAlphaWff [(nb070AlphaDummy005 A, nb070AlphaDummy007 x A b), (nb070AlphaDummy004 A, nb070AlphaDummy006 x A b)] ((SemanticCore.Wff.objMem (nb070AlphaDummy004 A) (nb070AlphaDummy005 A)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy005 A)) (SemanticCore.Class.cab (nb070AlphaDummy002 A) (SemanticCore.Wff.classEq (SemanticCore.Class.cab (nb070AlphaDummy000 A) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy000 A)) Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWrex (nb070AlphaDummy001 A) A (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb070AlphaDummy000 A)) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv (nb070AlphaDummy001 A)))))))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb070AlphaDummy002 A)))))).neg) ((SemanticCore.Wff.objMem (nb070AlphaDummy006 x A b) (nb070AlphaDummy007 x A b)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb070AlphaDummy007 x A b)) (SemanticCore.Class.cab (nb070AlphaDummy003 x A b) (SemanticCore.Wff.classEq (SemanticCore.Class.cab b (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv b) Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv x))))))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb070AlphaDummy003 x A b)))))).neg)

    Checked nominal proof certificate identified upstream as nb070_split_alpha_0006.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfTc (x : SemanticCore.Var) (A : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_b_x : b ≠ x) :
      Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc A) (Compiler.CompactSourceSyntax.synCio b (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv b) Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWrex x A (SemanticCore.Wff.classEq (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCpw1 (SemanticCore.Class.cv x))))))))

      Checked nominal proof certificate identified upstream as nominal_df_tc.

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