Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part038.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisoncutreplttargetdfdv (x : SemanticCore.Var) (D R S E : SemanticCore.Class) (dv_D_x : x ∉ D.fv) (dv_E_x : x ∉ E.fv) (dv_R_x : x ∉ R.fv) (dv_S_x : x ∉ S.fv) (hyp_wecomparisoncutreplttargetdfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc E) Compiler.CompactSourceSyntax.synCltc (Compiler.CompactSourceSyntax.synCnc D))).imp (Compiler.CompactSourceSyntax.synWrex x D (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc E) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))))

Checked nominal proof certificate identified upstream as g_wecomparisoncutreplttargetdfdv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part039.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisoncutreptypedliftdndv (x : SemanticCore.Var) (D R E : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_q : q ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_R_q : q ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_q_x : q ≠ x) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x D (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc E) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))).imp (Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc E) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))))))

Checked nominal proof certificate identified upstream as g_wecomparisoncutreptypedliftdndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisoncutreptypedtargetdfdv (D R S E : SemanticCore.Class) (q : SemanticCore.Var) (dv_D_q : q ∉ D.fv) (dv_E_q : q ∉ E.fv) (dv_R_q : q ∉ R.fv) (hyp_wecomparisoncutreptypedtargetdfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E) (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc E) Compiler.CompactSourceSyntax.synCltc (Compiler.CompactSourceSyntax.synCnc D))).imp (Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc E) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))))))

Checked nominal proof certificate identified upstream as g_wecomparisoncutreptypedtargetdfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandstrictslicecutrepfixdrfdv (C D R : SemanticCore.Class) (k : SemanticCore.Var) (F : SemanticCore.Class) (q : SemanticCore.Var) (_dv_C_k : k ∉ C.fv) (dv_C_q : q ∉ C.fv) (_dv_D_k : k ∉ D.fv) (dv_D_q : q ∉ D.fv) (_dv_F_k : k ∉ F.fv) (dv_F_q : q ∉ F.fv) (_dv_R_k : k ∉ R.fv) (dv_R_q : q ∉ R.fv) (dv_k_q : k ≠ q) (hyp_wppcandstrictslicecutrepfixdrfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wppcandstrictslicecutrepfixdrfdv_2 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCnc D))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))))))

Checked nominal proof certificate identified upstream as g_wppcandstrictslicecutrepfixdrfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandstrictslicenonemptyminndv (z : SemanticCore.Var) (C D R : SemanticCore.Class) (k n : SemanticCore.Var) (F : SemanticCore.Class) (q : SemanticCore.Var) (dv_C_k : k ∉ C.fv) (dv_C_n : n ∉ C.fv) (dv_C_q : q ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_D_k : k ∉ D.fv) (_dv_D_n : n ∉ D.fv) (dv_D_q : q ∉ D.fv) (_dv_D_z : z ∉ D.fv) (dv_F_k : k ∉ F.fv) (dv_F_n : n ∉ F.fv) (dv_F_q : q ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_R_k : k ∉ R.fv) (_dv_R_n : n ∉ R.fv) (dv_R_q : q ∉ R.fv) (_dv_R_z : z ∉ R.fv) (_dv_k_n : k ≠ n) (dv_k_q : k ≠ q) (dv_k_z : k ≠ z) (_dv_n_q : n ≠ q) (dv_n_z : n ≠ z) (_dv_q_z : q ≠ z) (hyp_wppcandstrictslicenonemptyminndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wppcandstrictslicenonemptyminndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppcandstrictslicenonemptyminndv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) (Compiler.CompactSourceSyntax.synWrex q (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv k) (Compiler.CompactSourceSyntax.synCnc (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv q))))))))))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWne (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWrex n (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv z)))))

Checked nominal proof certificate identified upstream as g_wppcandstrictslicenonemptyminndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part040.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandselfndv (C F : SemanticCore.Class) (hyp_wppcandselfndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv)).imp (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCwppcand F C)))

Checked nominal proof certificate identified upstream as g_wppcandselfndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandstrictsliceemptyminndv (C : SemanticCore.Class) (k : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_k : k ∉ C.fv) (dv_F_k : k ∉ F.fv) (hyp_wppcandstrictsliceemptyminndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppcandstrictsliceemptyminndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synCwppcand F C)) (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr C Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))))

Checked nominal proof certificate identified upstream as g_wppcandstrictsliceemptyminndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandstrictsliceemptypublicminndv (z : SemanticCore.Var) (C : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_F_n : n ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_n_z : n ≠ z) (hyp_wppcandstrictsliceemptypublicminndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) (hyp_wppcandstrictsliceemptypublicminndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))) : Nominal.NPrf ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv Compiler.CompactSourceSyntax.synCltc) (Compiler.CompactSourceSyntax.synCsn C))) Compiler.CompactSourceSyntax.synC0).imp (Compiler.CompactSourceSyntax.synWrex n (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv z)))))

Checked nominal proof certificate identified upstream as g_wppcandstrictsliceemptypublicminndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandminfixedpivotdrfdv (z : SemanticCore.Var) (C D R : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_D_n : n ∉ D.fv) (dv_D_z : z ∉ D.fv) (dv_F_n : n ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_R_n : n ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_n_z : n ≠ z) (hyp_wppcandminfixedpivotdrfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wppcandminfixedpivotdrfdv_2 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCnc D))) (hyp_wppcandminfixedpivotdrfdv_3 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWrex n (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv z))))

Checked nominal proof certificate identified upstream as g_wppcandminfixedpivotdrfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisondefaultemptywe : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCin (Compiler.CompactSourceSyntax.synCkqrel Compiler.CompactSourceSyntax.synClefin) (Compiler.CompactSourceSyntax.synCxp Compiler.CompactSourceSyntax.synC0 Compiler.CompactSourceSyntax.synC0)) Compiler.CompactSourceSyntax.synCwe Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_wecomparisondefaultemptywe.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part041.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandminfixedpivotpairdrfdv (z : SemanticCore.Var) (C D R : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_D_n : n ∉ D.fv) (dv_D_z : z ∉ D.fv) (dv_F_n : n ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_R_n : n ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_n_z : n ≠ z) (hyp_wppcandminfixedpivotpairdrfdv_1 : Nominal.NPrf (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCnc D))).imp (Compiler.CompactSourceSyntax.synWrex n (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv z)))))

Checked nominal proof certificate identified upstream as g_wppcandminfixedpivotpairdrfdv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part042.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandminfixedpivotsetdeddrfdv (z : SemanticCore.Var) (C D R : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_D_n : n ∉ D.fv) (dv_D_z : z ∉ D.fv) (dv_F_n : n ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_R_n : n ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_n_z : n ≠ z) : Nominal.NPrf ((SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv).imp ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCnc D))).imp (Compiler.CompactSourceSyntax.synWrex n (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv z))))))

Checked nominal proof certificate identified upstream as g_wppcandminfixedpivotsetdeddrfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandminhwndv (z : SemanticCore.Var) (C : SemanticCore.Class) (n : SemanticCore.Var) (F : SemanticCore.Class) (dv_C_n : n ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_F_n : n ∉ F.fv) (dv_F_z : z ∉ F.fv) (dv_n_z : n ≠ z) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem F Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem C (Compiler.CompactSourceSyntax.synChwcards Compiler.CompactSourceSyntax.synCvv))).imp (Compiler.CompactSourceSyntax.synWrex n (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWral z (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv n) Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv z)))))

Checked nominal proof certificate identified upstream as g_wppcandminhwndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWppcandleastuniqclndv (A B C : SemanticCore.Class) (k : SemanticCore.Var) (F : SemanticCore.Class) (dv_A_k : k ∉ A.fv) (dv_B_k : k ∉ B.fv) (dv_C_k : k ∉ C.fv) (dv_F_k : k ∉ F.fv) (hyp_wppcandleastuniqclndv_1 : Nominal.NPrf (SemanticCore.Wff.classMem A (Compiler.CompactSourceSyntax.synCwppcand F C))) (hyp_wppcandleastuniqclndv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr A Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))) (hyp_wppcandleastuniqclndv_3 : Nominal.NPrf (SemanticCore.Wff.classMem B (Compiler.CompactSourceSyntax.synCwppcand F C))) (hyp_wppcandleastuniqclndv_4 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWral k (Compiler.CompactSourceSyntax.synCwppcand F C) (Compiler.CompactSourceSyntax.synWbr B Compiler.CompactSourceSyntax.synClec (SemanticCore.Class.cv k)))) : Nominal.NPrf (SemanticCore.Wff.classEq A B)

Checked nominal proof certificate identified upstream as g_wppcandleastuniqclndv.

Equations

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