---

Step * 2 of Lemma combinations_aux_rem_wf


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

1
1. k : ℕ+
2. n : ℤ
3. 0 < n
4. ∀[b,m:ℕ].  (combinations_aux_rem(b;n - 1;m;k) ∈ ℕ)
5. ¬(n = 0 ∈ ℤ)
6. b : ℕ
7. m : ℕ
8. m = 0 ∈ ℤ
⊢ combinations_aux_rem(b * 0 rem k;n - 1;0 - 1;k) ∈ ℕ

2
1. k : ℕ+
2. n : ℤ
3. 0 < n
4. ∀[b,m:ℕ].  (combinations_aux_rem(b;n - 1;m;k) ∈ ℕ)
5. ¬(n = 0 ∈ ℤ)
6. b : ℕ
7. m : ℕ
8. ¬(m = 0 ∈ ℤ)
⊢ combinations_aux_rem(b * m rem k;n - 1;m - 1;k) ∈ ℕ

---

Latex:

---

Latex:

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


By

---

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

---

Home Index