---

Step * 1 2 4 of Lemma qadd_grp_wf2


1. z : ℚ
⊢ monot(ℚ;x,y.↑q_le(x;y);λw.(z + w))
BY
{ ((RepUR ``monot`` 0 THEN Auto)
   THEN (RWO "q_le-elim" (-1) THENA Complete (Auto))
   THEN (RW assert_pushdownC (-1) THENA Complete (Auto))
   THEN (RWO "q_le-elim" 0 THENA Complete (Auto))
   THEN (RW assert_pushdownC 0 THENA Complete (Auto))
   THEN (ParallelLast THEN Try (Complete (Auto)))
   THEN ((NthHypEq (-1)) THEN RepeatFor 2 ((EqCD THEN Auto)))
   THEN QAddReduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  z  :  \mBbbQ{}
\mvdash{}  monot(\mBbbQ{};x,y.\muparrow{}q\_le(x;y);\mlambda{}w.(z  +  w))


By

---

Latex:
((RepUR  ``monot``  0  THEN  Auto)
  THEN  (RWO  "q\_le-elim"  (-1)  THENA  Complete  (Auto))
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Complete  (Auto))
  THEN  (RWO  "q\_le-elim"  0  THENA  Complete  (Auto))
  THEN  (RW  assert\_pushdownC  0  THENA  Complete  (Auto))
  THEN  (ParallelLast  THEN  Try  (Complete  (Auto)))
  THEN  ((NthHypEq  (-1))  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))
  THEN  QAddReduce  0
  THEN  Auto)

---

Home Index