Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart032.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnsucelrlem1 (x m a : SemanticCore.Var) (dv_a_m : a ≠ m) (dv_a_x : a ≠ x) (dv_m_x : m ≠ x) : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab m (SemanticCore.Wff.all a (SemanticCore.Wff.all x ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.objMem x a).neg (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv a) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv m) Compiler.CompactSourceSyntax.synC1c))).imp (SemanticCore.Wff.objMem a m))))) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_nnsucelrlem1.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart033.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnsucelrlem2 (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B A).neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn B)) (Compiler.CompactSourceSyntax.synCsn B)) A))

Checked nominal proof certificate identified upstream as g_nnsucelrlem2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnsucelrlem3 (A B X Y : SemanticCore.Class) (hyp_nnsucelrlem3_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (Compiler.CompactSourceSyntax.synWne X Y) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn X)) (Compiler.CompactSourceSyntax.synCun B (Compiler.CompactSourceSyntax.synCsn Y))) (SemanticCore.Wff.classMem Y B).neg).imp (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCdif A (Compiler.CompactSourceSyntax.synCsn Y)) (Compiler.CompactSourceSyntax.synCsn X))))

Checked nominal proof certificate identified upstream as g_nnsucelrlem3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnsucelrlem4 (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCdif B (Compiler.CompactSourceSyntax.synCsn A)) (Compiler.CompactSourceSyntax.synCsn A)) B))

Checked nominal proof certificate identified upstream as g_nnsucelrlem4.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart034.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnsucelr (A M X : SemanticCore.Class) (hyp_nnsucelr_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_nnsucelr_2 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem X A).neg (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn X)) (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c)))).imp (SemanticCore.Wff.classMem A M))

Checked nominal proof certificate identified upstream as g_nnsucelr.

Equations

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