---

Step * 1 of Lemma lifting-strict-atom_eq


1. F : 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. 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 fi ;p;q;r])
13. is-exception(if a=b then c else d fi )
14. a ∈ Atom
15. is-exception(b)
⊢ F[if a=b then c else d fi ;p;q;r] ≤ if a=b then F[c;p;q;r] else F[d;p;q;r] fi 
BY
{ TACTIC:(ExceptionSqequal (-1)
          THEN HypSubst' (-1) 0
          THEN (RW (SweepDnC AtomEqExceptionC) 0 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  fi  ;p;q;r])
13.  is-exception(if  a=b  then  c  else  d  fi  )
14.  a  \mmember{}  Atom
15.  is-exception(b)
\mvdash{}  F[if  a=b  then  c  else  d  fi  ;p;q;r]  \mleq{}  if  a=b  then  F[c;p;q;r]  else  F[d;p;q;r]  fi 


By

---

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

---

Home Index