---

Step * of Lemma callbyvalueall_seq-lambdas-all

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

1
1. L : Top
2. G : Top
3. H : Top
4. F : Top
5. k : ℤ
6. K : Top
7. n : ℤ
8. 0 ≤ n
⊢ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.G[f]] H[g]);n;n + 0) 
~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.(g mk_lambdas(G[f];n + 0))] H[g]);n;n + 0)

2
1. L : Top
2. G : Top
3. H : Top
4. F : Top
5. k : ℤ
6. 0 < k
7. ∀K:Top. ∀n:ℤ.
     ((0 ≤ n)
     ⇒ (callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.G[f]] H[g]);n;n + (k - 1)) 
        ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.(g mk_lambdas(G[f];n + (k - 1)))] H[g]);n;n + (k - 1))))
8. K : Top
9. n : ℤ
10. 0 ≤ n
⊢ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.G[f]] H[g]);n;n + k) 
~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F[λf.(g mk_lambdas(G[f];n + k))] H[g]);n;n + k)

---

Latex:

---

Latex:
\mforall{}[L,G,H,K,F:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].
    (callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(F[\mlambda{}f.G[f]]  H[g]);n;m) 
    \msim{}  callbyvalueall\_seq(L;\mlambda{}f.mk\_applies(f;K;n);\mlambda{}g.(F[\mlambda{}f.(g  mk\_lambdas(G[f];m))]  H[g]);n;m))


By

---

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

---

Home Index