---

Step * of Lemma max-metric-leq-rn-metric

∀[n:ℕ]. max-metric(n) ≤ rn-metric(n)
BY
{ (RepUR ``metric-leq mdist max-metric rn-metric`` 0
   THEN InductionOnNat
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (OReduce 0 THEN Auto)
   THEN BLemma `rmax_lb`
   THEN Auto
   THEN RWO  "3" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  max-metric(n)  \mleq{}  rn-metric(n)


By

---

Latex:
(RepUR  ``metric-leq  mdist  max-metric  rn-metric``  0
  THEN  InductionOnNat
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (OReduce  0  THEN  Auto)
  THEN  BLemma  `rmax\_lb`
  THEN  Auto
  THEN  RWO    "3"  0
  THEN  Auto)

---

Home Index