Nominal proof certificates grouped in dependency order.

Certificates from NAR4C090C001Part066.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0044 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) : Nominal.TAlphaWff [(nb090AlphaDummy551 A, nb090AlphaDummy552 h), (nb090AlphaDummy549 A, nb090AlphaDummy550 h), (nb090AlphaDummy504 A, nb090AlphaDummy506 h), (nb090AlphaDummy503 A, nb090AlphaDummy505 h), (nb090AlphaDummy507 A, nb090AlphaDummy508 h), (nb090AlphaDummy425 A, nb090AlphaDummy428 h), (nb090AlphaDummy424 A, nb090AlphaDummy427 h), (nb090AlphaDummy423 A, nb090AlphaDummy426 h), (nb090AlphaDummy429 A, nb090AlphaDummy430 h), (nb090AlphaDummy421 A, nb090AlphaDummy422 h), (nb090AlphaDummy419 A, nb090AlphaDummy420 h), (nb090AlphaDummy000 A, h), (nb090AlphaDummy002 A, v), (nb090AlphaDummy001 A, u), (nb090AlphaDummy003 A, nb090AlphaDummy004 v u A h)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy551 A)) (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy551 A)) (SemanticCore.Class.cab (nb090AlphaDummy545 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy546 A) (SemanticCore.Class.cv (nb090AlphaDummy504 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy545 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy552 h)) (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy552 h)) (SemanticCore.Class.cab (nb090AlphaDummy547 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy548 h) (SemanticCore.Class.cv (nb090AlphaDummy506 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy547 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h))))))).neg)

Checked nominal proof certificate identified upstream as nb090_split_alpha_0044.

Equations

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

Certificates from NAR4C090C001Part067.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0045 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) : Nominal.TAlphaWff [(nb090AlphaDummy579 A, nb090AlphaDummy580 h), (nb090AlphaDummy577 A, nb090AlphaDummy578 h), (nb090AlphaDummy546 A, nb090AlphaDummy548 h), (nb090AlphaDummy545 A, nb090AlphaDummy547 h), (nb090AlphaDummy575 A, nb090AlphaDummy576 h), (nb090AlphaDummy549 A, nb090AlphaDummy550 h), (nb090AlphaDummy504 A, nb090AlphaDummy506 h), (nb090AlphaDummy503 A, nb090AlphaDummy505 h), (nb090AlphaDummy507 A, nb090AlphaDummy508 h), (nb090AlphaDummy425 A, nb090AlphaDummy428 h), (nb090AlphaDummy424 A, nb090AlphaDummy427 h), (nb090AlphaDummy423 A, nb090AlphaDummy426 h), (nb090AlphaDummy429 A, nb090AlphaDummy430 h), (nb090AlphaDummy421 A, nb090AlphaDummy422 h), (nb090AlphaDummy419 A, nb090AlphaDummy420 h), (nb090AlphaDummy000 A, h), (nb090AlphaDummy002 A, v), (nb090AlphaDummy001 A, u), (nb090AlphaDummy003 A, nb090AlphaDummy004 v u A h)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy579 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy579 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy546 A)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy580 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy580 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy548 h)))).neg)

Checked nominal proof certificate identified upstream as nb090_split_alpha_0045.

Equations

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

Certificates from NAR4C090C001Part068.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0046 (v u : SemanticCore.Var) (A : SemanticCore.Class) (h : SemanticCore.Var) : Nominal.TAlphaWff [(nb090AlphaDummy141 A, nb090AlphaDummy142 h), (nb090AlphaDummy139 A, nb090AlphaDummy140 h), (nb090AlphaDummy130 A, nb090AlphaDummy132 h), (nb090AlphaDummy129 A, nb090AlphaDummy131 h), (nb090AlphaDummy133 A, nb090AlphaDummy134 h), (nb090AlphaDummy504 A, nb090AlphaDummy506 h), (nb090AlphaDummy503 A, nb090AlphaDummy505 h), (nb090AlphaDummy507 A, nb090AlphaDummy508 h), (nb090AlphaDummy425 A, nb090AlphaDummy428 h), (nb090AlphaDummy424 A, nb090AlphaDummy427 h), (nb090AlphaDummy423 A, nb090AlphaDummy426 h), (nb090AlphaDummy429 A, nb090AlphaDummy430 h), (nb090AlphaDummy421 A, nb090AlphaDummy422 h), (nb090AlphaDummy419 A, nb090AlphaDummy420 h), (nb090AlphaDummy000 A, h), (nb090AlphaDummy002 A, v), (nb090AlphaDummy001 A, u), (nb090AlphaDummy003 A, nb090AlphaDummy004 v u A h)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy141 A)) (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy141 A)) (SemanticCore.Class.cab (nb090AlphaDummy135 A) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy136 A) (SemanticCore.Class.cv (nb090AlphaDummy129 A)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy135 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy136 A))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy142 h)) (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy142 h)) (SemanticCore.Class.cab (nb090AlphaDummy137 h) (Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy138 h) (SemanticCore.Class.cv (nb090AlphaDummy131 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy137 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy138 h))))))).neg)

Checked nominal proof certificate identified upstream as nb090_split_alpha_0046.

Equations

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