The concrete ExprSemantics Value instance: TLA⁺ expression evaluation as an inductive relation Eval Ξ Ω M e v, on the Value := ZFSet domain.

Evaluation is a relation, not a function, because a user-defined operator call re-descends into that operator's body — an unrelated syntax tree with no measure a termination checker sees — and because "no derivation" is exactly the meaning of "aborts". A genuinely non-terminating expression (were RECURSIVE ever to return) simply has no finite derivation tree.

Builtin operators are strict in their argument kinds: e₁ /\ e₂ denotes a boolean only when both operands denote booleans, e₁ + e₂ an integer only when both denote integers, and so on. A kind mismatch leaves the call with no value — the type checker is what rules such calls out in practice, so this partiality is never exercised on a well-typed program.

Name resolution follows a .var node's Origin (see ExprSemantics.evalVar): .binder reads memory, .module m consults the operator environment Ξ then the model Ω, .intrinsic denotes nothing on its own and only means something as an opCall head.

Value-level predicates and operations

def ComputableTLAPlus.Operational.IsBool (v : Value) : Prop

The value is one of the two booleans.

Equations

• ComputableTLAPlus.Operational.IsBool v = (v = ComputableTLAPlus.Value.tru ∨ v = ComputableTLAPlus.Value.fls)

def ComputableTLAPlus.Operational.IsInt (v : Value) : Prop

The value is an integer: a member of Integers's Int.

Equations

• ComputableTLAPlus.Operational.IsInt v = (v ∈ ZFSet.Int)

def ComputableTLAPlus.Operational.IsSet (v : Value) : Prop

The value denotes a set, as opposed to a scalar. Under the untagged encoding every value is a ZFSet, so this excludes only the scalar kinds by hand; a non-set with x ∈ e aborting is what it is for.

Equations

• ComputableTLAPlus.Operational.IsSet v = (¬ComputableTLAPlus.Operational.IsBool v ∧ ¬ComputableTLAPlus.Operational.IsInt v)

noncomputable def ComputableTLAPlus.Operational.fnApply {f A B : Value} (hf : ZFSet.IsPFunc f A B) (k : Value) (hk : k ∈ ZFSet.Dom f ⋯) : Value

Function application on a value: zflean's ZFSet.fapply (@ᶻ), which for a partial function f returns the unique w with ⟨k, w⟩ ∈ f. It is genuinely partial — an IsPFunc witness and a domain-membership proof are its inputs — so, unlike a Classical.epsilon stand-in, every use site must have those facts in hand.

Equations

• ComputableTLAPlus.Operational.fnApply hf k hk = ↑(@ᶻf hf ⟨k, hk⟩)

theorem ComputableTLAPlus.Operational.fnApply_spec {f A B : Value} (hf : ZFSet.IsPFunc f A B) {k : Value} (hk : k ∈ ZFSet.Dom f ⋯) : ZFSet.pair k (fnApply hf k hk) ∈ f

fnApply lands where zflean says it does: paired with k in f.

theorem ComputableTLAPlus.Operational.fnApply_eq {f A B : Value} (hf : ZFSet.IsPFunc f A B) {k w : Value} (hk : k ∈ ZFSet.Dom f ⋯) (hw : ZFSet.pair k w ∈ f) : fnApply hf k hk = w

fnApply is pinned by any pair of f at k — f is single-valued.

theorem ComputableTLAPlus.Operational.fnApply_congr {f A₁ B₁ A₂ B₂ : Value} (h₁ : ZFSet.IsPFunc f A₁ B₁) (h₂ : ZFSet.IsPFunc f A₂ B₂) {k : Value} (hk₁ : k ∈ ZFSet.Dom f ⋯) (hk₂ : k ∈ ZFSet.Dom f ⋯) : fnApply h₁ k hk₁ = fnApply h₂ k hk₂

fnApply does not depend on which IsPFunc witness it is taken with.

noncomputable def ComputableTLAPlus.Operational.fnRead (f k : Value) : Value

The set-theoretic read ⋂₀ f[{k}] — the value zflean's fapply reduces to (fapply_eq_Image_singleton), left total (junk ∅ off-domain) so it can drive updatePath's descent, where the recursion has no IsPFunc witness to offer. fnRead_eq_fnApply proves it agrees with fnApply wherever both are defined.

Equations

• ComputableTLAPlus.Operational.fnRead f k = (ZFSet.sep (fun (w : ZFSet.{0}) => ZFSet.pair k w ∈ f) (ZFSet.sUnion f).sUnion).sInter

theorem ComputableTLAPlus.Operational.fnRead_eq_fnApply {f A B : Value} (hf : ZFSet.IsPFunc f A B) {k : Value} (hk : k ∈ ZFSet.Dom f ⋯) : fnRead f k = fnApply hf k hk

fnRead agrees with zflean's fapply on a partial function at a domain point: both name the unique image of k.

noncomputable def ComputableTLAPlus.Operational.fnUpdate (f k w : Value) : Value

f with the key k rebound to w: drop every pair keyed at k, add ⟨k, w⟩. Uses zflean's first projection ZFSet.π₁ rather than reading the old value out first, so it is the correct override for any f with no functionhood precondition.

Equations

• ComputableTLAPlus.Operational.fnUpdate f k w = insert (ZFSet.pair k w) (ZFSet.sep (fun (p : ZFSet.{0}) => p.π₁ ≠ k) f)

noncomputable def ComputableTLAPlus.Operational.updatePath : Value → List (PathStep Value) → Value → Option Value

updatePath old path v — old with the position named by path overwritten by v, none when a .inr index does not resolve. path = [] overwrites outright.

Equations

• One or more equations did not get rendered due to their size.
• ComputableTLAPlus.Operational.updatePath x✝¹ [] x✝ = some x✝

noncomputable def ComputableTLAPlus.Operational.seqAppend (s v : Value) : Option Value

Append to a sequence value: succeeds exactly when s is a sequence, extending its element list on the right.

Equations

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

DOMAIN support

zflean's ZFSet.Dom — the domain of a partial function — needs the ambient A × B the function lives in. EvalBuiltin.domain supplies it as an IsPFunc witness; these three lemmas bridge that form to the graph-level ∃ w, ⟨z, w⟩ ∈ f characterisation the coercion proofs speak in.

theorem ComputableTLAPlus.Operational.mem_dom_iff {f A B : Value} (hf : ZFSet.IsPFunc f A B) {z : Value} : z ∈ ZFSet.Dom f ⋯ ↔ ∃ (w : ZFSet.{0}), ZFSet.pair z w ∈ f

f.Dom holds exactly the keys of f's graph, for f a partial function.

theorem ComputableTLAPlus.Operational.dom_eq_dom {f A₁ B₁ A₂ B₂ : Value} (h₁ : f ⊆ ZFSet.prod A₁ B₁) (h₂ : f ⊆ ZFSet.prod A₂ B₂) : ZFSet.Dom f h₁ = ZFSet.Dom f h₂

f.Dom does not depend on which ambient A × B witness it is taken with.

theorem ComputableTLAPlus.Operational.isPFunc_restrict_dom {f A B : Value} (hf : ZFSet.IsPFunc f A B) : ZFSet.IsPFunc f (ZFSet.Dom f ⋯) B

A partial function is still one over its own domain.

Sequence values

A sequence value is a total function over an index interval 1 .. n (Value.IsSeqVal); its element list is read back index by index. IsSeq s vs — the ExprSemantics.isSeq field — pairs that predicate with the read-back list. isSeq_iff_ofSeq connects it to the Value.ofSeq builder every sequence-valued rule produces.

theorem ComputableTLAPlus.Operational.fnRead_eq {f A B k w : Value} (hf : ZFSet.IsPFunc f A B) (hw : ZFSet.pair k w ∈ f) : fnRead f k = w

fnRead on a partial function returns the value paired with the key.

noncomputable def ComputableTLAPlus.Operational.seqElems (s : Value) : List Value

The element list of a sequence value: its entries at 1 .. Len s, in order. Junk off sequence values.

Equations

• ComputableTLAPlus.Operational.seqElems s = List.map (fun (i : ℕ) => ComputableTLAPlus.Operational.fnRead s (ComputableTLAPlus.Value.ofNat (i + 1))) (List.range s.lenOf)

def ComputableTLAPlus.Operational.IsSeq (s : Value) (vs : List Value) : Prop

s is the sequence value whose elements, in order, are vs: a total function over 1 .. n whose read-back list is vs.

Equations

• ComputableTLAPlus.Operational.IsSeq s vs = (s.IsSeqVal ∧ ComputableTLAPlus.Operational.seqElems s = vs)

theorem ComputableTLAPlus.Operational.fnRead_ofSeq {vs : List Value} {i : ℕ} (hi : i < vs.length) : fnRead (Value.ofSeq vs) (Value.ofNat (i + 1)) = vs[i]

Reading ofSeq vs at index i + 1 gives vs[i].

theorem ComputableTLAPlus.Operational.seqElems_ofSeq (vs : List Value) : seqElems (Value.ofSeq vs) = vs

The read-back list of ofSeq vs is vs.

theorem ComputableTLAPlus.Operational.isSeqVal_iff_ofSeq {s : Value} : s.IsSeqVal ↔ ∃ (vs : List Value), s = Value.ofSeq vs

A sequence value is exactly an ofSeq.

theorem ComputableTLAPlus.Operational.isSeq_iff_ofSeq {s : Value} {vs : List Value} : IsSeq s vs ↔ s = Value.ofSeq vs

IsSeq s vs holds exactly when s is the Value.ofSeq of vs — the bridge to every sequence-valued rule, which produces ofSeq directly.

theorem ComputableTLAPlus.Operational.isSeq_ofSeq (vs : List Value) : IsSeq (Value.ofSeq vs) vs

ofSeq vs is the sequence value of vs.

Expression evaluation

def ComputableTLAPlus.Operational.substParams (_params : List (String × ℕ)) (args : List (Expression Typ)) (body : Expression Typ) : Expression Typ

Substitute a call's actual arguments for its operator's formal parameters. The parameters form a de Bruijn binder over body in declaration order (Op(a, b) ⇒ a is .bound 1, b is .bound 0, Elaborator/Context.lean), so the arguments are instantiated innermost-first. params is carried only for the arity check at the call rule; capture is impossible — .bound and .free are disjoint.

Equations

• ComputableTLAPlus.Operational.substParams _params args body = ComputableTLAPlus.Expression.instantiate args.reverse body

theorem ComputableTLAPlus.Operational.substParams_freeVars {params : List (String × ℕ)} {args : List (Expression Typ)} {body : Expression Typ} {z : String} (_hlen : params.length = args.length) (hz : z ∈ (substParams params args body).freeVars) : z ∈ body.freeVars ∨ ∃ a ∈ args, z ∈ a.freeVars

A name free in a fully-applied substParams is either free in body or free in one of the arguments substituted in. evalLocal'/evalSubst' need this for their opCall_op case, since the derivation there recurses into this substituted body rather than a subterm of the call.

theorem ComputableTLAPlus.Operational.subst_substParams {x : String} {e' : Expression Typ} (hlc : e'.LC) {params : List (String × ℕ)} {args : List (Expression Typ)} {body : Expression Typ} (hbody : x ∉ body.freeVars) : Expression.subst x e' (substParams params args body) = substParams params (List.map (Expression.subst x e') args) body

subst pushes through substParams when the substituend is locally closed and the operator body is closed (Ξ.WellScoped): it lands on the arguments only. The opCall_op step of evalSubst', whose sub-derivation is on substParams params args body, not a call subterm.

theorem ComputableTLAPlus.Operational.subst_var_of_builtin {x : String} {e' : Expression Typ} {τ : Typ} {o : Origin} {op : TypedTLAPlus.BuiltinOp} (hop : TypedTLAPlus.builtinOpOf? o = some op) : Expression.subst x e' (Expression.var τ o) = Expression.var τ o

A builtin call's head origin (.module/.intrinsic) is untouched by subst.

inductive ComputableTLAPlus.Operational.Eval (Ξ : OperatorEnv) (Ω : Model Value) : Memory Value → Expression Typ → Value → Prop

Eval Ξ Ω M e v — under operator environment Ξ, model Ω, and memory M, expression e denotes v. Mutually defined with EvalList (a list of expressions against a list of values), EvalPath (a reference's syntactic access path against its resolved one), and EvalBuiltin (a builtin operator call, declared last in this block — see its own doc comment for why: mutual recursor motive numbering follows declaration order, and EvalList/EvalPath's existing motive_2/motive_3 call sites fix that order). A nested List.Forall₂ or ResolvesPath cannot carry Eval through the kernel's positivity check, so all three companions are inlined as mutual members. Every recursive premise mentions Eval directly — never wrapped in And/Exists/Iff, which the kernel rejects when the other arguments carry local variables.

• nat {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {s : String} {n : ℕ} (hn : s.toNat? = some n) : Eval Ξ Ω M (Expression.nat s) (Value.ofNat n)
• str {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {s : String} : Eval Ξ Ω M (Expression.str s) (Value.ofString s)
• tru {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} : Eval Ξ Ω M Expression.true Value.tru
• fls {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} : Eval Ξ Ω M Expression.false Value.fls
• var_free {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {name : String} {v : Value} (h : Finmap.lookup name M = some v) : Eval Ξ Ω M (Expression.var τ (TypedTLAPlus.Origin.free name)) v
• var_op0 {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {m name : String} {body : Expression Typ} {v : Value} (hΞ : Ξ m name = some ([], body)) (hnb : TypedTLAPlus.builtinOpOf? (TypedTLAPlus.Origin.module m name) = none) (hb : Eval Ξ Ω M body v) : Eval Ξ Ω M (Expression.var τ (TypedTLAPlus.Origin.module m name)) v
• var_const {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {m name : String} {v : Value} (hΞ : Ξ m name = none) (hnb : TypedTLAPlus.builtinOpOf? (TypedTLAPlus.Origin.module m name) = none) (hΩ : Ω m name = some v) : Eval Ξ Ω M (Expression.var τ (TypedTLAPlus.Origin.module m name)) v
• natSet {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} : Eval Ξ Ω M (Expression.var τ (TypedTLAPlus.Origin.module "Naturals" "Nat")) Value.natSet
• intSet {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} : Eval Ξ Ω M (Expression.var τ (TypedTLAPlus.Origin.module "Integers" "Int")) ZFSet.Int
• opCall_op {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {m name : String} {params : List (String × ℕ)} {body : Expression Typ} {args : List (Expression Typ)} {v : Value} (hΞ : Ξ m name = some (params, body)) (hnb : TypedTLAPlus.builtinOpOf? (TypedTLAPlus.Origin.module m name) = none) (hlen : params.length = args.length) (hb : Eval Ξ Ω M (substParams params args body) v) (hargs : args ≠ []) : Eval Ξ Ω M ((Expression.var τ (TypedTLAPlus.Origin.module m name)).opCall args) v
• opCall_builtin {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {o : Origin} {op : TypedTLAPlus.BuiltinOp} {args : List (Expression Typ)} {v : Value} (hop : TypedTLAPlus.builtinOpOf? o = some op) (hb : EvalBuiltin Ξ Ω M op args v) : Eval Ξ Ω M ((Expression.var τ o).opCall args) v
• forall_true {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {τ : Typ} {dom body : Expression Typ} {S : Value} (L : Finset String) (hdom : Eval Ξ Ω M dom S) (hall : ∀ z ∉ L, ∀ w ∈ S, Eval Ξ Ω (Finmap.insert z w M) (Expression.openVar z body) Value.tru) : Eval Ξ Ω M (Expression.forall x τ dom body) Value.tru
• forall_false {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {τ : Typ} {dom body : Expression Typ} {S w : Value} (L : Finset String) (hdom : Eval Ξ Ω M dom S) (hw : w ∈ S) (hbody : ∀ z ∉ L, Eval Ξ Ω (Finmap.insert z w M) (Expression.openVar z body) Value.fls) : Eval Ξ Ω M (Expression.forall x τ dom body) Value.fls
• exists_true {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {τ : Typ} {dom body : Expression Typ} {S w : Value} (L : Finset String) (hdom : Eval Ξ Ω M dom S) (hw : w ∈ S) (hbody : ∀ z ∉ L, Eval Ξ Ω (Finmap.insert z w M) (Expression.openVar z body) Value.tru) : Eval Ξ Ω M (Expression.exists x τ dom body) Value.tru
• exists_false {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {τ : Typ} {dom body : Expression Typ} {S : Value} (L : Finset String) (hdom : Eval Ξ Ω M dom S) (hall : ∀ z ∉ L, ∀ w ∈ S, Eval Ξ Ω (Finmap.insert z w M) (Expression.openVar z body) Value.fls) : Eval Ξ Ω M (Expression.exists x τ dom body) Value.fls
• choose {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {τ : Typ} {dom pred : Expression Typ} {S : Value} (filt : Value → Value) (L : Finset String) (hdom : Eval Ξ Ω M dom S) (hfilt : ∀ z ∉ L, ∀ w ∈ S, Eval Ξ Ω (Finmap.insert z w M) (Expression.openVar z pred) (filt w)) : Eval Ξ Ω M (Expression.choose x τ dom pred) (Classical.epsilon fun (w : Value) => w ∈ S ∧ filt w = Value.tru)
• set {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {es : List (Expression Typ)} {τ : Typ} {vs : List Value} (hes : EvalList Ξ Ω M es vs) : Eval Ξ Ω M (Expression.set es τ) (Value.ofFinSet vs)
• collect {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {τ : Typ} {dom pred : Expression Typ} {S : Value} (filt : Value → Value) (L : Finset String) (hdom : Eval Ξ Ω M dom S) (hfilt : ∀ y ∉ L, ∀ z ∈ S, Eval Ξ Ω (Finmap.insert y z M) (Expression.openVar y pred) (filt z)) : Eval Ξ Ω M (Expression.collect x τ dom pred) (ZFSet.sep (fun (z : ZFSet.{0}) => filt z = Value.tru) S)
• map' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {body : Expression Typ} {x : String} {ann cod : Typ} {dom : Expression Typ} {S v : Value} (img : Value → Value) (L : Finset String) (hdom : Eval Ξ Ω M dom S) (himg : ∀ z ∉ L, ∀ w ∈ S, Eval Ξ Ω (Finmap.insert z w M) (Expression.openVar z body) (img w)) (hto : ∀ z ∈ v, ∃ w ∈ S, z = img w) (hof : ∀ w ∈ S, img w ∈ v) : Eval Ξ Ω M (body.map' x ann cod dom) v
• fnCall {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {f : Expression Typ} {fnTyp : Typ} {arg : Expression Typ} {r k A B : Value} (hf : Eval Ξ Ω M f r) (hk : Eval Ξ Ω M arg k) (hpf : ZFSet.IsPFunc r A B) (hkdom : k ∈ ZFSet.Dom r ⋯) : Eval Ξ Ω M (f.fnCall fnTyp arg) (fnApply hpf k hkdom)
• fn {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {ann cod : Typ} {dom body : Expression Typ} {S G : Value} (img : Value → Value) (L : Finset String) (hdom : Eval Ξ Ω M dom S) (himg : ∀ z ∉ L, ∀ w ∈ S, Eval Ξ Ω (Finmap.insert z w M) (Expression.openVar z body) (img w)) (hto : ∀ z ∈ G, ∃ w ∈ S, z = w.pair (img w)) (hof : ∀ w ∈ S, w.pair (img w) ∈ G) : Eval Ξ Ω M (Expression.fn x ann cod dom body) G
• record {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {fs : List (Typ × String × Expression Typ)} {vs : List Value} (hfne : fs ≠ []) (hfs : EvalList Ξ Ω M (List.map (fun (x : Typ × String × Expression Typ) => x.2.2) fs) vs) : Eval Ξ Ω M (Expression.record fs) (Value.ofRecord ((List.map (fun (x : Typ × String × Expression Typ) => x.2.1) fs).zip vs))
• recordAccess {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {e : Expression Typ} {name : String} {r A B : Value} (he : Eval Ξ Ω M e r) (hpf : ZFSet.IsPFunc r A B) (hkdom : Value.ofString name ∈ ZFSet.Dom r ⋯) : Eval Ξ Ω M (e.recordAccess name) (fnApply hpf (Value.ofString name) hkdom)
• tuple {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {ets : List (Typ × Expression Typ)} {vs : List Value} (hets : ets ≠ []) (hes : EvalList Ξ Ω M (List.map (fun (x : Typ × Expression Typ) => x.2) ets) vs) : Eval Ξ Ω M (Expression.tuple ets) (Value.ofTuple vs)
• seq {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {es : List (Expression Typ)} {τ : Typ} {vs : List Value} (hes : EvalList Ξ Ω M es vs) : Eval Ξ Ω M (Expression.seq es τ) (Value.ofSeq vs)
• except {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {f : Expression Typ} {τ : Typ} {path : List (String ⊕ Expression Typ)} {rhs : Expression Typ} {vf vr v : Value} {resolved : List (PathStep Value)} (hf : Eval Ξ Ω M f vf) (hpath : EvalPath Ξ Ω M path resolved) (hrhs : Eval Ξ Ω M rhs vr) (hv : updatePath vf resolved vr = some v) : Eval Ξ Ω M (f.except τ [(path, rhs)]) v
• if_true {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {c t e : Expression Typ} {τ : Typ} {v : Value} (hc : Eval Ξ Ω M c Value.tru) (ht : Eval Ξ Ω M t v) : Eval Ξ Ω M (c.if t e τ) v
• if_false {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {c t e : Expression Typ} {τ : Typ} {v : Value} (hc : Eval Ξ Ω M c Value.fls) (he : Eval Ξ Ω M e v) : Eval Ξ Ω M (c.if t e τ) v
• case_hit {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {bs : List (Expression Typ × Expression Typ)} {other : Option (Expression Typ)} {τ : Typ} {i : ℕ} {p q : Expression Typ} {v : Value} (hi : bs[i]? = some (p, q)) (hbefore : ∀ j < i, ∀ (p' q' : Expression Typ), bs[j]? = some (p', q') → Eval Ξ Ω M p' Value.fls) (hp : Eval Ξ Ω M p Value.tru) (hq : Eval Ξ Ω M q v) : Eval Ξ Ω M (Expression.case bs other τ) v
• case_other {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {bs : List (Expression Typ × Expression Typ)} {e : Expression Typ} {τ : Typ} {v : Value} (hbefore : ∀ (j : ℕ) (p' q' : Expression Typ), bs[j]? = some (p', q') → Eval Ξ Ω M p' Value.fls) (hq : Eval Ξ Ω M e v) : Eval Ξ Ω M (Expression.case bs (some e) τ) v

inductive ComputableTLAPlus.Operational.EvalList (Ξ : OperatorEnv) (Ω : Model Value) : Memory Value → List (Expression Typ) → List Value → Prop

A list of expressions evaluated pointwise.

• nil {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} : EvalList Ξ Ω M [] []
• cons {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {e : Expression Typ} {v : Value} {es : List (Expression Typ)} {vs : List Value} (h : Eval Ξ Ω M e v) (hs : EvalList Ξ Ω M es vs) : EvalList Ξ Ω M (e :: es) (v :: vs)

inductive ComputableTLAPlus.Operational.EvalPath (Ξ : OperatorEnv) (Ω : Model Value) : Memory Value → List (String ⊕ Expression Typ) → List (PathStep Value) → Prop

A reference's syntactic access path resolved: field segments carry over, index expressions evaluate. The EvalPath companion of ExprSemantics.ResolvesPath.

• nil {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} : EvalPath Ξ Ω M [] []
• inl {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {f : String} {rest : List (String ⊕ Expression Typ)} {resolved : List (PathStep Value)} (h : EvalPath Ξ Ω M rest resolved) : EvalPath Ξ Ω M (Sum.inl f :: rest) (Sum.inl f :: resolved)
• inr {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {e : Expression Typ} {v : Value} {rest : List (String ⊕ Expression Typ)} {resolved : List (PathStep Value)} (h : Eval Ξ Ω M e v) (hs : EvalPath Ξ Ω M rest resolved) : EvalPath Ξ Ω M (Sum.inr e :: rest) (Sum.inr v :: resolved)

inductive ComputableTLAPlus.Operational.EvalBuiltin (Ξ : OperatorEnv) (Ω : Model Value) : Memory Value → TypedTLAPlus.BuiltinOp → List (Expression Typ) → Value → Prop

EvalBuiltin Ξ Ω M op args v — the builtin op, called on argument expressions args under Ξ/Ω/M, denotes v. Mutual with Eval (unlike before this operator joined the family): most arms evaluate every argument through an ordinary Eval premise, the same per-argument style Eval.fnCall/Eval.except/Eval.recordAccess already use elsewhere in this file — EvalList's old "evaluate every argument uniformly, then hand EvalBuiltin the values" no longer fits once an argument can be an operator reference rather than a value (bagOfAll/mkSeq, whose own argument F is called via a synthesized .opCall under a fresh binder, mirroring Eval.forall_true/ Eval.map'/Eval.fn's existence-law style rather than being evaluated itself). Strict in argument kinds otherwise: an arm exists only for the shapes the operator is defined on. Covers every operator reachable from a computable algorithm except Cardinality/IsFiniteSet and the Address order (\prec/\preceq/\succ/\succeq) — no arm for those, each already total and closed-form elsewhere (every Value set is finite by construction; the Address order is deliberately unspecified at this layer).

Set-valued results are given by a ZFSet/zflean term wherever one exists (∪/∩/\ for the set combinators, f.Dom for DOMAIN), and by a closed-form Value builder otherwise (Value.intRange for ..). bagOfAll/mkSeq characterise their result by an existence law instead, same reason Eval.fn/Eval.map' do: "which value did F return at w" is itself an Eval fact, not a closed-form term.

Declared last in this mutual block on purpose: the generated combined recursor numbers its sibling motives (motive_2, motive_3, …) by declaration order, and evalUnique'/evalLocal' already fix EvalList/EvalPath as motive_2/motive_3 — putting EvalBuiltin first would have shifted those, breaking every existing call site instead of just adding a new motive_4.

• eq_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ a) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.eq [a₁, a₂] Value.tru
• eq_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a b : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ b) (h : a ≠ b) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.eq [a₁, a₂] Value.fls
• neq_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a b : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ b) (h : a ≠ b) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.neq [a₁, a₂] Value.tru
• neq_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ a) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.neq [a₁, a₂] Value.fls
• and_tt {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} (h₁ : Eval Ξ Ω M a₁ Value.tru) (h₂ : Eval Ξ Ω M a₂ Value.tru) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.and [a₁, a₂] Value.tru
• and_ff {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a b : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ b) (ha : IsBool a) (hb : IsBool b) (h : a = Value.fls ∨ b = Value.fls) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.and [a₁, a₂] Value.fls
• or_tt {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a b : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ b) (ha : IsBool a) (hb : IsBool b) (h : a = Value.tru ∨ b = Value.tru) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.or [a₁, a₂] Value.tru
• or_ff {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} (h₁ : Eval Ξ Ω M a₁ Value.fls) (h₂ : Eval Ξ Ω M a₂ Value.fls) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.or [a₁, a₂] Value.fls
• implies_t {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a b : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ b) (ha : IsBool a) (hb : IsBool b) (h : a = Value.fls ∨ b = Value.tru) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.implies [a₁, a₂] Value.tru
• implies_f {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} (h₁ : Eval Ξ Ω M a₁ Value.tru) (h₂ : Eval Ξ Ω M a₂ Value.fls) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.implies [a₁, a₂] Value.fls
• iff_t {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ a) (ha : IsBool a) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.iff [a₁, a₂] Value.tru
• iff_f {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a b : Value} (h₁ : Eval Ξ Ω M a₁ a) (h₂ : Eval Ξ Ω M a₂ b) (ha : IsBool a) (hb : IsBool b) (h : a ≠ b) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.iff [a₁, a₂] Value.fls
• neg_t {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} (h : Eval Ξ Ω M a Value.tru) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.neg [a] Value.fls
• neg_f {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} (h : Eval Ξ Ω M a Value.fls) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.neg [a] Value.tru
• inSet_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a S : Expression Typ} {av Sv : Value} (ha : Eval Ξ Ω M a av) (hS : Eval Ξ Ω M S Sv) (h : av ∈ Sv) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.inSet [a, S] Value.tru
• inSet_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a S : Expression Typ} {av Sv : Value} (ha : Eval Ξ Ω M a av) (hS : Eval Ξ Ω M S Sv) (h : av ∉ Sv) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.inSet [a, S] Value.fls
• notInSet_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a S : Expression Typ} {av Sv : Value} (ha : Eval Ξ Ω M a av) (hS : Eval Ξ Ω M S Sv) (h : av ∉ Sv) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.notInSet [a, S] Value.tru
• notInSet_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a S : Expression Typ} {av Sv : Value} (ha : Eval Ξ Ω M a av) (hS : Eval Ξ Ω M S Sv) (h : av ∈ Sv) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.notInSet [a, S] Value.fls
• subseteq_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {A B : Value} (h₁ : Eval Ξ Ω M a₁ A) (h₂ : Eval Ξ Ω M a₂ B) (h : A ⊆ B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.subseteq [a₁, a₂] Value.tru
• subseteq_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {A B : Value} (h₁ : Eval Ξ Ω M a₁ A) (h₂ : Eval Ξ Ω M a₂ B) (h : ¬A ⊆ B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.subseteq [a₁, a₂] Value.fls
• cup {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {A B : Value} (h₁ : Eval Ξ Ω M a₁ A) (h₂ : Eval Ξ Ω M a₂ B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.cup [a₁, a₂] (A ∪ B)
• cap {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {A B : Value} (h₁ : Eval Ξ Ω M a₁ A) (h₂ : Eval Ξ Ω M a₂ B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.cap [a₁, a₂] (A ∩ B)
• setMinus {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {A B : Value} (h₁ : Eval Ξ Ω M a₁ A) (h₂ : Eval Ξ Ω M a₂ B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.setMinus [a₁, a₂] (A \ B)
• cartesianProduct {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {A B : Value} (h₁ : Eval Ξ Ω M a₁ A) (h₂ : Eval Ξ Ω M a₂ B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.cartesianProduct [a₁, a₂] (A.cartesian B)
• domain {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {f A B : Value} (ha : Eval Ξ Ω M a f) (hf : ZFSet.IsPFunc f A B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.domain [a] (ZFSet.Dom f ⋯)
• plus {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.plus [a₁, a₂] (Value.ofInt (x + y))
• minus {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.minus [a₁, a₂] (Value.ofInt (x - y))
• unaryMinus {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {x : ℤ} (h : Eval Ξ Ω M a (Value.ofInt x)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.unaryMinus [a] (Value.ofInt (-x))
• times {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.times [a₁, a₂] (Value.ofInt (x * y))
• intDiv {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.intDiv [a₁, a₂] (Value.ofInt (x.fdiv y))
• mod {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.mod [a₁, a₂] (Value.ofInt (x.fmod y))
• pow {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.pow [a₁, a₂] (Value.ofInt (x ^ y.toNat))
• lt_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : x < y) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.lt [a₁, a₂] Value.tru
• lt_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : ¬x < y) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.lt [a₁, a₂] Value.fls
• gt_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : y < x) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.gt [a₁, a₂] Value.tru
• gt_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : ¬y < x) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.gt [a₁, a₂] Value.fls
• leq_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : x ≤ y) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.leq [a₁, a₂] Value.tru
• leq_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : ¬x ≤ y) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.leq [a₁, a₂] Value.fls
• geq_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : y ≤ x) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.geq [a₁, a₂] Value.tru
• geq_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {x y : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt x)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt y)) (h : ¬y ≤ x) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.geq [a₁, a₂] Value.fls
• dotdot {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {a b : ℤ} (h₁ : Eval Ξ Ω M a₁ (Value.ofInt a)) (h₂ : Eval Ξ Ω M a₂ (Value.ofInt b)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.dotdot [a₁, a₂] (Value.intRange a b)
• len {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {vs : List Value} (h : Eval Ξ Ω M a (Value.ofSeq vs)) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.len [a] (Value.ofNat vs.length)
• head {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {v : Value} {vs : List Value} (h : Eval Ξ Ω M a (Value.ofSeq (v :: vs))) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.head [a] v
• tail {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {v : Value} {vs : List Value} (h : Eval Ξ Ω M a (Value.ofSeq (v :: vs))) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.tail [a] (Value.ofSeq vs)
• append {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {vs : List Value} {x : Value} (h₁ : Eval Ξ Ω M a₁ (Value.ofSeq vs)) (h₂ : Eval Ξ Ω M a₂ x) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.append [a₁, a₂] (Value.ofSeq (vs ++ [x]))
• strToSeq {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {v : Value} (h : Eval Ξ Ω M a v) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.strToSeq [a] v
• funAsSeq {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {f : Value} (h : Eval Ξ Ω M a f) (hf : f.IsSeqVal) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.funAsSeq [a] f
• setAsFun {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {S A B : Value} (ha : Eval Ξ Ω M a S) (h : ZFSet.IsPFunc S A B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.setAsFun [a] S
• emptyBag {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.emptyBag [] ∅
• setToBag {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {S : Value} (h : Eval Ξ Ω M a S) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.setToBag [a] S.setToBag
• bagAdd {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {B1 B2 : Value} (h₁ : Eval Ξ Ω M a₁ B1) (h₂ : Eval Ξ Ω M a₂ B2) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagAdd [a₁, a₂] (B1.bagAdd B2)
• bagSub {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {B1 B2 : Value} (h₁ : Eval Ξ Ω M a₁ B1) (h₂ : Eval Ξ Ω M a₂ B2) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagSub [a₁, a₂] (B1.bagSub B2)
• subBag {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {B : Value} (h : Eval Ξ Ω M a B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.subBag [a] B.subBag
• copiesIn {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {e B : Value} (h₁ : Eval Ξ Ω M a₁ e) (h₂ : Eval Ξ Ω M a₂ B) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.copiesIn [a₁, a₂] (Value.ofNat (e.copiesInRaw B))
• bagUnion {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {S : Value} (h : Eval Ξ Ω M a S) (hS : ZFSet.IsFinite S) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagUnion [a] (S.bagUnion hS)
• bagCardinality {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {B : Value} (h : Eval Ξ Ω M a B) (hB : ZFSet.IsFinite B.rawDom) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagCardinality [a] (Value.ofNat (B.bagCardinality hB))
• isABag {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {B : Value} (h : Eval Ξ Ω M a B) (hb : B.IsBagVal) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.isABag [a] Value.tru
• bagToSet {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {B : Value} (h : Eval Ξ Ω M a B) (hb : B.IsBagVal) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagToSet [a] B.rawDom
• bagIn_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {e B : Value} (h₁ : Eval Ξ Ω M a₁ e) (h₂ : Eval Ξ Ω M a₂ B) (he : e ∈ B.rawDom) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagIn [a₁, a₂] Value.tru
• bagIn_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {e B : Value} (h₁ : Eval Ξ Ω M a₁ e) (h₂ : Eval Ξ Ω M a₂ B) (he : e ∉ B.rawDom) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagIn [a₁, a₂] Value.fls
• bagLeq_pos {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {B1 B2 : Value} (h₁ : Eval Ξ Ω M a₁ B1) (h₂ : Eval Ξ Ω M a₂ B2) (h : ∀ e ∈ B1.rawDom, Value.copiesInRaw e B1 ≤ Value.copiesInRaw e B2) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagLeq [a₁, a₂] Value.tru
• bagLeq_neg {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a₁ a₂ : Expression Typ} {B1 B2 : Value} (h₁ : Eval Ξ Ω M a₁ B1) (h₂ : Eval Ξ Ω M a₂ B2) (h : ¬∀ e ∈ B1.rawDom, Value.copiesInRaw e B1 ≤ Value.copiesInRaw e B2) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagLeq [a₁, a₂] Value.fls
• mkSeq {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {N F : Expression Typ} {n : ℤ} {v : Value} (hN : Eval Ξ Ω M N (Value.ofInt n)) (img : Value → Value) (L : Finset String) (himg : ∀ z ∉ L, ∀ w ∈ Value.intRange 1 n, Eval Ξ Ω (Finmap.insert z w M) (F.opCall [Expression.var (SurfaceTLAPlus.Typ.var "_") (TypedTLAPlus.Origin.free z)]) (img w)) (hto : ∀ e ∈ v, ∃ w ∈ Value.intRange 1 n, e = w.pair (img w)) (hof : ∀ w ∈ Value.intRange 1 n, w.pair (img w) ∈ v) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.mkSeq [N, F] v
• bagOfAll {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {F B : Expression Typ} {Bval v : Value} (hB : Eval Ξ Ω M B Bval) (img : Value → Value) (L : Finset String) (hfin : ZFSet.IsFinite Bval.rawDom) (himg : ∀ z ∉ L, ∀ w ∈ Bval.rawDom, Eval Ξ Ω (Finmap.insert z w M) (F.opCall [Expression.var (SurfaceTLAPlus.Typ.var "_") (TypedTLAPlus.Origin.free z)]) (img w)) (hto : ∀ z ∈ v, ∃ (e : Value), (∃ w ∈ Bval.rawDom, e = img w) ∧ z = ZFSet.pair e (Value.ofNat (hfin.sum fun (w : ZFSet.{0}) => if img w = e then Value.copiesInRaw w Bval else 0))) (hof : ∀ w ∈ Bval.rawDom, ZFSet.pair (img w) (Value.ofNat (hfin.sum fun (w' : ZFSet.{0}) => if img w' = img w then Value.copiesInRaw w' Bval else 0)) ∈ v) : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.bagOfAll [F, B] v

Coercions

@[irreducible]

def ComputableTLAPlus.Operational.coerce : TypedTLAPlus.Coercion → Value → Value → Prop

coerce c v v' — the coercion c carries v to v'. Some <: witnesses are the identity on the untagged encoding: a string is already its code-point sequence (strToSeq). The rest describe the built expression's actual effect on v — either type-changing work (set/tuple/record/ function remapping element types) or a re-view whose result only coincides with v when v has the right shape (tupleToSeq: v must have entries at keys 1..n; the built <<v[1], …, v[n]>> denotes something else otherwise, and Eval.fnCall's domain premise makes it denote nothing when an entry is missing). A case that reads v at a key k names the read value existentially with a paired ⟨k, vk⟩ ∈ v, and (tupleToSeq/tuple/record/function) an ∃ A B, v.IsPFunc A B witness — the two facts Eval.fnCall/recordAccess demand, so evalCoerce can rebuild the derivation backwards.

A recursion on c, not an indexed inductive: evalCoerce' and coerceUnique both recurse on the Coercion structure and simp only [coerce] to expose each arm's ∃/∀/↔ body for iff_rintro; an inductive would replace every such unfold with a bespoke inversion lemma. The termination obligation it saves is one calc (the .tuple arm) plus sizeOf_record_field.

Equations

• One or more equations did not get rendered due to their size.
• ComputableTLAPlus.Operational.coerce TypedTLAPlus.Coercion.id x✝¹ x✝ = (x✝ = x✝¹)
• ComputableTLAPlus.Operational.coerce TypedTLAPlus.Coercion.strToSeq x✝¹ x✝ = (x✝ = x✝¹)
• ComputableTLAPlus.Operational.coerce (TypedTLAPlus.Coercion.seqToFun τ i) x✝¹ x✝ = ((∃ (vs : List ComputableTLAPlus.Value), ComputableTLAPlus.Operational.IsSeq x✝¹ vs) ∧ x✝ = x✝¹)
• ComputableTLAPlus.Operational.coerce (TypedTLAPlus.Coercion.bagToFun τ i) x✝¹ x✝ = (x✝¹.IsBagVal ∧ x✝ = x✝¹)
• ComputableTLAPlus.Operational.coerce (c₁.comp c₂) x✝¹ x✝ = ∃ (mid : ComputableTLAPlus.Value), ComputableTLAPlus.Operational.coerce c₁ x✝¹ mid ∧ ComputableTLAPlus.Operational.coerce c₂ mid x✝

The instance

@[reducible, inline]

abbrev ComputableTLAPlus.Operational.Aborts (Ξ : OperatorEnv) (Ω : Model Value) (M : Memory Value) (e : Expression Typ) : Prop

Aborts in the concrete instance's own vocabulary.

Equations

• ComputableTLAPlus.Operational.Aborts Ξ Ω M e = ¬∃ (v : ComputableTLAPlus.Value), ComputableTLAPlus.Operational.Eval Ξ Ω M e v

theorem ComputableTLAPlus.Operational.updatePath_nil' {old v : Value} : updatePath old [] v = some v

theorem ComputableTLAPlus.Operational.isSeq_inj' {s : Value} {vs ws : List Value} (h : IsSeq s vs) (h' : IsSeq s ws) : vs = ws

theorem ComputableTLAPlus.Operational.isSeq_tail' {s v : Value} {vs : List Value} : IsSeq s (v :: vs) → ∃ (t : Value), IsSeq t vs

theorem ComputableTLAPlus.Operational.eval_seq_nil' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} : ∃ (s : Value), Eval Ξ Ω M (Expression.seq [] τ) s ∧ IsSeq s []

theorem ComputableTLAPlus.Operational.seqAppend_isSeq' {s v : Value} {vs : List Value} (h : IsSeq s vs) : ∃ (s' : Value), seqAppend s v = some s' ∧ IsSeq s' (vs ++ [v])

theorem ComputableTLAPlus.Operational.evalVar' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {o : Origin} {v : Value} : Eval Ξ Ω M (Expression.var τ o) v ↔ match o with | TypedTLAPlus.Origin.bound idx => False | TypedTLAPlus.Origin.free name => Finmap.lookup name M = some v | TypedTLAPlus.Origin.intrinsic name => False | TypedTLAPlus.Origin.module m name => match TypedTLAPlus.builtinOpOf? (TypedTLAPlus.Origin.module m name) with | some TypedTLAPlus.BuiltinOp.natSet => v = Value.natSet | some TypedTLAPlus.BuiltinOp.intSet => v = ZFSet.Int | some val => False | none => match Ξ m name with | some ([], body) => Eval Ξ Ω M body v | some (head :: tail, snd) => False | none => Ω m name = some v

theorem ComputableTLAPlus.Operational.evalBuiltin_len_inv {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {b : Value} (h : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.len [a] b) : ∃ (vs : List Value), Eval Ξ Ω M a (Value.ofSeq vs) ∧ b = Value.ofNat vs.length

Len denotes only on sequences — inversion.

theorem ComputableTLAPlus.Operational.evalBuiltin_dotdot_inv {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a b : Expression Typ} {s : Value} (h : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.dotdot [a, b] s) : ∃ (x : ℤ) (y : ℤ), Eval Ξ Ω M a (Value.ofInt x) ∧ Eval Ξ Ω M b (Value.ofInt y) ∧ ∀ (z : ZFSet.{0}), z ∈ s ↔ ∃ (k : ℤ), x ≤ k ∧ k ≤ y ∧ z = Value.ofInt k

.. builds an integer interval — inversion.

theorem ComputableTLAPlus.Operational.evalBuiltin_domain_inv {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {s : Value} (h : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.domain [a] s) : ∃ (f : Value), Eval Ξ Ω M a f ∧ ∀ (z : ZFSet.{0}), z ∈ s ↔ ∃ (w : ZFSet.{0}), z.pair w ∈ f

DOMAIN denotes the set of keys of a function value — inversion.

theorem ComputableTLAPlus.Operational.evalBuiltin_domain_isPFunc {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a : Expression Typ} {s : Value} (h : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.domain [a] s) : ∃ (f : Value) (B : ZFSet.{0}), Eval Ξ Ω M a f ∧ ZFSet.IsPFunc f s B

DOMAIN denotes a set over which its argument is still a partial function — inversion.

theorem ComputableTLAPlus.Operational.evalBuiltin_eq_inv {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {a b : Expression Typ} {c : Value} (h : EvalBuiltin Ξ Ω M TypedTLAPlus.BuiltinOp.eq [a, b] c) : (∃ (v : Value), Eval Ξ Ω M a v ∧ Eval Ξ Ω M b v ∧ c = Value.tru) ∨ ∃ (v : Value) (w : Value), Eval Ξ Ω M a v ∧ Eval Ξ Ω M b w ∧ v ≠ w ∧ c = Value.fls

= on values denotes TRUE on equal arguments, FALSE otherwise — inversion.

theorem ComputableTLAPlus.Operational.evalOpCall1_inv {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {o : Origin} {op : TypedTLAPlus.BuiltinOp} {arg : Expression Typ} {s : Value} (hname : TypedTLAPlus.builtinOpOf? o = some op) (h : Eval Ξ Ω M ((Expression.var τ o).opCall [arg]) s) : EvalBuiltin Ξ Ω M op [arg] s

A one-argument builtin call inverts to the builtin step directly — EvalBuiltin already carries its own argument's Eval sub-derivation, so there is no separate value to extract first. The opCall_op alternative cannot fire: its hnb says the name is not a builtin, contradicting the premise that it is.

theorem ComputableTLAPlus.Operational.evalOpCall2_inv {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {o : Origin} {op : TypedTLAPlus.BuiltinOp} {a1 a2 : Expression Typ} {s : Value} (hname : TypedTLAPlus.builtinOpOf? o = some op) (h : Eval Ξ Ω M ((Expression.var τ o).opCall [a1, a2]) s) : EvalBuiltin Ξ Ω M op [a1, a2] s

A two-argument builtin call inverts to the builtin step directly.

theorem ComputableTLAPlus.Operational.evalUnique' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {e : Expression Typ} {v w : Value} (h₁ : Eval Ξ Ω M e v) (h₂ : Eval Ξ Ω M e w) : v = w

Evaluation is deterministic: an expression denotes at most one value. Proved through the mutual recursor Eval.rec — induction does not fire on a member of a mutual inductive family, so the EvalList/EvalPath determinism is threaded in as motive_2/motive_3 and discharged in the same pass. motive_4 is EvalBuiltinMotive (see its own doc) — the opCall_builtin step case-splits on op to pick the right shape back up.

theorem ComputableTLAPlus.Operational.evalBuiltinUnique {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {op : TypedTLAPlus.BuiltinOp} {args : List (Expression Typ)} {v w : Value} (h₁ : EvalBuiltin Ξ Ω M op args v) (h₂ : EvalBuiltin Ξ Ω M op args w) : v = w

Determinism for the builtin-operator relation: each (op, args) pair EvalBuiltin is defined on denotes a single value. Against full Eval determinism, so it is stated here rather than beside evalBuiltinUnique_of — its argument-wise premise is evalUnique'. mkSeq/bagOfAll case-split out first: their own img reconciliation needs full evalUnique' access at M.insert z w, not just ArgsDet's M-only, args-only shape, so evalBuiltinUnique_of can't carry it — same EvalBuiltinMotive/fn-style pointwise proof as evalUnique''s own mkSeq/bagOfAll case.

theorem ComputableTLAPlus.Operational.evalListUnique' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {es : List (Expression Typ)} {vs ws : List Value} : EvalList Ξ Ω M es vs → EvalList Ξ Ω M es ws → vs = ws

EvalList determinism, standalone: a list of expressions denotes at most one list of values. Recurses on the expression list; the mutual Eval determinism is evalUnique'.

theorem ComputableTLAPlus.Operational.evalPathUnique' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {path : List (String ⊕ Expression Typ)} {rs rs' : List (PathStep Value)} : EvalPath Ξ Ω M path rs → EvalPath Ξ Ω M path rs' → rs = rs'

EvalPath determinism, standalone: a syntactic access path resolves to at most one semantic path. Recurses on the syntactic path.

theorem ComputableTLAPlus.Operational.coerceUnique {c : TypedTLAPlus.Coercion} {v v₁' v₂' : Value} : coerce c v v₁' → coerce c v v₂' → v₁' = v₂'

coerce c v has at most one image. Every coerce case pins v' — an equation directly, or an extensional characterisation whose right-hand side names only c and v — so determinism follows without appeal to Eval. .tuple/.comp recurse on a sub-coercion.

theorem ComputableTLAPlus.Operational.evalList_fnCallNat {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {e : Expression Typ} {fnTyp : Typ} {r A B : Value} (hr : Eval Ξ Ω M e r) (hpf : ZFSet.IsPFunc r A B) {L : List ℕ} {vs : List Value} : EvalList Ξ Ω M (List.map (fun (i : ℕ) => e.fnCall fnTyp (Expression.nat (toString (i + 1)))) L) vs ↔ vs.length = L.length ∧ ∀ (idx i : ℕ) (vk : Value), L[idx]? = some i → vs[idx]? = some vk → ZFSet.pair (Value.ofNat (i + 1)) vk ∈ r

The EvalList behind .tupleToSeq's discharged .seq: a list of index projections e[i+1], one per i ∈ L. Every element re-evaluates the shared e, pinned to one r by evalUnique'; the .nat literal parses back (Nat.toNat?_repr). The result list is characterised by its graph — ⟨i+1, vsᵢ⟩ ∈ r — with hpf (r a partial function) doing the fnApply work.

theorem ComputableTLAPlus.Operational.evalList_fnCallNat_ex {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {e : Expression Typ} {fnTyp : Typ} {L : List ℕ} {vs : List Value} (h : EvalList Ξ Ω M (List.map (fun (j : ℕ) => e.fnCall fnTyp (Expression.nat (toString (j + 1)))) L) vs) (hne : L ≠ []) : ∃ (r : Value) (A : ZFSet.{0}) (B : ZFSet.{0}), Eval Ξ Ω M e r ∧ ZFSet.IsPFunc r A B

One index projection of a non-empty .tupleToSeq list is enough to pin down e's value and a partial-function witness for it.

theorem ComputableTLAPlus.Operational.evalList_iff_forall₂ {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {es : List (Expression Typ)} {vs : List Value} : EvalList Ξ Ω M es vs ↔ List.Forall₂ (Eval Ξ Ω M) es vs

EvalList is List.Forall₂ of Eval — the companion inductive undoes what the kernel's positivity check forced apart in Eval's definition. Stated post hoc, where nesting is fine.

theorem ComputableTLAPlus.Operational.evalList_getElem {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {es : List (Expression Typ)} {vs : List Value} : EvalList Ξ Ω M es vs ↔ es.length = vs.length ∧ ∀ (i : ℕ) (h₁ : i < es.length) (h₂ : i < vs.length), Eval Ξ Ω M es[i] vs[i]

EvalList by index: a length equation plus pointwise evaluation. The form the multi-component coercions (tuple/record) need, so their induction over components happens once here.

theorem ComputableTLAPlus.Operational.evalLocal' {Ξ : OperatorEnv} {Ω : Model Value} {M₁ M₂ : Memory Value} {e : Expression Typ} {v : Value} (hΞ : Ξ.WellScoped) (h : ∀ x ∈ e.freeVars, Finmap.lookup x M₁ = Finmap.lookup x M₂) : Eval Ξ Ω M₁ e v ↔ Eval Ξ Ω M₂ e v

theorem ComputableTLAPlus.Operational.fnApply_ofSeq {vs : List Value} {A B : Value} (hf : ZFSet.IsPFunc (Value.ofSeq vs) A B) {j : ℕ} (hj : j < vs.length) (hk : Value.ofNat (j + 1) ∈ ZFSet.Dom (Value.ofSeq vs) ⋯) : fnApply hf (Value.ofNat (j + 1)) hk = vs[j]

Application of a sequence value at a valid index: the value stored at that position.

theorem ComputableTLAPlus.Operational.evalCoerce'_seqToFun {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {i : String} {e : Expression Typ} {v' : Value} (hΞ : Ξ.WellScoped) : Eval Ξ Ω M ((TypedTLAPlus.Coercion.seqToFun τ i).applyComputable e) v' ↔ ∃ (v : Value), Eval Ξ Ω M e v ∧ coerce (TypedTLAPlus.Coercion.seqToFun τ i) v v'

The .seqToFun case of evalCoerce', standalone: it does not recurse on a sub-coercion, only re-evaluates e under the binder the coercion introduces. The cofinite Eval.fn rule opens that binder at a name chosen fresh for e, so evalLocal' relates the re-evaluation back to e's ambient value with no freshness hypothesis. The built function [i ∈ 1 .. Len(e) ↦ e[i]] reproduces e itself when e denotes a sequence — its graph already is that indexed family — and denotes nothing otherwise (Len is defined only on sequences), which is exactly what coerce (.seqToFun …) states.

theorem ComputableTLAPlus.Operational.evalCoerce'_bagToFun {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {τ : Typ} {i : String} {e : Expression Typ} {v' : Value} (hΞ : Ξ.WellScoped) : Eval Ξ Ω M ((TypedTLAPlus.Coercion.bagToFun τ i).applyComputable e) v' ↔ ∃ (v : Value), Eval Ξ Ω M e v ∧ coerce (TypedTLAPlus.Coercion.bagToFun τ i) v v'

The .bagToFun case of evalCoerce', standalone — same role evalCoerce'_seqToFun plays for .seqToFun. The built .fn's domain is Bags!BagToSet(e), its body Bags!CopiesIn(i, e); both now have real EvalBuiltin rules (.bagToSet, .copiesIn), so the eta-expansion genuinely evaluates, reconstructing e's own bag graph exactly (Value.IsBagVal.mem_iff).

theorem ComputableTLAPlus.Operational.evalCoerce'_function {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x y : String} {dom rng dom' rng' : Typ} {cD cR : TypedTLAPlus.Coercion} {e : Expression Typ} {v' : Value} (hΞ : Ξ.WellScoped) (ihD : ∀ {M : Memory Value} {e : Expression Typ} {v' : Value}, Eval Ξ Ω M (cD.applyComputable e) v' ↔ ∃ (v : Value), Eval Ξ Ω M e v ∧ coerce cD v v') (ihR : ∀ {M : Memory Value} {e : Expression Typ} {v' : Value}, Eval Ξ Ω M (cR.applyComputable e) v' ↔ ∃ (v : Value), Eval Ξ Ω M e v ∧ coerce cR v v') : Eval Ξ Ω M ((TypedTLAPlus.Coercion.function x y dom rng dom' rng' cD cR).applyComputable e) v' ↔ ∃ (v : Value), Eval Ξ Ω M e v ∧ coerce (TypedTLAPlus.Coercion.function x y dom rng dom' rng' cD cR) v v'

The .function case of evalCoerce', standalone. ihD/ihR are evalCoerce' at the strictly smaller cDom/cRng — passed in so this lives outside the evalCoerce' recursion block while the termination checker still sees the calls.

theorem ComputableTLAPlus.Operational.evalCoerce' {Ξ : OperatorEnv} {Ω : Model Value} (hΞ : Ξ.WellScoped) {c : TypedTLAPlus.Coercion} {M : Memory Value} {e : Expression Typ} {v' : Value} : Eval Ξ Ω M (c.applyComputable e) v' ↔ ∃ (v : Value), Eval Ξ Ω M e v ∧ coerce c v v'

Applying a coercion to an expression denotes the coercion applied to that expression's value. Recurses on c through the equation compiler — Coercion is a nested inductive, so induction does not fire. Needs hΞ : Ξ.WellScoped: the .seqToFun/.function cases build a .fn whose body re-evaluates e under a binder the coercion introduces, and evalLocal' relates that back to e's ambient value — the cofinite Eval rules open that binder at a name chosen fresh for e, so no Coercion.FreshFor hypothesis is needed.

theorem ComputableTLAPlus.Operational.evalSubst' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {x : String} {e' e : Expression Typ} {v' v : Value} (hΞ : Ξ.WellScoped) (hlc : e'.LC) (he' : Eval Ξ Ω M e' v') : Eval Ξ Ω (Finmap.insert x v' M) e v ↔ Eval Ξ Ω M (Expression.subst x e' e) v

Substitution is evaluation-under-extended-memory read backwards. .mp (forward) is evalSubst'_fwd; .mpr (backward) is evalSubst'_bwd. Both need Ξ.WellScoped (operator bodies are freeVars-closed) and e'.LC (the spliced expression has no dangling de Bruijn index, so it survives being lifted under e's binders).

theorem ComputableTLAPlus.Operational.resolvesPath_evalPath {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {path : List (String ⊕ Expression Typ)} {resolved : List (PathStep Value)} (h : ResolvesPath (Eval Ξ Ω) M path resolved) : EvalPath Ξ Ω M path resolved

ResolvesPath, stated against the abstract Eval parameter, unfolds to EvalPath, the mutual companion Eval's except constructor is stated with. The two inductives are the same shape; this is the only place the interface-level path relation meets the concrete one.

theorem ComputableTLAPlus.Operational.evalExcept' {Ξ : OperatorEnv} {Ω : Model Value} {M : Memory Value} {f rhs : Expression Typ} {τ : Typ} {path : List (String ⊕ Expression Typ)} {vf vr v : Value} {resolved : List (PathStep Value)} (hf : Eval Ξ Ω M f vf) (hpath : ResolvesPath (Eval Ξ Ω) M path resolved) (hrhs : Eval Ξ Ω M rhs vr) : Eval Ξ Ω M (f.except τ [(path, rhs)]) v ↔ updatePath vf resolved vr = some v

@[implicit_reducible]

noncomputable instance ComputableTLAPlus.Operational.instExprSemanticsValue : ExprSemantics Value

The concrete TLA⁺ expression evaluator over Value := ZFSet.

Equations

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