Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk016Compact001Part035.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecutisoextendedterminaldfdv (x y u : SemanticCore.Var) (D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_h : h ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_D_y : y ∉ D.fv) (dv_E_h : h ∉ E.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_E_y : y ∉ E.fv) (dv_R_h : h ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) (dv_S_h : h ∉ S.fv) (dv_S_u : u ∉ S.fv) (dv_S_x : x ∉ S.fv) (dv_S_y : y ∉ S.fv) (dv_h_u : h ≠ u) (dv_h_x : h ≠ x) (dv_h_y : h ≠ y) (dv_u_x : u ≠ x) (dv_u_y : u ≠ y) (dv_x_y : x ≠ y) (hyp_wecutisoextendedterminaldfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecutisoextendedterminaldfdv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) (hyp_wecutisoextendedterminaldfdv_3 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) D) (SemanticCore.Wff.classMem (SemanticCore.Class.cv u) E)) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) (Compiler.CompactSourceSyntax.synCdm (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)))).neg (Compiler.CompactSourceSyntax.synWiso (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv y) (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 y)))) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv y))) (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)))))).imp (Compiler.CompactSourceSyntax.synW3o (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R S D E)) (Compiler.CompactSourceSyntax.synWrex x E (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S 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 x)))))) D (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))) (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) S (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (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 D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) 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_wecutisoextendedterminaldfdv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part036.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisonterminalsetfdv (x : SemanticCore.Var) (D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_h : h ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_h : h ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_R_h : h ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_S_h : h ∉ S.fv) (dv_S_x : x ∉ S.fv) (dv_h_x : h ≠ x) (hyp_wecomparisonterminalsetfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecomparisonterminalsetfdv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) (hyp_wecomparisonterminalsetfdv_3 : Nominal.NPrf (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCwecutiso R D S E)) Compiler.CompactSourceSyntax.synCvv)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synW3o (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R S D E)) (Compiler.CompactSourceSyntax.synWrex x E (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S 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 x)))))) D (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))) (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) S (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (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 D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) 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_wecomparisonterminalsetfdv.

Equations

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

Certificates from NominalWPPReplayChunk016Compact001Part037.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisonterminalfdv (x : SemanticCore.Var) (D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_h : h ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_h : h ∉ E.fv) (dv_E_x : x ∉ E.fv) (dv_R_h : h ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_S_h : h ∉ S.fv) (dv_S_x : x ∉ S.fv) (dv_h_x : h ≠ x) (hyp_wecomparisonterminalfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecomparisonterminalfdv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf (Compiler.CompactSourceSyntax.synW3o (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R S D E)) (Compiler.CompactSourceSyntax.synWrex x E (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S 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 x)))))) D (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x))))))) (Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) S (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (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 D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) 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_wecomparisonterminalfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWeisoexnceqclfdv (A B T U : SemanticCore.Class) (h : SemanticCore.Var) (dv_A_h : h ∉ A.fv) (dv_B_h : h ∉ B.fv) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) T U A B)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCnc A) (Compiler.CompactSourceSyntax.synCnc B)))

Checked nominal proof certificate identified upstream as g_weisoexnceqclfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisonforwardnclecclfdv (x : SemanticCore.Var) (D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_h : h ∉ D.fv) (dv_D_x : x ∉ D.fv) (dv_E_h : h ∉ E.fv) (dv_E_x : x ∉ E.fv) (_dv_R_h : h ∉ R.fv) (_dv_R_x : x ∉ R.fv) (dv_S_h : h ∉ S.fv) (_dv_S_x : x ∉ S.fv) (dv_h_x : h ≠ x) (hyp_wecomparisonforwardnclecclfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWo (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R S D E)) (Compiler.CompactSourceSyntax.synWrex x E (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) R (Compiler.CompactSourceSyntax.synCin S (Compiler.CompactSourceSyntax.synCxp (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S 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 x)))))) D (Compiler.CompactSourceSyntax.synCin E (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))))).imp (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc D) Compiler.CompactSourceSyntax.synClec (Compiler.CompactSourceSyntax.synCnc E)))

Checked nominal proof certificate identified upstream as g_wecomparisonforwardnclecclfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisonreversecutrepfdv (x : SemanticCore.Var) (D R S : SemanticCore.Class) (h : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_h : h ∉ D.fv) (_dv_D_x : x ∉ D.fv) (dv_E_h : h ∉ E.fv) (_dv_E_x : x ∉ E.fv) (dv_R_h : h ∉ R.fv) (_dv_R_x : x ∉ R.fv) (dv_h_x : h ≠ x) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWrex x D (Compiler.CompactSourceSyntax.synWex h (Compiler.CompactSourceSyntax.synWiso (SemanticCore.Class.cv h) S (Compiler.CompactSourceSyntax.synCin R (Compiler.CompactSourceSyntax.synCxp (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 D (Compiler.CompactSourceSyntax.synCima (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)) (Compiler.CompactSourceSyntax.synCsn (SemanticCore.Class.cv x)))))) 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))))))).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_wecomparisonreversecutrepfdv.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gWecomparisoncutrepltfdv (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_wecomparisoncutrepltfdv_1 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr R Compiler.CompactSourceSyntax.synCwe D)) (hyp_wecomparisoncutrepltfdv_2 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr S Compiler.CompactSourceSyntax.synCwe E)) (hyp_wecomparisoncutrepltfdv_3 : Nominal.NPrf (Compiler.CompactSourceSyntax.synWbr (Compiler.CompactSourceSyntax.synCnc E) Compiler.CompactSourceSyntax.synCltc (Compiler.CompactSourceSyntax.synCnc D))) : 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)))))))

Checked nominal proof certificate identified upstream as g_wecomparisoncutrepltfdv.

Equations

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