NF weak partition development: NominalDfEu.

The source axiom df-eu chooses an arbitrary dummy which is fresh for its displayed body. syn_weu chooses a deterministic dummy. Both choices lower to the same de-Bruijn formula, so their biconditional is just reflexivity in the exact literal Flypitch theory.

def NFChoice.DirectNominalPrf.Nominal.euPrimitive (y x : SemanticCore.Var) (p : SemanticCore.Wff) : SemanticCore.Wff

The displayed right-hand side of df-eu, with its source dummy exposed.

Equations

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

theorem NFChoice.DirectNominalPrf.Nominal.lowerWff_doubleBind_fresh (rho : SemanticCore.Var → ℕ) (dummy y x : SemanticCore.Var) (p : SemanticCore.Wff) (hdummy_p : dummy ∉ p.fv) (hy_p : y ∉ p.fv) : lowerWff (bindRho (bindRho rho dummy) x) p = lowerWff (bindRho (bindRho rho y) x) p

Two fresh outer dummies induce the same environment on the free variables of the body below the dummy and object-variable binders.

theorem NFChoice.DirectNominalPrf.Nominal.lowerEuPrimitive_eq (rho : SemanticCore.Var → ℕ) (dummy y x : SemanticCore.Var) (p : SemanticCore.Wff) (hdummy_x : dummy ≠ x) (hy_x : y ≠ x) (hdummy_p : dummy ∉ p.fv) (hy_p : y ∉ p.fv) : lowerWff rho (euPrimitive dummy x p) = lowerWff rho (euPrimitive y x p)

Alpha-renaming the fresh source dummy is definitional after lowering.

noncomputable def NFChoice.DirectNominalPrf.Nominal.dfEu (x y : SemanticCore.Var) (p : SemanticCore.Wff) (hxy : x ≠ y) (hy_p : y ∉ p.fv) : NPrf (Compiler.CompactSourceSyntax.synWb (Compiler.CompactSourceSyntax.synWeu x p) (euPrimitive y x p))

Direct proof-algebra implementation of the Metamath df-eu axiom. The hypotheses are exactly its two source $d obligations.

Equations

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