Hello I am currently self-studying the book "Semantics with applications: An Appetizer" and I don't know if I've gotten the right base case for the problem below:
Prove that $\mathcal{A} [[ a\left[y \mapsto a_0\right] ]] s=\mathcal{A} [[ a ]]\left(s\left[y \mapsto \mathcal{A} [[ a_0 ]] s\right]\right)$ for all states $s$.
So i think I have to prove this using structural induction. For the base case $a=n$, I get: $\mathcal{A} [[ a\left[y \mapsto a_0\right] ]] = A[[n]] = n$ and $\mathcal{A} [[ a ]]\left(s\left[y \mapsto \mathcal{A} [[ a_0 ]] s\right]\right) = A[[n]] = n$
My question: Is my base case for this proof correct?
Here is some background information: This book is based on the "While" language and I will put the semantics below.
Semantics of arithmetic expressions (Aexp)
Language semantics: semantics
Definition of total function A: total function A
