---

Step * 2 3 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])
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]
BY
{ (RWO "-1" 0 THEN Reduce 0 THEN Auto) }

---

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])
9.  is-exception(x)
10.  u  :  Base
11.  v  :  Base
12.  x  \msim{}  exception(u;  v)
\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:
(RWO  "-1"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index