NF weak partition development: NominalWPPReplayChunk008.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnineq (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A C) (Compiler.CompactSourceSyntax.synCun B C)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A C) (Compiler.CompactSourceSyntax.synCin B C))) (SemanticCore.Wff.classEq A B))

Checked nominal proof certificate identified upstream as g_unineq.

Equations

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

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

Checked nominal proof certificate identified upstream as g_difundir.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnab (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cab x ph) (SemanticCore.Class.cab x ps)) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWo ph ps)))

Checked nominal proof certificate identified upstream as g_unab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInab (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cab x ph) (SemanticCore.Class.cab x ps)) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWa ph ps)))

Checked nominal proof certificate identified upstream as g_inab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifab (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cab x ph) (SemanticCore.Class.cab x ps)) (SemanticCore.Class.cab x (Compiler.CompactSourceSyntax.synWa ph ps.neg)))

Checked nominal proof certificate identified upstream as g_difab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gComplab (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab x ph)) (SemanticCore.Class.cab x ph.neg))

Checked nominal proof certificate identified upstream as g_complab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotab (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph.neg) (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv (SemanticCore.Class.cab x ph)))

Checked nominal proof certificate identified upstream as g_notab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnrab (ph ps : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCrab x A ph) (Compiler.CompactSourceSyntax.synCrab x A ps)) (Compiler.CompactSourceSyntax.synCrab x A (Compiler.CompactSourceSyntax.synWo ph ps)))

Checked nominal proof certificate identified upstream as g_unrab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfrab2 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x A ph) (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cab x ph) A))

Checked nominal proof certificate identified upstream as g_dfrab2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfrab3 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrab x A ph) (Compiler.CompactSourceSyntax.synCin A (SemanticCore.Class.cab x ph)))

Checked nominal proof certificate identified upstream as g_dfrab3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNotrab (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A (Compiler.CompactSourceSyntax.synCrab x A ph)) (Compiler.CompactSourceSyntax.synCrab x A ph.neg))

Checked nominal proof certificate identified upstream as g_notrab.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gCompleqb (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCcompl B)))

Checked nominal proof certificate identified upstream as g_compleqb.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNecompl (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCcompl A) A)

Checked nominal proof certificate identified upstream as g_necompl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfin5 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCcompl B))))

Checked nominal proof certificate identified upstream as g_dfin5.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfun4 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A B) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCcompl B))))

Checked nominal proof certificate identified upstream as g_dfun4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIunin (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCun A B)) (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCcompl B)))

Checked nominal proof certificate identified upstream as g_iunin.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIinun (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCin A B)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCcompl A) (Compiler.CompactSourceSyntax.synCcompl B)))

Checked nominal proof certificate identified upstream as g_iinun.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifsscompl (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif A B) (Compiler.CompactSourceSyntax.synCcompl B))

Checked nominal proof certificate identified upstream as g_difsscompl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfnul2 (x : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synC0 (SemanticCore.Class.cab x (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (SemanticCore.Class.cv x)).neg))

Checked nominal proof certificate identified upstream as g_dfnul2.

Equations

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

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

Checked nominal proof certificate identified upstream as g_noel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0i (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B A).imp (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0).neg)

Checked nominal proof certificate identified upstream as g_n0i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNe0i (A B : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classMem B A).imp (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ne0i.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVn0 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWne Compiler.CompactSourceSyntax.synCvv Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_vn0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0f (x : SemanticCore.Var) (A : SemanticCore.Class) (hyp_n0f_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWnfc x A)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_n0f.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_n0.

Equations

• NFChoice.DirectNominalPrf.WPPReplay.gN0 x A dv_A_x = NFChoice.DirectNominalPrf.WPPReplay.gN0f x A (NFChoice.DirectNominalPrf.WPPReplay.gNfcv x A ⋯)

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gNeq0 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0).neg (Compiler.CompactSourceSyntax.synWex x (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_neq0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRex0 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWrex x Compiler.CompactSourceSyntax.synC0 ph).neg

Checked nominal proof certificate identified upstream as g_rex0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEq0 (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).neg))

Checked nominal proof certificate identified upstream as g_eq0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEqv (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.all x (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A)))

Checked nominal proof certificate identified upstream as g_eqv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbvor0 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_abvor0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbn0 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWex x ph))

Checked nominal proof certificate identified upstream as g_abn0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAb0 (ph : SemanticCore.Wff) (x : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.all x ph.neg))

Checked nominal proof certificate identified upstream as g_ab0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUn0 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A Compiler.CompactSourceSyntax.synC0) A)

Checked nominal proof certificate identified upstream as g_un0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIn0 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A Compiler.CompactSourceSyntax.synC0) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_in0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInv1 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A Compiler.CompactSourceSyntax.synCvv) A)

Checked nominal proof certificate identified upstream as g_inv1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gN0ss (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synC0 A)

Checked nominal proof certificate identified upstream as g_n_0ss.

Equations

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

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

Checked nominal proof certificate identified upstream as g_ss0b.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSs0 (A : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWss A Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ss0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gAbf (ph : SemanticCore.Wff) (x : SemanticCore.Var) (hyp_abf_1 : Nominal.NPrf ph.neg) : Nominal.NPrf (SemanticCore.Wff.classEq (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_abf.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gEq0rdv (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_ph_x : x ∉ ph.fv) (hyp_eq0rdv_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).neg)) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_eq0rdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUn00 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.classEq B Compiler.CompactSourceSyntax.synC0)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A B) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_un00.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gVss (A : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss Compiler.CompactSourceSyntax.synCvv A) (SemanticCore.Wff.classEq A Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_vss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDisj (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWral x A (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).neg))

Checked nominal proof certificate identified upstream as g_disj.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDisjr (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWral x B (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).neg))

Checked nominal proof certificate identified upstream as g_disjr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDisj1 (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A B) Compiler.CompactSourceSyntax.synC0) (SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).neg)))

Checked nominal proof certificate identified upstream as g_disj1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsdif0 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A B) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_ssdif0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInssdif0 (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCin A B) C) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCdif B C)) Compiler.CompactSourceSyntax.synC0))

Checked nominal proof certificate identified upstream as g_inssdif0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifid (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A A) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_difid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDif0 (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif A Compiler.CompactSourceSyntax.synC0) A)

Checked nominal proof certificate identified upstream as g_dif0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDisjdif (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin A (Compiler.CompactSourceSyntax.synCdif B A)) Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_disjdif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUndifv (A : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCdif Compiler.CompactSourceSyntax.synCvv A)) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_undifv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUndif1 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCdif A B) B) (Compiler.CompactSourceSyntax.synCun A B))

Checked nominal proof certificate identified upstream as g_undif1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUndif2 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCdif B A)) (Compiler.CompactSourceSyntax.synCun A B))

Checked nominal proof certificate identified upstream as g_undif2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gInundif (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin A B) (Compiler.CompactSourceSyntax.synCdif A B)) A)

Checked nominal proof certificate identified upstream as g_inundif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDifun2 (A B : SemanticCore.Class) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdif (Compiler.CompactSourceSyntax.synCun A B) B) (Compiler.CompactSourceSyntax.synCdif A B))

Checked nominal proof certificate identified upstream as g_difun2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUndif (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCun A (Compiler.CompactSourceSyntax.synCdif B A)) B))

Checked nominal proof certificate identified upstream as g_undif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSsundif (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A (Compiler.CompactSourceSyntax.synCun B C)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif A B) C))

Checked nominal proof certificate identified upstream as g_ssundif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gR192z (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWne A Compiler.CompactSourceSyntax.synC0) (Compiler.CompactSourceSyntax.synWral x A ph)).imp (Compiler.CompactSourceSyntax.synWrex x A ph))

Checked nominal proof certificate identified upstream as g_r19_2z.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSscon34 (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWss A B) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCcompl B) (Compiler.CompactSourceSyntax.synCcompl A)))

Checked nominal proof certificate identified upstream as g_sscon34.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfif2 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) (SemanticCore.Class.cab x (((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B).imp ph).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) ph))))

Checked nominal proof certificate identified upstream as g_dfif2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDfif6 (ph : SemanticCore.Wff) (x : SemanticCore.Var) (A B : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_B_x : x ∉ B.fv) (dv_ph_x : x ∉ ph.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCrab x A ph) (Compiler.CompactSourceSyntax.synCrab x B ph.neg)))

Checked nominal proof certificate identified upstream as g_dfif6.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfeq1 (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A C) (Compiler.CompactSourceSyntax.synCif ph B C)))

Checked nominal proof certificate identified upstream as g_ifeq1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfeq2 (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) : Nominal.NPrf ((SemanticCore.Wff.classEq A B).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph C A) (Compiler.CompactSourceSyntax.synCif ph C B)))

Checked nominal proof certificate identified upstream as g_ifeq2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIftrue (ph : SemanticCore.Wff) (A B : SemanticCore.Class) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) A))

Checked nominal proof certificate identified upstream as g_iftrue.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIffalse (ph : SemanticCore.Wff) (A B : SemanticCore.Class) : Nominal.NPrf (ph.neg.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) B))

Checked nominal proof certificate identified upstream as g_iffalse.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfeq1d (ph ps : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_ifeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ps A C) (Compiler.CompactSourceSyntax.synCif ps B C)))

Checked nominal proof certificate identified upstream as g_ifeq1d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfeq2d (ph ps : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_ifeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ps C A) (Compiler.CompactSourceSyntax.synCif ps C B)))

Checked nominal proof certificate identified upstream as g_ifeq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfeq12d (ph ps : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_ifeq1d_1 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) (hyp_ifeq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq C D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ps A C) (Compiler.CompactSourceSyntax.synCif ps B D)))

Checked nominal proof certificate identified upstream as g_ifeq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfbi (ph ps : SemanticCore.Wff) (A B : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWb ph ps).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) (Compiler.CompactSourceSyntax.synCif ps A B)))

Checked nominal proof certificate identified upstream as g_ifbi.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfbid (ph ps ch : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_ifbid_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ps A B) (Compiler.CompactSourceSyntax.synCif ch A B)))

Checked nominal proof certificate identified upstream as g_ifbid.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfbieq2d (ph ps ch : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_ifbieq2d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_ifbieq2d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A B))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ps C A) (Compiler.CompactSourceSyntax.synCif ch C B)))

Checked nominal proof certificate identified upstream as g_ifbieq2d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfbieq12d (ph ps ch : SemanticCore.Wff) (A B C D : SemanticCore.Class) (hyp_ifbieq12d_1 : Nominal.NPrf (ph.imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_ifbieq12d_2 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq A C))) (hyp_ifbieq12d_3 : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq B D))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ps A B) (Compiler.CompactSourceSyntax.synCif ch C D)))

Checked nominal proof certificate identified upstream as g_ifbieq12d.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfclda (ph ps : SemanticCore.Wff) (A B C : SemanticCore.Class) (hyp_ifclda_1 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps).imp (SemanticCore.Wff.classMem A C))) (hyp_ifclda_2 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ph ps.neg).imp (SemanticCore.Wff.classMem B C))) : Nominal.NPrf (ph.imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCif ps A B) C))

Checked nominal proof certificate identified upstream as g_ifclda.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElimif (ph ps ch th : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_elimif_1 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) A).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_elimif_2 : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) B).imp (Compiler.CompactSourceSyntax.synWb ps th))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb ps (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWa ph ch) (Compiler.CompactSourceSyntax.synWa ph.neg th)))

Checked nominal proof certificate identified upstream as g_elimif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfbothda (ph ps ch th et : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_ifboth_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A B)).imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_ifboth_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph A B)).imp (Compiler.CompactSourceSyntax.synWb ch th))) (hyp_ifbothda_3 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa et ph).imp ps)) (hyp_ifbothda_4 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa et ph.neg).imp ch)) : Nominal.NPrf (et.imp th)

Checked nominal proof certificate identified upstream as g_ifbothda.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfboth (ph ps ch th : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_ifboth_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A B)).imp (Compiler.CompactSourceSyntax.synWb ps th))) (hyp_ifboth_2 : Nominal.NPrf ((SemanticCore.Wff.classEq B (Compiler.CompactSourceSyntax.synCif ph A B)).imp (Compiler.CompactSourceSyntax.synWb ch th))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa ps ch).imp th)

Checked nominal proof certificate identified upstream as g_ifboth.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElif (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCif ph B C)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWa ph (SemanticCore.Wff.classMem A B)) (Compiler.CompactSourceSyntax.synWa ph.neg (SemanticCore.Wff.classMem A C))))

Checked nominal proof certificate identified upstream as g_elif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfcl (ph : SemanticCore.Wff) (A B C : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem A C) (SemanticCore.Wff.classMem B C)).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCif ph A B) C))

Checked nominal proof certificate identified upstream as g_ifcl.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gIfeqor (ph : SemanticCore.Wff) (A B : SemanticCore.Class) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) A) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCif ph A B) B))

Checked nominal proof certificate identified upstream as g_ifeqor.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gDedth (ph ps ch : SemanticCore.Wff) (A B : SemanticCore.Class) (hyp_dedth_1 : Nominal.NPrf ((SemanticCore.Wff.classEq A (Compiler.CompactSourceSyntax.synCif ph A B)).imp (Compiler.CompactSourceSyntax.synWb ps ch))) (hyp_dedth_2 : Nominal.NPrf ch) : Nominal.NPrf (ph.imp ps)

Checked nominal proof certificate identified upstream as g_dedth.

Equations

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