### Nuprl Lemma : RankEx4_ind_wf

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

Proof

Definitions occuring in Statement :  RankEx4_ind: RankEx4_ind RankEx4_Foo: `RankEx4_Foo(foo)` RankEx4: `RankEx4()` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` true: `True` member: `t ∈ T` 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 :  top_wf has-value_wf_base lifting-strict-atom_eq base_wf RankEx4_wf true_wf RankEx4_Foo_wf all_wf set_wf subtype_rel-equal
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  RankEx4()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:RankEx4()].  \mforall{}[Foo:foo:(\mBbbZ{}  +  RankEx4())
{}\mrightarrow{}  case  foo
of  inl(u)  =>
True
|  inr(u1)  =>
\{x:A|  R[x;u1]\}
{}\mrightarrow{}  \{x:A|  R[x;RankEx4\_Foo(foo)]\}  ].
(RankEx4\_ind(v;
RankEx4\_Foo(foo){}\mRightarrow{}  rec1.Foo[foo;rec1])    \mmember{}  \{x:A|  R[x;v]\}  )

Date html generated: 2015_07_17-AM-07_51_21
Last ObjectModification: 2015_01_29-PM-04_39_08

Home Index