---

Step * 2 of Lemma combinations_aux_linear


1. n : ℤ
2. 0 < n
3. ∀[b,m:ℤ].  (combinations_aux(b;n - 1;m) = (b * combinations_aux(1;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 
    = (b
      * if (n =z 0)
        then 1
        else eval b2 = 1 * 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 3 ((CallByValueReduce 0 THENA Auto)))⋅ }

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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index