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