### Nuprl Lemma : basic-bar-induction

`∀[T:Type]. ∀[R,A:(T List) ⟶ ℙ].`
`  ((∀s:T List. Dec(R[s]))`
`  `` (∀s:T List. (R[s] `` A[s]))`
`  `` (∀s:T List. ((∀t:T. A[s @ [t]]) `` A[s]))`
`  `` (∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[map(alpha;upto(n))]))`
`  `` A[[]])`

Proof

Definitions occuring in Statement :  upto: `upto(n)` map: `map(f;as)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` nat: `ℕ` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` nat: `ℕ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` all: `∀x:A. B[x]` guard: `{T}` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]`
Lemmas referenced :  bar-induction all_wf nat_wf squash_wf exists_wf map_wf int_seg_wf subtype_rel_dep_function int_seg_subtype_nat false_wf upto_wf list_wf append_wf cons_wf nil_wf decidable_wf list_ind_nil_lemma
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation independent_functionElimination functionEquality cumulativity sqequalRule lambdaEquality because_Cache applyEquality natural_numberEquality setElimination rename independent_isectElimination independent_pairFormation universeEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R,A:(T  List)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}s:T  List.  Dec(R[s]))
{}\mRightarrow{}  (\mforall{}s:T  List.  (R[s]  {}\mRightarrow{}  A[s]))
{}\mRightarrow{}  (\mforall{}s:T  List.  ((\mforall{}t:T.  A[s  @  [t]])  {}\mRightarrow{}  A[s]))
{}\mRightarrow{}  (\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  R[map(alpha;upto(n))]))
{}\mRightarrow{}  A[[]])

Date html generated: 2016_05_14-PM-03_19_30
Last ObjectModification: 2015_12_26-PM-01_41_16

Theory : list_1

Home Index