English
For a relation symbol R and a term t with a valuation v and sequence xs, the true/false realization of the bounded formula R(t) corresponds to applying the relation R to the interpretation of t under v and xs.
Русский
Для отношения R и терма t с оценкой v и xs истинность реализации ограниченной формулы R(t) равна применению отношения R к трактовке t под v и xs.
LaTeX
$$$\\operatorname{Realize}(R.boundedFormula_1\\, t)\\;\\; v\\; xs \\;\\longleftrightarrow\\; \\operatorname{RelMap} R(\\![t.realize (Sum.elim\\ v\\ xs)]\\!)$$$
Lean4
@[simp]
theorem realize_rel₁ {R : L.Relations 1} {t : L.Term _} :
(R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![t.realize (Sum.elim v xs)] :=
by
rw [Relations.boundedFormula₁, realize_rel, iff_eq_eq]
refine congr rfl (funext fun _ => ?_)
simp only [Matrix.cons_val_fin_one]
