English
For terms t1, t2 of type α ⊕ Fin l, the bounded formula t1.bdEqual t2 realized under v xs is equivalent to the equality of t1 and t2 realized under the same substitution.
Русский
Для термов t1, t2 типа α ⊕ Fin l, ограниченная формула t1.bdEqual t2 после реализации по v xs эквивалентна равенству реализаций t1 и t2 по той же подстановке.
LaTeX
$$$ (t_1.bdEqual t_2).Realize v xs \;\Longleftrightarrow\; t_1.realize (Sum.elim v xs) = t_2.realize (Sum.elim v xs) $$$
Lean4
/-- A bounded formula can be evaluated as true or false by giving values to each free and bound
variable. -/
def Realize : ∀ {l} (_f : L.BoundedFormula α l) (_v : α → M) (_xs : Fin l → M), Prop
| _, falsum, _v, _xs => False
| _, equal t₁ t₂, v, xs => t₁.realize (Sum.elim v xs) = t₂.realize (Sum.elim v xs)
| _, rel R ts, v, xs => RelMap R fun i => (ts i).realize (Sum.elim v xs)
| _, imp f₁ f₂, v, xs => Realize f₁ v xs → Realize f₂ v xs
| _, all f, v, xs => ∀ x : M, Realize f v (snoc xs x)
