NF weak partition development: NAR4C082C001Part006.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082WppRefl0008 (A B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_A_p : p ∉ A.fv) (dv_B_p : p ∉ B.fv) (dv_R_p : p ∉ R.fv) : Nominal.TReflOn [(nb082AlphaDummy050 A B R, nb082AlphaDummy052 A B R p), (nb082AlphaDummy049 A B R, nb082AlphaDummy051 A B R p), (nb082AlphaDummy047 A B R, nb082AlphaDummy048 A B R p), (nb082AlphaDummy045 A B R, nb082AlphaDummy046 A B R p), (nb082AlphaDummy042 A B R, nb082AlphaDummy044 A B R p), (nb082AlphaDummy041 A B R, nb082AlphaDummy043 A B R p), (nb082AlphaDummy001 A B R, nb082AlphaDummy002 A B R p), (nb082AlphaDummy000 A B R, p), (nb082AlphaDummy003 A B R, nb082AlphaDummy004 A B R p)] (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

Checked nominal proof certificate identified upstream as nb082_wpp_refl_0008.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082WppRefl0008 A B R p dv_A_p dv_B_p dv_R_p = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082SplitAlpha0003 (A B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_A_p : p ∉ A.fv) (dv_B_p : p ∉ B.fv) (dv_R_p : p ∉ R.fv) : Nominal.TAlphaWff [(nb082AlphaDummy045 A B R, nb082AlphaDummy046 A B R p), (nb082AlphaDummy042 A B R, nb082AlphaDummy044 A B R p), (nb082AlphaDummy041 A B R, nb082AlphaDummy043 A B R p), (nb082AlphaDummy001 A B R, nb082AlphaDummy002 A B R p), (nb082AlphaDummy000 A B R, p), (nb082AlphaDummy003 A B R, nb082AlphaDummy004 A B R p)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy045 A B R)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb082AlphaDummy000 A B R)))) Compiler.CompactSourceSyntax.synC1c)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy045 A B R)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv (nb082AlphaDummy000 A B R)))) Compiler.CompactSourceSyntax.synC1c)).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy046 A B R p)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv p))) Compiler.CompactSourceSyntax.synC1c)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb082AlphaDummy046 A B R p)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCimak (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv p))) Compiler.CompactSourceSyntax.synC1c)).neg)

Checked nominal proof certificate identified upstream as nb082_split_alpha_0003.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFdpivmap2 (A B R : SemanticCore.Class) (p : SemanticCore.Var) (__dv_A_B : Disjoint A.fv B.fv) (__dv_A_R : Disjoint A.fv R.fv) (dv_A_p : p ∉ A.fv) (__dv_B_R : Disjoint B.fv R.fv) (dv_B_p : p ∉ B.fv) (dv_R_p : p ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdpivmap2 R A B) (Compiler.CompactSourceSyntax.synCmpt p (Compiler.CompactSourceSyntax.synCxpk B B) (Compiler.CompactSourceSyntax.synCfdminvalp R A B (SemanticCore.Class.cv p))))

Checked nominal proof certificate identified upstream as nominal_df_fdpivmap2.

Equations

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