---

Step * of Lemma spread-sqle-pi12

∀[P:Base]
  ∀[t:Top]. (let x,y = t in P[x;y] ≤ P[fst(t);snd(t)]) 
  supposing ∀u,v:Base.  (P[exception(u; v);exception(u; v)] ~ exception(u; v))
BY
{ SqReasoning }

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

---

Latex:

---

Latex:
\mforall{}[P:Base]
    \mforall{}[t:Top].  (let  x,y  =  t  in  P[x;y]  \mleq{}  P[fst(t);snd(t)]) 
    supposing  \mforall{}u,v:Base.    (P[exception(u;  v);exception(u;  v)]  \msim{}  exception(u;  v))


By

---

Latex:
SqReasoning

---

Home Index