---

Step * 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 ⊥)
⊢ 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 ⊥
BY
{ ((Assert ⌜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 ⊥)⌝⋅
    THENA ((UnivCD THENA Auto)
           THEN SqequalSqle
           THEN ExceptionSqequal (-1)
           THEN (HypSubst' (-1) 0 THEN Reduce 0)
           THEN Auto)
    )
   THEN (Assert ⌜(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 ⊥)⌝⋅
         THENA ((UnivCD THENA Auto)
                THEN SqequalSqle
                THEN ExceptionSqequal (-1)
                THEN (HypSubst' (-1) 0 THEN Reduce 0)
                THEN RW (SweepDnC LessExceptionC) 0
                THEN 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 ⊥)
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 ⊥)
⊢ 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:

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{})
\mvdash{}  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{}


By

---

Latex:
((Assert  \mkleeneopen{}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{})\mkleeneclose{}\mcdot{}
    THENA  ((UnivCD  THENA  Auto)
                  THEN  SqequalSqle
                  THEN  ExceptionSqequal  (-1)
                  THEN  (HypSubst'  (-1)  0  THEN  Reduce  0)
                  THEN  Auto)
    )
  THEN  (Assert  \mkleeneopen{}(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{})\mkleeneclose{}\mcdot{}
              THENA  ((UnivCD  THENA  Auto)
                            THEN  SqequalSqle
                            THEN  ExceptionSqequal  (-1)
                            THEN  (HypSubst'  (-1)  0  THEN  Reduce  0)
                            THEN  RW  (SweepDnC  LessExceptionC)  0
                            THEN  Auto)
              )
  )

---

Home Index