Refactoring

Binder:

In $λ$ -calculus, a binder is a $λ$ abstraction that introduces a new variable. so for example $λ x . b o d y$ introduces a variable $x$ hence $λ x$ is a binder for all the $x^{'} s$ that are in $b o d y$ . To convert a named lambda term into a deBrujin indexed nameless expression, for each variable, we have to replace it with the (nearest) distance of the binder that binds this variable. So if the nearest binder of $x$ is THE nearest binder, we give it an index $0$ , if the nearest binder of $x$ is the second near binder, we give it an index $1$ and so forth.

So, let's write a named expression in deBrujin form:
consider

λ z . (λ y . y (λ x . x)) (λ x . z x)

for each variable, we have to find the nearest lambda on the left that binds it. First of all, $λ z$ is the outermost and only binder for $z$ . if we notice closely, the above expression looks something like $λ z . (t_{1}) (t_{2})$ , that is we are talking about a function that takes z as the argument and returns an application $(t 1) (t 2)$ . which means that any $z$ in $(t 1)$ or $(t 2)$ are bound by this outer lambda. Notice $t 2 = λ x . z x$ , so $λ z$ binds $t 2$ , and in $t 2$ $λ x$ bind $z x$ . hence, the nearest binding of $z$ is two levels deep, (and using zero indexing) the index of $z$ is hence $1$ .
using this logic over and over again, seeing the nearest lambda that binds a variable, and how deep it is, we can re-write the expression in deBrujin form.

λ . (λ . 0 (λ . 0)) (λ . 1 0)

how do we convert it back? it's pretty straight forward, we just give each binder a variable name, and use distances given by the indices to re-name the indices.

but now we have the mysterious shift operator:

upShift

for any nameless term $t$ , the upshift of $t$ by $k$ with cutoff $c$ , written $↑_{c}^{k} t$ is defined as follows:
if $t$ is an index: if $t \geq c$ then $t + k$ . if $t < c$ then $t$ .
if t is a lambda abstraction $λ t^{'}$ then $λ ↑_{c + 1}^{k} t^{'}$ .
if t is an application $(t_{1} t_{2})$ then $(↑_{c}^{k} t_{1} ↑_{c}^{k} t_{2})$ .

Substitution:

The rough idea of substitution is that functions are only dependent on how the transform an input. Not on what the inputs are named or what they look like. So we want to have some rules to re-write variables in such a way that a re-write (or substitution) is functionally equivalent to its original.

usually, in named form, a lambda abstraction looks like $u = λ x . t$ , where $t$ is any term. in nameless (deBrujin index) form, $u = λ . t$ . in any even, we see that all $x$ that appear in $t$ are bound by the outer lambda. similarly, in the deBrujin form $u$ , there might be indices who's nearest binding is in fact this outer lambda.
The key thing to internalize is that we are not substituting a variable NAME anymore. deBrujin indices are not just names. They represents distances from the nearest lambda that binds them.
but there are more issues here:
Let us look at some substitutions in the case of named expressions.

$\begin{array}{lll} [x \mapsto s] x & = s \\ [x \mapsto s] y & = y & if x \neq y \\ [x \mapsto s] (λ y . t_{1}) & = λ y \cdot [x \mapsto s] t_{1} \\ [x \mapsto s] (t_{1} t_{2}) & = ([x \mapsto s] t_{1}) ([x \mapsto s] t_{2}) \end{array}$

for example $[x \to y] λ x . x$ our result is $λ x . y$ which is quite funny, as it changes the identity function into a constant function.

Hence, it should be a rule that once we encounter a variable name in binding,we can't substitute it. so we account for that.

$\begin{array}{lll} [x \mapsto s] x & = s \\ [x \mapsto s] y & = y & if x \neq y \\ [x \mapsto s] (λ y . t_{1}) & = λ y \cdot [x \mapsto s] t_{1} & if x \neq y \\ [x \mapsto s] (λ y . t_{1}) & = λ y \cdot t_{1} & if x = y \\ [x \mapsto s] (t_{1} t_{2}) & = ([x \mapsto s] t_{1}) ([x \mapsto s] t_{2}) \end{array}$

Next, consider $[x \mapsto z] λ z . x$ : this results in $λ z . z$ . This time we morphed a constant function into the identity function. In the general substitution $[x \mapsto s] λ y . t$ , the free variables in $s$ becoming bound when substituting in $t$ is called "capture". let's correct that.
$\begin{array}{lll} [x \mapsto s] x & = s \\ [x \mapsto s] y & = y & if x \neq y \\ [x \mapsto s] (λ y . t_{1}) & = λ y \cdot [x \mapsto s] t_{1} & if x \neq y and y \notin F V (s) \\ [x \mapsto s] (λ y . t_{1}) & = λ y \cdot t_{1} & if x = y \\ [x \mapsto s] (t_{1} t_{2}) & = ([x \mapsto s] t_{1}) ([x \mapsto s] t_{2}) \end{array}$

Whenever the above definition doesn't give us an answer, we can use alpha conversion to fully re-name all bound variables appropriately.

Now, we need to figure out the analog of the substitution for deBrujin expressions.

In order to do this, we need to develop deBrujin expressions a little more.

The first thing we need is the definition of a term

Term

a term is an element of $T$ : the smallest family of sets ${T_{0}, T_{1} \dots}$ such that:
An index $k$ is in $T_{n}$ if $0 \leq k < n$
If a term $t \in T_{n}$ and $n > 0$ , $λ . t \in T_{n - 1}$
if terms $t_{1}, t_{2} \in T_{n}$ then $(t_{1} t_{2}) \in T_{n}$

Essentially, each $T_{i}$ represents the set of all terms that have at most $i$ free-variables.

when we were talking about binders, we knew how to set index of a variable, by finding the distance of the nearest binder that binds that variable. What about free variables? well, for that, we need a context.

Context

let $V$ be the set of variable names in named lambda calculus.
The context $Γ$ select $n + 1$ names $x_{n}, x_{n - 1} . . x_{0}$ from $V$ and assigns them indices $n, n - 1, . . 0$ respectively. ( $x_{i} \mapsto i$ ),

The rough idea is that having an $n + 1$ length context allows us to write any term in ${T_{0}, T_{1}, \dots T_{n + 1}}$ cause we do have $n + 1$ free variables.
Let's setup a context for our free variables: $Γ = e \to 4, d \to 3, c \to 2, b \to 1, a \to 0$ .
now, lets try to convert $λ x . a x$ into deBrujin form. we know that the nearest binder to $x$ is at distance $0$ , so $x \to 0$ but $a \to 0$ as well? NOT SO FAST! the moment we go inside the "context" of a binder, $λ x . b o d y$ , we know that $x$ can appear in the body such that $λ x$ is it's nearest binder and at a distance $0$ . so this means that inside the context of this binder, all our indices free variables must be incremented.
so $x \to 0$ and $a \to 1$ , hence written as $λ . 1 0$ .

So now, we can build up our Substitution in deBrujin form.
Remember that we can only substitute free variables. let $Γ$ be an $n$ length context. let $j$ be the index of a free variable in $Γ$ that we want to replace by a term $s$ , in the term $λ t$ .
so this lambda binds some index. whatever it binds, assuming there is no more $λ$ 's in $t$ , that bound index is $0$ . and inside the lambda, the free variable $j$ is actually $j + 1$ . Moreover, in $s$ , we need to ensure all the free variables are incremented, so we need to upshift it.

The cutoff $c$ in the upshift operator $↑_{c}^{k}$ makes a lot of sense right now. suppose $s = λ s^{'}$ , then of course, the context inside the lambda (ie in $s^{'}$ ) has all it's free variables indices from $1$ to $n$ instead of $0$ to $n - 1$ in the outer context $Γ$ . so if we want to upshift all the free variables in $λ s^{'}$
we should up shift variables $1 . . n$ in $s^{'}$ and ignore $0$ as the lambda binds it.
Therefore, it makes sense that $↑_{0}^{1} λ s^{'} = λ ↑_{1}^{1} s^{'}$ .

So now, we finally have made it.

Substitution in DeBrujin expressions

Let $Γ$ be an $n$ length context for free variables, and $t, s \in T_{n}$ (notice $T_{n}$ contains $T_{i}$ for $i \leq n$ ). Then the substitution of a free index $j$ with the term $s$ in the term $t$ is defined recursively as follows:
If $t$ is an index, $[j \mapsto s] t = {s if t = j else t}$
if $t = λ t^{'}$ : $[j \mapsto s] λ t^{'} = λ [j + 1 \mapsto ↑_{0}^{1} s] t^{'}$
if $t = (t_{1} t_{2})$ : $[j \mapsto s] (t_{1} t_{2}) = ([j \mapsto s] t_{1} [j \mapsto s] t_{2})$

The great beta reduction:

So, here we are, and now we want to write the $β$ reduction as a substitution in deBrujin expressions.
so we are given a context of length $n$ , $Γ$ , and a lambda abstraction $λ b$ , a term $v$ and we need to evaluate $(λ b) v$ which is the beta reduction. so in a beta reduction, we always substitute the index bound by the outermost lambda. It is pretty safe to say that we are substituting the index $0$ in $b$ with $v$ . But there is a slight catch. if $b, v \in T_{n}$ , then we see that the context of free variables in $b$ is upshifted because it is inside a lambda.
but the context of free variables, $v$ is still the global context $Γ$ . so we need to ensure that we upshift $v$ before substituting.

so we have something along the lines of $[0 \mapsto ↑^{1} v] b$ . The second issue is, that the beta reduction actually removes the outermost lambda, which means that it unbinds some variable. Which then means that we need to downshift the context.
so the final beta reduction is $↑^{- 1} [0 \mapsto ↑^{1} v] b$ .

jumping through hoops, the kth beta reduction:

beta reduction

let $v, λ b$ be deBrujin terms in some $n$ context $Γ$ . The beta reduction of $λ b$ at $v$ is: $$ \uparrow^{-1}[0 \mapsto \uparrow^1v]b $$
the $k$ beta reduction is (denoted as $β_{k} (b, v)$ ):

↑_{k}^{- 1} [k \mapsto ↑^{k + 1} v] b

Lets try to notice something, suppose $b = λ b^{'}$ . Try simplify the expression $\uparrow^{-1}[0 \mapsto \uparrow{#1v}]\lambda b'$ :

↑^{- 1} [0 \mapsto ↑^{1} v] λ b^{'} = ↑^{- 1} λ [1 \mapsto ↑^{1} ↑^{1} v] b^{'} = λ ↑_{1}^{- 1} [1 \mapsto ↑^{2} v] b^{'}

Wow! if $b$ has a chain of $k$ lambdas, then then the beta reduction of $λ b$ at $v$ is equivalent to $λ λ . ._{k times} λ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} v] b_{k}^{'}$

Version space:

Version space

a version space is one of the following:
An index $i$
An abstraction $λ v$ where $v$ is a version space
An application $(f x)$ where $f, x$ are version spaces.
A union $\cup^{+} V$ where $V$ is a set of version spaces.
The set of all lambda expressions $Λ$
The empty set $\emptyset$

We are back to the paper now, and are again in thinking about our deBrujin expressions as programs. Now basically, a version space for a program, efficiently and compactly maintains refactorings of a program. (we will explore this in detail later)

Now, we want to define an operator $S_{0} (u)$ that takes in version spaces and spits out sets of "substitutions" ${a ⟶ b}$ between two version spaces (note that $a, b, u$ are version spaces).
But these substitutions are not the substitutions defined earlier, the idea is that these represent refactorings of programs in the version space $u$ . in particular if $a^{'} \in a$ and $b^{'} \in b$ are programs, then the beta reduction of $λ b^{'}$ at $a^{'}$ : $β_{0} (b^{'}, a^{'})$ is a program in $u$ . (a notion of consistency)

Moreover, if $a^{'}$ and $b^{'}$ are programs, and we have that $β_{0} (b^{'}, a^{'}) \in u$ , then it must mean that there are version spaces $a, b$ such that ${a ⟶ b} \in S_{0} (u)$ and $a^{'} \in a, b^{'} \in b$ . (a notion of completeness)

But as is the nature of inductive definitions, we actually want to define $S_{k}$ . TAKE THE DOWNSHIFT OPERATOR NOW!

downshift

$\begin{aligned} ↓_{c}^{k} i & = i, when i < c \\ ↓_{c}^{k} i & = (i - k), when i \geq c + k \\ ↓_{c}^{k} i & = \emptyset, when c \leq i < c + k \\ ↓_{c}^{k} λ b & = λ ↓_{c + 1}^{k} b \\ ↓_{c}^{k} (f x) & = (↓_{c}^{k} f ↓_{c}^{k} x) \\ ↓_{c}^{k} ⊎ V & = ⊎ {↓_{c}^{k} v ∣ v \in V} \\ ↓_{c}^{k} v & = v, when v is a primitive or \emptyset or Λ \end{aligned}$

We can think of shifting operations applied to version spaces (which are basically sets of programs) as applying it to to each program in that set.

kth refactor operator

$S_{k} (v) = {↓_{0}^{k} v \mapsto k} \cup {\begin{cases} if v is primitive: & {Λ \mapsto v} \\ if v = i and i < k : & {Λ \mapsto i} \\ if v = i and i \geq k : & {Λ \mapsto (i + 1)} \\ if v = λ b : & {v^{'} \mapsto λ b^{'} : v^{'} \mapsto b^{'} \in S_{k + 1} (b)} \\ if v = (f x) : & {v_{1} \cap v_{2} \mapsto (f^{'} x^{'}) : v_{1} \mapsto f^{'} \in S_{k} (f), v_{2} \mapsto x^{'} \in S_{k} (x)} \\ if v = ⊎ V : & ⋃_{v^{'} \in V} S_{n} (v^{'}) \\ if v is \emptyset : & \emptyset \\ if v is Λ : & {Λ \mapsto Λ} \end{cases}$

Lemma 1. Let e be a program or version space and n, c be natural numbers. Then $\uparrow_{n+c}^{-1} \uparrow_c^{n+1} e=\uparrow_c{#n} e$ , and in particular $↑_{n}^{- 1} ↑^{n + 1} e = ↑^{n} e$ .

Lemma 2. Let e be a program or version space and n, c be natural numbers. Then $↓_{c}^{n} ↑_{c}^{n} e = e$ , and in particular $↓^{n} ↑^{n} e = e$ .

Consistency of

S_{k}

If $(a \mapsto b) \in S_{k} (v)$ , then for all programs $a^{'} \in a$ and $b^{'} \in b$ , the $k$ beta reduction of $b^{'}$ at $a^{'}$ , $↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] b^{'} \in v$ .

$* p r o o f * :$ We first deal with the case that $b = k$ . in this case, $a = \downarrow_{0}{#kv}$ let $v^{'}$ be any program in $v$ . we know that arbitrary $a^{'} \in a$ can be written as $a^{'} = ↓_{0}^{k} v^{'}$ for some $v^{'} \in v$ . In particular, $a^{'} \in a ⟺ a^{'} = ↓_{0}^{k} v^{'} : v^{'} \in v$ . moreover, $b^{'} = k$ . hence: $$ \uparrow_{k}^{-1}[k \mapsto \uparrow^{k+1}a']b' = \uparrow_{k}^{-1}[k \mapsto \uparrow^{k+1}\downarrow_{0}^kv']k = \uparrow^{-1}_{k}(\uparrow^{k+1}\downarrow^kv')$$
invoking the above lemmas, we notice that the rightmost expression evaluates to $v^{'}$ .

Now, for the other cases, we use structural induction:

if $v = i$ and $i < k$ , we have to deal with $a = Λ$ and $b = i = b^{'}$ . pick any program $a^{'} \in Λ$ . we want to evaluate $$\uparrow_{k}^{-1}[k \mapsto \uparrow^{k+1}a']i = i$$ (because $i < k$ ) and we are done.
if $v = i$ and $i \geq k$ , we deal with $a = Λ$ and $b = i + 1 = b^{'}$ . pick arbitrary $a^{'} \in Λ$ , we get:

↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] i + 1 = ↑_{k}^{- 1} (i + 1) = i $ $ (a s $ i + 1 > k $), a n d w e a r e d o n e . - i f $ v $ i s a p r i m i t i v e, w e d e a l w i t h $ a = Λ $ a n d $ b = b^{'} = v $ . p i c k a r b i t r a r y $ a^{'} \in Λ $ . w e g e t : $ $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] v = ↑_{k}^{- 1} v = v $ $ (w e a s s u m e a p r i m i t i v e i s n o t a d e B r u j i n i n d e x o r a n y o t h e r t h i n g, I D K W H Y (g o t t a i n v e s t i g a t e)) I t h i n k i t s b e c a u s e t h e u p s h i f t a n d d o w n s h i f t f o r p r i m i t i v e s o r $ \emptyset $ o r $ Λ $ i s e q u a l t o i t s e l f . - i f $ v = λ t $, w e a r e d e a l i n g w i t h t h e s u b s t i t u t i o n $ (u \mapsto λ p) $ w h e r e $ (u \mapsto p) \in S_{k + 1} (t) $ . T h e r e i s a c l e v e r h y p o t h e s i s t o p r o v e h e r e : w e c l a i m t h a t f o r a l l $ u^{'} \in u $ a n d $ p^{'} \in p $, $ ↑_{k + 1}^{- 1} [k + 1 \mapsto ↑^{k + 2} u^{'}] p^{'} \in t $ . T h i s i s t h e n o t i o n o f c o n s i s t e n c y o f $ S_{k + 1} $ . T h e r e a s o n w e c a n d o t h i s, i s b e c a u s e i f $ t $ i s n^{'} t a l a m b d a, a l l t h e o t h e r c a s e s w i l l s u f f i c e t o s h o w c o n s i s t e n c y o f $ S_{k + 1} $ . o t h e r w i s e, i f $ t $ i s a l a m b d a, t h e n w e c a n r e c u r s i v e l y c o m e b a c k t o t h i s c a s e : a n y e x p r e s s i o n i s f i n i t e a n d i s e v e n t u a l l y n o t a l a m b d a, s o t h e c o n s i s t e n c y b u b b l e s b a c k t o $ S_{k + 1} $ . (t h i s c a n b e s h o w v i a i n d u c t i o n) N o w, w e n o t i c e $ $ ↑_{k + 1}^{- 1} [k + 1 \mapsto ↑^{k + 2} u^{'}] p^{'} \in t ⟹ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} u^{'}] λ p^{'} \in λ t = v $ $ H e n c e w e a r e d o n e . - i f $ v = (f x) $ t h e n w e d e a l w i t h $ (v_{1} \cap v_{2} \mapsto (g y)) $ w h e r e $ v_{1} \mapsto g \in S_{k} (f) $ a n d $ v_{2} \mapsto y \in S_{k} (x) $ . N o w a s s u m e r e c u r s i v e l y t h a t $ (S_{k}) $ i s c o n s i s t e n t f o r o t h e r c a s e s, o r r e c u r s e b a c k t o t h i s c a s e (t h e r e c a n o n l y b e a f i n i t e n u m b e r o f a p p l i c a t i o n s i n t h e e x p r e s s i o n $ v $) N o w p i c k $ g^{'} \in g $, $ y^{'} \in y $ a n d $ p^{'} \in v_{1} \cap v_{2} $ . $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} p^{'}] g^{'} \in f $ a n d $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} p^{'}] y^{'} \in x $ . h e n c e, c o m b i n i n g, $ $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} p^{'}] g^{'} \in (f x) = v $ $ a n d w e a r e d o n e . - i f $ v = \emptyset $ o r $ v = Λ $, o r u n i o n w e a r e d o n e v a c u o u s l y o r b y r e c u r s i o n / i n d u c t i o n . $ ◻ $ * * * > [! t h e o r e m] $ S_{k} $ i s c o m p l e t e > l e t $ v $ b e a v e r s i o n s p a c e, a n d $ a^{'} $, $ b^{'} $ b e p r o g r a m s . T h e n i f $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] b^{'} \in v $ t h e n t h e r e e x i s t s v e r s i o n s p a c e s $ a, b $ s u c h t h a t $ a^{'} \in a, b^{'} \in b $ a n d $ (a \mapsto b) \in S_{k} (v) $ . $ * p r o o f * : $ - W e w i l l f i r s t d e a l w i t h t h e c a s e t h a t $ b^{'} = k $ . T h e n, w e h a v e t h a t $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] k^{'} \in v $ . H e n c e, $ ↑_{k}^{- 1} ↑^{k + 1} a^{'} \in v $ t h e r e f o r e $ ↑^{k} a^{'} \in v $, h e n c e $ ↓^{k} ↑^{k} a^{'} \in ↓^{k} v $ . T h e r e f o r e $ a^{'} \in ↓^{k} v $ . G i v e n t h a t $ (↓^{k} v \mapsto k) \in S_{k} (v) $, w e a r e d o n e . W e w i l l f u r t h e r d e a l w i t h t h e o t h e r c a s e s v i a s t r u c t u r a l i n d u c t i o n . - i f $ v = i $, t h e n $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] b^{'} = i $ A n d b y e x a m i n i n g t h e d e f i n i t i o n o f s u b s t i t u t i o n, i t i s c l e a r t h a t $ b^{'} $ m u s t b e a n i n d e x, a n d $ b^{'} \neq k $ f o l l o w s a s w e h a v e a l r e a d y d e a l t w i t h t h a t c a s e . T h e r e f o r e, $ ↑_{k}^{- 1} b^{'} = i $ . W e c a n f i g u r e o u t w h a t $ b^{'} $ i s : i f $ i < k $, i t h a s t o b e t h a t $ b^{'} = i $ . i f $ i \geq k $, i t h a s t o b e t h a t $ b^{'} = i + 1 $ f o r t h e a b o v e e q u a t i o n t o h o l d . I n t h e f i r s t c a s e, i n v o k e $ (Λ \mapsto i) \in S_{k} (v) $ a n d i n t h e s e c o n d, $ (Λ \mapsto i + 1) \in S_{k} (v) $ a n d w e a r e d o n e . - i f $ v = λ t $ t h e n $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] b^{'} \in λ t $ f o r s o m e $ v^{'} \in v $ . s i n c e $ b^{'} \neq k $ w e c a n^{'} t s u b s t i t u t e $ b^{'} $ f o r a l a m b d a f o r m, a n d $ b^{'} $ i s a n y o t h e r i n d e x o r a p p l i c a t i o n, i t s i m p l y d o e s n^{'} t w o r k . T h e r e f o r e $ b^{'} = λ c^{'} $ . H e n c e, $ $ λ ↑_{k + 1}^{- 1} [k \mapsto ↑^{k + 2} a^{'}] c^{'} \in λ t ⟺ ↑_{k + 1}^{- 1} [k \mapsto ↑^{k + 2} a^{'}] c^{'} \in t $ $ W h i c h m e a n s t h a t i n d u c t i v e l y, $ (a \mapsto c) \in S_{k + 1} (t) $ s u c h t h a t $ a^{'} \in a $ a n d $ c^{'} \in c $ * (t h i s h o l d s b e c a u s e $ t $ c o n t a i n s f i n i t e l y m a n y l a m b d a a b s t r a c t i o n s, s o e v e n t u a l l y c o n s i s t e n c y w i l l d e f e r t o s o m e o t h e r c a s e w h i c h w e h a v e p r o v e d, a n d b u b b l e b a c k w a r d t o s h o w t h a t $ S_{k + 1} $ i s c o n s i s t e n t, u s i n g t h i s c a s e^{'} s p r o o f e a c h t i m e t h e r e i s a n e w l a m b d a) * H e n c e, b y d e f i n i t i o n o f $ S_{k} $, $ (a \mapsto λ c) \in S_{k} (λ t) $ a n d $ a^{'} i n a $ a n d $ b^{'} = λ c^{'} \in λ c $ . - i f $ v = (f x) $ t h e n s i n c e $ b^{'} \neq k $ a g a i n w e c a n^{'} t s u b s t i t u t e a n a p p l i c a t i o n f o r $ b^{'} $, a n d $ b^{'} $ c a n^{'} t b e a n y o t h e r i n d e x, o r a u n i o n o r a l a m b d a a b s t r a c t i o n . T h o s e s i m p l y d o n^{'} t w o r k . h e n c e, $ b^{'} = (g^{'} y^{'}) $ . - $ $ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] (g^{'} y^{'}) \in (f x) ⟺ ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] g^{'} \in f and ↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] y^{'} \in x

again inductively, $(a_{1} \mapsto g) \in S_{k} (f)$ and $(a_{2} \mapsto y) \in S_{k} (x)$ such that $g^{'} \in g, y^{'} \in y, a^{'} \in a_{1} \cap a_{2}$ . then by definition of $S_{k}$ , $(a_{1} \cap a_{2} \mapsto (g y)) \in S_{k} (v)$ .
if $v$ is a primitive, then we have $↑_{k}^{- 1} [k \mapsto ↑^{k + 1} a^{'}] b^{'} = v$ . but $b^{'}! = k$ and hence can't be substituted, and $b^{'}$ not being an index also doesn't help. Therefore, $↑_{k}^{- 1} b^{'} = v$ hence $b^{'} = v$ , and $(Λ \mapsto v) \in S_{k} (v)$ so we good.
Finally if $v$ is a union of version spaces, apply the hypothesis of the theorem inductively to the version spaces inside v, and so forth. If $v$ is empty or $Λ$ the theorem holds vacuously.
$◻$