---

Step * of Lemma test6

∀[x:ℤ]. (if 0 <z x then x else -x fi  ∈ ℕ)
BY
{ (Try (Complete (Auto'))
   THEN skip{ We want this to prove it without MaAuto.
             It will work when ifthenelse_wf is changed.⋅}
   ) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (if  0  <z  x  then  x  else  -x  fi    \mmember{}  \mBbbN{})


By

---

Latex:
(Try  (Complete  (Auto'))
  THEN  skip\{  We  want  this  to  prove  it  without  MaAuto.
                      It  will  work  when  ifthenelse\_wf  is  changed.\mcdot{}\}
  )

---

Home Index