---

Step * 1 of Lemma sqeq-copath3


1. n : ℤ
2. m : ℤ
3. x : Base
4. c : Base
5. b : Base
6. a : Base
7. f : Base
8. (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
{ (HasValueD (-1) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  Base
4.  c  :  Base
5.  b  :  Base
6.  a  :  Base
7.  f  :  Base
8.  (if  (x)  <  (m)    then  f  if  x=n  then  a[x]  else  b[x]    else  c[x])\mdownarrow{}
\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:
(HasValueD  (-1)  THEN  AutoSplit)

---

Home Index