---

Step * 2 of Lemma combinations_aux_wf


1. n : ℤ
2. 0 < n
3. ∀[b,m:ℕ].  (combinations_aux(b;n - 1;m) ∈ ℕ)
⊢ ∀[b,m:ℕ].
    (if (n =z 0) then b else eval b2 = b * m in eval n2 = n - 1 in eval m2 = m - 1 in   combinations_aux(b2;n2;m2) fi 
     ∈ ℕ)
BY
{ ((SplitOnConclITE THEN Try (Complete (Auto)))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN CaseNat 0 `m')⋅ }

1
1. n : ℤ
2. 0 < n
3. ∀[b,m:ℕ].  (combinations_aux(b;n - 1;m) ∈ ℕ)
4. ¬(n = 0 ∈ ℤ)
5. b : ℕ
6. m : ℕ
7. m = 0 ∈ ℤ
⊢ eval m2 = 0 - 1 in
  combinations_aux(b * 0;n - 1;m2) ∈ ℕ

2
1. n : ℤ
2. 0 < n
3. ∀[b,m:ℕ].  (combinations_aux(b;n - 1;m) ∈ ℕ)
4. ¬(n = 0 ∈ ℤ)
5. b : ℕ
6. m : ℕ
7. ¬(m = 0 ∈ ℤ)
⊢ eval m2 = m - 1 in
  combinations_aux(b * m;n - 1;m2) ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[b,m:\mBbbN{}].    (combinations\_aux(b;n  -  1;m)  \mmember{}  \mBbbN{})
\mvdash{}  \mforall{}[b,m:\mBbbN{}].
        (if  (n  =\msubz{}  0)
          then  b
          else  eval  b2  =  b  *  m  in
                    eval  n2  =  n  -  1  in
                    eval  m2  =  m  -  1  in
                        combinations\_aux(b2;n2;m2)
          fi    \mmember{}  \mBbbN{})


By

---

Latex:
((SplitOnConclITE  THEN  Try  (Complete  (Auto)))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  CaseNat  0  `m')\mcdot{}

---

Home Index