---

Step * of Lemma Long-theorem

∀[x,y:Atom].
  ∀[a,b:ℤ]. ∀[n,k:ℕ+].
    (Moessner(ℤ-rng;x;y;((a - b)*atom(x)+(b)*atom(y));λi.if (i =z 0) then 1
                                                         if (i =z 1) then n - 1
                                                         else 0
                                                         fi ;k)[bag-rep(n;x)]
    = ((a + ((k - 1) * b)) * k^(n - 1))
    ∈ ℤ) 
  supposing ¬(x = y ∈ Atom)
BY
{ ((InstLemma `KozenSilva-theorem` [⌜ℤ-rng⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN OnMaybeHyp 3 (\h. ((InstHyp [⌜((a - b)*atom(x)+(b)*atom(y))⌝] h⋅ THENA Complete (Auto)) THEN Thin h))
   THEN Auto
   THEN (RWO "-3" 0 THEN Auto)
   THEN Reduce 0) }

1
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. a : ℤ
5. b : ℤ
6. ∀[d:ℕ ⟶ ℕ]. ∀[k:ℕ].
     (Moessner(ℤ-rng;x;y;((a - b)*atom(x)+(b)*atom(y));d;k)
     = ([((a - b)*atom(x)+(b)*atom(y))]_d 
                                        0(y:=((k ⋅ℤ-rng 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅ℤ-rng 1)*atom(x)
                                                                                            +atom(y)))^(d (i + 1)))
     ∈ PowerSeries(ℤ-rng))
7. n : ℕ+
8. k : ℕ+
⊢ ([((a - b)*atom(x)+(b)*atom(y))]_1(y:=((k ⋅ℤ-rng 1)*atom(x)+atom(y)))*Π(i∈upto(k)).((((k - i) ⋅ℤ-rng 1)*atom(x)
                                                                                       +atom(y)))^(if (i + 1 =z 0)
                                                                                                     then 1
if (i + 1 =z 1) then n - 1
else 0
fi ))[bag-rep(n;x)]
= ((a + ((k - 1) * b)) * k^(n - 1))
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[x,y:Atom].
    \mforall{}[a,b:\mBbbZ{}].  \mforall{}[n,k:\mBbbN{}\msupplus{}].
        (Moessner(\mBbbZ{}-rng;x;y;((a  -  b)*atom(x)+(b)*atom(y));\mlambda{}i.if  (i  =\msubz{}  0)  then  1
                                                                                                                  if  (i  =\msubz{}  1)  then  n  -  1
                                                                                                                  else  0
                                                                                                                  fi  ;k)[bag-rep(n;x)]
        =  ((a  +  ((k  -  1)  *  b))  *  k\^{}(n  -  1))) 
    supposing  \mneg{}(x  =  y)


By

---

Latex:
((InstLemma  `KozenSilva-theorem`  [\mkleeneopen{}\mBbbZ{}-rng\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  OnMaybeHyp  3  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}((a  -  b)*atom(x)+(b)*atom(y))\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))
                                                  THEN  Thin  h
                                                  ))
  THEN  Auto
  THEN  (RWO  "-3"  0  THEN  Auto)
  THEN  Reduce  0)

---

Home Index