---

Step * 1 of Lemma seq-normalize-normalize


1. n : ℕ
2. m : ℕ
3. ¬n < m
4. s : Base
5. k : Base
⊢ if (k) < (n)  then if (k) < (m)  then s k  else ⊥  else ⊥ ~ if (k) < (m)  then s k  else ⊥
BY
{ (Assert ⌜(k ∈ ℤ) ⇒ (if (k) < (n)  then if (k) < (m)  then s k  else ⊥  else ⊥ ~ if (k) < (m)  then s k  else ⊥)⌝⋅
   THENA ((D 0 THENA Auto) THEN AutoSplit)
   ) }

1
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 ⊥

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  \mneg{}n  <  m
4.  s  :  Base
5.  k  :  Base
\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:
(Assert  \mkleeneopen{}(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{})\mkleeneclose{}\mcdot{}
  THENA  ((D  0  THENA  Auto)  THEN  AutoSplit)
  )

---

Home Index