Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012BCompact001Part001.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsoeq1 (A B R S G H : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq H G).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso G R S A B)))

Checked nominal proof certificate identified upstream as g_isoeq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsoeq2 (A B R S T H : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq R T).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso H T S A B)))

Checked nominal proof certificate identified upstream as g_isoeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsoeq3 (A B R S T H : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq S T).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso H R T A B)))

Checked nominal proof certificate identified upstream as g_isoeq3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsoeq4 (A B C R S H : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A C).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso H R S C B)))

Checked nominal proof certificate identified upstream as g_isoeq4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsoeq5 (A B C R S H : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq B C).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso H R S A C)))

Checked nominal proof certificate identified upstream as g_isoeq5.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part002.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsof1o (A B R S H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWiso H R S A B).imp (Compiler.CompactSourceSyntax.synWf1o H A B))

Checked nominal proof certificate identified upstream as g_isof1o.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsorel (A B C D R S H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C A) (SemanticCore.Wff.classMem D A))).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr C R D) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCfv H C) S (Compiler.CompactSourceSyntax.synCfv H D))))

Checked nominal proof certificate identified upstream as g_isorel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsoid (A R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCres Compiler.CompactSourceSyntax.synCid A) R R A A)

Checked nominal proof certificate identified upstream as g_isoid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsocnv (A B R S H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWiso H R S A B).imp (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCcnv H) S R B A))

Checked nominal proof certificate identified upstream as g_isocnv.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part003.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsores2 (A B R S H : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso H R (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp B B)) A B))

Checked nominal proof certificate identified upstream as g_isores2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsores1 (A B R S H : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso H (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp A A)) S A B))

Checked nominal proof certificate identified upstream as g_isores1.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part004.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsotr (A B C R S T G H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso H R S A B) (Compiler.CompactSourceSyntax.synWiso G S T B C)).imp (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCcom G H) R T A C))

Checked nominal proof certificate identified upstream as g_isotr.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part005.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIsoini (A B D R S H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWiso H R S A B) (SemanticCore.Wff.classMem D A)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCima H (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv R) (Compiler.CompactSourceSyntax.synCsn D)))) (Compiler.CompactSourceSyntax.synCin B (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv S) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCfv H D))))))

Checked nominal proof certificate identified upstream as g_isoini.

Equations

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