Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk009StructuralPart025.

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

Checked nominal proof certificate identified upstream as g_nncex.

Equations

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

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

Checked nominal proof certificate identified upstream as g_finex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEladdc (A M N : SemanticCore.Class) (b c : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_c : c ∉ A.fv) (dv_M_b : b ∉ M.fv) (dv_M_c : c ∉ M.fv) (dv_N_b : b ∉ N.fv) (dv_N_c : c ∉ N.fv) (dv_b_c : b ≠ c) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCplc M N)) (Compiler.CompactSourceSyntax.synWrex b M (Compiler.CompactSourceSyntax.synWrex c N (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv b) (SemanticCore.Class.cv c)) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv b) (SemanticCore.Class.cv c)))))))

Checked nominal proof certificate identified upstream as g_eladdc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEladdci (A B M N : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A M) (SemanticCore.Wff.classMem B N) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun A B) (Compiler.CompactSourceSyntax.synCplc M N)))

Checked nominal proof certificate identified upstream as g_eladdci.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0nelsuc (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c)).neg

Checked nominal proof certificate identified upstream as g_n_0nelsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0cnsuc (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC0c)

Checked nominal proof certificate identified upstream as g_n_0cnsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPeano1 : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_peano1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPeano2 (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_peano2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPeano3 (A : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC1c) Compiler.CompactSourceSyntax.synC0c))

Checked nominal proof certificate identified upstream as g_peano3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcid1 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A Compiler.CompactSourceSyntax.synC0c) A)

Checked nominal proof certificate identified upstream as g_addcid1.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart026.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddccom (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc A B) (Compiler.CompactSourceSyntax.synCplc B A))

Checked nominal proof certificate identified upstream as g_addccom.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcid2 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc Compiler.CompactSourceSyntax.synC0c A) A)

Checked nominal proof certificate identified upstream as g_addcid2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN1cnnc : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC1c Compiler.CompactSourceSyntax.synCnnc)

Checked nominal proof certificate identified upstream as g_n_1cnnc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gPeano5 (x : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem A V) (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0c A) (Compiler.CompactSourceSyntax.synWral x Compiler.CompactSourceSyntax.synCnnc ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c) A)))).imp (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCnnc A))

Checked nominal proof certificate identified upstream as g_peano5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFindsd (ph ps ch th ta et : SemanticCore.Wff) (x y : SemanticCore.Var) (A V : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_et_y : y ∉ et.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_ta_x : x ∉ ta.fv) (dv_th_x : x ∉ th.fv) (dv_x_y : x ≠ y) (hyp_findsd_1 : Nominal.NPrf (et.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cab x ph) V))) (hyp_findsd_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC0c).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_findsd_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_findsd_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC1c)).imp (Compiler.CompactSourceSyntax.synWb ph th))) (hyp_findsd_5 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ta))) (hyp_findsd_6 : Nominal.NPrf (et.imp ps)) (hyp_findsd_7 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCnnc) et).imp (ch.imp th))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) et).imp ta)

Checked nominal proof certificate identified upstream as g_findsd.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFinds (ph ps ch th ta : SemanticCore.Wff) (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_y : y ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_ta_x : x ∉ ta.fv) (dv_th_x : x ∉ th.fv) (dv_x_y : x ≠ y) (hyp_finds_1 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synCvv)) (hyp_finds_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC0c).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_finds_3 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_finds_4 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synC1c)).imp (Compiler.CompactSourceSyntax.synWb ph th))) (hyp_finds_5 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph ta))) (hyp_finds_6 : Nominal.NPrf ps) (hyp_finds_7 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCnnc).imp (ch.imp th))) : Nominal.NPrf ((SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc).imp ta)

Checked nominal proof certificate identified upstream as g_finds.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart027.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNnc0suc (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0c) (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synC1c)))))

Checked nominal proof certificate identified upstream as g_nnc0suc.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart028.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElsuc (x : SemanticCore.Var) (A M : SemanticCore.Class) (b : SemanticCore.Var) (dv_A_b : b ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_M_b : b ∉ M.fv) (dv_b_x : b ≠ x) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCplc M Compiler.CompactSourceSyntax.synC1c)) (Compiler.CompactSourceSyntax.synWrex b M (Compiler.CompactSourceSyntax.synWrex x (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv b)) (SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))))

Checked nominal proof certificate identified upstream as g_elsuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElsuci (A N X : SemanticCore.Class) (hyp_elsuci_1 : Nominal.NPrf (SemanticCore.Wff.classMem X Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A N) (SemanticCore.Wff.classMem X A).neg).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCsn X)) (Compiler.CompactSourceSyntax.synCplc N Compiler.CompactSourceSyntax.synC1c)))

Checked nominal proof certificate identified upstream as g_elsuci.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart029.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddcass (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A B) C) (Compiler.CompactSourceSyntax.synCplc A (Compiler.CompactSourceSyntax.synCplc B C)))

Checked nominal proof certificate identified upstream as g_addcass.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart030.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddc32 (A B C : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A B) C) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A C) B))

Checked nominal proof certificate identified upstream as g_addc32.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddc4 (A B C D : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A B) (Compiler.CompactSourceSyntax.synCplc C D)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A C) (Compiler.CompactSourceSyntax.synCplc B D)))

Checked nominal proof certificate identified upstream as g_addc4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAddc6 (A B C D E F : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A B) (Compiler.CompactSourceSyntax.synCplc C D)) (Compiler.CompactSourceSyntax.synCplc E F)) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc A C) E) (Compiler.CompactSourceSyntax.synCplc (Compiler.CompactSourceSyntax.synCplc B D) F)))

Checked nominal proof certificate identified upstream as g_addc6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNncaddccl (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCnnc) (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCnnc)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCplc A B) Compiler.CompactSourceSyntax.synCnnc))

Checked nominal proof certificate identified upstream as g_nncaddccl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfin (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCfin) (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synCnnc (SemanticCore.Wff.classMem A (SemanticCore.Class.cv x))))

Checked nominal proof certificate identified upstream as g_elfin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEl0c (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synC0c) (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_el0c.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNulel0c : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0c)

Checked nominal proof certificate identified upstream as g_nulel0c.

Equations

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

Certificates from NominalWPPReplayChunk009StructuralPart031.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0fin : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synCfin)

Checked nominal proof certificate identified upstream as g_n_0fin.

Equations

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