---

Step * of Lemma seq-append1

∀[n:ℕ]. ∀[s,t:Top].  (seq-append(n;1;s;λi.t) ~ seq-normalize(n + 1;λm.if m=n  then t  else (s m)))
BY
{ (RepUR ``seq-append seq-single seq-normalize`` 0
   THEN (UnivCD THENA Auto)
   THEN EqCD
   THEN SqEqualBase
   THEN (Assert ⌜(i ∈ ℤ)
                 ⇒ (n ∈ ℤ)
                 ⇒ (if (i) < (n)  then s i  else if (i) < (n + 1)  then t  else ⊥ ~ if (i) < (n + 1)
                                                                                        then if i=n  then t  else (s i)
                                                                                        else ⊥)⌝⋅
         THENA Auto
         )) }

1
1. t : Base
2. s : Base
3. n : Base
4. i : Base
5. (i ∈ ℤ)
⇒ (n ∈ ℤ)
⇒ (if (i) < (n)  then s i  else if (i) < (n + 1)  then t  else ⊥ ~ if (i) < (n + 1)
                                                                       then if i=n  then t  else (s i)
                                                                       else ⊥)
⊢ if (i) < (n)  then s i  else if (i) < (n + 1)  then t  else ⊥ ~ if (i) < (n + 1)
                                                                     then if i=n  then t  else (s i)
                                                                     else ⊥

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[s,t:Top].    (seq-append(n;1;s;\mlambda{}i.t)  \msim{}  seq-normalize(n  +  1;\mlambda{}m.if  m=n    then  t    else  (s  m)))


By

---

Latex:
(RepUR  ``seq-append  seq-single  seq-normalize``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  EqCD
  THEN  SqEqualBase
  THEN  (Assert  \mkleeneopen{}(i  \mmember{}  \mBbbZ{})
                              {}\mRightarrow{}  (n  \mmember{}  \mBbbZ{})
                              {}\mRightarrow{}  (if  (i)  <  (n)    then  s  i    else  if  (i)  <  (n  +  1)    then  t    else  \mbot{} 
                                    \msim{}  if  (i)  <  (n  +  1)    then  if  i=n    then  t    else  (s  i)    else  \mbot{})\mkleeneclose{}\mcdot{}
              THENA  Auto
              ))

---

Home Index