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