Nuprl Lemma : accessible-induction

[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[P:T ⟶ ℙ].
  ((∀t:T. ((∀x:T. (R[x;t]  P[x]))  P[t]))  (∀t:T. (accessible(T;x,y.R[x;y];t)  P[t])))


Proof




Definitions occuring in Statement :  accessible: accessible(T;x,y.R[x; y];t) uall: [x:A]. B[x] prop: so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] subtype_rel: A ⊆B prop: so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] accessible: accessible(T;x,y.R[x; y];t) pi1: fst(t)
Lemmas referenced :  param-W-induction unit_wf2 pi1_wf param-W_wf all_wf accessible_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache sqequalRule lambdaEquality hypothesis hypothesisEquality productEquality applyEquality universeEquality dependent_functionElimination independent_functionElimination functionEquality cumulativity productElimination rename dependent_pairEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}t:T.  ((\mforall{}x:T.  (R[x;t]  {}\mRightarrow{}  P[x]))  {}\mRightarrow{}  P[t]))  {}\mRightarrow{}  (\mforall{}t:T.  (accessible(T;x,y.R[x;y];t)  {}\mRightarrow{}  P[t])))



Date html generated: 2016_05_14-AM-06_18_47
Last ObjectModification: 2015_12_26-PM-00_02_57

Theory : co-recursion


Home Index