---

Step * 1 of Lemma no_repeats-polynomial-mon-vars


1. u : iMonomial()@i
2. v : iMonomial() List@i
3. ∀L:ℤ List List
     (no_repeats(ℤ List;L)
     ⇒ no_repeats(ℤ List;accumulate (with value vss and list item m):
                           let c,vs = m 
                           in insert(vs;vss)
                          over list:
                            v
                          with starting value:
                           L)))@i
4. L : ℤ List List@i
5. no_repeats(ℤ List;L)@i
⊢ no_repeats(ℤ List;let c,vs = u 
                    in insert(vs;L))
BY
{ ((D 1 THEN Reduce 0) THEN EAuto 1) }

---

Latex:

---

Latex:

1.  u  :  iMonomial()@i
2.  v  :  iMonomial()  List@i
3.  \mforall{}L:\mBbbZ{}  List  List
          (no\_repeats(\mBbbZ{}  List;L)
          {}\mRightarrow{}  no\_repeats(\mBbbZ{}  List;accumulate  (with  value  vss  and  list  item  m):
                                                      let  c,vs  =  m 
                                                      in  insert(vs;vss)
                                                    over  list:
                                                        v
                                                    with  starting  value:
                                                      L)))@i
4.  L  :  \mBbbZ{}  List  List@i
5.  no\_repeats(\mBbbZ{}  List;L)@i
\mvdash{}  no\_repeats(\mBbbZ{}  List;let  c,vs  =  u 
                                        in  insert(vs;L))


By

---

Latex:
((D  1  THEN  Reduce  0)  THEN  EAuto  1)

---

Home Index