|
42 | 42 | For the inductive step, assume that $t = \Atom{f}{t_1, \dots, t_k}$ |
43 | 43 | and that the claim holds for $t_1$, \dots, $t_k$. Then |
44 | 44 | \begin{align*} |
45 | | - \Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] =\\ |
46 | | - & = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]) |
| 45 | + \Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] \\ |
| 46 | + & = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]). |
47 | 47 | \intertext{For $j = 1$, \dots,~$k$, the !!{variable}s of~$t_j$ are |
48 | | - among $x_1$, \dots,~$x_n$. By induction hypothesis, |
| 48 | + among $x_1$, \dots,~$x_n$. By the induction hypothesis, |
49 | 49 | $\Value{t_j}{M}[s_1] = \Value{t_j}{M}[s_2]$. So,} |
50 | | -\Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] =\\ |
51 | | - & = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]) =\\ |
52 | | - & = \Assign{f}{M}(\Value{t_1}{M}[s_2], \dots, \Value{t_k}{M}[s_2]) =\\ |
| 50 | +\Value{t}{M}[s_1] & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_1] \\ |
| 51 | + & = \Assign{f}{M}(\Value{t_1}{M}[s_1], \dots, \Value{t_k}{M}[s_1]) \\ |
| 52 | + & = \Assign{f}{M}(\Value{t_1}{M}[s_2], \dots, \Value{t_k}{M}[s_2]) \\ |
53 | 53 | & = \Value{\Atom{f}{t_1, \dots, t_k}}{M}[s_2] = \Value{t}{M}[s_2]. |
54 | 54 | \end{align*} |
55 | 55 | \end{proof} |
|
0 commit comments