Free variables of, and de Bruijn index manipulation for, a ComputableTLAPlus.Expression under locally-nameless binding.

Expression.freeVars collects every .var _ (.free name) node: a Memory-keyed name (PlusCal variable/channel/fifo, self, a statement with). .bound occurrences resolve to an enclosing expression binder and .module/.intrinsic occurrences resolve through Ξ/Ω — none of them read memory, so none contribute.

Origin.bound uses standard de Bruijn indices: .bound 0 is the nearest enclosing expression-level binder. liftBound/openVar/close/subst/instantiate are all one depth-tracking traversal, mapVars. .bound and .free are disjoint namespaces, so subst of a free name captures nothing and needs no freshness side condition.

@[irreducible]

def ComputableTLAPlus.Expression.freeVars {α : Type} (target : Expression α) : Finset String

Every name a target reads from memory: every .var _ (.free name) node. .bound and .module/.intrinsic occurrences resolve elsewhere and contribute nothing.

Equations

• One or more equations did not get rendered due to their size.
• (ComputableTLAPlus.Expression.var a (TypedTLAPlus.Origin.free n)).freeVars = {n}
• (ComputableTLAPlus.Expression.var a a_1).freeVars = ∅
• (ComputableTLAPlus.Expression.forall a a_1 dom body).freeVars = dom.freeVars ∪ body.freeVars
• (ComputableTLAPlus.Expression.exists a a_1 dom body).freeVars = dom.freeVars ∪ body.freeVars
• (ComputableTLAPlus.Expression.choose a a_1 dom body).freeVars = dom.freeVars ∪ body.freeVars
• (ComputableTLAPlus.Expression.collect a a_1 dom pred).freeVars = dom.freeVars ∪ pred.freeVars
• (body.map' a ann cod dom).freeVars = dom.freeVars ∪ body.freeVars
• (f.fnCall fnTyp e').freeVars = f.freeVars ∪ e'.freeVars
• (ComputableTLAPlus.Expression.fn a ann cod dom body).freeVars = dom.freeVars ∪ body.freeVars
• (f.recordAccess a).freeVars = f.freeVars
• (e₁.if e₂ e₃ τ).freeVars = e₁.freeVars ∪ e₂.freeVars ∪ e₃.freeVars
• (ComputableTLAPlus.Expression.nat a).freeVars = ∅
• (ComputableTLAPlus.Expression.str a).freeVars = ∅
• ComputableTLAPlus.Expression.true.freeVars = ∅
• ComputableTLAPlus.Expression.false.freeVars = ∅

@[irreducible]

def ComputableTLAPlus.Expression.mapVars {α : Type} (f : ℕ → α → Origin → SourceSpan → Expression α) (k : ℕ) (target : Expression α) : Expression α

Rebuild every .var node knowing the number of expression-level binders enclosing it: f k τ o pos is the replacement for a .var τ o at binder depth k. Each binder arm recurses into its scoped body at k + 1; domain and annotation positions stay at k.

Equations

• One or more equations did not get rendered due to their size.
• ComputableTLAPlus.Expression.mapVars f k (ComputableTLAPlus.Expression.var τ o) = f k τ o (posOf (ComputableTLAPlus.Expression.var τ o))
• ComputableTLAPlus.Expression.mapVars f k (g.recordAccess nm) = (ComputableTLAPlus.Expression.mapVars f k g).recordAccess nm @@ posOf (g.recordAccess nm)
• ComputableTLAPlus.Expression.mapVars f k (ComputableTLAPlus.Expression.nat n) = ComputableTLAPlus.Expression.nat n @@ posOf (ComputableTLAPlus.Expression.nat n)
• ComputableTLAPlus.Expression.mapVars f k (ComputableTLAPlus.Expression.str s) = ComputableTLAPlus.Expression.str s @@ posOf (ComputableTLAPlus.Expression.str s)
• ComputableTLAPlus.Expression.mapVars f k ComputableTLAPlus.Expression.true = ComputableTLAPlus.Expression.true @@ posOf ComputableTLAPlus.Expression.true
• ComputableTLAPlus.Expression.mapVars f k ComputableTLAPlus.Expression.false = ComputableTLAPlus.Expression.false @@ posOf ComputableTLAPlus.Expression.false

def ComputableTLAPlus.Expression.liftBoundLam {α : Type} (d : ℕ) : ℕ → α → Origin → SourceSpan → Expression α

The mapVars action liftBound d runs at every .var node: add d to a .bound index that sits at or past the current binder depth, leave everything else. Named so lemmas can talk about the traversal without re-inlining it.

Equations

• ComputableTLAPlus.Expression.liftBoundLam d k τ (TypedTLAPlus.Origin.bound i) pos = ComputableTLAPlus.Expression.var τ (TypedTLAPlus.Origin.bound (if k ≤ i then i + d else i)) @@ pos
• ComputableTLAPlus.Expression.liftBoundLam d k τ o pos = ComputableTLAPlus.Expression.var τ o @@ pos

def ComputableTLAPlus.Expression.liftBound {α : Type} (d : ℕ) (e : Expression α) : Expression α

Add d to every .bound index that refers past e's own binders.

Equations

• ComputableTLAPlus.Expression.liftBound d e = ComputableTLAPlus.Expression.mapVars (ComputableTLAPlus.Expression.liftBoundLam d) 0 e

def ComputableTLAPlus.Expression.openVarLam {α : Type} (name : String) : ℕ → α → Origin → SourceSpan → Expression α

The mapVars action openVar name runs at every .var node: the .bound index equal to the current depth becomes .free name, deeper indices shift down by one, shallower ones stay. Named so lemmas can talk about the traversal without re-inlining it.

Equations

• One or more equations did not get rendered due to their size.
• ComputableTLAPlus.Expression.openVarLam name k τ o pos = ComputableTLAPlus.Expression.var τ o @@ pos

def ComputableTLAPlus.Expression.openVar {α : Type} (name : String) (e : Expression α) : Expression α

In a binder's body — already stripped of that binder — turn the reference to the removed binder into the free name name, and shift every deeper free index down by one.

Equations

• ComputableTLAPlus.Expression.openVar name e = ComputableTLAPlus.Expression.mapVars (ComputableTLAPlus.Expression.openVarLam name) 0 e

def ComputableTLAPlus.Expression.close {α : Type} (name : String) (e : Expression α) : Expression α

Bind every free occurrence of name as a new outermost .bound, shifting every deeper free index up by one. Inverse of openVar.

Equations

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

theorem ComputableTLAPlus.Expression.doubleAttach_map_eq {β γ : Type} {l : List β} {f : { x : β // x ∈ l } → γ} {g : { y : γ // y ∈ List.map f l.attach } → γ} {h : { x : β // x ∈ l } → γ} (H : ∀ (a : { x : β // x ∈ l }) (hm : f a ∈ List.map f l.attach), g ⟨f a, hm⟩ = h a) : List.map g (List.map f l.attach).attach = List.map h l.attach

Collapse the outer attach ∘ map a second mapVars (or applyComputable) traversal wraps around a list arm: (l.attach.map f).attach.map g matches the single-layer l.attach.map h when g on each element f a agrees with h a. The applyComputable list arms (tuple/record) need this — the source term carries one attach.map, the traversed term two.

theorem ComputableTLAPlus.Expression.mapVars_mapVars_id {α : Type} {g h : ℕ → α → Origin → SourceSpan → Expression α} (H : ∀ (k : ℕ) (τ : α) (o : Origin) (pos : SourceSpan), mapVars h k (g k τ o pos) = var τ o @@ pos) (k : ℕ) (e : Expression α) : mapVars h k (mapVars g k e) = e

Two mapVars traversals at the same depth that undo one another at every .var node cancel over the whole term. Used to state .liftBound/.openVar cancellations.

theorem ComputableTLAPlus.Expression.mapVars_shift_comm {α : Type} {g gf f fg : ℕ → α → Origin → SourceSpan → Expression α} (n : ℕ) (H : ∀ (j : ℕ) (τ : α) (o : Origin) (pos : SourceSpan), mapVars g (n + 1 + j) (f j τ o pos) = mapVars gf j (fg (n + j) τ o pos)) (j : ℕ) (e : Expression α) : mapVars g (n + 1 + j) (mapVars f j e) = mapVars gf j (mapVars fg (n + j) e)

Two mapVars traversals commute when the left one runs n + 1 binder levels deeper than the right: applying f at depth j then g at n + 1 + j equals applying fg at n + j then gf at j, provided the four .var-node actions satisfy that identity pointwise. The n offset is what a splice under n + 1 binders (an operator/function body) needs — e.g. openVar at depth n + 1 past a liftBound 1 at depth 0 matches liftBound 1 past openVar at depth n (openVar_liftBound_one_comm). applyComputable never builds except/case, but those arms are discharged too so the lemma holds for every term.

theorem ComputableTLAPlus.Expression.mapVars_comm {α : Type} {g gf f fg : ℕ → α → Origin → SourceSpan → Expression α} (H : ∀ (k : ℕ) (τ : α) (o : Origin) (pos : SourceSpan), mapVars g k (f k τ o pos) = mapVars gf k (fg k τ o pos)) (k : ℕ) (e : Expression α) : mapVars g k (mapVars f k e) = mapVars gf k (mapVars fg k e)

Two mapVars traversals at the same depth commute when the four .var-node actions commute pointwise. The zero-offset companion of mapVars_shift_comm — needed where a splice happens directly under the binder being opened, not one level deeper (subst_openVar_comm).

theorem ComputableTLAPlus.Expression.openVar_liftBound_one_comm {α : Type} (name : String) (n : ℕ) (e : Expression α) : mapVars (openVarLam name) (n + 1) (liftBound 1 e) = liftBound 1 (mapVars (openVarLam name) n e)

Opening the binder n + 1 levels out (openVar name at depth n + 1) commutes with the liftBound 1 a splice under that binder carries: doing the lift first and opening at n + 1 matches opening at n first and lifting. The instance of mapVars_shift_comm that openVar_applyComputable needs for every arm of applyComputable that puts e under a binder.

theorem ComputableTLAPlus.Expression.openVar_liftBound_one {α : Type} (name : String) (e : Expression α) : openVar name (liftBound 1 e) = e

Lifting every de Bruijn index up by one and then opening the (now vacant) innermost binder with name is the identity: the lift moves every index past the cutoff, so openVar finds nothing bound at depth 0 to rename and shifts everything back down. No freshness needed.

def ComputableTLAPlus.Expression.openHints {α : Type} (outer : List String := []) (e : Expression α) : Expression α

Resolve every .bound occurrence in e to the free name its binding hint carries. outer names the binders enclosing e that are not nodes within it — operator/function parameters, a multicast filter's recipient — in source order, outermost first. Afterwards e holds no .bound node: every former bound occurrence reads as .free of the string its binder recorded. The inverse the elaborator performs is close; consumers that only read a term (code generation, pretty printing) use this to work with names instead of indices.

Equations

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

partial def ComputableTLAPlus.Expression.openHints.go {α : Type} (e : Expression α) : Expression α

def ComputableTLAPlus.Expression.substLam {α : Type} (x : String) (e : Expression α) : ℕ → α → Origin → SourceSpan → Expression α

The mapVars action subst x e runs at every .var node: a .var _ (.free x) becomes e lifted by the current binder depth; everything else is left. Named so lemmas compose without re-inlining it.

Equations

• One or more equations did not get rendered due to their size.
• ComputableTLAPlus.Expression.substLam x e k τ o pos = ComputableTLAPlus.Expression.var τ o @@ pos

def ComputableTLAPlus.Expression.subst {α : Type} (x : String) (e target : Expression α) : Expression α

Substitute e for every free occurrence of the free name x. Captures nothing — .free and .bound are disjoint — with e liftBound-ed by the binder depth it is spliced under. Sound only when e is locally closed (Expression.LC); the liftBound is meaningless otherwise.

Equations

• ComputableTLAPlus.Expression.subst x e target = ComputableTLAPlus.Expression.mapVars (ComputableTLAPlus.Expression.substLam x e) 0 target

def ComputableTLAPlus.Expression.LC {α : Type} (e : Expression α) : Prop

e has no dangling de Bruijn index: every .bound i node sits under more than i enclosing binders. Phrased so that any depth-tracking traversal that is the identity on .bound i below its own depth (and on non-.bound origins) leaves e untouched, from any base depth — which is what liftBound/openVar/subst all are, on their .bound arms, once i is genuinely bound.

Equations

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

theorem ComputableTLAPlus.Expression.LC.liftBound_eq {α : Type} {e : Expression α} (h : e.LC) (k : ℕ) : Expression.liftBound k e = e

A locally-closed term is fixed by liftBound at any amount.

theorem ComputableTLAPlus.Expression.LC.mapVars_openVarLam_eq {α : Type} {e : Expression α} (h : e.LC) (name : String) (k : ℕ) : mapVars (openVarLam name) k e = e

A locally-closed term is fixed by an openVar traversal at any base depth: there is no outermost .bound for it to rename.

theorem ComputableTLAPlus.Expression.LC.of_openVar_eq {α : Type} {name : String} {e : Expression α} (h : openVar name e = e) : e.LC

The converse of LC.mapVars_openVarLam_eq: openVar fixing a term certifies it locally closed.

theorem ComputableTLAPlus.Expression.subst_openVar_comm {α : Type} {x : String} {e' : Expression α} {z : String} (hlc : e'.LC) (hzx : z ≠ x) (k : ℕ) (body : Expression α) : mapVars (openVarLam z) k (mapVars (substLam x e') k body) = mapVars (substLam x e') k (mapVars (openVarLam z) k body)

Substituting a free name and opening a binder body commute, provided the opened name is distinct from the substituted one and the substituend is locally closed. The binder case of evalSubst'.

theorem ComputableTLAPlus.Expression.subst_eq_mapVars {α : Type} (x : String) (e target : Expression α) : subst x e target = mapVars (substLam x e) 0 target

subst is the mapVars of substLam. Definitional; stated so simp can move between the two without unfolding subst to a raw lambda.

def ComputableTLAPlus.Expression.instLam {α : Type} (args : List (Expression α)) : ℕ → α → Origin → SourceSpan → Expression α

The mapVars action instantiate args runs at every .var node: a .bound index at or past the current binder depth is replaced by the corresponding arg (lifted past the crossed binders) or shifted down by args.length when it points past them. Named so lemmas compose without re-inlining it.

Equations

• One or more equations did not get rendered due to their size.
• ComputableTLAPlus.Expression.instLam args k τ o pos = ComputableTLAPlus.Expression.var τ o @@ pos

def ComputableTLAPlus.Expression.instantiate {α : Type} (args : List (Expression α)) (target : Expression α) : Expression α

Instantiate the outermost de Bruijn binders with args (args[0] for .bound 0, …), shifting every deeper index down by args.length. Operator/function parameter substitution.

Equations

• ComputableTLAPlus.Expression.instantiate args target = ComputableTLAPlus.Expression.mapVars (ComputableTLAPlus.Expression.instLam args) 0 target

theorem ComputableTLAPlus.Expression.mapVars_succ_base {α : Type} {f : ℕ → α → Origin → SourceSpan → Expression α} (hf : ∀ (d : ℕ) (τ : α) (o : Origin) (pos : SourceSpan), f (d + 1) τ o pos = f d τ o pos) (k : ℕ) (e : Expression α) : mapVars f (k + 1) e = mapVars f k e

Bumping the base depth of a mapVars by one is unobservable when the per-node action f's answer at depth d + 1 matches its answer at d.

theorem ComputableTLAPlus.Expression.mapVars_base_irrel {α : Type} {f : ℕ → α → Origin → SourceSpan → Expression α} (hf : ∀ (d : ℕ) (τ : α) (o : Origin) (pos : SourceSpan), f (d + 1) τ o pos = f d τ o pos) (k : ℕ) (e : Expression α) : mapVars f k e = mapVars f 0 e

Iterated mapVars_succ_base: a depth-agnostic action's mapVars is depth-independent.

theorem ComputableTLAPlus.Expression.LC.mapVars_liftBoundLam_eq {α : Type} {e : Expression α} (h : e.LC) (d k : ℕ) : mapVars (liftBoundLam d) k e = e

A locally-closed term is fixed by a liftBound traversal at any base depth.

theorem ComputableTLAPlus.Expression.LC.mapVars_instLam_eq {α : Type} {e : Expression α} (h : e.LC) (args : List (Expression α)) (k : ℕ) : mapVars (instLam args) k e = e

A locally-closed term is fixed by an instantiate traversal at any base depth: it has no free .bound for instLam to replace.

theorem ComputableTLAPlus.Expression.LC.mapVars_substLam_eq {α : Type} {x : String} {e' : Expression α} (hlc : e'.LC) (k : ℕ) (t : Expression α) : mapVars (substLam x e') k t = subst x e' t

For a locally-closed substituend, substLam ignores the depth it runs at, so subst reads off a mapVars of substLam at any base depth.

subst, structurally

subst pushes through every constructor. The binder arms descend the body at depth 1; under e'.LC that mapVars _ 1 is subst again (LC.mapVars_substLam_eq), so LC.subst_* state the fully-recursive shape evalSubst' reads off.

theorem ComputableTLAPlus.Expression.subst_nat {α : Type} {x : String} {e' : Expression α} {s : String} : subst x e' (nat s) = nat s

theorem ComputableTLAPlus.Expression.subst_str {α : Type} {x : String} {e' : Expression α} {s : String} : subst x e' (str s) = str s

theorem ComputableTLAPlus.Expression.subst_true {α : Type} {x : String} {e' : Expression α} : subst x e' true = true

theorem ComputableTLAPlus.Expression.subst_false {α : Type} {x : String} {e' : Expression α} : subst x e' false = false

theorem ComputableTLAPlus.Expression.subst_var_module {α : Type} {x : String} {e' : Expression α} {τ : α} {m n : String} : subst x e' (var τ (TypedTLAPlus.Origin.module m n)) = var τ (TypedTLAPlus.Origin.module m n)

theorem ComputableTLAPlus.Expression.subst_var_intrinsic {α : Type} {x : String} {e' : Expression α} {τ : α} {n : String} : subst x e' (var τ (TypedTLAPlus.Origin.intrinsic n)) = var τ (TypedTLAPlus.Origin.intrinsic n)

theorem ComputableTLAPlus.Expression.subst_var_bound {α : Type} {x : String} {e' : Expression α} {τ : α} {i : ℕ} : subst x e' (var τ (TypedTLAPlus.Origin.bound i)) = var τ (TypedTLAPlus.Origin.bound i)

theorem ComputableTLAPlus.Expression.subst_var_free_ne {α : Type} {x : String} {e' : Expression α} {τ : α} {n : String} (h : n ≠ x) : subst x e' (var τ (TypedTLAPlus.Origin.free n)) = var τ (TypedTLAPlus.Origin.free n)

theorem ComputableTLAPlus.Expression.LC.subst_var_free_eq {α : Type} {x : String} {e' : Expression α} {τ : α} (hlc : e'.LC) : subst x e' (var τ (TypedTLAPlus.Origin.free x)) = e'

theorem ComputableTLAPlus.Expression.subst_opCall {α : Type} {x : String} {e' g : Expression α} {es : List (Expression α)} : subst x e' (g.opCall es) = (subst x e' g).opCall (List.map (subst x e') es)

theorem ComputableTLAPlus.Expression.subst_fnCall {α : Type} {x : String} {e' f e'' : Expression α} {τ : α} : subst x e' (f.fnCall τ e'') = (subst x e' f).fnCall τ (subst x e' e'')

theorem ComputableTLAPlus.Expression.subst_recordAccess {α : Type} {x : String} {e' f : Expression α} {n : String} : subst x e' (f.recordAccess n) = (subst x e' f).recordAccess n

theorem ComputableTLAPlus.Expression.subst_if {α : Type} {x : String} {e' a b c : Expression α} {τ : α} : subst x e' (a.if b c τ) = (subst x e' a).if (subst x e' b) (subst x e' c) τ

theorem ComputableTLAPlus.Expression.subst_set {α : Type} {x : String} {e' : Expression α} {es : List (Expression α)} {τ : α} : subst x e' (set es τ) = set (List.map (subst x e') es) τ

theorem ComputableTLAPlus.Expression.subst_seq {α : Type} {x : String} {e' : Expression α} {es : List (Expression α)} {τ : α} : subst x e' (seq es τ) = seq (List.map (subst x e') es) τ

theorem ComputableTLAPlus.Expression.subst_tuple {α : Type} {x : String} {e' : Expression α} {es : List (α × Expression α)} : subst x e' (tuple es) = tuple (List.map (fun (p : α × Expression α) => (p.1, subst x e' p.2)) es)

theorem ComputableTLAPlus.Expression.subst_record {α : Type} {x : String} {e' : Expression α} {fs : List (α × String × Expression α)} : subst x e' (record fs) = record (List.map (fun (p : α × String × Expression α) => (p.1, p.2.1, subst x e' p.2.2)) fs)

theorem ComputableTLAPlus.Expression.LC.subst_forall {α : Type} {x : String} {e' : Expression α} {x' : String} {τ : α} {dom body : Expression α} (hlc : e'.LC) : subst x e' («forall» x' τ dom body) = «forall» x' τ (subst x e' dom) (subst x e' body)

theorem ComputableTLAPlus.Expression.LC.subst_exists {α : Type} {x : String} {e' : Expression α} {x' : String} {τ : α} {dom body : Expression α} (hlc : e'.LC) : subst x e' («exists» x' τ dom body) = «exists» x' τ (subst x e' dom) (subst x e' body)

theorem ComputableTLAPlus.Expression.LC.subst_choose {α : Type} {x : String} {e' : Expression α} {x' : String} {τ : α} {dom body : Expression α} (hlc : e'.LC) : subst x e' (choose x' τ dom body) = choose x' τ (subst x e' dom) (subst x e' body)

theorem ComputableTLAPlus.Expression.LC.subst_collect {α : Type} {x : String} {e' : Expression α} {x' : String} {τ : α} {dom body : Expression α} (hlc : e'.LC) : subst x e' (collect x' τ dom body) = collect x' τ (subst x e' dom) (subst x e' body)

theorem ComputableTLAPlus.Expression.LC.subst_map' {α : Type} {x : String} {e' : Expression α} {x' : String} {ann cod : α} {dom body : Expression α} (hlc : e'.LC) : subst x e' (body.map' x' ann cod dom) = (subst x e' body).map' x' ann cod (subst x e' dom)

theorem ComputableTLAPlus.Expression.LC.subst_fn {α : Type} {x : String} {e' : Expression α} {x' : String} {ann cod : α} {dom body : Expression α} (hlc : e'.LC) : subst x e' (fn x' ann cod dom body) = fn x' ann cod (subst x e' dom) (subst x e' body)

theorem ComputableTLAPlus.Expression.subst_except_single {α : Type} {x : String} {e' f : Expression α} {τ : α} {path : List (String ⊕ Expression α)} {rhs : Expression α} : subst x e' (f.except τ [(path, rhs)]) = (subst x e' f).except τ [(List.map (fun (s : String ⊕ Expression α) => Sum.map id (subst x e') s) path, subst x e' rhs)]

theorem ComputableTLAPlus.Expression.subst_case {α : Type} {x : String} {e' : Expression α} {bs : List (Expression α × Expression α)} {other : Option (Expression α)} {τ : α} : subst x e' (case bs other τ) = case (List.map (fun (p : Expression α × Expression α) => (subst x e' p.1, subst x e' p.2)) bs) (Option.map (subst x e') other) τ

theorem ComputableTLAPlus.Expression.subst_openVar_one_comm {α : Type} {x : String} {e' : Expression α} {z : String} (hlc : e'.LC) (hzx : z ≠ x) (body : Expression α) : mapVars (openVarLam z) 0 (mapVars (substLam x e') 1 body) = subst x e' (mapVars (openVarLam z) 0 body)

Opening a binder body one level out commutes with a subst that descended one level into it, when the opened name is distinct from the substituted one and the substituend is locally closed. The .forall/.exists/… case of evalSubst'.

theorem ComputableTLAPlus.Expression.LC.subst_openVar {α : Type} {x z : String} {e' : Expression α} (hlc : e'.LC) (hzx : z ≠ x) (body : Expression α) : openVar z (subst x e' body) = subst x e' (openVar z body)

Opening a substituted body and substituting an opened body agree, once the opened name avoids the substituted one and the substituend is locally closed. The evalSubst' binder step, phrased directly on subst/openVar.

theorem ComputableTLAPlus.Expression.subst_liftBound_comm {α : Type} {x : String} {e' t : Expression α} (hlc : e'.LC) (k : ℕ) : subst x e' (liftBound k t) = liftBound k (subst x e' t)

subst commutes with liftBound when the substituend is locally closed.

LC introduction

theorem ComputableTLAPlus.Expression.LC.varClosed {α : Type} {τ : α} {o : Origin} (ho : ∀ (i : ℕ), o ≠ TypedTLAPlus.Origin.bound i) : (var τ o).LC

A .var at a non-.bound origin is locally closed.

theorem ComputableTLAPlus.Expression.LC.opCall {α : Type} {g : Expression α} {es : List (Expression α)} (hg : g.LC) (hes : ∀ e ∈ es, e.LC) : (g.opCall es).LC

An .opCall of locally-closed parts is locally closed.

theorem ComputableTLAPlus.Expression.LC.except_single {α : Type} {g : Expression α} {τ : α} {path : List (String ⊕ Expression α)} {rhs : Expression α} (hg : g.LC) (hpath : ∀ (e : Expression α), Sum.inr e ∈ path → e.LC) (hrhs : rhs.LC) : (g.except τ [(path, rhs)]).LC

A one-entry except of locally-closed parts is locally closed.

theorem ComputableTLAPlus.Expression.LC.liftBound {α : Type} {e : Expression α} (h : e.LC) (k : ℕ) : (Expression.liftBound k e).LC

liftBound of a locally-closed term is locally closed (it is the term itself).

theorem ComputableTLAPlus.Expression.LC.fnCall {α : Type} {g : Expression α} {fnTyp : α} {e : Expression α} (hg : g.LC) (he : e.LC) : (g.fnCall fnTyp e).LC

A .fnCall of locally-closed parts is locally closed.

theorem ComputableTLAPlus.Expression.LC.recordAccess {α : Type} {g : Expression α} {nm : String} (hg : g.LC) : (g.recordAccess nm).LC

A .recordAccess of a locally-closed part is locally closed.

def ComputableTLAPlus.Expression.substRef {α : Type} (r : ElaboratedPlusCal.Ref α (Expression α)) (rhs e' : Expression α) : Expression α

e'[e\r]: substitutes a preceding r≔e assignment's effect into a later expression e'. A bare-variable r (no .args) substitutes the name directly; a compound r (with field/index segments) instead substitutes the whole variable with [var(r) EXCEPT !path = e]. r.args is already the List (String ⊕ Expression α) shape Expression.except takes, so it is a one-entry except list, no reshaping needed.

Equations

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

The two branches of substRef, named. Both readings get used — ExprSemantics.evalSubstRef (Core/ComputableTLAPlus/Semantics/Interface.lean) proves one case of its ↔ from each — and neither states the @@ tags, which are definitionally transparent (Common/Position.lean) and only noise in a consumer's goal.

theorem ComputableTLAPlus.Expression.substRef_of_args_nil {α : Type} {r : ElaboratedPlusCal.Ref α (Expression α)} (h : r.args = []) (rhs e' : Expression α) : substRef r rhs e' = subst r.name rhs e'

At a bare reference, substRef is plain substitution of the right-hand side.

theorem ComputableTLAPlus.Expression.substRef_of_args_ne_nil {α : Type} {r : ElaboratedPlusCal.Ref α (Expression α)} (h : r.args ≠ []) (rhs e' : Expression α) : substRef r rhs e' = subst r.name ((var r.baseType (TypedTLAPlus.Origin.free r.name)).except r.baseType [(r.args, rhs)]) e'

At a compound reference, substRef substitutes the base variable by a one-entry EXCEPT rebuilding it along the reference's own path.