---

Step * of Lemma Moessner-theorem

∀[x,y:Atom].
  ∀[n:ℕ]. ∀[k:ℕ+].
    (Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then 0 if (i =z 1) then n else 0 fi ;k)[bag-rep(n;x)] = k^n ∈ ℤ) 
  supposing ¬(x = y ∈ Atom)
BY
{ TACTIC:(InstLemma `KozenSilva-corollary2` []
          THEN RepeatFor 3 (ParallelLast')
          THEN (D 0 THENA Auto)
          THEN (InstHyp [⌜λi.if (i =z 0) then n else 0 fi ⌝] (-2)⋅ THENA Auto)
          THEN ParallelLast'
          THEN NthHypEq (-1)
          THEN EqCD
          THEN Auto) }

1
.....subterm..... T:t
2:n
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. ∀[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)
     ∈ ℤ)
5. n : ℕ
6. k : ℕ+
7. Moessner(ℤ-rng;x;y;1;λi.if (i =z 0)
                           then 0
                           else (λi.if (i =z 0) then n else 0 fi ) (i - 1)
                           fi ;k)[bag-rep(Σ((λi.if (i =z 0) then n else 0 fi ) i | i < k);x)]
= Π((k - i)^((λi.if (i =z 0) then n else 0 fi ) i) | i < k)
∈ ℤ
⊢ Moessner(ℤ-rng;x;y;1;λi.if (i =z 0) then 0
                          if (i =z 1) then n
                          else 0
                          fi ;k)[bag-rep(n;x)]
= Moessner(ℤ-rng;x;y;1;λi.if (i =z 0)
                          then 0
                          else (λi.if (i =z 0) then n else 0 fi ) (i - 1)
                          fi ;k)[bag-rep(Σ((λi.if (i =z 0) then n else 0 fi ) i | i < k);x)]
∈ ℤ

2
.....subterm..... T:t
3:n
1. x : Atom
2. y : Atom
3. ¬(x = y ∈ Atom)
4. ∀[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)
     ∈ ℤ)
5. n : ℕ
6. k : ℕ+
7. Moessner(ℤ-rng;x;y;1;λi.if (i =z 0)
                           then 0
                           else (λi.if (i =z 0) then n else 0 fi ) (i - 1)
                           fi ;k)[bag-rep(Σ((λi.if (i =z 0) then n else 0 fi ) i | i < k);x)]
= Π((k - i)^((λi.if (i =z 0) then n else 0 fi ) i) | i < k)
∈ ℤ
⊢ k^n = Π((k - i)^((λi.if (i =z 0) then n else 0 fi ) i) | i < k) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
TACTIC:(InstLemma  `KozenSilva-corollary2`  []
                THEN  RepeatFor  3  (ParallelLast')
                THEN  (D  0  THENA  Auto)
                THEN  (InstHyp  [\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  0)  then  n  else  0  fi  \mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                THEN  ParallelLast'
                THEN  NthHypEq  (-1)
                THEN  EqCD
                THEN  Auto)

---

Home Index