---

Step * 1 of Lemma isPolyOne_wf


1. p : iPolynomial()
⊢ if p is a pair then let m,more = p 
                      in null(more) ∧b isMonomialOne(m) otherwise ff ∈ 𝔹
BY
{ ((RepeatFor 2 (D 1) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  iPolynomial()
\mvdash{}  if  p  is  a  pair  then  let  m,more  =  p 
                                            in  null(more)  \mwedge{}\msubb{}  isMonomialOne(m)  otherwise  ff  \mmember{}  \mBbbB{}


By

---

Latex:
((RepeatFor  2  (D  1)  THEN  Reduce  0)  THEN  Auto)

---

Home Index