---

Step * 2 1 2 1 1 1 of Lemma 1-dim-cube-endpoints


1. k : ℤ
2. 0 < k
3. ∀x:ℕ. (filter(λj.(j =z x);upto(k - 1)) ~ if x <z k - 1 then [x] else [] fi )
4. x : ℕ
⊢ filter(λj.(j =z x);upto(k)) = if x <z k then [x] else [] fi  ∈ (ℤ List)
BY
{ (Subst' upto(k) = (upto(k - 1) @ [k - 1]) ∈ (ℤ List) 0
   THEN (RWW "filter_append 3" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  0  <  k
3.  \mforall{}x:\mBbbN{}.  (filter(\mlambda{}j.(j  =\msubz{}  x);upto(k  -  1))  \msim{}  if  x  <z  k  -  1  then  [x]  else  []  fi  )
4.  x  :  \mBbbN{}
\mvdash{}  filter(\mlambda{}j.(j  =\msubz{}  x);upto(k))  =  if  x  <z  k  then  [x]  else  []  fi 


By

---

Latex:
(Subst'  upto(k)  =  (upto(k  -  1)  @  [k  -  1])  0
  THEN  (RWW  "filter\_append  3"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index