Step
*
1
2
of Lemma
nat_add_mon_wf2
.....wf..... 
λx.x ∈ |<ℕ,+>| ⟶ |<ℤ+>|
BY
{ (Reduce 0 THEN Auto) }
Latex:
Latex:
.....wf..... 
\mlambda{}x.x  \mmember{}  |<\mBbbN{},+>|  {}\mrightarrow{}  |<\mBbbZ{}+>|
By
Latex:
(Reduce  0  THEN  Auto)
Home
Index