---

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


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]) ∈ ℤ)
BY
{ (Auto
   THEN RecUnfold `add-polynom` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN Reduce 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (Assert q ∈ polyform(n) BY
               (RecUnfold `polyform` 0 THEN Auto))
   THEN Auto) }

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 ∈ ℤ} 
7. q : polyform(n - 1) List
8. rmz : 𝔹
9. ¬(n = 0 ∈ ℤ)
10. q ∈ polyform(n)
⊢ q@[u / v] = ([]@[u / v] + q@[u / v]) ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
(Auto
  THEN  RecUnfold  `add-polynom`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  Reduce  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (Assert  q  \mmember{}  polyform(n)  BY
                          (RecUnfold  `polyform`  0  THEN  Auto))
  THEN  Auto)

---

Home Index