Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk014Compact001Part014.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstrictcomplement (A R : SemanticCore.Class) (e c : SemanticCore.Var) (_dv_A_R : Disjoint A.fv R.fv) (_dv_A_c : c ∉ A.fv) (_dv_A_e : e ∉ A.fv) (_dv_R_c : c ∉ R.fv) (_dv_R_e : e ∉ R.fv) (_dv_c_e : c ≠ e) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv c) A)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv e)).neg (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv e) R (SemanticCore.Class.cv c))))

Checked nominal proof certificate identified upstream as g_wppstrictcomplement.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppstrictleastbridge (ph : SemanticCore.Wff) (A R : SemanticCore.Class) (e c : SemanticCore.Var) (dv_A_R : Disjoint A.fv R.fv) (dv_A_c : c ∉ A.fv) (dv_A_e : e ∉ A.fv) (dv_R_c : c ∉ R.fv) (dv_R_e : e ∉ R.fv) (dv_c_e : c ≠ e) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A)).imp (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWral c A ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid) (SemanticCore.Class.cv e)).imp ph.neg)) (Compiler.CompactSourceSyntax.synWral c A (ph.imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv e) R (SemanticCore.Class.cv c))))))

Checked nominal proof certificate identified upstream as g_wppstrictleastbridge.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminsepfpivred (A B C D R : 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_R : Disjoint A.fv R.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_e : e ∉ B.fv) (dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_C_e : e ∉ C.fv) (dv_D_R : Disjoint D.fv R.fv) (dv_D_e : e ∉ D.fv) (dv_R_e : e ∉ R.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (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)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCfpiv R A C D))))

Checked nominal proof certificate identified upstream as g_fdminsepfpivred.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfdminvalp (A B C R : SemanticCore.Class) (d : 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_d : d ∉ A.fv) (dv_B_C : Disjoint B.fv C.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_B_d : d ∉ B.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_C_d : d ∉ C.fv) (dv_R_d : d ∉ R.fv) (hyp_elfdminvalp_1 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) (Compiler.CompactSourceSyntax.synCfdminvalp R A B C)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv d) A) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv d)) C) (Compiler.CompactSourceSyntax.synCfdminsep R A B))))

Checked nominal proof certificate identified upstream as g_elfdminvalp.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part015.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminvalpfpivred (A B C D R : SemanticCore.Class) (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_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_D_R : Disjoint D.fv R.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C B) (SemanticCore.Wff.classMem D B))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdminvalp R A B (Compiler.CompactSourceSyntax.synCopk C D)) (Compiler.CompactSourceSyntax.synCfpiv R A C D)))

Checked nominal proof certificate identified upstream as g_fdminvalpfpivred.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdminvalpeq4 (A B C D R : SemanticCore.Class) (_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_B_C : Disjoint B.fv C.fv) (_dv_B_D : Disjoint B.fv D.fv) (_dv_B_R : Disjoint B.fv R.fv) (_dv_C_D : Disjoint C.fv D.fv) (_dv_C_R : Disjoint C.fv R.fv) (_dv_D_R : Disjoint D.fv R.fv) : Nominal.NPrf ((SemanticCore.Wff.classEq C D).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdminvalp R A B C) (Compiler.CompactSourceSyntax.synCfdminvalp R A B D)))

Checked nominal proof certificate identified upstream as g_fdminvalpeq4.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdpivinrange (A B C D R : SemanticCore.Class) (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_B_C : Disjoint B.fv C.fv) (dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_D_R : Disjoint D.fv R.fv) (hyp_fdpivinrange_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivinrange_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdpivinrange_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C B) (SemanticCore.Wff.classMem D B))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfpiv R A C D) (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B)))

Checked nominal proof certificate identified upstream as g_fdpivinrange.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfdif (x y : SemanticCore.Var) (A B R : SemanticCore.Class) (e : SemanticCore.Var) (dv_A_B : Disjoint A.fv B.fv) (dv_A_R : Disjoint A.fv R.fv) (_dv_A_e : e ∉ A.fv) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_B_R : Disjoint B.fv R.fv) (_dv_B_e : e ∉ B.fv) (dv_B_x : x ∉ B.fv) (dv_B_y : y ∉ B.fv) (_dv_R_e : e ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_e_x : e ≠ x) (dv_e_y : e ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCfdif R A B)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) A) (Compiler.CompactSourceSyntax.synWrex x B (Compiler.CompactSourceSyntax.synWrex y B (SemanticCore.Wff.classMem (SemanticCore.Class.cv e) (Compiler.CompactSourceSyntax.synCfpiv R A (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_elfdif.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdifssunirange2x (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_fdifssunirange2x_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdifssunirange2x_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdifssunirange2x_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfdif R A B) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B))))

Checked nominal proof certificate identified upstream as g_fdifssunirange2x.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part017.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gUnirange2ssfdifx (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_unirange2ssfdifx_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_unirange2ssfdifx_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_unirange2ssfdifx_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B)) (Compiler.CompactSourceSyntax.synCfdif R A B)))

Checked nominal proof certificate identified upstream as g_unirange2ssfdifx.

Equations

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

Certificates from NominalWPPReplayChunk014Compact001Part018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdifequnirange2x (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_fdifequnirange2x_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdifequnirange2x_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdifequnirange2x_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdif R A B) (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCfdpivrange2 R A B))))

Checked nominal proof certificate identified upstream as g_fdifequnirange2x.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdifex2 (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_fdifex2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdifex2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdifex2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdif R A B) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fdifex2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdrowss (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) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfdrow R A B C) (Compiler.CompactSourceSyntax.synCfdif R A B))

Checked nominal proof certificate identified upstream as g_fdrowss.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfdrowg (A B C D R : SemanticCore.Class) (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_B_C : Disjoint B.fv C.fv) (_dv_B_D : Disjoint B.fv D.fv) (dv_B_R : Disjoint B.fv R.fv) (_dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (_dv_D_R : Disjoint D.fv R.fv) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfdrow R A B C)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfdif R A B)) (SemanticCore.Wff.classMem C D)))

Checked nominal proof certificate identified upstream as g_elfdrowg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdrowex2 (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_fdrowex2_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_fdrowex2_2 : Nominal.NPrf (SemanticCore.Wff.classMem A Compiler.CompactSourceSyntax.synCvv)) (hyp_fdrowex2_3 : Nominal.NPrf (SemanticCore.Wff.classMem B Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe A).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCfdrow R A B C) Compiler.CompactSourceSyntax.synCvv))

Checked nominal proof certificate identified upstream as g_fdrowex2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gElfdcodeg (x : SemanticCore.Var) (A B C D R : SemanticCore.Class) (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_x : x ∉ 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_x : x ∉ B.fv) (_dv_C_D : Disjoint C.fv D.fv) (dv_C_R : Disjoint C.fv R.fv) (dv_C_x : x ∉ C.fv) (_dv_D_R : Disjoint D.fv R.fv) (dv_D_x : x ∉ D.fv) (dv_R_x : x ∉ R.fv) : Nominal.NPrf ((SemanticCore.Wff.classMem D Compiler.CompactSourceSyntax.synCvv).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem D (Compiler.CompactSourceSyntax.synCfdcode R A B C)) (Compiler.CompactSourceSyntax.synWrex x C (SemanticCore.Wff.classEq D (Compiler.CompactSourceSyntax.synCfdrow R A B (SemanticCore.Class.cv x))))))

Checked nominal proof certificate identified upstream as g_elfdcodeg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gFdcodesspw2 (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) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCfdcode R A B C) (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCfdif R A B)))

Checked nominal proof certificate identified upstream as g_fdcodesspw2.

Equations

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