---

Step * of Lemma rmaximum-shift

∀[k,n,m:ℤ]. ∀[x:Top].  rmaximum(n;m;i.x[i]) ~ rmaximum(n - k;m - k;i.x[i + k]) supposing n ≤ m
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `rmaximum` 0
   THEN (Subst' m - k - n - k ~ m - n 0 THENA Auto)
   THEN (GenConcl ⌜(m - n) = N ∈ ℕ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN NatInd (-1)
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0⋅
   THEN Try (AutoSplit)) }

1
1. k : ℤ
2. n : ℤ
3. m : ℤ
4. x : Top
5. n ≤ m
6. N : ℤ
⊢ x[n] ~ x[(n - k) + k]

---

Latex:

---

Latex:
\mforall{}[k,n,m:\mBbbZ{}].  \mforall{}[x:Top].    rmaximum(n;m;i.x[i])  \msim{}  rmaximum(n  -  k;m  -  k;i.x[i  +  k])  supposing  n  \mleq{}  m


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `rmaximum`  0
  THEN  (Subst'  m  -  k  -  n  -  k  \msim{}  m  -  n  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(m  -  n)  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  NatInd  (-1)
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0\mcdot{}
  THEN  Try  (AutoSplit))

---

Home Index