---

Step * 1 2 1 of Lemma sq_stable__rless-or3


1. x : ℝ
2. y : ℝ
3. a : ℝ
4. b : ℝ
5. c : ℝ
6. d : ℝ
7. ((x < y) ∨ (a < b)) ∨ (c < d)
8. v : {1...}
9. ¬(c v) + 4 < d v
10. ↑(((x v) + 4 <z y v ∨b(a v) + 4 <z b v) ∨bff)
⊢ if (x v) + 4 <z y v then inl inl v else inl (inr v ) fi  ∈ ((x < y) ∨ (a < b)) ∨ (c < d)
BY
{ ((BoolCase ⌜(x v) + 4 <z y v⌝⋅ THENA Auto) THEN Try ((RepeatFor 2 ((MemCD THENA Auto)) THEN MemTypeCD THEN Auto))) }

1
.....set predicate..... 
1. x : ℝ
2. y : ℝ
3. a : ℝ
4. b : ℝ
5. c : ℝ
6. d : ℝ
7. ((x < y) ∨ (a < b)) ∨ (c < d)
8. v : {1...}
9. ¬(x v) + 4 < y v
10. ¬(c v) + 4 < d v
11. ↑((a v) + 4 <z b v ∨bff)
⊢ (a v) + 4 < b v

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  a  :  \mBbbR{}
4.  b  :  \mBbbR{}
5.  c  :  \mBbbR{}
6.  d  :  \mBbbR{}
7.  ((x  <  y)  \mvee{}  (a  <  b))  \mvee{}  (c  <  d)
8.  v  :  \{1...\}
9.  \mneg{}(c  v)  +  4  <  d  v
10.  \muparrow{}(((x  v)  +  4  <z  y  v  \mvee{}\msubb{}(a  v)  +  4  <z  b  v)  \mvee{}\msubb{}ff)
\mvdash{}  if  (x  v)  +  4  <z  y  v  then  inl  inl  v  else  inl  (inr  v  )  fi    \mmember{}  ((x  <  y)  \mvee{}  (a  <  b))  \mvee{}  (c  <  d)


By

---

Latex:
((BoolCase  \mkleeneopen{}(x  v)  +  4  <z  y  v\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((RepeatFor  2  ((MemCD  THENA  Auto))  THEN  MemTypeCD  THEN  Auto))
  )

---

Home Index