---

Step * 1 of Lemma seq-append-assoc


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index