---

Step * 1 of Lemma stamps-example

.....basecase..... 
∃i:ℕ. (∃j:ℕ [((0 + 8) = ((3 * i) + (5 * j)) ∈ ℤ)])
BY
{ TACTIC:(InstConcl [⌜1⌝;⌜1⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
\mexists{}i:\mBbbN{}.  (\mexists{}j:\mBbbN{}  [((0  +  8)  =  ((3  *  i)  +  (5  *  j)))])


By

---

Latex:
TACTIC:(InstConcl  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index