---

Step * 2 1 2 of Lemma equipollent-nat-prod-nsub

.....subterm..... T:t
2:n
1. k : ℕ+
2. b1 : ℕ
3. b2 : ℕk
⊢ ((k * b1) + b2 rem k) = b2 ∈ ℕk
BY
{ ((InstLemma `rem_invariant` [⌜b2⌝;⌜b1⌝;⌜k⌝]⋅ THEN Auto) THEN InstLemma `rem_base_case` [⌜b2⌝;⌜k⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  k  :  \mBbbN{}\msupplus{}
2.  b1  :  \mBbbN{}
3.  b2  :  \mBbbN{}k
\mvdash{}  ((k  *  b1)  +  b2  rem  k)  =  b2


By

---

Latex:
((InstLemma  `rem\_invariant`  [\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `rem\_base\_case`  [\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index