---

Step * of Lemma oal_merge_conses_lemma

∀qs,vq,kq,ps,vp,kp,b,a:Top.
  ([<kp, vp> / ps] ++ [<kq, vq> / qs] ~ 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
{ (UnivCD THENA Auto) }

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
⊢ [<kp, vp> / ps] ++ [<kq, vq> / qs] ~ 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:
\mforall{}qs,vq,kq,ps,vp,kp,b,a:Top.
    ([<kp,  vp>  /  ps]  ++  [<kq,  vq>  /  qs]  \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:
(UnivCD  THENA  Auto)

---

Home Index