Nuprl Lemma : RankEx2-defop-extract

`∀[T,S,P:Type]. ∀[R:P ─→ RankEx2(S;T) ─→ ℙ].`
`  ((∀t:T. (∃x:{P| (R x RankEx2_LeafT(t))}))`
`  `` (∀s:S. (∃x:{P| (R x RankEx2_LeafS(s))}))`
`  `` (∀d:RankEx2(S;T). ∀s:S. ∀t:T.  ((∃x:{P| (R x d)}) `` (∃x:{P| (R x RankEx2_Prod(<<d, s>, t>))})))`
`  `` (∀z:S × RankEx2(S;T) + RankEx2(S;T)`
`        (case z of inl(p) => ∃x:{P| (R x (snd(p)))} | inr(d) => ∃x:{P| (R x d)} `` (∃x:{P| (R x RankEx2_Union(z))})))`
`  `` (∀L:(S × RankEx2(S;T)) List. ((∀p∈L.∃x:{P| (R x (snd(p)))}) `` (∃x:{P| (R x RankEx2_ListProd(L))})))`
`  `` (∀z:T + (RankEx2(S;T) List)`
`        (case z of inl(p) => True | inr(L) => (∀p∈L.∃x:{P| (R x p)}) `` (∃x:{P| (R x RankEx2_UnionList(z))})))`
`  `` {∀t:RankEx2(S;T). (∃x:{P| (R x t)})})`

Proof

Definitions occuring in Statement :  RankEx2_UnionList: `RankEx2_UnionList(unionlist)` RankEx2_ListProd: `RankEx2_ListProd(listprod)` RankEx2_Union: `RankEx2_Union(union)` RankEx2_Prod: `RankEx2_Prod(prod)` RankEx2_LeafS: `RankEx2_LeafS(leafs)` RankEx2_LeafT: `RankEx2_LeafT(leaft)` RankEx2: `RankEx2(S;T)` l_all: `(∀x∈L.P[x])` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` pi2: `snd(t)` all: `∀x:A. B[x]` sq_exists: `∃x:{A| B[x]}` implies: `P `` Q` true: `True` apply: `f a` function: `x:A ─→ B[x]` pair: `<a, b>` product: `x:A × B[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` union: `left + right` universe: `Type`
Lemmas :  top_wf has-value_wf_base lifting-strict-atom_eq base_wf base_sq lifting-strict-spread pair-eta
\mforall{}[T,S,P:Type].  \mforall{}[R:P  {}\mrightarrow{}  RankEx2(S;T)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}t:T.  (\mexists{}x:\{P|  (R  x  RankEx2\_LeafT(t))\}))
{}\mRightarrow{}  (\mforall{}s:S.  (\mexists{}x:\{P|  (R  x  RankEx2\_LeafS(s))\}))
{}\mRightarrow{}  (\mforall{}d:RankEx2(S;T).  \mforall{}s:S.  \mforall{}t:T.    ((\mexists{}x:\{P|  (R  x  d)\})  {}\mRightarrow{}  (\mexists{}x:\{P|  (R  x  RankEx2\_Prod(<<d,  s>,  t>))\}))\000C)
{}\mRightarrow{}  (\mforall{}z:S  \mtimes{}  RankEx2(S;T)  +  RankEx2(S;T)
(case  z  of  inl(p)  =>  \mexists{}x:\{P|  (R  x  (snd(p)))\}  |  inr(d)  =>  \mexists{}x:\{P|  (R  x  d)\}
{}\mRightarrow{}  (\mexists{}x:\{P|  (R  x  RankEx2\_Union(z))\})))
{}\mRightarrow{}  (\mforall{}L:(S  \mtimes{}  RankEx2(S;T))  List
((\mforall{}p\mmember{}L.\mexists{}x:\{P|  (R  x  (snd(p)))\})  {}\mRightarrow{}  (\mexists{}x:\{P|  (R  x  RankEx2\_ListProd(L))\})))
{}\mRightarrow{}  (\mforall{}z:T  +  (RankEx2(S;T)  List)
(case  z  of  inl(p)  =>  True  |  inr(L)  =>  (\mforall{}p\mmember{}L.\mexists{}x:\{P|  (R  x  p)\})
{}\mRightarrow{}  (\mexists{}x:\{P|  (R  x  RankEx2\_UnionList(z))\})))
{}\mRightarrow{}  \{\mforall{}t:RankEx2(S;T).  (\mexists{}x:\{P|  (R  x  t)\})\})

Date html generated: 2015_07_17-AM-07_50_35
Last ObjectModification: 2015_04_23-PM-11_32_00

Home Index