---

Step * 1 of Lemma gamma-neighbourhood-prop3


1. beta : ℕ ⟶ ℕ
2. n : ℕ
3. m : ℕ
4. (beta 0) = 0 ∈ ℤ
5. ↑isl(gamma-neighbourhood(beta;0s^(n)) 0s^(m))
⊢ n < m ∧ ((gamma-neighbourhood(beta;0s^(n)) 0s^(m)) = (inl 0) ∈ (ℕ?))
BY
{ (MoveToConcl (-1)
   THEN RepUR ``gamma-neighbourhood`` 0
   THEN (BoolCase ⌜init-seg-nat-seq(0s^(m);0s^(n))⌝⋅ THENA Auto)) }

1
1. beta : ℕ ⟶ ℕ
2. n : ℕ
3. m : ℕ
4. (beta 0) = 0 ∈ ℤ
5. ↑init-seg-nat-seq(0s^(m);0s^(n))
⊢ False ⇒ (n < m ∧ ((inr ⋅ ) = (inl 0) ∈ (ℕ?)))

2
1. beta : ℕ ⟶ ℕ
2. n : ℕ
3. m : ℕ
4. ¬↑init-seg-nat-seq(0s^(m);0s^(n))
5. (beta 0) = 0 ∈ ℤ
⊢ (↑isl(if TERMOF{extend-seq1-all-dec:o, 1:l} 0s^(m) 0s^(n) beta then inl 1 else inl 0 fi ))
⇒ (n < m ∧ (if TERMOF{extend-seq1-all-dec:o, 1:l} 0s^(m) 0s^(n) beta then inl 1 else inl 0 fi  = (inl 0) ∈ (ℕ?)))

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  (beta  0)  =  0
5.  \muparrow{}isl(gamma-neighbourhood(beta;0s\^{}(n))  0s\^{}(m))
\mvdash{}  n  <  m  \mwedge{}  ((gamma-neighbourhood(beta;0s\^{}(n))  0s\^{}(m))  =  (inl  0))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  RepUR  ``gamma-neighbourhood``  0
  THEN  (BoolCase  \mkleeneopen{}init-seg-nat-seq(0s\^{}(m);0s\^{}(n))\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index