---

Step * 1 of Lemma gamma-neighbourhood-prop5


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 1) ∈ (ℕ?))
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 1) ∈ (ℕ?)))

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 1) ∈ (ℕ?)))

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  \mneg{}((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  1))


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