---

Step * 2 1 1 of Lemma add-polynom-int-val


1. n : {1...}
2. u : ℤ
3. v : ℤ List
4. [%2] : ||[u / v]|| = n ∈ ℤ
5. ∀[p,q:polyform(n - 1)]. ∀[rmz:𝔹].  (add-polynom(n - 1;rmz;p;q)@v = (p@v + q@v) ∈ ℤ)
⊢ ∀[p,q:polyform(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;p;q)@[u / v] = (p@[u / v] + q@[u / v]) ∈ ℤ)
BY
{ ((Assert v ∈ {l:ℤ List| ||l|| = (n - 1) ∈ ℤ}  BY
          ((Unhide THENA Auto) THEN All Reduce THEN MemTypeCD THEN Auto))
   THEN (Thin (-3)
         THEN (Assert [u / v] ∈ {l:ℤ List| ||l|| = n ∈ ℤ}  BY
                     ((MemTypeHD 5 THENA Auto) THEN MemTypeCD THEN Reduce 0 THEN Auto))
         )
   THEN InductionOnList) }

1
1. n : {1...}
2. u : ℤ
3. v : ℤ List
4. ∀[p,q:polyform(n - 1)]. ∀[rmz:𝔹].  (add-polynom(n - 1;rmz;p;q)@v = (p@v + q@v) ∈ ℤ)
5. v ∈ {l:ℤ List| ||l|| = (n - 1) ∈ ℤ} 
6. [u / v] ∈ {l:ℤ List| ||l|| = n ∈ ℤ} 
⊢ ∀[q:polyform(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;[];q)@[u / v] = ([]@[u / v] + q@[u / v]) ∈ ℤ)

2
1. n : {1...}
2. u : ℤ
3. v : ℤ List
4. ∀[p,q:polyform(n - 1)]. ∀[rmz:𝔹].  (add-polynom(n - 1;rmz;p;q)@v = (p@v + q@v) ∈ ℤ)
5. v ∈ {l:ℤ List| ||l|| = (n - 1) ∈ ℤ} 
6. [u / v] ∈ {l:ℤ List| ||l|| = n ∈ ℤ} 
7. u1 : polyform(n - 1)
8. v1 : polyform(n - 1) List
9. ∀[q:polyform(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;v1;q)@[u / v] = (v1@[u / v] + q@[u / v]) ∈ ℤ)
⊢ ∀[q:polyform(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;[u1 / v1];q)@[u / v] = ([u1 / v1]@[u / v] + q@[u / v]) ∈ ℤ)

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  [\%2]  :  ||[u  /  v]||  =  n
5.  \mforall{}[p,q:polyform(n  -  1)].  \mforall{}[rmz:\mBbbB{}].    (add-polynom(n  -  1;rmz;p;q)@v  =  (p@v  +  q@v))
\mvdash{}  \mforall{}[p,q:polyform(n  -  1)  List].  \mforall{}[rmz:\mBbbB{}].    (add-polynom(n;rmz;p;q)@[u  /  v]  =  (p@[u  /  v]  +  q@[u  /  v]))


By

---

Latex:
((Assert  v  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  (n  -  1)\}    BY
                ((Unhide  THENA  Auto)  THEN  All  Reduce  THEN  MemTypeCD  THEN  Auto))
  THEN  (Thin  (-3)
              THEN  (Assert  [u  /  v]  \mmember{}  \{l:\mBbbZ{}  List|  ||l||  =  n\}    BY
                                      ((MemTypeHD  5  THENA  Auto)  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto))
              )
  THEN  InductionOnList)

---

Home Index