---

Step * 1 2 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 : {m:{1...}| ↑((λn.(((x n) + 4 <z y n ∨b(a n) + 4 <z b n) ∨b(c n) + 4 <z d n)) m)} 
9. quick-find(λn.(((x n) + 4 <z y n ∨b(a n) + 4 <z b n) ∨b(c n) + 4 <z d n);1)
= v
∈ {m:{1...}| ↑((λn.(((x n) + 4 <z y n ∨b(a n) + 4 <z b n) ∨b(c n) + 4 <z d n)) m)} 
⊢ eval n = v in
  if (c n) + 4 <z d n then inr n 
  if (x n) + 4 <z y n then inl inl n
  else inl (inr n )
  fi  ∈ ((x < y) ∨ (a < b)) ∨ (c < d)
BY
{ ((Thin (-1) THEN D (-1) THEN Reduce -1)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (BoolCase ⌜(c v) + 4 <z d v⌝⋅ THENA Auto)
   THEN Try (((MemCD THENA Auto) THEN MemTypeCD THEN Auto))) }

1
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)

---

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  :  \{m:\{1...\}|  \muparrow{}((\mlambda{}n.(((x  n)  +  4  <z  y  n  \mvee{}\msubb{}(a  n)  +  4  <z  b  n)  \mvee{}\msubb{}(c  n)  +  4  <z  d  n))  m)\} 
9.  quick-find(\mlambda{}n.(((x  n)  +  4  <z  y  n  \mvee{}\msubb{}(a  n)  +  4  <z  b  n)  \mvee{}\msubb{}(c  n)  +  4  <z  d  n);1)  =  v
\mvdash{}  eval  n  =  v  in
    if  (c  n)  +  4  <z  d  n  then  inr  n 
    if  (x  n)  +  4  <z  y  n  then  inl  inl  n
    else  inl  (inr  n  )
    fi    \mmember{}  ((x  <  y)  \mvee{}  (a  <  b))  \mvee{}  (c  <  d)


By

---

Latex:
((Thin  (-1)  THEN  D  (-1)  THEN  Reduce  -1)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}(c  v)  +  4  <z  d  v\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (((MemCD  THENA  Auto)  THEN  MemTypeCD  THEN  Auto)))

---

Home Index