---

Step * 1 of Lemma finite-partition

.....basecase..... 
∀k:ℕ. ∀c:ℕ0 ⟶ ℕk.
  ∃p:ℕk ⟶ (ℕ List)
   ((Σ(||p j|| | j < k) = 0 ∈ ℤ)
   ∧ (∀j:ℕk. ∀x,y:ℕ||p j||.  p j[x] > p j[y] supposing x < y)
   ∧ (∀j:ℕk. ∀x:ℕ||p j||.  (p j[x] < 0 c∧ ((c p j[x]) = j ∈ ℤ))))
BY
{ TACTIC:(Auto THEN InstConcl [⌜λj.[]⌝]⋅ THEN Reduce 0 THEN Auto THEN RWW "sum_constant" 0 THEN Auto') }

---

Latex:

---

Latex:
.....basecase..... 
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbN{}0  {}\mrightarrow{}  \mBbbN{}k.
    \mexists{}p:\mBbbN{}k  {}\mrightarrow{}  (\mBbbN{}  List)
      ((\mSigma{}(||p  j||  |  j  <  k)  =  0)
      \mwedge{}  (\mforall{}j:\mBbbN{}k.  \mforall{}x,y:\mBbbN{}||p  j||.    p  j[x]  >  p  j[y]  supposing  x  <  y)
      \mwedge{}  (\mforall{}j:\mBbbN{}k.  \mforall{}x:\mBbbN{}||p  j||.    (p  j[x]  <  0  c\mwedge{}  ((c  p  j[x])  =  j))))


By

---

Latex:
TACTIC:(Auto  THEN  InstConcl  [\mkleeneopen{}\mlambda{}j.[]\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto  THEN  RWW  "sum\_constant"  0  THEN  Auto')

---

Home Index