---

Step * of Lemma lifting-strict-atom_eq

∀[F:Base]. ∀[p,q,r:Top].
  ∀[a,b,c,d:Top].  (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 ) 
  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=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 

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=b then F[c;p;q;r] else F[d;p;q;r] fi )
11. a ∈ Atom
12. is-exception(b)
⊢ if a=b then F[c;p;q;r] else F[d;p;q;r] fi  ≤ F[if a=b then c else d fi ;p;q;r]

---

Latex:

---

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


By

---

Latex:
SqReasoning

---

Home Index