---

Step * of Lemma rminimum_functionality

∀[n,m:ℤ].
  ∀[x,y:{n..m + 1-} ⟶ ℝ].
    rminimum(n;m;k.x[k]) = rminimum(n;m;k.y[k]) supposing ∀k:ℤ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (x[k] = y[k])) 
  supposing n ≤ m
BY
{ (Auto
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN Unfold `rminimum` 0
   THEN (GenConcl ⌜(m - n) = k ∈ ℕ⌝⋅ THENA Auto')
   THEN (Subst ⌜m ~ n + k⌝ 0⋅ THENL [Auto'; (ThinVar `m' THEN (NatInd (-1)) THEN Reduce 0)])) }

1
1. n : ℤ
2. k : ℤ
⊢ ∀x,y:{n..(n + 0) + 1-} ⟶ ℝ.  ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + 0)) ⇒ (x[k@0] = y[k@0]))) ⇒ (x[n] = y[n]))

2
.....upcase..... 
1. n : ℤ
2. k : ℤ
3. 0 < k
4. ∀x,y:{n..(n + (k - 1)) + 1-} ⟶ ℝ.
     ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + (k - 1))) ⇒ (x[k@0] = y[k@0])))
     ⇒ (primrec(k - 1;x[n];λi,s. rmin(s;x[n + i + 1])) = primrec(k - 1;y[n];λi,s. rmin(s;y[n + i + 1]))))
⊢ ∀x,y:{n..(n + k) + 1-} ⟶ ℝ.
    ((∀k@0:ℤ. ((n ≤ k@0) ⇒ (k@0 ≤ (n + k)) ⇒ (x[k@0] = y[k@0])))
    ⇒ (primrec(k;x[n];λi,s. rmin(s;x[n + i + 1])) = primrec(k;y[n];λi,s. rmin(s;y[n + i + 1]))))

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].
    \mforall{}[x,y:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].
        rminimum(n;m;k.x[k])  =  rminimum(n;m;k.y[k]) 
        supposing  \mforall{}k:\mBbbZ{}.  ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  m)  {}\mRightarrow{}  (x[k]  =  y[k])) 
    supposing  n  \mleq{}  m


By

---

Latex:
(Auto
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  Unfold  `rminimum`  0
  THEN  (GenConcl  \mkleeneopen{}(m  -  n)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  (Subst  \mkleeneopen{}m  \msim{}  n  +  k\mkleeneclose{}  0\mcdot{}  THENL  [Auto';  (ThinVar  `m'  THEN  (NatInd  (-1))  THEN  Reduce  0)]))

---

Home Index