Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part055.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTaddc (A B X : SemanticCore.Class) (c : SemanticCore.Var) (dv_X_c : c ∉ X.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCncs)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCtc A) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCtc B) X))).imp (Compiler.CompactSourceSyntax.synWrex c Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq X (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv c)))))

Checked nominal proof certificate identified upstream as g_taddc.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part056.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTlecg (M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec N) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc M) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc N))))

Checked nominal proof certificate identified upstream as g_tlecg.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part057.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLetc (M N : SemanticCore.Class) (p : SemanticCore.Var) (dv_M_p : p ∉ M.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem N Compiler.CompactSourceSyntax.synCncs) (Compiler.CompactSourceSyntax.synWbr M Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCtc N))).imp (Compiler.CompactSourceSyntax.synWrex p Compiler.CompactSourceSyntax.synCncs (SemanticCore.Wff.classEq M (Compiler.CompactSourceSyntax.synCtc (SemanticCore.Class.cv p)))))

Checked nominal proof certificate identified upstream as g_letc.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part058.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTlenc1c (M : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem M Compiler.CompactSourceSyntax.synCncs).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCtc M) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_tlenc1c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1ne0c : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synC0c)

Checked nominal proof certificate identified upstream as g_n_1ne0c.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part059.

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

Checked nominal proof certificate identified upstream as g_tcfnex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part060.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFntcfn : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn Compiler.CompactSourceSyntax.synCtcfn Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_fntcfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrtcfn (A B : SemanticCore.Class) (hyp_brtcfn_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCsn A) Compiler.CompactSourceSyntax.synCtcfn B) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCtc A)))

Checked nominal proof certificate identified upstream as g_brtcfn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcdi (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc (Compiler.CompactSourceSyntax.synCplc B C)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc B) (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc C))))

Checked nominal proof certificate identified upstream as g_addcdi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcdir (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCncs)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCo (Compiler.CompactSourceSyntax.synCplc A B) Compiler.CompactSourceSyntax.synCmuc C) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc C) (Compiler.CompactSourceSyntax.synCo B Compiler.CompactSourceSyntax.synCmuc C))))

Checked nominal proof certificate identified upstream as g_addcdir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLemuc1 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCncs)) (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec B)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc C) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCo B Compiler.CompactSourceSyntax.synCmuc C)))

Checked nominal proof certificate identified upstream as g_lemuc1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gLemuc2 (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCncs) (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCncs)) (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synClec C)).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc B) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCo A Compiler.CompactSourceSyntax.synCmuc C)))

Checked nominal proof certificate identified upstream as g_lemuc2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0lt1c : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synCltc Compiler.CompactSourceSyntax.synC1c)

Checked nominal proof certificate identified upstream as g_n_0lt1c.

Equations

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