---

Step * of Lemma KozenSilva-corollary2

∀[x,y:Atom].
  ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
    (Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then 0 else d (i - 1) fi ;k)[bag-rep(Σ(d i | i < k);x)]
    = Π((k - i)^(d i) | i < k)
    ∈ ℤ) 
  supposing ¬(x = y ∈ Atom)
BY
{ (InstLemma `KozenSilva-corollary1` []
   THEN RepeatFor 5 (ParallelLast')
   THEN HypSubst (-1) 0
   THEN Auto
   THEN Try ((MemTypeCD THEN Auto THEN BLemma `non_neg_sum` THEN Auto))
   THEN Assert ⌜∀d:ℕ ⟶ ℕ
                  (Π(i∈upto(k)).(((k - i)*atom(x)+atom(y)))^(d i)[bag-rep(Σ(d i | i < k);x)]
                  = Π((k - i)^(d i) | i < k)
                  ∈ ℤ)⌝⋅
   THEN Try (Complete (Auto))
   THEN ThinVar `d'
   THEN NatInd (-1)) }

1
.....basecase..... 
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℤ
⊢ ∀d:ℕ ⟶ ℕ. (Π(i∈upto(0)).(((0 - i)*atom(x)+atom(y)))^(d i)[bag-rep(Σ(d i | i < 0);x)] = Π((0 - i)^(d i) | i < 0) ∈ ℤ)

2
.....upcase..... 
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. k : ℤ
5. 0 < k
6. ∀d:ℕ ⟶ ℕ
     (Π(i∈upto(k - 1)).(((k - 1 - i)*atom(x)+atom(y)))^(d i)[bag-rep(Σ(d i | i < k - 1);x)]
     = Π((k - 1 - i)^(d i) | i < k - 1)
     ∈ ℤ)
⊢ ∀d:ℕ ⟶ ℕ. (Π(i∈upto(k)).(((k - i)*atom(x)+atom(y)))^(d i)[bag-rep(Σ(d i | i < k);x)] = Π((k - i)^(d i) | i < k) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}[x,y:Atom].
    \mforall{}[d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[k:\mBbbN{}].
        (Moessner(\mBbbZ{}-rng;x;y;1;\mlambda{}i.if  (i  =\msubz{}  0)  then  0  else  d  (i  -  1)  fi  ;k)[bag-rep(\mSigma{}(d  i  |  i  <  k);x)]
        =  \mPi{}((k  -  i)\^{}(d  i)  |  i  <  k)) 
    supposing  \mneg{}(x  =  y)


By

---

Latex:
(InstLemma  `KozenSilva-corollary1`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  HypSubst  (-1)  0
  THEN  Auto
  THEN  Try  ((MemTypeCD  THEN  Auto  THEN  BLemma  `non\_neg\_sum`  THEN  Auto))
  THEN  Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                                (\mPi{}(i\mmember{}upto(k)).(((k  -  i)*atom(x)+atom(y)))\^{}(d  i)[bag-rep(\mSigma{}(d  i  |  i  <  k);x)]
                                =  \mPi{}((k  -  i)\^{}(d  i)  |  i  <  k))\mkleeneclose{}\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  ThinVar  `d'
  THEN  NatInd  (-1))

---

Home Index