---

Step * of Lemma seq-append-normalize

∀[n,m:ℕ]. ∀[s1,s2:Top].  (seq-append(n;m;s1;seq-normalize(m;s2)) ~ seq-append(n;m;s1;s2))
BY
{ (RepUR ``seq-normalize 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)  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 ⊥)⋅
         THENA ((D 0 THENA Auto) THEN RepeatFor 3 (AutoSplit) THEN Try (Complete (Auto')))
         )) }

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

---

Latex:

---

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


By

---

Latex:
(RepUR  ``seq-normalize  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)    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{})\mcdot{}
              THENA  ((D  0  THENA  Auto)  THEN  RepeatFor  3  (AutoSplit)  THEN  Try  (Complete  (Auto')))
              ))

---

Home Index