---

Step * 1 of Lemma lifting-strict-atom_eq1


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


By

---

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

---

Home Index