---

Step * 1 1 1 of Lemma spread-sqle-pi12


1. P : Base
2. ∀u,v:Base.  (P[exception(u; v);exception(u; v)] ~ exception(u; v))
3. t : Base
4. is-exception(let x,y = t 
                in P[x;y])
5. is-exception(t)
6. u : Base
7. v : Base
8. t ~ exception(u; v)
⊢ exception(u; v) ≤ P[exception(u; v);exception(u; v)]
BY
{ (RWO "2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  P  :  Base
2.  \mforall{}u,v:Base.    (P[exception(u;  v);exception(u;  v)]  \msim{}  exception(u;  v))
3.  t  :  Base
4.  is-exception(let  x,y  =  t 
                                in  P[x;y])
5.  is-exception(t)
6.  u  :  Base
7.  v  :  Base
8.  t  \msim{}  exception(u;  v)
\mvdash{}  exception(u;  v)  \mleq{}  P[exception(u;  v);exception(u;  v)]


By

---

Latex:
(RWO  "2"  0  THEN  Auto)

---

Home Index