Step * 1 2 of Lemma nat_add_mon_wf2

.....wf..... 
λx.x ∈ |<ℕ,+>| ⟶ |<ℤ+>|
BY
(Reduce THEN Auto) }


Latex:


Latex:
.....wf..... 
\mlambda{}x.x  \mmember{}  |<\mBbbN{},+>|  {}\mrightarrow{}  |<\mBbbZ{}+>|


By


Latex:
(Reduce  0  THEN  Auto)




Home Index