---

Step * 1 of Lemma max-metric_wf


1. n : ℤ
2. 0 < n
3. (λp,q. primrec(n - 1;r0;λi,r. rmax(r;|(p i) - q i|)))
= (λp,q. primrec(n - 1;r0;λi,r. rmax(r;|(p i) - q i|)))
∈ (ℝ^n - 1 ⟶ ℝ^n - 1 ⟶ ℝ)
4. ∀x,y,z:ℝ^n - 1.
     (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - z i|)) ≤ (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - y i|))
     + primrec(n - 1;r0;λi,r. rmax(r;|(z i) - y i|))))
5. ∀x:ℝ^n - 1. (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - x i|)) = r0)
6. x : ℝ^n
7. y : ℝ^n
8. z : ℝ^n
⊢ rmax(primrec(n - 1;r0;λi,r. rmax(r;|(x i) - z i|));|(x (n - 1)) - z 
                                                                (n - 1)|) ≤ (rmax(primrec(n - 1;r0;λi,r. rmax(r;|(x i) 
                                                                                                        - y i|));|(x 
                                                                                                               (n - 1)) 
- y (n - 1)|)
+ rmax(primrec(n - 1;r0;λi,r. rmax(r;|(z i) - y i|));|(z (n - 1)) - y (n - 1)|))
BY
{ ((InstHyp [⌜x⌝;⌜y⌝;⌜z⌝] 4⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;1]⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2;1]⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2;2]⋅ THENA Auto)
   THEN (Assert |(x (n - 1)) - z (n - 1)| ≤ (|(x (n - 1)) - y (n - 1)| + |(z (n - 1)) - y (n - 1)|) BY
               (UseTriangleInequality [⌜y (n - 1)⌝]⋅
                THEN Auto
                THEN RW (AddrC [1;2] (LemmaC `rabs-difference-symmetry`)) 0
                THEN Auto))
   THEN MoveToConcl (-1)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;1]⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2;1]⋅ THENA Auto)
   THEN (GenConclAtAddrType ⌜ℝ⌝ [1;2;2]⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. v : ℝ
2. v1 : ℝ
3. v2 : ℝ
4. v3 : ℝ
5. v4 : ℝ
6. v5 : ℝ
7. v3 ≤ (v4 + v5)
8. v ≤ (v1 + v2)
⊢ rmax(v;v3) ≤ (rmax(v1;v4) + rmax(v2;v5))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  (\mlambda{}p,q.  primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(p  i)  -  q  i|)))
=  (\mlambda{}p,q.  primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(p  i)  -  q  i|)))
4.  \mforall{}x,y,z:\mBbbR{}\^{}n  -  1.
          (primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  z  i|))  \mleq{}  (primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  y  i|))
          +  primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(z  i)  -  y  i|))))
5.  \mforall{}x:\mBbbR{}\^{}n  -  1.  (primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  x  i|))  =  r0)
6.  x  :  \mBbbR{}\^{}n
7.  y  :  \mBbbR{}\^{}n
8.  z  :  \mBbbR{}\^{}n
\mvdash{}  rmax(primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  z  i|));|(x  (n  -  1)) 
-  z  (n  -  1)|)  \mleq{}  (rmax(primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  y  i|));|(x  (n  -  1))  -  y  (n  -  1)|)
+  rmax(primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(z  i)  -  y  i|));|(z  (n  -  1))  -  y  (n  -  1)|))


By

---

Latex:
((InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;1]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2;1]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2;2]\mcdot{}  THENA  Auto)
  THEN  (Assert  |(x  (n  -  1))  -  z  (n  -  1)|  \mleq{}  (|(x  (n  -  1))  -  y  (n  -  1)|  +  |(z  (n  -  1))  -  y  (n  -  1)|)  BY
                          (UseTriangleInequality  [\mkleeneopen{}y  (n  -  1)\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  RW  (AddrC  [1;2]  (LemmaC  `rabs-difference-symmetry`))  0
                            THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;1]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2;1]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType  \mkleeneopen{}\mBbbR{}\mkleeneclose{}  [1;2;2]\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index