---

Step * 1 1 of Lemma oal_merge_conses_lemma


1. qs : Top@i
2. vq : Top@i
3. kq : Top@i
4. ps : Top@i
5. vp : Top@i
6. kp : Top@i
7. b : Top@i
8. a : Top@i
⊢ if kq <b kp then [<kp, vp> / (ps ++ [<kq, vq> / qs])]
if kp <b kq then [<kq, vq> / ([<kp, vp> / ps] ++ qs)]
if (vp * vq) =b e then ps ++ qs
else [<kp, vp * vq> / (ps ++ qs)]
fi  ~ if kq <b kp then [<kp, vp> / (ps ++ [<kq, vq> / qs])]
if kp <b kq then [<kq, vq> / ([<kp, vp> / ps] ++ qs)]
if (vp * vq) =b e then ps ++ qs
else [<kp, vp * vq> / (ps ++ qs)]
fi 
BY
{ Try (RW (AddrC [2] (IdC)) 0)⋅ }

1
1. qs : Top@i
2. vq : Top@i
3. kq : Top@i
4. ps : Top@i
5. vp : Top@i
6. kp : Top@i
7. b : Top@i
8. a : Top@i
⊢ if kq <b kp then [<kp, vp> / (ps ++ [<kq, vq> / qs])]
if kp <b kq then [<kq, vq> / ([<kp, vp> / ps] ++ qs)]
if (vp * vq) =b e then ps ++ qs
else [<kp, vp * vq> / (ps ++ qs)]
fi  ~ if kq <b kp then [<kp, vp> / (ps ++ [<kq, vq> / qs])]
if kp <b kq then [<kq, vq> / ([<kp, vp> / ps] ++ qs)]
if (vp * vq) =b e then ps ++ qs
else [<kp, vp * vq> / (ps ++ qs)]
fi 

---

Latex:

---

Latex:

1.  qs  :  Top@i
2.  vq  :  Top@i
3.  kq  :  Top@i
4.  ps  :  Top@i
5.  vp  :  Top@i
6.  kp  :  Top@i
7.  b  :  Top@i
8.  a  :  Top@i
\mvdash{}  if  kq  <\msubb{}  kp  then  [<kp,  vp>  /  (ps  ++  [<kq,  vq>  /  qs])]
if  kp  <\msubb{}  kq  then  [<kq,  vq>  /  ([<kp,  vp>  /  ps]  ++  qs)]
if  (vp  *  vq)  =\msubb{}  e  then  ps  ++  qs
else  [<kp,  vp  *  vq>  /  (ps  ++  qs)]
fi    \msim{}  if  kq  <\msubb{}  kp  then  [<kp,  vp>  /  (ps  ++  [<kq,  vq>  /  qs])]
if  kp  <\msubb{}  kq  then  [<kq,  vq>  /  ([<kp,  vp>  /  ps]  ++  qs)]
if  (vp  *  vq)  =\msubb{}  e  then  ps  ++  qs
else  [<kp,  vp  *  vq>  /  (ps  ++  qs)]
fi 


By

---

Latex:
Try  (RW  (AddrC  [2]  (IdC))  0)\mcdot{}

---

Home Index