---

Step * 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)
⊢ let x,y = exception(u; v) 
  in P[x;y] ≤ P[fst((exception(u; v)));snd((exception(u; v)))]
BY
{ (RW (AddrC [1] (TagC (mk_tag_term 1))) 0
   THEN RW (AddrC [2;2] (TagC (mk_tag_term 2))) 0
   THEN RW (AddrC [2;3] (TagC (mk_tag_term 2))) 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)
⊢ exception(u; v) ≤ P[exception(u; v);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)
6.  u  :  Base
7.  v  :  Base
8.  t  \msim{}  exception(u;  v)
\mvdash{}  let  x,y  =  exception(u;  v) 
    in  P[x;y]  \mleq{}  P[fst((exception(u;  v)));snd((exception(u;  v)))]


By

---

Latex:
(RW  (AddrC  [1]  (TagC  (mk\_tag\_term  1)))  0
  THEN  RW  (AddrC  [2;2]  (TagC  (mk\_tag\_term  2)))  0
  THEN  RW  (AddrC  [2;3]  (TagC  (mk\_tag\_term  2)))  0)

---

Home Index