---

Step * 1 of Lemma polyvar-val


1. v : ℤ
2. l : {l:ℤ List| 0 < ||l||} 
⊢ tree_node(tree_leaf(0);tree_leaf(1))@l = l[0] ∈ ℤ
BY
{ RepUR ``poly-int-val poly-val-fun`` 0 }

1
1. v : ℤ
2. l : {l:ℤ List| 0 < ||l||} 
⊢ eval t = tl(l) in eval h = hd(l) in   0 + (h * 1) = l[0] ∈ ℤ

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}
2.  l  :  \{l:\mBbbZ{}  List|  0  <  ||l||\} 
\mvdash{}  tree\_node(tree\_leaf(0);tree\_leaf(1))@l  =  l[0]


By

---

Latex:
RepUR  ``poly-int-val  poly-val-fun``  0

---

Home Index