---

Step * of Lemma bs_tree_ind_wf_simple

∀[E,A:Type]. ∀[v:bs_tree(E)]. ∀[null:A]. ∀[leaf:value:E ⟶ A]. ∀[node:left:bs_tree(E)
                                                                      ⟶ value:E
                                                                      ⟶ right:bs_tree(E)
                                                                      ⟶ A
                                                                      ⟶ A
                                                                      ⟶ A].
  (case(v)
   null=>null
   leaf(value)=>leaf[value]
   node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2] ∈ A)
BY
{ ProveDatatypeIndWfSimple 1 `bs_tree_ind_wf` }

---

Latex:

---

Latex:
\mforall{}[E,A:Type].  \mforall{}[v:bs\_tree(E)].  \mforall{}[null:A].  \mforall{}[leaf:value:E  {}\mrightarrow{}  A].  \mforall{}[node:left:bs\_tree(E)
                                                                                                                                            {}\mrightarrow{}  value:E
                                                                                                                                            {}\mrightarrow{}  right:bs\_tree(E)
                                                                                                                                            {}\mrightarrow{}  A
                                                                                                                                            {}\mrightarrow{}  A
                                                                                                                                            {}\mrightarrow{}  A].
    (case(v)
      null=>null
      leaf(value)=>leaf[value]
      node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2]  \mmember{}  A)


By

---

Latex:
ProveDatatypeIndWfSimple  1  `bs\_tree\_ind\_wf`

---

Home Index