---

Step * of Lemma callbyvalueall_seq-shift

∀[L,F,K:Top]. ∀[m,n,k:ℕ].  (callbyvalueall_seq(λi.(L (i + k));K;F;n;m) ~ callbyvalueall_seq(L;K;F;n + k;m + k))
BY
{ ((UnivCD THENA Auto)
   THEN (Decide n ≤ m THENA Auto)
   THEN Try (Complete ((RecUnfold `callbyvalueall_seq` 0 THEN RepeatFor 2 (AutoSplit) THEN Auto')))
   THEN (Assert ⌜∃j:ℕ. (m = (n + j) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto'))
   THEN D (-1)
   THEN HypSubst' (-1) 0
   THEN ThinVar `m'
   THEN RepeatFor 3 (MoveToConcl (-2))
   THEN NatInd (-1)
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((RecUnfold `callbyvalueall_seq` 0 THEN RepeatFor 2 (AutoSplit))))) }

1
1. L : Top
2. F : Top
3. j : ℤ
4. 0 < j
5. ∀K:Top. ∀n,k:ℕ.
     (callbyvalueall_seq(λi.(L (i + k));K;F;n;n + (j - 1)) ~ callbyvalueall_seq(L;K;F;n + k;(n + (j - 1)) + k))
6. K : Top
7. n : ℕ
8. k : ℕ
⊢ callbyvalueall_seq(λi.(L (i + k));K;F;n;n + j) ~ callbyvalueall_seq(L;K;F;n + k;(n + j) + k)

---

Latex:

---

Latex:
\mforall{}[L,F,K:Top].  \mforall{}[m,n,k:\mBbbN{}].
    (callbyvalueall\_seq(\mlambda{}i.(L  (i  +  k));K;F;n;m)  \msim{}  callbyvalueall\_seq(L;K;F;n  +  k;m  +  k))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Decide  n  \mleq{}  m  THENA  Auto)
  THEN  Try  (Complete  ((RecUnfold  `callbyvalueall\_seq`  0  THEN  RepeatFor  2  (AutoSplit)  THEN  Auto')))
  THEN  (Assert  \mkleeneopen{}\mexists{}j:\mBbbN{}.  (m  =  (n  +  j))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  D  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  ThinVar  `m'
  THEN  RepeatFor  3  (MoveToConcl  (-2))
  THEN  NatInd  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((RecUnfold  `callbyvalueall\_seq`  0  THEN  RepeatFor  2  (AutoSplit)))))

---

Home Index