---

Step * 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)
⊢ let x,y = t 
  in P[x;y] ≤ P[fst(t);snd(t)]
BY
{ (ExceptionSqequal (-1) THEN HypSubst' (-1) 0) }

1
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)
⊢ let x,y = exception(u; v) 
  in P[x;y] ≤ P[fst((exception(u; v)));snd((exception(u; v)))]

---

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)
\mvdash{}  let  x,y  =  t 
    in  P[x;y]  \mleq{}  P[fst(t);snd(t)]


By

---

Latex:
(ExceptionSqequal  (-1)  THEN  HypSubst'  (-1)  0)

---

Home Index