Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAntisymex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCantisym Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_antisymex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part021.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gConnexex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCconnex Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_connexex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFoundex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCfound Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_foundex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part023.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPartialex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCpartial Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_partialex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStrictex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCstrict Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_strictex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWeex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCwe Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_weex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTrd (ph : SemanticCore.Wff) (A R X Y Z : SemanticCore.Class) (hyp_trd_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCtrans A))) (hyp_trd_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem X A))) (hyp_trd_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Y A))) (hyp_trd_4 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem Z A))) (hyp_trd_5 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Y))) (hyp_trd_6 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr Y R Z))) : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWbr X R Z))

Checked nominal proof certificate identified upstream as g_trd.

Equations

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