English
A version of Realize MapTermRel when adding a shift and using castLE interacts with a more complex xs-shift.
Русский
Версия Realize MapTermRel при добавлении сдвига и использовании castLE взаимодействует со сдвигом xs.
LaTeX
$$$ (\phi.mapTermRel ft fr \dots).Realize v' xs \iff φ.Realize (v xs) (xs \circ Fin.natAdd _) $$$
Lean4
theorem realize_mapTermRel_add_castLe [L'.Structure M] {k : ℕ}
{ft : ∀ n, L.Term (α ⊕ (Fin n)) → L'.Term (β ⊕ (Fin (k + n)))} {fr : ∀ n, L.Relations n → L'.Relations n} {n}
{φ : L.BoundedFormula α n} (v : ∀ {n}, (Fin (k + n) → M) → α → M) {v' : β → M} (xs : Fin (k + n) → M)
(h1 :
∀ (n) (t : L.Term (α ⊕ (Fin n))) (xs' : Fin (k + n) → M),
(ft n t).realize (Sum.elim v' xs') = t.realize (Sum.elim (v xs') (xs' ∘ Fin.natAdd _)))
(h2 : ∀ (n) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x)
(hv : ∀ (n) (xs : Fin (k + n) → M) (x : M), @v (n + 1) (snoc xs x : Fin _ → M) = v xs) :
(φ.mapTermRel ft fr fun _ => castLE (add_assoc _ _ _).symm.le).Realize v' xs ↔
φ.Realize (v xs) (xs ∘ Fin.natAdd _) :=
by
induction φ with
| falsum => rfl
| equal => simp [mapTermRel, Realize, h1]
| rel => simp [mapTermRel, Realize, h1, h2]
| imp _ _ ih1 ih2 => simp [mapTermRel, Realize, ih1, ih2]
| all _ ih => simp [mapTermRel, Realize, ih, hv]
