---

Step * of Lemma callbyvalueall_seq-decomp-last

∀[L,K,F:Top]. ∀[m:ℕ]. ∀[n:ℕm].
  (callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;m) ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ g 
                                                                                                            (L (m - 1))
                                                                                                   in F (λf.(g f x));n
                                                                        ;m - 1))
BY
{ ((UnivCD THENA Auto)
   THEN RepeatFor 2 ((D (-1) THENA Auto))
   THEN (Assert ⌜∃k:ℕ. (m = ((n + k) + 1) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n + 1⌝]⋅ THEN Auto'))
   THEN D (-1)
   THEN HypSubst' (-1) 0
   THEN ThinVar `m'
   THEN (Subst ⌜((n + k) + 1) - 1 ~ n + k⌝ 0⋅ THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-3))
   THEN NatInd (-1)) }

1
.....basecase..... 
1. L : Top
2. F : Top
3. k : ℤ
⊢ ∀K:Top. ∀n:ℤ.
    ((0 ≤ n)
    ⇒ (callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;(n + 0) + 1) 
       ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ g (L (n + 0))
                                                      in F (λf.(g f x));n;n + 0)))

2
.....upcase..... 
1. L : Top
2. F : Top
3. k : ℤ
4. 0 < k
5. ∀K:Top. ∀n:ℤ.
     ((0 ≤ n)
     ⇒ (callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;(n + (k - 1)) + 1) 
        ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ g (L (n + (k - 1)))
                                                       in F (λf.(g f x));n;n + (k - 1))))
⊢ ∀K:Top. ∀n:ℤ.
    ((0 ≤ n)
    ⇒ (callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;(n + k) + 1) 
       ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.let x ⟵ g (L (n + k))
                                                      in F (λf.(g f x));n;n + k)))

---

Latex:

---

Latex:
\mforall{}[L,K,F:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m].
    (callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);F;n;m) 
    \msim{}  callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.let  x  \mleftarrow{}{}  g  (L  (m  -  1))
                                                                                                  in  F  (\mlambda{}f.(g  f  x));n;m  -  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepeatFor  2  ((D  (-1)  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}.  (m  =  ((n  +  k)  +  1))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n  +  1\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  D  (-1)
  THEN  HypSubst'  (-1)  0
  THEN  ThinVar  `m'
  THEN  (Subst  \mkleeneopen{}((n  +  k)  +  1)  -  1  \msim{}  n  +  k\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-3))
  THEN  NatInd  (-1))

---

Home Index