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]} })


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:  Q true: True set: {x:A| B[x]}  function: x:A ─→ B[x] decide: case 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