---

Step * 1 of Lemma seq-append-normalize


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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  i  :  Base
4.  s2  :  Base
5.  s1  :  Base
6.  (i  \mmember{}  \mBbbZ{})
{}\mRightarrow{}  (if  (i)  <  (n)
              then  s1  i
              else  if  (i)  <  (n  +  m)    then  if  (i  -  n)  <  (m)    then  s2  (i  -  n)    else  \mbot{}    else  \mbot{} 
      \msim{}  if  (i)  <  (n)    then  s1  i    else  if  (i)  <  (n  +  m)    then  s2  (i  -  n)    else  \mbot{})
\mvdash{}  if  (i)  <  (n)
          then  s1  i
          else  if  (i)  <  (n  +  m)    then  if  (i  -  n)  <  (m)    then  s2  (i  -  n)    else  \mbot{}    else  \mbot{} 
\msim{}  if  (i)  <  (n)    then  s1  i    else  if  (i)  <  (n  +  m)    then  s2  (i  -  n)    else  \mbot{}


By

---

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

---

Home Index