Nuprl Lemma : bs_tree-definition
∀[E,A:Type]. ∀[R:A ⟶ bs_tree(E) ⟶ ℙ].
  ({x:A| R[x;bst_null()]} 
  
⇒ (∀value:E. {x:A| R[x;bst_leaf(value)]} )
  
⇒ (∀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)]} ))
  
⇒ {∀v:bs_tree(E). {x:A| R[x;v]} })
Proof
Definitions occuring in Statement : 
bst_node: bst_node(left;value;right)
, 
bst_leaf: bst_leaf(value)
, 
bst_null: bst_null()
, 
bs_tree: bs_tree(E)
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
guard: {T}
, 
so_apply: x[s1;s2]
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
set: {x:A| B[x]} 
, 
function: x:A ⟶ B[x]
, 
universe: Type
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
implies: P 
⇒ Q
, 
guard: {T}
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s1;s2]
, 
subtype_rel: A ⊆r B
, 
so_apply: x[s]
, 
prop: ℙ
, 
all: ∀x:A. B[x]
Lemmas referenced : 
bst_null_wf, 
bst_leaf_wf, 
bst_node_wf, 
all_wf, 
bs_tree_wf, 
set_wf, 
bs_tree-induction
Rules used in proof : 
cut, 
lemma_by_obid, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
hypothesis, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
lambdaFormation, 
sqequalRule, 
lambdaEquality, 
cumulativity, 
applyEquality, 
functionExtensionality, 
because_Cache, 
independent_functionElimination, 
functionEquality, 
setEquality, 
setElimination, 
rename, 
universeEquality
Latex:
\mforall{}[E,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  bs\_tree(E)  {}\mrightarrow{}  \mBbbP{}].
    (\{x:A|  R[x;bst\_null()]\} 
    {}\mRightarrow{}  (\mforall{}value:E.  \{x:A|  R[x;bst\_leaf(value)]\}  )
    {}\mRightarrow{}  (\mforall{}left:bs\_tree(E).  \mforall{}value:E.  \mforall{}right:bs\_tree(E).
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;bst\_node(left;value;right)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:bs\_tree(E).  \{x:A|  R[x;v]\}  \})
Date html generated:
2016_05_15-PM-01_50_57
Last ObjectModification:
2016_04_07-PM-02_26_29
Theory : tree_1
Home
Index