---

Step * of Lemma lifting-strict-atom_eq1

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c,d:Top].  (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]) 
  supposing strict4(λx,y,z,w. F[x;y;z;w])
BY
{ SqReasoning }

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

2
1. F : Base
2. strict4(λx,y,z,w. F[x;y;z;w])
3. d : Base
4. r : Base
5. q : Base
6. p : Base
7. c : Base
8. b : Base
9. a : Base
10. is-exception(if a=1 b
                  then F[c;p;q;r]
                  else F[d;p;q;r])
11. a ∈ Atom1
12. is-exception(b)
⊢ if a=1 b
   then F[c;p;q;r]
   else F[d;p;q;r] ≤ F[if a=1 b
                        then c
                        else d;p;q;r]

---

Latex:

---

Latex:
\mforall{}[F:Base].  \mforall{}[p,q,r:Top].
    \mforall{}[a,b,c,d:Top].    (F[if  a=1  b  then  c  else  d;p;q;r]  \msim{}  if  a=1  b  then  F[c;p;q;r]  else  F[d;p;q;r]) 
    supposing  strict4(\mlambda{}x,y,z,w.  F[x;y;z;w])


By

---

Latex:
SqReasoning

---

Home Index