---

Step * 1 2 2 of Lemma add-polynom-length


1. n : ℕ
2. n + 1 ≠ 0
3. u : polyform(n)
4. v : polyform(n) List
5. ∀[q:polyform(n) List]. (||add-polynom(n + 1;ff;v;q)|| = imax(||v||;||q||) ∈ ℤ)
6. u1 : polyform(n)
7. v1 : polyform(n) List
8. ||add-polynom(n + 1;ff;[u / v];v1)|| = imax(||[u / v]||;||v1||) ∈ ℤ
9. ¬||v|| + 1 < ||v1|| + 1
10. ¬||v1|| + 1 < ||v|| + 1
⊢ ||let c ⟵ add-polynom((n + 1) - 1;tt;u;u1)
    in let cs ⟵ add-polynom(n + 1;ff;v;v1)
       in [c / cs]||
= imax(||v|| + 1;||v1|| + 1)
∈ ℤ
BY
{ ((Subst' (n + 1) - 1 ~ n 0 THENA Auto)
   THEN (Assert add-polynom(n;tt;u;u1) ∈ polyform(n) BY
               (BLemma `add-polynom_wf1` THEN Auto))
   THEN ((CallByValueReduce 0 THENM Reduce 0) THENA Auto)
   THEN (Assert add-polynom(n + 1;ff;v;v1) ∈ polyform(n + 1) BY
               (BLemma `add-polynom_wf1` THEN Auto THEN RecUnfold `polyform` 0 THEN Auto))
   THEN ((CallByValueReduce 0 THENM Reduce 0) THENA Auto)) }

1
1. n : ℕ
2. n + 1 ≠ 0
3. u : polyform(n)
4. v : polyform(n) List
5. ∀[q:polyform(n) List]. (||add-polynom(n + 1;ff;v;q)|| = imax(||v||;||q||) ∈ ℤ)
6. u1 : polyform(n)
7. v1 : polyform(n) List
8. ||add-polynom(n + 1;ff;[u / v];v1)|| = imax(||[u / v]||;||v1||) ∈ ℤ
9. ¬||v|| + 1 < ||v1|| + 1
10. ¬||v1|| + 1 < ||v|| + 1
11. add-polynom(n;tt;u;u1) ∈ polyform(n)
12. add-polynom(n + 1;ff;v;v1) ∈ polyform(n + 1)
⊢ (||add-polynom(n + 1;ff;v;v1)|| + 1) = imax(||v|| + 1;||v1|| + 1) ∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  n  +  1  \mneq{}  0
3.  u  :  polyform(n)
4.  v  :  polyform(n)  List
5.  \mforall{}[q:polyform(n)  List].  (||add-polynom(n  +  1;ff;v;q)||  =  imax(||v||;||q||))
6.  u1  :  polyform(n)
7.  v1  :  polyform(n)  List
8.  ||add-polynom(n  +  1;ff;[u  /  v];v1)||  =  imax(||[u  /  v]||;||v1||)
9.  \mneg{}||v||  +  1  <  ||v1||  +  1
10.  \mneg{}||v1||  +  1  <  ||v||  +  1
\mvdash{}  ||let  c  \mleftarrow{}{}  add-polynom((n  +  1)  -  1;tt;u;u1)
        in  let  cs  \mleftarrow{}{}  add-polynom(n  +  1;ff;v;v1)
              in  [c  /  cs]||
=  imax(||v||  +  1;||v1||  +  1)


By

---

Latex:
((Subst'  (n  +  1)  -  1  \msim{}  n  0  THENA  Auto)
  THEN  (Assert  add-polynom(n;tt;u;u1)  \mmember{}  polyform(n)  BY
                          (BLemma  `add-polynom\_wf1`  THEN  Auto))
  THEN  ((CallByValueReduce  0  THENM  Reduce  0)  THENA  Auto)
  THEN  (Assert  add-polynom(n  +  1;ff;v;v1)  \mmember{}  polyform(n  +  1)  BY
                          (BLemma  `add-polynom\_wf1`  THEN  Auto  THEN  RecUnfold  `polyform`  0  THEN  Auto))
  THEN  ((CallByValueReduce  0  THENM  Reduce  0)  THENA  Auto))

---

Home Index