---

Step * of Lemma seq-append-assoc

∀[n,m,k:ℕ]. ∀[s1,s2,s3:Top].
  (seq-append(n;m + k;s1;seq-append(m;k;s2;s3)) ~ seq-append(n + m;k;seq-append(n;m;s1;s2);s3))
BY
{ (RepUR ``seq-append`` 0
   THEN (UnivCD THENA Auto)
   THEN EqCD
   THEN SqEqualTopToBase
   THEN (Assert (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 ⊥) BY
               ((D 0 THENA Auto)
                THEN (RW  IntNormC 0 THENA Auto)
                THEN Repeat (AutoSplit)
                THEN Assert ⌜False⌝⋅
                THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}[n,m,k:\mBbbN{}].  \mforall{}[s1,s2,s3:Top].
    (seq-append(n;m  +  k;s1;seq-append(m;k;s2;s3))  \msim{}  seq-append(n  +  m;k;seq-append(n;m;s1;s2);s3))


By

---

Latex:
(RepUR  ``seq-append``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  EqCD
  THEN  SqEqualTopToBase
  THEN  (Assert  (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{})  BY
                          ((D  0  THENA  Auto)
                            THEN  (RW    IntNormC  0  THENA  Auto)
                            THEN  Repeat  (AutoSplit)
                            THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
                            THEN  Auto)))

---

Home Index