---

Step * of Lemma callbyvalueall_seq-partial-ap-all

∀[L,K,F:Top]. ∀[m:ℕ]. ∀[n:ℕm + 1].
  (callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;m) 
  ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F partial_ap(g;m;m));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. F : Top
3. k : ℤ
4. K : Top
5. n : ℤ
6. 0 ≤ n
⊢ callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;n + 0) ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F 
                                                                                                       partial_ap(g;n
                                                                                                       + 0;n + 0));n;n
                                                                           + 0)

2
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)) 
        ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F partial_ap(g;n + (k - 1);n + (k - 1)));n;n + (k - 1))))
6. K : Top
7. n : ℤ
8. 0 ≤ n
⊢ callbyvalueall_seq(L;λf.mk_applies(f;K;n);F;n;n + k) ~ callbyvalueall_seq(L;λf.mk_applies(f;K;n);λg.(F 
                                                                                                       partial_ap(g;n
                                                                                                       + k;n + k));n;n
                                                                           + k)

---

Latex:

---

Latex:
\mforall{}[L,K,F:Top].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].
    (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.(F  partial\_ap(g;m;m));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