Step
*
1
1
3
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. is-exception(if (i) < (n + 1) then if i=n then t else (s i) else ⊥)
9. i ∈ ℤ
10. is-exception(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
{ ExceptionCases (-1) }
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 ⊥)
8. is-exception(if (i) < (n + 1) then if i=n then t else (s i) else ⊥)
9. i ∈ ℤ
10. is-exception(n + 1)
11. n ∈ ℤ
12. is-exception(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 ⊥
2
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. is-exception(if (i) < (n + 1) then if i=n then t else (s i) else ⊥)
9. i ∈ ℤ
10. is-exception(n + 1)
11. is-exception(n)
⊢ 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 ⊥
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. is-exception(if (i) < (n + 1) then if i=n then t else (s i) else \mbot{})
9. i \mmember{} \mBbbZ{}
10. is-exception(n + 1)
\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:
ExceptionCases (-1)
Home
Index