Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdprj1valV (x : SemanticCore.Var) (C D : SemanticCore.Class) (_dv_C_D : Disjoint C.fv D.fv) (_dv_C_x : x ∉ C.fv) (_dv_D_x : x ∉ D.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCopk C D)) Compiler.CompactSourceSyntax.synCfdprj1) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCsn D)))))

Checked nominal proof certificate identified upstream as g_fdprj1valV.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFde1valJp (A B C D : SemanticCore.Class) (e : SemanticCore.Var) (_dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (_dv_A_D : Disjoint A.fv D.fv) (_dv_A_e : e ∉ A.fv) (_dv_B_C : Disjoint B.fv C.fv) (_dv_B_D : Disjoint B.fv D.fv) (_dv_B_e : e ∉ B.fv) (dv_C_D : Disjoint C.fv D.fv) (_dv_C_e : e ∉ C.fv) (_dv_D_e : e ∉ D.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C B) (SemanticCore.Wff.classMem D B)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCopk C D)) (Compiler.CompactSourceSyntax.synCfde1 A B)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A) (SemanticCore.Wff.classMem D (SemanticCore.Class.cv e)))))

Checked nominal proof certificate identified upstream as g_fde1valJp.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gSep2valJp (C D : SemanticCore.Class) (e : SemanticCore.Var) (dv_C_D : Disjoint C.fv D.fv) (_dv_C_e : e ∉ C.fv) (_dv_D_e : e ∉ D.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCsep2 C D)) (Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C (SemanticCore.Class.cv e)) (SemanticCore.Wff.classMem D (SemanticCore.Class.cv e)).neg) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem D (SemanticCore.Class.cv e)) (SemanticCore.Wff.classMem C (SemanticCore.Class.cv e)).neg)))

Checked nominal proof certificate identified upstream as g_sep2valJp.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part011.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdsepvalJ (A B C D : SemanticCore.Class) (e : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_D : Disjoint A.fv D.fv) (dv_A_e : e ∉ A.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_e : e ∉ B.fv) (dv_C_D : Disjoint C.fv D.fv) (dv_C_e : e ∉ C.fv) (dv_D_e : e ∉ D.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C B) (SemanticCore.Wff.classMem D B)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCopk C D)) (Compiler.CompactSourceSyntax.synCfdsep A B)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCsep2 C D)))))

Checked nominal proof certificate identified upstream as g_fdsepvalJ.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gStrictbr (R : SemanticCore.Class) (e c : SemanticCore.Var) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) R (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synWne (SemanticCore.Class.cv c) (SemanticCore.Class.cv e))))

Checked nominal proof certificate identified upstream as g_strictbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdnonminval0J (A B C D R : SemanticCore.Class) (e c : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_D : Disjoint A.fv D.fv) (_dv_A_R : Disjoint A.fv R.fv) (dv_A_c : c ∉ A.fv) (_dv_A_e : e ∉ A.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (_dv_B_R : Disjoint B.fv R.fv) (dv_B_c : c ∉ B.fv) (_dv_B_e : e ∉ B.fv) (dv_C_D : Disjoint C.fv D.fv) (_dv_C_R : Disjoint C.fv R.fv) (dv_C_c : c ∉ C.fv) (_dv_C_e : e ∉ C.fv) (_dv_D_R : Disjoint D.fv R.fv) (dv_D_c : c ∉ D.fv) (_dv_D_e : e ∉ D.fv) (dv_R_c : c ∉ R.fv) (dv_R_e : e ∉ R.fv) (dv_c_e : c ≠ e) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C B) (SemanticCore.Wff.classMem D B)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCopk C D)) (Compiler.CompactSourceSyntax.synCfdnonmin R A B)) (Compiler.CompactSourceSyntax.synWrex c A (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv e)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCsep2 C D))))))

Checked nominal proof certificate identified upstream as g_fdnonminval0J.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqrelex (A : SemanticCore.Class) (hyp_kqrelex_1 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCkqrel A) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_kqrelex.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part012.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gKqrelbr (A B C : SemanticCore.Class) (_dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (_dv_B_C : Disjoint B.fv C.fv) (hyp_kqrelbr_1 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) (hyp_kqrelbr_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop B C) (Compiler.CompactSourceSyntax.synCkqrel A)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk B C) A))

Checked nominal proof certificate identified upstream as g_kqrelbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminvalpex (A B C R : SemanticCore.Class) (_dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (_dv_A_R : Disjoint A.fv R.fv) (_dv_B_C : Disjoint B.fv C.fv) (_dv_B_R : Disjoint B.fv R.fv) (_dv_C_R : Disjoint C.fv R.fv) (hyp_fdminvalpex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdminvalpex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdminvalpex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdminvalp R A B C) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdminvalpex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminvalpbr (z : SemanticCore.Var) (A B C R : SemanticCore.Class) (_dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (_dv_A_R : Disjoint A.fv R.fv) (_dv_A_z : z ∉ A.fv) (_dv_B_C : Disjoint B.fv C.fv) (_dv_B_R : Disjoint B.fv R.fv) (_dv_B_z : z ∉ B.fv) (_dv_C_R : Disjoint C.fv R.fv) (_dv_C_z : z ∉ C.fv) (_dv_R_z : z ∉ R.fv) (hyp_fdminvalpbr_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCfdminvalp R A B C)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv z)) C) (Compiler.CompactSourceSyntax.synCfdminsep R A B)))

Checked nominal proof certificate identified upstream as g_fdminvalpbr.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminqex (A B R : SemanticCore.Class) (hyp_fdminqex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdminqex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdminqex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdminq R A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdminqex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpivmap2ex (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdpivmap2ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdpivmap2 R A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdpivmap2ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpivmap2fn (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdpivmap2ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfn (Compiler.CompactSourceSyntax.synCfdpivmap2 R A B) (Compiler.CompactSourceSyntax.synCxpk B B))

Checked nominal proof certificate identified upstream as g_fdpivmap2fn.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpivrange2ex (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdpivmap2ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B) Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_fdpivrange2ex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpivmap2onto (A B R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_R : Disjoint B.fv R.fv) (hyp_fdpivmap2ex_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2ex_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWfo (Compiler.CompactSourceSyntax.synCfdpivmap2 R A B) (Compiler.CompactSourceSyntax.synCxpk B B) (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B))

Checked nominal proof certificate identified upstream as g_fdpivmap2onto.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part013.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpivmap2val (A B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_p : p ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_p : p ∉ B.fv) (dv_R_p : p ∉ R.fv) (hyp_fdpivmap2val_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2val_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivmap2val_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv p) (Compiler.CompactSourceSyntax.synCxpk B B)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfv (Compiler.CompactSourceSyntax.synCfdpivmap2 R A B) (SemanticCore.Class.cv p)) (Compiler.CompactSourceSyntax.synCfdminvalp R A B (SemanticCore.Class.cv p))))

Checked nominal proof certificate identified upstream as g_fdpivmap2val.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpivrange2br (A B C R : SemanticCore.Class) (p : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (_dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_p : p ∉ A.fv) (_dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_p : p ∉ B.fv) (_dv_C_R : Disjoint C.fv R.fv) (dv_C_p : p ∉ C.fv) (dv_R_p : p ∉ R.fv) (hyp_fdpivrange2br_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivrange2br_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivrange2br_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B)) (Compiler.CompactSourceSyntax.synWrex p (Compiler.CompactSourceSyntax.synCxpk B B) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdminvalp R A B (SemanticCore.Class.cv p)) C)))

Checked nominal proof certificate identified upstream as g_fdpivrange2br.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminvalpss (A B C R : SemanticCore.Class) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_R : Disjoint C.fv R.fv) (hyp_fdminvalpss_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfdminvalp R A B C) A)

Checked nominal proof certificate identified upstream as g_fdminvalpss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfpiv (A B C R : SemanticCore.Class) (e c : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_c : c ∉ A.fv) (_dv_A_e : e ∉ A.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_c : c ∉ B.fv) (_dv_B_e : e ∉ B.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_C_c : c ∉ C.fv) (_dv_C_e : e ∉ C.fv) (dv_R_c : c ∉ R.fv) (_dv_R_e : e ∉ R.fv) (dv_c_e : c ≠ e) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCfpiv R A B C)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCsep2 B C))) (Compiler.CompactSourceSyntax.synWral c A ((SemanticCore.Wff.classMem (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCsep2 B C)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv e) R (SemanticCore.Class.cv c))))))

Checked nominal proof certificate identified upstream as g_elfpiv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminsepval0J (A B C D R : SemanticCore.Class) (e c : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_C : Disjoint A.fv C.fv) (dv_A_D : Disjoint A.fv D.fv) (dv_A_R : Disjoint A.fv R.fv) (dv_A_c : c ∉ A.fv) (dv_A_e : e ∉ A.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_c : c ∉ B.fv) (dv_B_e : e ∉ B.fv) (dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_C_c : c ∉ C.fv) (dv_C_e : e ∉ C.fv) (dv_D_R : Disjoint D.fv R.fv) (dv_D_c : c ∉ D.fv) (dv_D_e : e ∉ D.fv) (dv_R_c : c ∉ R.fv) (dv_R_e : e ∉ R.fv) (dv_c_e : c ≠ e) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C B) (SemanticCore.Wff.classMem D B)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv e)) (Compiler.CompactSourceSyntax.synCopk C D)) (Compiler.CompactSourceSyntax.synCfdminsep R A B)) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCsep2 C D))) (Compiler.CompactSourceSyntax.synWrex c A (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv e)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCsep2 C D)))).neg)))

Checked nominal proof certificate identified upstream as g_fdminsepval0J.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppwepo (A R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCpartial A))

Checked nominal proof certificate identified upstream as g_wppwepo.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppweref (A R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCref A))

Checked nominal proof certificate identified upstream as g_wppweref.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppweconnex (A R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCconnex A))

Checked nominal proof certificate identified upstream as g_wppweconnex.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppweantisym (A R : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCantisym A))

Checked nominal proof certificate identified upstream as g_wppweantisym.

Equations

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