Step
*
2
of Lemma
sqeq-copath3
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. is-exception(if (x) < (m) then f if x=n then a[x] else b[x] else c[x])
⊢ if (x) < (m) then f if x=n then a[x] else b[x] else c[x] ≤ if (x) < (m)
then if x=n then f a[x] else (f b[x])
else c[x]
BY
{ (ExceptionCases (-1) THEN Try (ExceptionSqequal (-1))) }
1
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. is-exception(if (x) < (m) then f if x=n then a[x] else b[x] else c[x])
9. x ∈ ℤ
10. m ∈ ℤ
⊢ if (x) < (m) then f if x=n then a[x] else b[x] else c[x] ≤ if (x) < (m)
then if x=n then f a[x] else (f b[x])
else c[x]
2
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. is-exception(if (x) < (m) then f if x=n then a[x] else b[x] else c[x])
9. x ∈ ℤ
10. is-exception(m)
11. u : Base
12. v : Base
13. m ~ exception(u; v)
⊢ if (x) < (m) then f if x=n then a[x] else b[x] else c[x] ≤ if (x) < (m)
then if x=n then f a[x] else (f b[x])
else c[x]
3
1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. is-exception(if (x) < (m) then f if x=n then a[x] else b[x] else c[x])
9. is-exception(x)
10. u : Base
11. v : Base
12. x ~ exception(u; v)
⊢ if (x) < (m) then f if x=n then a[x] else b[x] else c[x] ≤ if (x) < (m)
then if x=n then f a[x] else (f b[x])
else c[x]
Latex:
Latex:
1. n : \mBbbZ{}
2. m : \mBbbZ{}
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. is-exception(if (x) < (m) then f if x=n then a[x] else b[x] else c[x])
\mvdash{} if (x) < (m) then f if x=n then a[x] else b[x] else c[x] \mleq{} if (x) < (m)
then if x=n
then f a[x]
else (f b[x])
else c[x]
By
Latex:
(ExceptionCases (-1) THEN Try (ExceptionSqequal (-1)))
Home
Index