### Nuprl Lemma : basic_strong_bar_induction

`∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[B,A:n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ].`
`  ((∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s]))`
`  `` (∀n:ℕ. ∀s:R-consistent-seq(n).  (B[n;s] `` A[n;s]))`
`  `` (∀n:ℕ. ∀s:R-consistent-seq(n).  ((∀t:{t:T| R n s t} . A[n + 1;s.t@n]) `` A[n;s]))`
`  `` (∀alpha:{f:ℕ ⟶ T| ∀x:ℕ. (R x f (f x))} . (↓∃m:ℕ. B[m;alpha]))`
`  `` (∀x:Top. A[0;x]))`

Proof

Definitions occuring in Statement :  consistent-seq: `R-consistent-seq(n)` seq-add: `s.x@n` int_seg: `{i..j-}` nat: `ℕ` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` top: `Top` prop: `ℙ` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` squash: `↓T` implies: `P `` Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` nat: `ℕ` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` consistent-seq: `R-consistent-seq(n)` int_seg: `{i..j-}` lelt: `i ≤ j < k` less_than: `a < b` squash: `↓T` so_apply: `x[s]` cand: `A c∧ B` guard: `{T}` exists: `∃x:A. B[x]` prop: `ℙ` top: `Top` istype: `istype(T)` true: `True` subtract: `n - m` sq_stable: `SqStable(P)` uiff: `uiff(P;Q)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` or: `P ∨ Q` decidable: `Dec(P)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction extract_by_obid hypothesis sqequalRule functionIsType setIsType because_Cache universeIsType hypothesisEquality applyEquality sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename independent_isectElimination independent_pairFormation lambdaEquality_alt dependent_set_memberEquality_alt productElimination imageElimination inhabitedIsType intEquality dependent_functionElimination productIsType instantiate universeEquality equalityIsType1 functionExtensionality_alt voidElimination isect_memberEquality_alt independent_functionElimination equalitySymmetry equalityTransitivity cumulativity setEquality functionEquality functionExtensionality minusEquality baseClosed imageMemberEquality unionElimination addEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B,A:n:\mBbbN{}  {}\mrightarrow{}  R-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    Dec(B[n;s]))
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    (B[n;s]  {}\mRightarrow{}  A[n;s]))
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    ((\mforall{}t:\{t:T|  R  n  s  t\}  .  A[n  +  1;s.t@n])  {}\mRightarrow{}  A[n;s]))
{}\mRightarrow{}  (\mforall{}alpha:\{f:\mBbbN{}  {}\mrightarrow{}  T|  \mforall{}x:\mBbbN{}.  (R  x  f  (f  x))\}  .  (\mdownarrow{}\mexists{}m:\mBbbN{}.  B[m;alpha]))
{}\mRightarrow{}  (\mforall{}x:Top.  A[0;x]))

Date html generated: 2020_05_19-PM-09_35_52
Last ObjectModification: 2020_01_04-PM-07_56_43

Theory : bar-induction

Home Index