Step
*
1
2
of Lemma
int_add_grp_wf
Ident(ℤ;λx,y. (x + y);0)
BY
{ ((AbEval ``ident`` 0) THEN Auto) }
Latex:
Latex:
Ident(\mBbbZ{};\mlambda{}x,y.  (x  +  y);0)
By
Latex:
((AbEval  ``ident``  0)  THEN  Auto)
Home
Index