NF weak partition development: AlphaTransport.

@[reducible, inline]

abbrev NFChoice.DefinitionLeaves.AlphaTransport.BinderEnv : Type

A paired stack of corresponding nominal binders, nearest binder first.

Equations

• NFChoice.DefinitionLeaves.AlphaTransport.BinderEnv = List (NFChoice.SemanticCore.Var × NFChoice.SemanticCore.Var)

inductive NFChoice.DefinitionLeaves.AlphaTransport.AlphaVar : BinderEnv → SemanticCore.Var → SemanticCore.Var → Prop

Two variable occurrences denote the same de Bruijn position, or are the same free nominal variable outside the paired binder environment.

• here (env : BinderEnv) (x y : SemanticCore.Var) : AlphaVar ((x, y) :: env) x y
• there {env : BinderEnv} {x y a b : SemanticCore.Var} (ha : a ≠ x) (hb : b ≠ y) (h : AlphaVar env a b) : AlphaVar ((x, y) :: env) a b
• free {env : BinderEnv} {x : SemanticCore.Var} (hl : x ∉ List.map Prod.fst env) (hr : x ∉ List.map Prod.snd env) : AlphaVar env x x

inductive NFChoice.DefinitionLeaves.AlphaTransport.AlphaClass : BinderEnv → SemanticCore.Class → SemanticCore.Class → Prop

Alpha-equivalence of nominal class terms under paired binders.

• cv {env : BinderEnv} {x y : SemanticCore.Var} (h : AlphaVar env x y) : AlphaClass env (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)
• cab {env : BinderEnv} {x y : SemanticCore.Var} {p q : SemanticCore.Wff} (h : AlphaWff ((x, y) :: env) p q) : AlphaClass env (SemanticCore.Class.cab x p) (SemanticCore.Class.cab y q)

inductive NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff : BinderEnv → SemanticCore.Wff → SemanticCore.Wff → Prop

Alpha-equivalence of nominal formulas under paired binders.

• falsum {env : BinderEnv} : AlphaWff env SemanticCore.Wff.falsum SemanticCore.Wff.falsum
• imp {env : BinderEnv} {p p' q q' : SemanticCore.Wff} (hp : AlphaWff env p p') (hq : AlphaWff env q q') : AlphaWff env (p.imp q) (p'.imp q')
• all {env : BinderEnv} {x y : SemanticCore.Var} {p q : SemanticCore.Wff} (h : AlphaWff ((x, y) :: env) p q) : AlphaWff env (SemanticCore.Wff.all x p) (SemanticCore.Wff.all y q)
• objEq {env : BinderEnv} {x x' y y' : SemanticCore.Var} (hx : AlphaVar env x x') (hy : AlphaVar env y y') : AlphaWff env (SemanticCore.Wff.objEq x y) (SemanticCore.Wff.objEq x' y')
• objMem {env : BinderEnv} {x x' y y' : SemanticCore.Var} (hx : AlphaVar env x x') (hy : AlphaVar env y y') : AlphaWff env (SemanticCore.Wff.objMem x y) (SemanticCore.Wff.objMem x' y')
• classEq {env : BinderEnv} {A A' B B' : SemanticCore.Class} (hA : AlphaClass env A A') (hB : AlphaClass env B B') : AlphaWff env (SemanticCore.Wff.classEq A B) (SemanticCore.Wff.classEq A' B')
• classMem {env : BinderEnv} {A A' B B' : SemanticCore.Class} (hA : AlphaClass env A A') (hB : AlphaClass env B B') : AlphaWff env (SemanticCore.Wff.classMem A B) (SemanticCore.Wff.classMem A' B')

def NFChoice.DefinitionLeaves.AlphaTransport.ValAgree {S : Type u_1} (env : BinderEnv) (v w : SemanticCore.Var → S) : Prop

Corresponding nominal variables have equal values in paired valuations.

Equations

• NFChoice.DefinitionLeaves.AlphaTransport.ValAgree env v w = ∀ ⦃x y : NFChoice.SemanticCore.Var⦄, NFChoice.DefinitionLeaves.AlphaTransport.AlphaVar env x y → v x = w y

theorem NFChoice.DefinitionLeaves.AlphaTransport.ValAgree.extend {S : Type u_1} {env : BinderEnv} {v w : SemanticCore.Var → S} (h : ValAgree env v w) (x y : SemanticCore.Var) (a : S) : ValAgree ((x, y) :: env) (SemanticCore.update v x a) (SemanticCore.update w y a)

theorem NFChoice.DefinitionLeaves.AlphaTransport.valAgree_empty {S : Type u_1} (v : SemanticCore.Var → S) : ValAgree [] v v

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaClass.holds_iff {S : Fol.Structure Foundation.LNF} {env : BinderEnv} {A B : SemanticCore.Class} (h : AlphaClass env A B) {v w : SemanticCore.Var → S.carrier} (hv : ValAgree env v w) (a : S.carrier) : SemanticCore.Class.Holds S v A a ↔ SemanticCore.Class.Holds S w B a

Alpha-equivalent classes have identical denotations.

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.holds_iff {S : Fol.Structure Foundation.LNF} {env : BinderEnv} {p q : SemanticCore.Wff} (h : AlphaWff env p q) {v w : SemanticCore.Var → S.carrier} (hv : ValAgree env v w) : SemanticCore.Wff.Holds S v p ↔ SemanticCore.Wff.Holds S w q

Alpha-equivalent formulas have identical truth values.

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.neg {env : BinderEnv} {p q : SemanticCore.Wff} (h : AlphaWff env p q) : AlphaWff env p.neg q.neg

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.conj {env : BinderEnv} {p p' q q' : SemanticCore.Wff} (hp : AlphaWff env p p') (hq : AlphaWff env q q') : AlphaWff env (p.conj q) (p'.conj q')

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.biimp {env : BinderEnv} {p p' q q' : SemanticCore.Wff} (hp : AlphaWff env p p') (hq : AlphaWff env q q') : AlphaWff env (p.biimp q) (p'.biimp q')

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.ex {env : BinderEnv} {x y : SemanticCore.Var} {p q : SemanticCore.Wff} (h : AlphaWff ((x, y) :: env) p q) : AlphaWff env (SemanticCore.Wff.ex x p) (SemanticCore.Wff.ex y q)

def NFChoice.DefinitionLeaves.AlphaTransport.EnvFresh (env : BinderEnv) (support : Finset SemanticCore.Var) : Prop

A finite support is fresh for every genuinely renamed environment pair.

Equations

• NFChoice.DefinitionLeaves.AlphaTransport.EnvFresh env support = ∀ ⦃x y : NFChoice.SemanticCore.Var⦄, (x, y) ∈ env → x ≠ y → x ∉ support ∧ y ∉ support

theorem NFChoice.DefinitionLeaves.AlphaTransport.EnvFresh.mono {env : BinderEnv} {small large : Finset SemanticCore.Var} (h : EnvFresh env large) (hsub : small ⊆ large) : EnvFresh env small

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaVar.reflOfFresh (env : BinderEnv) (u : SemanticCore.Var) (h : EnvFresh env {u}) : AlphaVar env u u

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaClass.reflOfFresh (env : BinderEnv) (A : SemanticCore.Class) (h : EnvFresh env A.vars) : AlphaClass env A A

Reflexive alpha certificate under externally fresh renamed binders.

theorem NFChoice.DefinitionLeaves.AlphaTransport.AlphaWff.reflOfFresh (env : BinderEnv) (p : SemanticCore.Wff) (h : EnvFresh env p.vars) : AlphaWff env p p

Reflexive formula alpha certificate under externally fresh binders.

theorem NFChoice.DefinitionLeaves.AlphaTransport.valid_biimp_of_alpha {S : Fol.Structure Foundation.LNF} {p q : SemanticCore.Wff} (h : AlphaWff [] p q) : SemanticCore.Wff.Valid S (p.biimp q)

Semantic alpha transport for the Wff-definition leaves.

theorem NFChoice.DefinitionLeaves.AlphaTransport.valid_classEq_of_alpha {S : Fol.Structure Foundation.LNF} {A B : SemanticCore.Class} (h : AlphaClass [] A B) : SemanticCore.Wff.Valid S (SemanticCore.Wff.classEq A B)

Semantic alpha transport for the class-definition leaves.