Nominal proof certificates grouped in dependency order.

Certificates from NominalWPPReplayChunk013Compact001Part016.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1induct (x z : SemanticCore.Var) (C R S V X : SemanticCore.Class) (dv_C_x : x ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_R_x : x ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_X_x : x ∉ X.fv) (dv_X_z : z ∉ X.fv) (dv_x_z : x ≠ z) (hyp_clos1induct_1 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1induct_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1induct_3 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 S R))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem X V) (Compiler.CompactSourceSyntax.synWss S X) (Compiler.CompactSourceSyntax.synWral x C (SemanticCore.Wff.all z ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) X) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv z))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv z) X))))).imp (Compiler.CompactSourceSyntax.synWss C X))

Checked nominal proof certificate identified upstream as g_clos1induct.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1is (ph ps ch th : SemanticCore.Wff) (x y z : SemanticCore.Var) (A C R S : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_y : y ∉ C.fv) (dv_C_z : z ∉ C.fv) (dv_R_y : y ∉ R.fv) (dv_R_z : z ∉ R.fv) (dv_S_x : x ∉ S.fv) (dv_ch_x : x ∉ ch.fv) (dv_ph_y : y ∉ ph.fv) (dv_ph_z : z ∉ ph.fv) (dv_ps_x : x ∉ ps.fv) (dv_th_x : x ∉ th.fv) (dv_x_y : x ≠ y) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) (hyp_clos1is_1 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1is_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1is_3 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 S R))) (hyp_clos1is_4 : Nominal.NPrf (SemanticCore.Wff.classMem (SemanticCore.Class.cab x ph) Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1is_5 : Nominal.NPrf ((SemanticCore.Wff.objEq x y).imp (Compiler.CompactSourceSyntax.synWb ph ps))) (hyp_clos1is_6 : Nominal.NPrf ((SemanticCore.Wff.objEq x z).imp (Compiler.CompactSourceSyntax.synWb ph ch))) (hyp_clos1is_7 : Nominal.NPrf ((SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A).imp (Compiler.CompactSourceSyntax.synWb ph th))) (hyp_clos1is_8 : Nominal.NPrf ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) S).imp ph)) (hyp_clos1is_9 : Nominal.NPrf ((Compiler.CompactSourceSyntax.synW3a (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) C) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv y) R (SemanticCore.Class.cv z)) ps).imp ch)) : Nominal.NPrf ((SemanticCore.Wff.classMem A C).imp th)

Checked nominal proof certificate identified upstream as g_clos1is.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part017.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1basesuc (x : SemanticCore.Var) (A C R S : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_x : x ∉ C.fv) (dv_R_x : x ∉ R.fv) (hyp_clos1basesuc_1 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1basesuc_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1basesuc_3 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 S R))) : Nominal.NPrf (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A C) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem A S) (Compiler.CompactSourceSyntax.synWrex x C (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R A))))

Checked nominal proof certificate identified upstream as g_clos1basesuc.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1baseima (C R S : SemanticCore.Class) (hyp_clos1basesuc_1 : Nominal.NPrf (SemanticCore.Wff.classMem S Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1basesuc_2 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_clos1basesuc_3 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 S R))) : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCun S (Compiler.CompactSourceSyntax.synCima R C)))

Checked nominal proof certificate identified upstream as g_clos1baseima.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos1basesucg (x : SemanticCore.Var) (A C R S V W : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_C_x : x ∉ C.fv) (dv_R_x : x ∉ R.fv) (dv_S_x : x ∉ S.fv) (hyp_clos1basesucg_1 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 S R))) : Nominal.NPrf ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem S V) (SemanticCore.Wff.classMem R W)).imp (Compiler.CompactSourceSyntax.synWb (SemanticCore.Wff.classMem A C) (Compiler.CompactSourceSyntax.synWo (SemanticCore.Wff.classMem A S) (Compiler.CompactSourceSyntax.synWrex x C (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R A)))))

Checked nominal proof certificate identified upstream as g_clos1basesucg.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gClos10 (C R : SemanticCore.Class) (hyp_clos10_1 : Nominal.NPrf (SemanticCore.Wff.classMem R Compiler.CompactSourceSyntax.synCvv)) (hyp_clos10_2 : Nominal.NPrf (SemanticCore.Wff.classEq C (Compiler.CompactSourceSyntax.synCclos1 Compiler.CompactSourceSyntax.synC0 R))) : Nominal.NPrf (SemanticCore.Wff.classEq C Compiler.CompactSourceSyntax.synC0)

Checked nominal proof certificate identified upstream as g_clos10.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part018.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gTransex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCtrans Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_transex.

Equations

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

Certificates from NominalWPPReplayChunk013Compact001Part019.

noncomputable def NFChoice.DirectNominalPrf.WPPReplay.gRefex : Nominal.NPrf (SemanticCore.Wff.classMem Compiler.CompactSourceSyntax.synCref Compiler.CompactSourceSyntax.synCvv)

Checked nominal proof certificate identified upstream as g_refex.

Equations

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