Step
*
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 ⊥)
⊢ 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
{ (SqequalSqle
THEN AssumeHasValue
THEN (HasValueD (-1) ORELSE ExceptionCases (-1))
THEN Try ((RWO "5" 0 THEN (Trivial ORELSE Complete (SqLeCD))))
THEN Try (((FHyp 6 [-1] THENA Auto) THEN HypSubst' (-1) 0 THEN Auto))
THEN Try (((FHyp 7 [-1] THENA Auto) THEN HypSubst' (-1) 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 ⊥)
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 ⊥
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. 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 ⊥
3
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 ⊥
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{})
\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:
(SqequalSqle
THEN AssumeHasValue
THEN (HasValueD (-1) ORELSE ExceptionCases (-1))
THEN Try ((RWO "5" 0 THEN (Trivial ORELSE Complete (SqLeCD))))
THEN Try (((FHyp 6 [-1] THENA Auto) THEN HypSubst' (-1) 0 THEN Auto))
THEN Try (((FHyp 7 [-1] THENA Auto) THEN HypSubst' (-1) 0 THEN Auto)))
Home
Index