---

Step * 1 1 1 of Lemma seq-append1


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 ⊥)
6. is-exception(i)
⇒ (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 ⊥)
7. (i ∈ ℤ)
⇒ is-exception(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 ⊥)
8. (if (i) < (n + 1)  then if i=n  then t  else (s i)  else ⊥)↓
9. i ∈ ℤ
10. n + 1 ∈ ℤ
⊢ 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 ⊥
BY
{ ((Assert (n + 1)↓ BY Auto) THEN HasValueD (-1) THEN Try ((RWO "5" 0 THEN (Trivial ORELSE Complete (SqLeCD))))) }

---

Latex:

---

Latex:

1.  t  :  Base
2.  s  :  Base
3.  n  :  Base
4.  i  :  Base
5.  (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{})
6.  is-exception(i)
{}\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{})
7.  (i  \mmember{}  \mBbbZ{})
{}\mRightarrow{}  is-exception(n)
{}\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{})
8.  (if  (i)  <  (n  +  1)    then  if  i=n    then  t    else  (s  i)    else  \mbot{})\mdownarrow{}
9.  i  \mmember{}  \mBbbZ{}
10.  n  +  1  \mmember{}  \mBbbZ{}
\mvdash{}  if  (i)  <  (n  +  1)    then  if  i=n    then  t    else  (s  i)    else  \mbot{}  \mleq{}  if  (i)  <  (n)
                                                                                                                                  then  s  i
                                                                                                                                  else  if  (i)  <  (n  +  1)
                                                                                                                                                  then  t
                                                                                                                                                  else  \mbot{}


By

---

Latex:
((Assert  (n  +  1)\mdownarrow{}  BY
                Auto)
  THEN  HasValueD  (-1)
  THEN  Try  ((RWO  "5"  0  THEN  (Trivial  ORELSE  Complete  (SqLeCD)))))

---

Home Index