---

Step * 1 1 of Lemma seq-normalize-normalize


1. n : ℕ
2. m : ℕ
3. ¬n < m
4. s : Base
5. k : Base
6. (k ∈ ℤ) ⇒ (if (k) < (n)  then if (k) < (m)  then s k  else ⊥  else ⊥ ~ if (k) < (m)  then s k  else ⊥)
⊢ if (k) < (n)  then if (k) < (m)  then s k  else ⊥  else ⊥ ~ if (k) < (m)  then s k  else ⊥
BY
{ (SqequalSqle
   THEN AssumeHasValue
   THEN (HasValueD (-1) ORELSE (ExceptionCases (-1) THEN Try (Complete (SameException))))
   THEN RWO "6" 0
   THEN Complete (Auto)) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  \mneg{}n  <  m
4.  s  :  Base
5.  k  :  Base
6.  (k  \mmember{}  \mBbbZ{})
{}\mRightarrow{}  (if  (k)  <  (n)    then  if  (k)  <  (m)    then  s  k    else  \mbot{}    else  \mbot{}  \msim{}  if  (k)  <  (m)    then  s  k    else  \mbot{})
\mvdash{}  if  (k)  <  (n)    then  if  (k)  <  (m)    then  s  k    else  \mbot{}    else  \mbot{}  \msim{}  if  (k)  <  (m)    then  s  k    else  \mbot{}


By

---

Latex:
(SqequalSqle
  THEN  AssumeHasValue
  THEN  (HasValueD  (-1)  ORELSE  (ExceptionCases  (-1)  THEN  Try  (Complete  (SameException))))
  THEN  RWO  "6"  0
  THEN  Complete  (Auto))

---

Home Index