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
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  RankEx4_ind: RankEx4_ind,  so_apply: x[s1;s2],  RankEx4-definition,  RankEx4-induction,  uniform-comp-nat-induction,  RankEx4-ext,  eq_atom: x =a y,  bool_cases_sqequal,  eqff_to_assert,  any: any x,  btrue: tt,  bfalse: ff,  it: ⋅,  top: Top,  all: ∀x:A. B[x],  implies: P ⇒ Q,  has-value: (a)↓,  so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),  so_apply: x[s1;s2;s3;s4],  so_lambda: λ2x.t[x],  so_apply: x[s],  uimplies: b supposing a,  strict4: strict4(F),  and: P ∧ Q,  prop: ℙ,  guard: {T},  or: P ∨ Q,  squash: ↓T,  subtype_rel: A ⊆r B
Lemmas referenced :  RankEx4-definition,  RankEx4-induction,  uniform-comp-nat-induction,  RankEx4-ext,  bool_cases_sqequal,  eqff_to_assert,  subtype_rel-equal,  set_wf,  all_wf,  guard_wf,  RankEx4_Foo_wf,  true_wf,  RankEx4_wf,  base_wf,  lifting-strict-atom_eq,  is-exception_wf,  has-value_wf_base,  top_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  sqequalRule,  isect_memberEquality,  voidElimination,  voidEquality,  thin,  lemma_by_obid,  hypothesis,  lambdaFormation,  because_Cache,  sqequalSqle,  divergentSqle,  callbyvalueDecide,  sqequalHypSubstitution,  unionEquality,  unionElimination,  sqleReflexivity,  equalityEquality,  equalityTransitivity,  equalitySymmetry,  hypothesisEquality,  dependent_functionElimination,  independent_functionElimination,  decideExceptionCases,  axiomSqleEquality,  exceptionSqequal,  baseApply,  closedConclusion,  baseClosed,  isectElimination,  independent_isectElimination,  independent_pairFormation,  inrFormation,  imageMemberEquality,  imageElimination,  inlFormation,  instantiate,  extract_by_obid,  applyEquality,  lambdaEquality,  isectEquality,  functionEquality,  cumulativity,  universeEquality,  intEquality,  decideEquality,  setEquality,  axiomEquality
Latex:
\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: 2016_05_16-AM-09_04_51
Last ObjectModification: 2016_01_17-AM-09_41_49

Theory : C-semantics


Home Index