---

Step * 1 2 of Lemma gamma-neighbourhood-prop3


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) ∈ (ℕ?)))
BY
{ (GenConclAtAddr [1;1;1;1] THEN Thin (-1) THEN DVar `v' THEN Reduce 0 THEN (D 0 THENA Auto) THEN Thin (-1)) }

1
1. beta : ℕ ⟶ ℕ
2. n : ℕ
3. m : ℕ
4. ¬↑init-seg-nat-seq(0s^(m);0s^(n))
5. (beta 0) = 0 ∈ ℤ
6. x : ∃x:ℕ. ((↑init-seg-nat-seq(0s^(n)**λi.x^(1);0s^(m))) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ)))
⊢ n < m ∧ ((inl 1) = (inl 0) ∈ (ℕ?))

2
1. beta : ℕ ⟶ ℕ
2. n : ℕ
3. m : ℕ
4. ¬↑init-seg-nat-seq(0s^(m);0s^(n))
5. (beta 0) = 0 ∈ ℤ
6. y : ¬(∃x:ℕ. ((↑init-seg-nat-seq(0s^(n)**λi.x^(1);0s^(m))) ∧ (¬((beta x) = 0 ∈ ℤ)) ∧ (∀y:ℕx. ((beta y) = 0 ∈ ℤ))))
⊢ n < m ∧ ((inl 0) = (inl 0) ∈ (ℕ?))

---

Latex:

---

Latex:

1.  beta  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbN{}
3.  m  :  \mBbbN{}
4.  \mneg{}\muparrow{}init-seg-nat-seq(0s\^{}(m);0s\^{}(n))
5.  (beta  0)  =  0
\mvdash{}  (\muparrow{}isl(if  TERMOF\{extend-seq1-all-dec:o,  1:l\}  0s\^{}(m)  0s\^{}(n)  beta  then  inl  1  else  inl  0  fi  ))
{}\mRightarrow{}  (n  <  m
      \mwedge{}  (if  TERMOF\{extend-seq1-all-dec:o,  1:l\}  0s\^{}(m)  0s\^{}(n)  beta  then  inl  1  else  inl  0  fi    =  (inl  0)))


By

---

Latex:
(GenConclAtAddr  [1;1;1;1]
  THEN  Thin  (-1)
  THEN  DVar  `v'
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index