---

Step * 4 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 if x=n then f a[x] else (f 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 if x=n then f a[x] else (f b[x])  else c[x] ≤ if (x) < (m)
                                                                      then f if x=n then a[x] else b[x]
                                                                      else c[x]
BY
{ (InstLemma `exception-not-value_1` [⌜u⌝;⌜v⌝;⌜m⌝]⋅ THEN Auto THEN RWO "-2" 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  if  x=n  then  f  a[x]  else  (f  b[x])    else  c[x])
9.  x  \mmember{}  \mBbbZ{}
10.  is-exception(m)
11.  u  :  Base
12.  v  :  Base
13.  m  \msim{}  exception(u;  v)
\mvdash{}  if  (x)  <  (m)    then  if  x=n  then  f  a[x]  else  (f  b[x])    else  c[x]  \mleq{}  if  (x)  <  (m)
                                                                                                                                            then  f 
                                                                                                                                                      if  x=n
                                                                                                                                                      then  a[x]
                                                                                                                                                      else  b[x]
                                                                                                                                            else  c[x]


By

---

Latex:
(InstLemma  `exception-not-value\_1`  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  RWO  "-2"  0  THEN  Auto)

---

Home Index