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