---

Step * of Lemma cbv_sqle_2

∀[a,b,X,Y:Base].
  eval x = a in
  X[x] ≤ eval x = b in
         Y[x] 
  supposing ((a)↓ ⇒ (X[a] ≤ eval x = b in Y[x]))
  ∧ (∀u,v:Base.  ((a ~ exception(u; v)) ⇒ (eval x = b in Y[x] ~ exception(u; v))))
BY
{ (SqReasoning
   THEN ExceptionSqequal (-1)⋅
   THEN HypSubst' (-1) 0
   THEN (Subst' eval x = b in Y[x] ~ exception(u; v) 0 THENA Auto)
   THEN RW  (SubC (TagC (mk_tag_term 1))) 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b,X,Y:Base].
    eval  x  =  a  in
    X[x]  \mleq{}  eval  x  =  b  in
                  Y[x] 
    supposing  ((a)\mdownarrow{}  {}\mRightarrow{}  (X[a]  \mleq{}  eval  x  =  b  in  Y[x]))
    \mwedge{}  (\mforall{}u,v:Base.    ((a  \msim{}  exception(u;  v))  {}\mRightarrow{}  (eval  x  =  b  in  Y[x]  \msim{}  exception(u;  v))))


By

---

Latex:
(SqReasoning
  THEN  ExceptionSqequal  (-1)\mcdot{}
  THEN  HypSubst'  (-1)  0
  THEN  (Subst'  eval  x  =  b  in  Y[x]  \msim{}  exception(u;  v)  0  THENA  Auto)
  THEN  RW    (SubC  (TagC  (mk\_tag\_term  1)))  0
  THEN  Auto)

---

Home Index