---

Step * of Lemma poly-val-fun_wf

∀[n:ℕ]. ∀[p:polyform(n)].  (poly-val-fun(p) ∈ {l:ℤ List| n ≤ ||l||}  ⟶ ℤ)
BY
{ ((Assert ⌜∀k:ℕ. ∀[n:ℕ]. ∀[p:polyform(n)].  ((tree_size(p) ≤ k) ⇒ (poly-val-fun(p) ∈ {l:ℤ List| n ≤ ||l||}  ⟶ ℤ))⌝⋅
   THENM (Auto THEN InstHyp [⌜tree_size(p)⌝;⌜n⌝;⌜p⌝] 1⋅ THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto
   THEN (RepeatFor 2 (DVar `p')
         THEN RecUnfold `tree_size` (-1)
         THEN Reduce -1
         THEN Try (((Assert (0 ≤ tree_size(left)) ∧ (0 ≤ tree_size(p2)) BY Auto) THEN Auto))
         THEN RepUR ``poly-val-fun`` 0
         THEN (Fold `poly-val-fun` 0 ORELSE Auto))⋅) }

1
1. k : ℤ
2. 0 < k
3. ∀[n:ℕ]. ∀[p:polyform(n)].  ((tree_size(p) ≤ (k - 1)) ⇒ (poly-val-fun(p) ∈ {l:ℤ List| n ≤ ||l||}  ⟶ ℤ))
4. n : ℕ
5. left : tree(ℤ)
6. p2 : tree(ℤ)
7. ↑(ispolyform(tree_node(left;p2)) n)
8. ((1 + tree_size(left)) + tree_size(p2)) ≤ k
9. 0 ≤ tree_size(left)
10. 0 ≤ tree_size(p2)
⊢ λl.eval t = tl(l) in
     eval av = poly-val-fun(left) tl(l) in
     eval bv = poly-val-fun(p2) l in
       if bv=0  then av  else eval h = hd(l) in av + (h * bv) ∈ {l:ℤ List| n ≤ ||l||}  ⟶ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p:polyform(n)].    (poly-val-fun(p)  \mmember{}  \{l:\mBbbZ{}  List|  n  \mleq{}  ||l||\}    {}\mrightarrow{}  \mBbbZ{})


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}k:\mBbbN{}
                        \mforall{}[n:\mBbbN{}].  \mforall{}[p:polyform(n)].
                            ((tree\_size(p)  \mleq{}  k)  {}\mRightarrow{}  (poly-val-fun(p)  \mmember{}  \{l:\mBbbZ{}  List|  n  \mleq{}  ||l||\}    {}\mrightarrow{}  \mBbbZ{}))\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}tree\_size(p)\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto
  THEN  (RepeatFor  2  (DVar  `p')
              THEN  RecUnfold  `tree\_size`  (-1)
              THEN  Reduce  -1
              THEN  Try  (((Assert  (0  \mleq{}  tree\_size(left))  \mwedge{}  (0  \mleq{}  tree\_size(p2))  BY  Auto)  THEN  Auto))
              THEN  RepUR  ``poly-val-fun``  0
              THEN  (Fold  `poly-val-fun`  0  ORELSE  Auto))\mcdot{})

---

Home Index