Step
*
1
4
of Lemma
nat_add_mon_wf2
RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x =b y);x,y.↑(x =b y);λx.x)
BY
{ AGenRepD ["basic";"compound"] THEN All Reduce THEN Auto⋅ }
Latex:
Latex:
RelsIso(|<\mBbbN{},+>|;|<\mBbbZ{}+>|;x,y.\muparrow{}(x =\msubb{} y);x,y.\muparrow{}(x =\msubb{} y);\mlambda{}x.x)
By
Latex:
AGenRepD ["basic";"compound"] THEN All Reduce THEN Auto\mcdot{}
Home
Index