NF weak partition development: NAR4C068C001Part036.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0085
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy293, nb068AlphaDummy294 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f))))
Checked nominal proof certificate identified upstream as nb068_split_alpha_0085.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0086
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy303, nb068AlphaDummy306 f), (nb068AlphaDummy302, nb068AlphaDummy305 f), (nb068AlphaDummy301, nb068AlphaDummy304 f), (nb068AlphaDummy299, nb068AlphaDummy300 f), (nb068AlphaDummy295, nb068AlphaDummy297 f), (nb068AlphaDummy296, nb068AlphaDummy298 f), (nb068AlphaDummy321, nb068AlphaDummy322 f), (nb068AlphaDummy319, nb068AlphaDummy320 f), (nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy317, nb068AlphaDummy318 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy302)
(SemanticCore.Class.cv nb068AlphaDummy303))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy301)
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy302)
(SemanticCore.Class.cv nb068AlphaDummy303))).neg)
((SemanticCore.Wff.classEq
(Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy305 f))
(SemanticCore.Class.cv (nb068AlphaDummy306 f)))
Compiler.CompactSourceSyntax.synC0).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy304 f))
(Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy305 f))
(SemanticCore.Class.cv (nb068AlphaDummy306 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0086.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0087
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy295, nb068AlphaDummy297 f), (nb068AlphaDummy296, nb068AlphaDummy298 f), (nb068AlphaDummy321, nb068AlphaDummy322 f), (nb068AlphaDummy319, nb068AlphaDummy320 f), (nb068AlphaDummy288, nb068AlphaDummy290 f), (nb068AlphaDummy287, nb068AlphaDummy289 f), (nb068AlphaDummy317, nb068AlphaDummy318 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy295) (SemanticCore.Class.cv nb068AlphaDummy288)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy296)
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy295) Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy295)
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv nb068AlphaDummy295))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy297 f))
(SemanticCore.Class.cv (nb068AlphaDummy290 f))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy298 f))
(Compiler.CompactSourceSyntax.synCif
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy297 f))
Compiler.CompactSourceSyntax.synCnnc)
(Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy297 f))
Compiler.CompactSourceSyntax.synC1c)
(SemanticCore.Class.cv (nb068AlphaDummy297 f)))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0087.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0088
(x y f : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb068AlphaDummy317, nb068AlphaDummy318 f), (nb068AlphaDummy291, nb068AlphaDummy292 f), (nb068AlphaDummy284, nb068AlphaDummy286 f), (nb068AlphaDummy283, nb068AlphaDummy285 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy317)
(SemanticCore.Class.cab nb068AlphaDummy287
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy317)
(SemanticCore.Class.cab nb068AlphaDummy287
(Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy288 (SemanticCore.Class.cv nb068AlphaDummy283)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy287)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy288))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy318 f))
(SemanticCore.Class.cab (nb068AlphaDummy289 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy318 f))
(SemanticCore.Class.cab (nb068AlphaDummy289 f)
(Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy290 f) (SemanticCore.Class.cv (nb068AlphaDummy285 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy289 f))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy290 f)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)
Checked nominal proof certificate identified upstream as nb068_split_alpha_0088.
Equations
- One or more equations did not get rendered due to their size.