---

Step * of Lemma add-polynom-length

∀[n:ℕ]. ∀[p,q:polyform(n) List].  (||add-polynom(n + 1;ff;p;q)|| = imax(||p||;||q||) ∈ ℤ)
BY
{ ((InductionOnList THEN Auto)
   THENL [(RecUnfold `add-polynom` 0
           THEN AutoSplit
           THEN (CallByValueReduce 0 THENA Auto)
           THEN RWO "imax_unfold" 0
           THEN Auto)
         ; ((ListInd (-1)
             THEN RecUnfold `add-polynom` 0
             THEN AutoSplit
             THEN (CallByValueReduce 0 THENA Auto)
             THEN Reduce 0)
            THENL [(RWO "imax_unfold" 0 THEN Auto THEN Assert ⌜0 ≤ ||v||⌝⋅ THEN Auto)
                  ; ((CallByValueReduce 0 THENA Auto)
                     THEN Reduce 0
                     THEN RepeatFor 2 ((CallByValueReduce 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||) ∈ ℤ
⊢ ||if (||v|| + 1) < (||v1|| + 1)
       then let cs ⟵ add-polynom(n + 1;ff;[u / v];v1)
            in [u1 / cs]
       else if (||v1|| + 1) < (||v|| + 1)
               then let cs ⟵ add-polynom(n + 1;ff;v;[u1 / v1])
                    in [u / cs]
               else 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)
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p,q:polyform(n)  List].    (||add-polynom(n  +  1;ff;p;q)||  =  imax(||p||;||q||))


By

---

Latex:
((InductionOnList  THEN  Auto)
  THENL  [(RecUnfold  `add-polynom`  0
                  THEN  AutoSplit
                  THEN  (CallByValueReduce  0  THENA  Auto)
                  THEN  RWO  "imax\_unfold"  0
                  THEN  Auto)
              ;  ((ListInd  (-1)
                      THEN  RecUnfold  `add-polynom`  0
                      THEN  AutoSplit
                      THEN  (CallByValueReduce  0  THENA  Auto)
                      THEN  Reduce  0)
                    THENL  [(RWO  "imax\_unfold"  0  THEN  Auto  THEN  Assert  \mkleeneopen{}0  \mleq{}  ||v||\mkleeneclose{}\mcdot{}  THEN  Auto)
                                ;  ((CallByValueReduce  0  THENA  Auto)
                                      THEN  Reduce  0
                                      THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))]
              )]
)

---

Home Index