### Nuprl Lemma : bar_recursion_wf_strong

`∀[T:Type]. ∀[R:n:ℕ ⟶ (ℕn ⟶ T) ⟶ T ⟶ ℙ]. ∀[B:n:ℕ ⟶ {s:ℕn ⟶ T| ∀x:ℕn. (R x s (s x))}  ⟶ ℙ].`
`∀[A:n:ℕ ⟶ R-consistent-seq(n) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:R-consistent-seq(n).  Dec(B[n;s])]. ∀[b:∀n:ℕ. ∀s:R-consistent-seq(n).`
`                                                                                             (B[n;s] `` A[n;s])].`
`∀[i:∀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. (bar_recursion(d;b;i;0;x) ∈ A[0;x])))`

Proof

Definitions occuring in Statement :  bar_recursion: bar_recursion 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` member: `t ∈ T` 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` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` exists: `∃x:A. B[x]` consistent-seq: `R-consistent-seq(n)` decidable: `Dec(P)` bar_recursion: bar_recursion or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` sq_stable: `SqStable(P)` squash: `↓T` subtract: `n - m` true: `True` seq-add: `s.x@n` top: `Top`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  Error :universeIsType,  cut introduction extract_by_obid hypothesis sqequalRule Error :functionIsType,  Error :setIsType,  because_Cache hypothesisEquality applyEquality sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename independent_isectElimination independent_pairFormation lambdaFormation lambdaEquality functionEquality dependent_set_memberEquality productElimination intEquality setEquality dependent_functionElimination universeEquality instantiate strong_bar_Induction unionElimination functionExtensionality independent_functionElimination voidElimination cumulativity equalityTransitivity equalitySymmetry addEquality imageMemberEquality baseClosed imageElimination minusEquality isect_memberEquality voidEquality

Latex:
\mforall{}[T:Type].  \mforall{}[R:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[B:n:\mBbbN{}  {}\mrightarrow{}  \{s:\mBbbN{}n  {}\mrightarrow{}  T|  \mforall{}x:\mBbbN{}n.  (R  x  s  (s  x))\}    {}\mrightarrow{}  \mBbbP{}].
\mforall{}[A:n:\mBbbN{}  {}\mrightarrow{}  R-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    Dec(B[n;s])].
\mforall{}[b:\mforall{}n:\mBbbN{}.  \mforall{}s:R-consistent-seq(n).    (B[n;s]  {}\mRightarrow{}  A[n;s])].  \mforall{}[i:\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])].
((\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.  (bar\_recursion(d;b;i;0;x)  \mmember{}  A[0;x])))

Date html generated: 2019_06_20-AM-11_28_54
Last ObjectModification: 2018_09_26-AM-11_13_41

Theory : bar-induction

Home Index