NF weak partition development: NominalAlphaRepairedBase001037OpabFVReflOnHelpers004.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_notmem_syn_cop_cv_cv {a x y : SemanticCore.Var} (ha_x : a ≠ x) (ha_y : a ≠ y) : a ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_support_mem_x (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : x ∈ {x} ∪ {y} ∪ ph.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_support_mem_y (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : y ∈ {x} ∪ {y} ∪ ph.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_fresh_ne_x (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : ReplaySupport.freshVar ({x} ∪ {y} ∪ ph.fv) ≠ x

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_fresh_ne_y (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : ReplaySupport.freshVar ({x} ∪ {y} ∪ ph.fv) ≠ y

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_fresh_notmem_syn_cop_cv_cv (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : ReplaySupport.freshVar ({x} ∪ {y} ∪ ph.fv) ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_z_notmem_syn_cop_cv_cv (x y z : SemanticCore.Var) (dv_x_z : x ≠ z) (dv_y_z : y ≠ z) : z ∉ (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_notmem_neg_of_notmem {a : SemanticCore.Var} {ph : SemanticCore.Wff} (h : a ∉ ph.fv) : a ∉ ph.neg.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_fresh_notmem_ph (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : ReplaySupport.freshVar ({x} ∪ {y} ∪ ph.fv) ∉ ph.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_fresh_notmem_neg (ph : SemanticCore.Wff) (x y : SemanticCore.Var) : ReplaySupport.freshVar ({x} ∪ {y} ∪ ph.fv) ∉ ph.neg.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037_opab_z_notmem_neg (ph : SemanticCore.Wff) (z : SemanticCore.Var) (dv_ph_z : z ∉ ph.fv) : z ∉ ph.neg.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb037OpabReflOnThreePair (support : Finset SemanticCore.Var) (x y d z : SemanticCore.Var) (d_notmem : d ∉ support) (z_notmem : z ∉ support) : Nominal.TReflOn [(y, y), (x, x), (d, z)] support

Checked nominal proof certificate identified upstream as nb037_opab_reflOn_three_pair.

Equations

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