---

Step * 2 1 1 2 of Lemma add-polynom_wf


1. n : {1...}
2. ∀[p,q:polynom(n - 1)].  (add-polynom(n - 1;tt;p;q) ∈ polynom(n - 1))
3. u : polynom(n - 1)
4. v : polynom(n - 1) List
5. ∀[q:polynom(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;v;q) ∈ polynom(n - 1) List)
6. q : polynom(n - 1) List
7. rmz : 𝔹
⊢ add-polynom(n;rmz;[u / v];q) ∈ polynom(n - 1) List
BY
{ (MoveToConcl (-1)
   THEN ListInd (-1)
   THEN Auto
   THEN RecUnfold `add-polynom` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN ((Assert ⌜False⌝⋅ THEN Complete (Auto)) ORELSE Reduce 0)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Reduce 0
   THEN ((CallByValueReduce 0 THENA Auto) ORELSE Auto)
   THEN Reduce 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. n : {1...}
2. ∀[p,q:polynom(n - 1)].  (add-polynom(n - 1;tt;p;q) ∈ polynom(n - 1))
3. u : polynom(n - 1)
4. v : polynom(n - 1) List
5. ∀[q:polynom(n - 1) List]. ∀[rmz:𝔹].  (add-polynom(n;rmz;v;q) ∈ polynom(n - 1) List)
6. u1 : polynom(n - 1)
7. v1 : polynom(n - 1) List
8. ∀rmz:𝔹. (add-polynom(n;rmz;[u / v];v1) ∈ polynom(n - 1) List)
9. rmz : 𝔹@i
10. ¬(n = 0 ∈ ℤ)
⊢ if (||v|| + 1) < (||v1|| + 1)
     then let cs ⟵ add-polynom(n;ff;[u / v];v1)
          in [u1 / cs]
     else if (||v1|| + 1) < (||v|| + 1)
             then let cs ⟵ add-polynom(n;ff;v;[u1 / v1])
                  in [u / cs]
             else let c ⟵ add-polynom(n - 1;tt;u;u1)
                  in let cs ⟵ add-polynom(n;ff;v;v1)
                     in if rmz then rm-zeros(n - 1;[c / cs]) else [c / cs] fi  ∈ polynom(n - 1) List

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  \mforall{}[p,q:polynom(n  -  1)].    (add-polynom(n  -  1;tt;p;q)  \mmember{}  polynom(n  -  1))
3.  u  :  polynom(n  -  1)
4.  v  :  polynom(n  -  1)  List
5.  \mforall{}[q:polynom(n  -  1)  List].  \mforall{}[rmz:\mBbbB{}].    (add-polynom(n;rmz;v;q)  \mmember{}  polynom(n  -  1)  List)
6.  q  :  polynom(n  -  1)  List
7.  rmz  :  \mBbbB{}
\mvdash{}  add-polynom(n;rmz;[u  /  v];q)  \mmember{}  polynom(n  -  1)  List


By

---

Latex:
(MoveToConcl  (-1)
  THEN  ListInd  (-1)
  THEN  Auto
  THEN  RecUnfold  `add-polynom`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto))  ORELSE  Reduce  0)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Reduce  0
  THEN  ((CallByValueReduce  0  THENA  Auto)  ORELSE  Auto)
  THEN  Reduce  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index