Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk012BCompact001Part020.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTrtxp (A B C R S : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCtxp R S) (Compiler.CompactSourceSyntax.synCop B C)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr A R B) (Compiler.CompactSourceSyntax.synWbr A S C)))

Checked nominal proof certificate identified upstream as g_trtxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOteltxp (A B C R S : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCop B C)) (Compiler.CompactSourceSyntax.synCtxp R S)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) R) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A C) S)))

Checked nominal proof certificate identified upstream as g_oteltxp.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part021.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrtxp (x y : SemanticCore.Var) (A B R S : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCtxp R S) B) (Compiler.CompactSourceSyntax.synWex x (Compiler.CompactSourceSyntax.synWex y (Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))) (Compiler.CompactSourceSyntax.synWbr A R (SemanticCore.Class.cv x)) (Compiler.CompactSourceSyntax.synWbr A S (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_brtxp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTxpexg (A B V W : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem B W)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtxp A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_txpexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTxpex (A B : SemanticCore.Class) (hyp_txpex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_txpex_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCtxp A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_txpex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfix (A R : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCfix R)) (Compiler.CompactSourceSyntax.synWbr A R A))

Checked nominal proof certificate identified upstream as g_elfix.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFixexg (R V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem R V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfix R) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fixexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFixex (R : SemanticCore.Class) (hyp_fixex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfix R) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fixex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOp1st2nd (A B C : SemanticCore.Class) (hyp_op1st2nd_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_op1st2nd_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synC1st A) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synC2nd B)) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCop A B)))

Checked nominal proof certificate identified upstream as g_op1st2nd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOtelins2 (A B C R : SemanticCore.Class) (hyp_otelins2_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCop B C)) (Compiler.CompactSourceSyntax.synCins2 R)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A C) R))

Checked nominal proof certificate identified upstream as g_otelins2.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part022.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOtelins3 (A B C R : SemanticCore.Class) (hyp_otelins3_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCop B C)) (Compiler.CompactSourceSyntax.synCins3 R)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A B) R))

Checked nominal proof certificate identified upstream as g_otelins3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gBrimage (A B R : SemanticCore.Class) (hyp_brimage_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_brimage_2 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr A (Compiler.CompactSourceSyntax.synCimage R) B) (SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCima R A)))

Checked nominal proof certificate identified upstream as g_brimage.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part023.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gOqelins4 (A B C D R : SemanticCore.Class) (hyp_oqelins4_4 : Nominal.NPrf (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCop B (Compiler.CompactSourceSyntax.synCop C D))) (Compiler.CompactSourceSyntax.synCins4 R)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop A (Compiler.CompactSourceSyntax.synCop B C)) R))

Checked nominal proof certificate identified upstream as g_oqelins4.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part024.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns2exg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCins2 A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_ins2exg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns3exg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCins3 A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_ins3exg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns2ex (A : SemanticCore.Class) (hyp_insex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCins2 A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ins2ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns3ex (A : SemanticCore.Class) (hyp_insex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCins3 A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ins3ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIns4ex (A : SemanticCore.Class) (hyp_insex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCins4 A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_ins4ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImageexg (A V : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A V).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCimage A) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_imageexg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gImageex (A : SemanticCore.Class) (hyp_imageex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCimage A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_imageex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDmtxp (R S : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCtxp R S)) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCdm R) (Compiler.CompactSourceSyntax.synCdm S)))

Checked nominal proof certificate identified upstream as g_dmtxp.

Equations

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

Certificates from NominalWPPReplayChunk012BCompact001Part025.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFntxp (A B F G : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWfn F A) (Compiler.CompactSourceSyntax.synWfn G B)).imp (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCtxp F G) (Compiler.CompactSourceSyntax.synCin A B)))

Checked nominal proof certificate identified upstream as g_fntxp.

Equations

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