### Nuprl Lemma : RankEx4-definition

`∀[A:Type]. ∀[R:A ─→ RankEx4() ─→ ℙ].`
`  ((∀foo:ℤ + RankEx4(). (case foo of inl(u) => True | inr(u1) => {x:A| R[x;u1]}  `` {x:A| R[x;RankEx4_Foo(foo)]} ))`
`  `` {∀v:RankEx4(). {x:A| R[x;v]} })`

Proof

Definitions occuring in Statement :  RankEx4_Foo: `RankEx4_Foo(foo)` RankEx4: `RankEx4()` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` true: `True` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` union: `left + right` int: `ℤ` universe: `Type`
Lemmas :  RankEx4-induction set_wf all_wf RankEx4_wf true_wf RankEx4_Foo_wf
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  RankEx4()  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}foo:\mBbbZ{}  +  RankEx4()
(case  foo  of  inl(u)  =>  True  |  inr(u1)  =>  \{x:A|  R[x;u1]\}    {}\mRightarrow{}  \{x:A|  R[x;RankEx4\_Foo(foo)]\}  ))
{}\mRightarrow{}  \{\mforall{}v:RankEx4().  \{x:A|  R[x;v]\}  \})

Date html generated: 2015_07_17-AM-07_51_16
Last ObjectModification: 2015_01_27-AM-09_36_10

Home Index