---

Step * of Lemma bs_tree_ind_wf

No Annotations
∀[E,A:Type]. ∀[R:A ⟶ bs_tree(E) ⟶ ℙ]. ∀[v:bs_tree(E)]. ∀[null:{x:A| R[x;bst_null()]} ].
∀[leaf:value:E ⟶ {x:A| R[x;bst_leaf(value)]} ]. ∀[node:left:bs_tree(E)
                                                       ⟶ value:E
                                                       ⟶ right:bs_tree(E)
                                                       ⟶ {x:A| R[x;left]} 
                                                       ⟶ {x:A| R[x;right]} 
                                                       ⟶ {x:A| R[x;bst_node(left;value;right)]} ].
  (case(v)
   null=>null
   leaf(value)=>leaf[value]
   node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2] ∈ {x:A| R[x;v]} )
BY
{ (ProveDatatypeIndWfByLemma (ioid Obid: bs_tree-definition)⋅ THEN (ProveDatatypeIndWfByLemma bs_tree-definition)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[E,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  bs\_tree(E)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:bs\_tree(E)].  \mforall{}[null:\{x:A|  R[x;bst\_null()]\}  ].
\mforall{}[leaf:value:E  {}\mrightarrow{}  \{x:A|  R[x;bst\_leaf(value)]\}  ].  \mforall{}[node:left:bs\_tree(E)
                                                                                                              {}\mrightarrow{}  value:E
                                                                                                              {}\mrightarrow{}  right:bs\_tree(E)
                                                                                                              {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                                              {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                                              {}\mrightarrow{}  \{x:A|  R[x;bst\_node(left;value;right)]\}  ].
    (case(v)
      null=>null
      leaf(value)=>leaf[value]
      node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2]  \mmember{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
(ProveDatatypeIndWfByLemma  (ioid  Obid:  bs\_tree-definition)\mcdot{}
  THEN  (ProveDatatypeIndWfByLemma  bs\_tree-definition)
  )

---

Home Index