### Nuprl Lemma : MMTree-definition

`∀[T,A:Type]. ∀[R:A ─→ MMTree(T) ─→ ℙ].`
`  ((∀val:T. {x:A| R[x;MMTree_Leaf(val)]} )`
`  `` (∀forest:MMTree(T) List List. ((∀u∈forest.(∀u1∈u.{x:A| R[x;u1]} )) `` {x:A| R[x;MMTree_Node(forest)]} ))`
`  `` {∀v:MMTree(T). {x:A| R[x;v]} })`

Proof

Definitions occuring in Statement :  MMTree_Node: `MMTree_Node(forest)` MMTree_Leaf: `MMTree_Leaf(val)` MMTree: `MMTree(T)` l_all: `(∀x∈L.P[x])` list: `T List` 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`
Lemmas :  MMTree-induction set_wf all_wf list_wf MMTree_wf l_all_wf2 l_member_wf MMTree_Node_wf MMTree_Leaf_wf
\mforall{}[T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  MMTree(T)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}val:T.  \{x:A|  R[x;MMTree\_Leaf(val)]\}  )
{}\mRightarrow{}  (\mforall{}forest:MMTree(T)  List  List
((\mforall{}u\mmember{}forest.(\mforall{}u1\mmember{}u.\{x:A|  R[x;u1]\}  ))  {}\mRightarrow{}  \{x:A|  R[x;MMTree\_Node(forest)]\}  ))
{}\mRightarrow{}  \{\mforall{}v:MMTree(T).  \{x:A|  R[x;v]\}  \})

Date html generated: 2015_07_17-AM-07_47_19
Last ObjectModification: 2015_01_27-AM-09_39_22

Home Index