Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part009.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisomemberrndownndv (w v : SemanticCore.Var) (D R S : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (hyp_wecutisomemberrndownndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv w) E) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv w) S (SemanticCore.Class.cv v))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv w) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))))

Checked nominal proof certificate identified upstream as g_wecutisomemberrndownndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniondmdownndv (y z : SemanticCore.Var) (D R S E : SemanticCore.Class) (hyp_wecutisouniondmdownndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) D) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv z) R (SemanticCore.Class.cv y)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))))

Checked nominal proof certificate identified upstream as g_wecutisouniondmdownndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisounionrndownndv (w v : SemanticCore.Var) (D R S E : SemanticCore.Class) (hyp_wecutisounionrndownndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv v) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv w) E) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv w) S (SemanticCore.Class.cv v)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv w) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))))

Checked nominal proof certificate identified upstream as g_wecutisounionrndownndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part010.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniondmsscutndv (x : SemanticCore.Var) (D R S E : SemanticCore.Class) (hyp_wecutisouniondmsscutndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).neg).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (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_wecutisouniondmsscutndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisounionrnsscutndv (u : SemanticCore.Var) (D R S E : SemanticCore.Class) (hyp_wecutisounionrnsscutndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) E) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).neg).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_wecutisounionrnsscutndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisouniondmexactcutndv (x : SemanticCore.Var) (D R S E : SemanticCore.Class) (hyp_wecutisouniondmexactcutndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).neg) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif D (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))) (Compiler.CompactSourceSyntax.synCima R (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (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_wecutisouniondmexactcutndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part011.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisounionrnexactcutndv (u : SemanticCore.Var) (D R S E : SemanticCore.Class) (hyp_wecutisounionrnexactcutndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) E) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).neg) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif E (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))) (Compiler.CompactSourceSyntax.synCima S (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCrn (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u))))))

Checked nominal proof certificate identified upstream as g_wecutisounionrnexactcutndv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisoaddpairf1ondv (x u : SemanticCore.Var) (D R S E H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) E)) (Compiler.CompactSourceSyntax.synWiso H R S (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))).imp (Compiler.CompactSourceSyntax.synWf1o (Compiler.CompactSourceSyntax.synCun H (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_wecutisoaddpairf1ondv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part012.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisoaddpairisondv (x u : SemanticCore.Var) (D R S E H : SemanticCore.Class) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D) (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) E))) (Compiler.CompactSourceSyntax.synWiso H R S (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))).imp (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCun H (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv u)))) R S (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv u)))))

Checked nominal proof certificate identified upstream as g_wecutisoaddpairisondv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part013.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWedifleastssndv (x y : SemanticCore.Var) (C D R : SemanticCore.Class) (dv_C_x : x ∉ C.fv) (dv_C_y : y ∉ C.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (_dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_x_y : x ≠ y) (hyp_wedifleastssndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wedifleastssndv_2 : Nominal.NPrf (SemanticCore.Wff.classMem C Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x D (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C).neg).imp (Compiler.CompactSourceSyntax.synWrex y D (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) C).neg (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif D C) (Compiler.CompactSourceSyntax.synCima R (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y)))))))

Checked nominal proof certificate identified upstream as g_wedifleastssndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part014.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWeincsegsscutndv (x y : SemanticCore.Var) (D R : SemanticCore.Class) (_dv_x_y : x ≠ y) (hyp_weincsegsscutndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))).neg).imp (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))) (Compiler.CompactSourceSyntax.synCin D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))))))

Checked nominal proof certificate identified upstream as g_weincsegsscutndv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part015.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWedownexactcutndv (x : SemanticCore.Var) (C D R : SemanticCore.Class) (hyp_wedownexactcutndv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) C).neg) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCdif D C) (Compiler.CompactSourceSyntax.synCima R (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))) (Compiler.CompactSourceSyntax.synWss C (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 (SemanticCore.Wff.classEq C (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_wedownexactcutndv.

Equations

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