Step * 1 of Lemma lifting-strict-int_eq


1. Base
2. ∀x,y,z,w:Base.  ((F[x;y;z;w])↓  (x)↓)
3. ∀u,v,y,z,w:Base.  (F[exception(u; v);y;z;w] exception(u; v))
4. ∀x,y,z,w:Base.  (is-exception(F[x;y;z;w])  (↓is-exception(x) ∨ (x)↓))
5. Base
6. Base
7. Base
8. Base
9. Base
10. Base
11. Base
12. is-exception(F[if a=b then else d;p;q;r])
13. is-exception(if a=b then else d)
14. a ∈ ℤ
15. is-exception(b)
⊢ F[if a=b then else d;p;q;r] ≤ if a=b then F[c;p;q;r] else F[d;p;q;r]
BY
TACTIC:(ExceptionSqequal (-1)
          THEN HypSubst' (-1) 0
          THEN (RW (SweepDnC IntEqExceptionC) THENA Auto)
          THEN RWO "3" 0
          THEN Auto) }


Latex:


Latex:

1.  F  :  Base
2.  \mforall{}x,y,z,w:Base.    ((F[x;y;z;w])\mdownarrow{}  {}\mRightarrow{}  (x)\mdownarrow{})
3.  \mforall{}u,v,y,z,w:Base.    (F[exception(u;  v);y;z;w]  \msim{}  exception(u;  v))
4.  \mforall{}x,y,z,w:Base.    (is-exception(F[x;y;z;w])  {}\mRightarrow{}  (\mdownarrow{}is-exception(x)  \mvee{}  (x)\mdownarrow{}))
5.  r  :  Base
6.  q  :  Base
7.  p  :  Base
8.  d  :  Base
9.  c  :  Base
10.  b  :  Base
11.  a  :  Base
12.  is-exception(F[if  a=b  then  c  else  d;p;q;r])
13.  is-exception(if  a=b  then  c  else  d)
14.  a  \mmember{}  \mBbbZ{}
15.  is-exception(b)
\mvdash{}  F[if  a=b  then  c  else  d;p;q;r]  \mleq{}  if  a=b  then  F[c;p;q;r]  else  F[d;p;q;r]


By


Latex:
TACTIC:(ExceptionSqequal  (-1)
                THEN  HypSubst'  (-1)  0
                THEN  (RW  (SweepDnC  IntEqExceptionC)  0  THENA  Auto)
                THEN  RWO  "3"  0
                THEN  Auto)




Home Index