NF weak partition development: NAR4C072C001Part017.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0007
(x y : SemanticCore.Var)
(A B R S_cls H : SemanticCore.Class)
(dv_H_x : x ∉ H.fv)
(dv_H_y : y ∉ H.fv)
(dv_R_x : x ∉ R.fv)
(dv_R_y : y ∉ R.fv)
(dv_S_x : x ∉ S_cls.fv)
(dv_S_y : y ∉ S_cls.fv)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaWff [(nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)]
((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H)) R
(SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H))).imp
(Compiler.CompactSourceSyntax.synWbr
(Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H))) S_cls
(Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H)))))
((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)).imp
(Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x)) S_cls
(Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv y))))
Checked nominal proof certificate identified upstream as nb072_split_alpha_0007.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb072SplitAlpha0008
(x y : SemanticCore.Var)
(A B R S_cls H : SemanticCore.Class)
(dv_H_x : x ∉ H.fv)
(dv_H_y : y ∉ H.fv)
(dv_R_x : x ∉ R.fv)
(dv_R_y : y ∉ R.fv)
(dv_S_x : x ∉ S_cls.fv)
(dv_S_y : y ∉ S_cls.fv)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaWff [(nb072AlphaDummy001 A B R S_cls H, y), (nb072AlphaDummy000 A B R S_cls H, x)]
((Compiler.CompactSourceSyntax.synWbr
(Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H))) S_cls
(Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H)))).imp
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb072AlphaDummy000 A B R S_cls H)) R
(SemanticCore.Class.cv (nb072AlphaDummy001 A B R S_cls H))))
((Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x)) S_cls
(Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv y))).imp
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)))
Checked nominal proof certificate identified upstream as nb072_split_alpha_0008.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfIso
(x y : SemanticCore.Var)
(A B R S_cls H : SemanticCore.Class)
(dv_A_x : x ∉ A.fv)
(dv_A_y : y ∉ A.fv)
(__dv_B_x : x ∉ B.fv)
(__dv_B_y : y ∉ B.fv)
(dv_H_x : x ∉ H.fv)
(dv_H_y : y ∉ H.fv)
(dv_R_x : x ∉ R.fv)
(dv_R_y : y ∉ R.fv)
(dv_S_x : x ∉ S_cls.fv)
(dv_S_y : y ∉ S_cls.fv)
(dv_x_y : x ≠ y)
:
Nominal.NPrf
(Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S_cls A B)
(Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWf1o H A B)
(Compiler.CompactSourceSyntax.synWral x A
(Compiler.CompactSourceSyntax.synWral y A
(Compiler.CompactSourceSyntax.synWb
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y))
(Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv x)) S_cls
(Compiler.CompactSourceSyntax.synCfv H (SemanticCore.Class.cv y))))))))
Checked nominal proof certificate identified upstream as nominal_df_iso.
Equations
- One or more equations did not get rendered due to their size.